Core.uip

-- UIP for the identity QIIT, via its eliminator. In intensional MLTT
-- J cannot prove UIP (Hofmann–Streicher); here it can, because the
-- would-be-ill-typed motive "w ≡ refl a u ∈ (Id a u v)" becomes
-- well-typed under a reflected index equation — the motive carries
-- that equation INSIDE a squashed Π, so its binder is in scope (and
-- reflected) exactly while the codomain is typed.
-- canonicity: under the index equation (always derivable from the
-- proof itself, by idToEq), every proof of Id a x y IS refl.

import Core.id (Id, refl, IdElimP, idToEq)
import Core.equality (sym, trans)

idCanon : {a : 𝕌} {x y : a} (p : Id _ x y) (h : x ≡ y) → p ≡ refl a x
  using (hyp.rw, Core.id.Id.eq, Core.id.Id.unfold, Core.id.refl.eq)
idCanon =
  λa x y p h. squash-elim
    IdElimP a (λu v w. ∥(k : u ≡ v) → w ≡ refl a u ∈ Id _ u v∥) (λu. ⋆ (λk. ⋆)) x y p
    f. f h

-- uniqueness of identity proofs: both are refl, by canonicity.
uip : {a : 𝕌} {x y : a} {p q : Id _ x y} → p ≡ q
  using (hyp.rw, Core.id.Id.eq, Core.id.Id.unfold, Core.id.idToEq.eq)
uip =
  λa x y p q. let h = idToEq _ _ _ p
                  trans _ (refl a x) _ (idCanon p h) (sym _ (refl a x) (idCanon q h))