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 |