# Idris and Homotopy Type-Theory HoTT

see other sites:

### 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```