# Proofs Type Equality

### Leibniz equality

 In this example we have two types AType and BType. Since they have the same structure, as each other, then they are essentially the same. ```data AType = A data BType = B eq3 : AType = BType eq3 = Refl``` They are not detected as being the same by '=' ```36 | eq3 = Refl | ~~~~ When checking right hand side of eq3 with expected type AType = BType Type mismatch between x = x (Type of Refl) and AType = BType (Expected type) Specifically: Type mismatch between AType and BType``` And if we change it to compare elements ```eq3 : A = B eq3 = Refl``` They will not be equal. ``` | 32 | eq3 : A = B | ^ When checking type of Main.eq3: When checking argument y to type constructor =: Type mismatch between BType (Type of B) and AType (Expected type)```

### Heterogeneous Equality

Also included in the prelude:

 ```||| Explicit heterogeneous ("John Major") equality. Use this when Idris ||| incorrectly chooses homogeneous equality for `(=)`. ||| @ a the type of the left side ||| @ b the type of the right side ||| @ x the left side ||| @ y the right side (~=~) : (x : a) -> (y : b) -> Type (~=~) x y = (x = y)```

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