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:

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:

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

 

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

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.

flag flag flag flag flag flag 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.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.