{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Erased.Box-cong-axiomatisation
{e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where
open Derived-definitions-and-properties eq
open import Erased.Basics
open import Prelude
open import Equivalence eq using (Is-equivalence)
record []-cong-axiomatisation a : Type (lsuc a) where
field
[]-cong :
{@0 A : Type a} {@0 x y : A} →
Erased (x ≡ y) → [ x ] ≡ [ y ]
[]-cong-[refl] :
{@0 A : Type a} {@0 x : A} →
[]-cong [ refl x ] ≡ refl [ x ]