------------------------------------------------------------------------
-- An axiomatisation for []-cong
------------------------------------------------------------------------

-- The definitions below are reexported from Erased.Level-1.

{-# 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)

-- An axiomatisation for []-cong.

record []-cong-axiomatisation a : Type (lsuc a) where
  field
    []-cong :
      {@ A : Type a} {@ x y : A} →
      Erased (x ≡ y) → [ x ] ≡ [ y ]
    []-cong-[refl] :
      {@ A : Type a} {@ x : A} →
      []-cong [ refl x ] ≡ refl [ x ]