id

-- The identity FAMILY: structural equality as a small QIIT
-- (docs/NovaFoundation.txt, Ω block — the prf-code construction).
-- Equality the PROPOSITION lives at Ω and carries no data; Id is its
-- structural counterpart IN 𝕌: a code, storable inside small types,
-- usable as an eliminator motive, indexwise-injective through the
-- qidx selector. The two are logically equivalent (the bridge lemmas
-- below), and that iff is all a proposition can soundly give.
import prop (↔, iffIntro)

data [a : 𝕌] ( Id   : El a → El a → U
             ; refl : (x : El a) → El (Id x x) )

-- reflection, by prop-motive induction (J into a proposition): the
-- refl method's equation is evident, and ElimP asks no coherences
def idToEq : (a : 𝕌) (x : El a) (y : El a) → El (Id _ x y) → x ≡ y ∈ _ ≔
  λa. λx. λy. λp. IdElimP _ (λu. λv. λw. (u ≡ v ∈ _)) (λu. ⋆) _ _ p

-- introduction: with x ≐ y reflected from the hypothesis, refl a x
-- already inhabits Id a x y (index congruence)
def eqToId : (a : 𝕌) (x : El a) (y : El a) → (x ≡ y ∈ El a) → El (Id _ x y) ≔
  λa. λx. λy. λh. refl _ x

-- the bridge, packaged: Id and ≡ are the same proposition up to iff
def idIffEq : (a : 𝕌) (x : El a) (y : El a) →
              Prf (∥ El (Id _ x y) ∥ ↔ (x ≡ y ∈ _)) ≔
  λa. λx. λy. iffIntro ∥ El (Id _ x y) ∥ (x ≡ y ∈ _)
    (λh. squash-elim h (p. idToEq _ _ _ p))
    (λh. ⋆ (eqToId _ _ _ h))

-- round trips compute: β at refl on one side, index congruence on the
-- other
def idToEqBeta : (a : 𝕌) (x : El a) →
                 idToEq _ _ _ (refl _ x) ≡ ⋆ ∈ Prf (x ≡ x ∈ _) ≔
  λa. λx. ⋆
def eqToIdBeta : (a : 𝕌) (x : El a) →
                 eqToId _ x x ⋆ ≡ refl _ x ∈ El (Id _ x x) ≔
  λa. λx. ⋆

-- equality as DATA in a small type — what the Ω-valued ≡ cannot do
-- (no 𝕌-code) and Id restores: a subset code by an equation
def OnlyZ : 𝕌 ≔ (n : ℕ) ⨯ Id _ n Z
def onlyZ : El OnlyZ ≔ Z , refl _ Z
def onlyZIsZ : (v : El OnlyZ) → v .π₁ ≡ Z ∈ _ ≔
  λv. idToEq _ _ _ (v .π₂)