PATH SPACES

The homotopy identity system defines a space indexed over type with elements as functions from interval to values of that path space . HoTT book defines two induction principles for identity types: path induction and based path induction. The cubical type system CCHM briefly described in [1,2,3,4,5].

¹ — Bezem, Coquand, Huber (2014)
² — Cohen, Coquand, Huber, Mörtberg (2015)
³ — Pitts, Orton (2016)
⁴ — Huber (2017)
⁵ — Vezzosi, Mörtberg , Abel (2019)

Formation

(Path Formation).

def Path (A : U) (x y : A) : U
 := PathP (<_> A) x y

def Pathᴵ (A : U) (x y : A)
 := Π (i : I),
    A [∂ i |-> [(i = 0) → x ,
                (i = 1) → y ]]

Introduction

(Path Introduction).

def idp (A: U) (x: A)
  : Path A x x := <_> x

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 that returns a constant value . Written in syntax as .

(Path Application).

def at0 (A: U) (a b: A)
    (p: Path A a b) : A := p @ 0

def at1 (A: U) (a b: A)
    (p: Path A a b): A := p @ 1

(Path Connections).

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

def join (A: U) (a b: A) (p: Path A a b)
  : PathP (<x> Path A (p@x) b) p (<i> b)
 := <y x> p @ (x \/ y)

def meet (A: U) (a b: A) (p: Path A a b)
  : PathP (<x> Path A a (p@x)) (<i> a) p
 := <x y> p @ (x /\ y)

(Path Inversion).

(Congruence).

def ap (A B: U) (f: A -> B)
    (a b: A) (p: Path A a b)
  : Path B (f a) (f b)

def 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 that returns application of encode function to path application of the given path to lamda argument in both cases.

(Generalized Transport Kan Operation). 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.

def transp' (A: U) (x y: A) (p : PathP (<_>A) x y) (i: I)
 := transp (<i> (\(_:A),A) (p @ i)) i x

def transpᵁ (A B: U) (p : PathP (<_>U) A B) (i: I)
 := transp (<i> (\(_:U),U) (p @ i)) i A

(Partial Elements).

def Partial' (A : U) (i : I)
  : V := Partial A i

(Cubical Subtypes).

def sub (A : U) (i : I) (u : Partial A i)
  : V := A [i ↦ u]

(Cubical Elements).

def inS (A : U) (i : I) (a : A)
  : sub A i [(i = 1) → a] := inc A i a

def outS (A : U) (i : I) (u : Partial A i)
  : A [i ↦ u] -> A := λ (a: A[i ↦ u]), ouc a

(Heterogeneous Composition Kan Operation).

def compCCHM (A : I → U) (r : I)
    (u : Π (i : I), Partial (A i) r)
    (u₀ : (A 0)[r ↦ u 0]) : A 1
 := hcomp (A 1) r (λ (i : I),
    [ (r = 1) → transp (<j> A (i ∨ j)) i (u i 1=>1)])
      (transp (<i> A i) 0 (ouc u₀))

(Homogeneous Composition Kan Operation).

def compCHM (A : U) (r : I)
    (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : A
 := hcomp A r u (ouc u₀)

(Substitution).

def subst (A: U) (P: A -> U) (x y: A) (p: Path A x y)
  : P x -> P y
 := λ (e: P x), transp (<i> P (p @ i)) 0 e

Other synonyms are and .

(Path Composition).

def pcomp (A: U) (a b c: A)
    (p: Path A a b) (q: Path A b c)
  : Path A a c := subst A (Path A a) b c q p

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

Elimination

(J by Paulin-Mohring).

def 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.

(Contractability of Singleton).

def singl (A: U) (a: A) : U
 := Σ (x: A), Path A a x

def contr (A: U) (a b: A) (p: Path A a b)
  : Path (singl A a) (a,<_>a) (b,p)

Proof that singleton is contractible space. Implemented as .

(HoTT Dependent Eliminator).

def 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 Path Induction).

def D (A: U) : U
 := П (x y: A), Path A x y -> U

def 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

(Path Computation).

def trans_comp (A: U) (a: A)
  : Path A a (trans A A (<_> A) a)

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

def 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, see the PROP type.