identity

Eq

data Eq {l : Level} (A : Type l) (a : A) : A -> Type l

Eq A a b (written a = b): a proof that a and b are equal. Its only constructor is refl : Eq A a a. Universe polymorphic.

Eq.elim

def elim {l : Level} {m : Level} {A : Type l} {a : A} {b : A} (h : Eq A a b) (P : (c : A) -> Eq A a c -> Type m) (d : P a Eq.refl) : P b h

Elimination (J): a property that holds for refl holds for every proof. The motive may live in any universe.

Eq.sym

def sym {l : Level} {A : Type l} {a : A} {b : A} (h : Eq A a b) : Eq A b a

Symmetry: from a = b, b = a.

Eq.trans

def trans {l : Level} {A : Type l} {a : A} {b : A} {c : A} (h : Eq A a b) (k : Eq A b c) : Eq A a c

Transitivity: from a = b and b = c, a = c.

Eq.cong

def cong {l : Level} {m : Level} {A : Type l} {B : Type m} {a : A} {b : A} (h : Eq A a b) (f : A -> B) : Eq B (f a) (f b)

Congruence: a function maps equal arguments to equal results.

Eq.cong2

def cong2 {l : Level} {m : Level} {n : Level} {A : Type l} {B : Type m} {C : Type n} {a1 : A} {a2 : A} {b1 : B} {b2 : B} (h1 : Eq A a1 a2) (h2 : Eq B b1 b2) (f : A -> B -> C) : Eq C (f a1 b1) (f a2 b2)

Congruence in two arguments: equal arguments give equal results, h1.cong2 h2 f : f a1 b1 = f a2 b2. First the left argument changes with the right one fixed at b1, then the right one with the left fixed at a2.

Eq.subst

def subst {l : Level} {m : Level} {A : Type l} {a : A} {b : A} (h : Eq A a b) (P : A -> Type m) (x : P a) : P b

Substitution: equal things satisfy the same property.

Eq.transport

def r#transport {l : Level} {A : Type l} {B : Type l} (h : Eq (Type l) A B) (x : A) : B

Transport along an equality of types.