# IDENTITY SPACES

## Formation

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

## Introduction

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

## Elimination

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

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

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

# THEOREMS

```
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: