3.8 Equality

8.16.0.1

3.8 Equality🔗ℹ

package: cur-lib

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))

1	Curnel Forms
2	Reflection
3	Standard Library
4	Olly: Ott-like Librar Y
5	ntac: The New Tactic System

3.1	Datum
3.2	Sugar
3.3	Bool
3.4	Nat
3.5	Dependent Pairs
3.6	Maybe
3.7	List
3.8	Equality
3.9	ASCII
3.10	Racket ASCII
3.11	Typeclass