In dependently typed type theory there's a equality type. Usually when this type is defined, a number of utilities, namely cong and subst are introduced. How expressive they are? Is it possible to express everything we can with eliminator for equality with them?
1
votes
1 Answers
1
votes
No, you can't prove uniqueness of identity proofs only with cong, subst and eliminator.
uip : {α : Level} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q
Here is the explanation: http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/
