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

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 Type-Driven Development with Idris

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.