- Leibniz equality
- Leibniz characterized the notion of equality as follows:
- Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y).
- https://jesper.sikanda.be/files/leibniz-equality.pdf
- Heterogeneous equality
- 'John Major equality'
- http://adam.chlipala.net/cpdt/html/Equality.html#lab66
- Identity of indiscernibles
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 |
