IDENTITY SPACES

-type is an inductive family that contains evidence of equality of two elements from that family.

Formation

(-Formation, Family). The inductive family with domains and codomain in universe represents inhabitants carrying proofs that given indexed elements are equal.

def IdV (A: V) (x y: A)
  : V := Id A x y

Introduction

(-Intro, Reflection). The inductive family elements are instantiated by single constructor that carries proof that element are equals to itself.

def Id-ref (A : V) (a: A)
  : Id A a a := ref a

Elimination

(-Elimination, J). Given a family and a function there is a function such that .

def =-ind (A : V)
    (C : Π (x y : A), Id A x y -> V)
    (x y : A) (c : C x x (ref x))
    (p : Id A x y)
  : C x y p
:= indJ A C x c y p

Computation

(-Computation).

def Jˢ-β (A : V)
    (C : Π (a b : A), Id A a b -> V)
    (a : A) (c : C a a (ref a))
  : Id (C a a (ref a)) (Jˢ A C a a c (ref a)) c
 := ref c

Uniqueness

(-Uniqueness).

def UIP (A : V) (a b : A) (p q : Id A a b)
  : Id (Id A a b) p q
 := ref p

THEOREMS

(Identity System). An identity system over type in universe is a family with a function such that any type family and , there exists a function such that for all .

def IdentitySystem (A : U) : U ≔
  Σ (=-form : A → A → U)
    (=-ctor : Π (a : A), =-form a a)
    (=-elim : Π (a : A) (C: Π (x y : A)
                (p : =-form x y), U)
                (d : C a a (=-ctor a)) (y : A)
                (p : =-form a y), C a y p)
    (=-comp : Π (a : A) (C: Π (x y : A)
                (p : =-form x y), U)
                (d : C a a (=-ctor a)),
                Path (C a a (=-ctor a)) d
                     (=-elim a C d a (=-ctor a))), 𝟏

There are number of equality signs used in this tutorial, all of them listed in the following table of identity systems:

(Fundamental Theorem of Identity System).

(Strict Identity System). An identity system over type and universe of pretypes is called strict identity system (), which respects UIP.

(Homotopy Identity System). An identity system over type and universe of homotopy types is called homotopy identity system (), which models discrete infinity groupoid.