see other sites:
- https://www.reddit.com/r/Idris/comments/8r2trg/any_hope_for_hott_in_idris/
- https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/
- Idris and HoTT
Uniqueness of Identity Proofs
There is a principle that is built into Idris and applies to Martin-Löf type theory but not HoTT. This principle can be looked at from 3 equivalent ways:
- The uniqueness of identity proofs principle (UIP).
- The K axiom.
- The sort of dependant pattern matching that Idris uses.
To support HoTT, in a language like Idris, we need to remove all reliance on this principle in any form.
First, the uniqueness of identity proofs principle (UIP):
uip: (A : Type) -> (x,y : A) -> (p : x = y) -> (q : x = y) -> p = q uip A x x Refl Refl = Refl |
That is elements 'x' and 'y' can only be equal to each other in one way, if we have:
- (p : x = y)
- (q : x = y)
then p = q
However HoTT requires that this is not true and there are potentially many ways that x and y can be 'equal'.
K Axiom
The K axiom applies to Martin-Löf type theory but not HoTT. The K axiom is equivalent to the uniqueness of identity proofs principle (UIP).
K : (P:a≡a->Set)-> (p:Prefl)(e:a≡a)->P e K P p Refl=p |
K : (A : Set) (M : A) (C : Id M M -> Set)
-> C Refl
-> (loop : Id M M) -> C loop |
