equality

-- The equality combinators. In an extensional theory each is one
-- ⋆ (or the coerced term itself): reflecting the hypotheses makes
-- the sides — and, for coercion and transport, the types — equal, so
-- what other theories build from J is judgemental here.

def refl : (A : 𝕌) (a : El A) → a ≡ a ∈ El A ≔
  λA. λa. ⋆

def sym : (A : 𝕌) (a : El A) (b : El A) → (a ≡ b ∈ El A) →
          b ≡ a ∈ El A ≔
  λA. λa. λb. λh. ⋆

def trans : (A : 𝕌) (a : El A) (b : El A) (c : El A) →
            (a ≡ b ∈ El A) → (b ≡ c ∈ El A) →
            a ≡ c ∈ El A ≔
  λA. λa. λb. λc. λab. λbc. ⋆

-- coercion along a universe equation: the element itself, at the
-- other type (El A ≐ El B by reflection)
def coe : (A : 𝕌) (B : 𝕌) → (A ≡ B ∈ 𝕌) → El A → El B ≔
  λA. λB. λh. λa. a

-- transport along an equation in the base: again the element itself
-- (P a ≐ P b by congruence over the reflected hypothesis)
def transport : (A : 𝕌) (P : El A → 𝕌) (a : El A) (b : El A) →
                (a ≡ b ∈ El A) → El (P a) → El (P b) ≔
  λA. λP. λa. λb. λh. λp. p

-- transport at a PROP motive: equality is Ω-valued, so prop-indexed
-- facts move along an equation the same way elements do — the proof
-- itself, at the other instance (Prf (P a) ≐ Prf (P b) by congruence
-- over the reflected hypothesis)
def transportP : (A : 𝕌) (P : El A → Ω) (a : El A) (b : El A) →
                 (a ≡ b ∈ El A) → Prf (P a) → Prf (P b) ≔
  λA. λP. λa. λb. λh. λp. p

-- transport of an equality proof: an a-indexed equation, moved to b.
-- Not a bare ⋆ — the discharge engine rewrites hypotheses one way
-- only, and this needs composition (f b ← f a ≐ g a → g b). That
-- composition is exactly transport at an equality-prop motive.
def transportEq : (A : 𝕌) (B : 𝕌) (f : El A → El B) (g : El A → El B) →
                  (a : El A) (b : El A) → (a ≡ b ∈ _) →
                  (f a ≡ g a ∈ _) →
                  f b ≡ g b ∈ _ ≔
  λA. λB. λf. λg. λa. λb. λh. λe.
    transportP _ (λx. (f x ≡ g x ∈ _)) _ _ h e

-- dependent congruence: in an extensional theory it is one ⋆, since
-- reflecting the hypothesis makes the sides and their types equal
def cong : (A : 𝕌) (B : El A → 𝕌) (f : (v : El A) → El (B v)) →
           (v : El A) (w : El A) → (v ≡ w ∈ _) →
           f v ≡ f w ∈ _ ≔
  λA. λB. λf. λv. λw. λh. ⋆

def irr : (A : 𝕌) (v : El A) (u : El A) (p : v ≡ u ∈ _) → p ≡ ⋆ ∈ (v ≡ u ∈ _)
  ≔ λA. λv. λu. λp. ⋆