# PATH

The Path identity type defines a Path space with elements and values.
Elements of that space are functions
from interval ^{2} cubicaltt model with connections.
There is a PO^{3}
paper about CCHM axiomatic in a topos.

^{1}— Bezem, Coquand, Huber (2014)

^{2}— Cohen, Coquand, Huber, Mörtberg (2015)

^{3}— Pitts, Orton (2016)

## Constructors

`refl (A: U) (a: A) : Path A a a`

Returns a reflexivity path space for a given value of the type.
The inhabitant of that path space is the lambda on the homotopy
interval

## Eliminators

```
app1 (A: U) (a b: A) (p: Path A a b): A = p @ 0
app2 (A: U) (a b: A) (p: Path A a b): A = p @ 1
```

Connections allow you to build a square
with only one element of path: i)

```
connection1 (A: U) (a b: A) (p: Path A a b)
: PathP (<x> Path A ([email protected]) b) p (<i> b)
= <y x> p @ (x \/ y)
connection2 (A: U) (a b: A) (p: Path A a b)
: PathP (<x> Path A a ([email protected])) (<i> a) p
= <x y> p @ (x /\ y)
```

## Congruence

```
ap (A B: U) (f: A -> B)
(a b: A) (p: Path A a b)
: Path B (f a) (f b)
apd (A: U) (a x:A) (B:A->U) (f: A->B a)
(b: B a) (p: Path A a x)
: Path (B a) (f a) (f x)
```

Maps a given path space between values of one type
to path space of another type using an encode function between types.
Implemented as a lambda defined on

## Transport

`trans (A B: U) (p: Path U A B) (a: A) : B`

Transports a value of the left type to the value of the right type
by a given path element of the path space between left and right types.
Defined as path composition with

## Substitution

```
subst (A: U) (P: A -> U)
(a b: A) (p: Path A a b)
(u: P a) : P b
```

Acts like transport of mapOnPath value, representing the dependent function transport or substitution.

## Composition

```
composition (A: U) (a b c: A)
(p: Path A a b) (q: Path A b c): Path A a c
```

Composition operation allows building a new path from two given paths
in a connected point. The proofterm is

## Contractability of Singleton

```
singl (A: U) (a: A) : U = (x: A) * Path A a x
contrSingl (A: U) (a b: A) (p: Path A a b)
: Path (singl A a) (a,refl A a) (b,p)
```

Proof that singleton is contractible space. Implemented as

# Eliminators

## J by Paulin-Mohring

```
J (A: U)
(a b: A)
(P: singl A a -> U)
(u: P (a,refl A a))
(p: Path A a b) : P (b,p)
```

J is formulated in a form of Paulin-Mohring and implemented using two facts that singletons are contractible and dependent function transport.

## Dependent Eliminator (HoTT)

```
J (A: U)
(a: A)
(C: (x: A) -> Path A a x -> U)
(d: C a (refl A a))
(x: A)
(p: Path A a x) : C x p
```

J from HoTT book.

## Diagonal Version

```
D (A: U) : U = (x y: A) -> Path A x y -> U
J (A: U)
(x: A)
(C: D A)
(d: C x x (refl A x))
(y: A)
(p: Path A x y) : C x y p
```

## Computation

```
trans_comp (A: U) (a: A)
: Path A a (trans A A (<_> A) a)
subst_comp (A: U) (P: A -> U) (a: A) (e: P a)
: Path (P a) e (subst A P a a (refl A a) e)
J_comp (A: U) (a: A) (C: (x: A) -> Path A a x -> U)
(d: C a (refl A a))
: Path (C a (refl A a)) d (J A a C d a (refl A a))
```

Note that in HoTT there is no Eta rule, otherwise Path between element would requested to be unique applying UIP at any Path level which is prohibited. UIP in HoTT is defined only as instance of n-groupoid, the PROP type.