On this page:
==
refl
sym
trans
PM-=
PM-refl
PM-sym
PM-trans
ML-=
ML-refl
8.12

3.8 Equality🔗ℹ

This library defines the Paulin-Mohring and Martin-Löf equality types.

2 parameter type

== : (-> (A : Type) (x : A) (y : A) Type)

constructor

refl : (-> (A : Type) (x : A) (== A x x))

procedure

(sym A n m n=m)  (== A m n)

  A : Type
  n : A
  m : A
  n=m : (PM-= A n m)

procedure

(trans A a b c H1 H2)  (== A a c)

  A : Type
  a : A
  b : A
  c : A
  H1 : (PM-= A a b)
  H2 : (PM-= A b c)
Equivalent to PM-=, PM-refl, PM-sym, and PM-trans, respectively.

2 parameter type

PM-= : (-> (A : Type) (x : A) (y : A) Type)

constructor

PM-refl : (-> (A : Type) (x : A) (PM-= A x x))

The Paulin-Mohring equality type (PM equality).

Also provided as == and refl, as this should be considered the default equality.

Examples:
> (:: (PM-refl Nat z) (PM-= Nat z z))

::: unbound identifier in module

> (new-elim (PM-refl Nat z)
            (lambda (x : Nat) (t : (PM-= Nat z x))
              (PM-= Nat z z))
            (PM-refl Nat z))

(refl (Nat) (z))

procedure

(PM-sym A n m n=m)  (PM-= A m n)

  A : Type
  n : A
  m : A
  n=m : (PM-= A n m)
A proof of symmetry for PM equality.

Also provided as sym.

procedure

(PM-trans A a b c H1 H2)  (PM-= A a c)

  A : Type
  a : A
  b : A
  c : A
  H1 : (PM-= A a b)
  H2 : (PM-= A b c)
A proof of transitivity for PM equality.

Also provided as trans.

1 parameter type

ML-= : (-> (A : Type) (x : A) (y : A) Type)

constructor

ML-refl : (-> (A : Type) (x : A) (PM-= A x x))

The Martin-Löf equality type (ML equality).

Examples:
> (:: (ML-refl Nat z) (ML-= Nat z z))

::: unbound identifier in module

> (new-elim (ML-refl Nat z)
            (lambda (x : Nat) (y : Nat) (t : (ML-= Nat x y))
              (ML-= Nat x y))
            (lambda (x : Nat) (ML-refl Nat x)))

(ML-refl (Nat) (z))