path

$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapleft#1{\xleftarrow{{#1}}} \def\mapup#1{\Big\uparrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapupl#1{\Big\uparrow\llap{\raise2pt{\scriptstyle{#1}}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdownl#1{\Big\downarrow\llap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

Path package contains basic theorems about general homotopy path types. In the core the cubical has heterogeneous PathP type,

HeteroPath (A B: U) (a: A) (b: B) (P: Path U A B) : U = PathP P a b

so you can easily define homogeneous Path:

Path (A: U) (a b: A) : U = PathP ( A) a b

The Path identity type defines a Path space with elements and values. Elements of that space are functions from interval $[0,1]$ to values of that path space. This ctt file reflects CCHM² cubicaltt model with connections. For ABCFHL⁴ yacctt model with variables please refer to ytt file. You may also want to read BCH¹, AFH⁵. There is a PO³ paper about CCHM axiomatic in a topos.

¹ — Bezem, Coquand, Huber (2014)
² — Cohen, Coquand, Huber, Mörtberg (2015)
³ — Pitts, Orton (2016)
⁴ — Angiuli, Brunerie, Coquand, Favonia, Harper, Licata (2017)
⁵ — Angiuli, Favonia, Harper (2018)

Definitions

Introduction

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 $[0,1]$ that returns a constant value a. Written in syntax as a.

Applications

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

Connections allow you to build a square with only one element of path: i) $\\(i,j:I) \rightarrow p\ @\ min(i,j)$; ii) $\\(i,j:I)\rightarrow p\ @\ max(i,j)$.

$$ \begin{array}{ccc} b & \mapright{\\(i:I) \rightarrow b} & b \\ \mapupl{p} & & \mapup{\\(i:I)\rightarrow b} \\ a & \mapright{p} & b \\ \end{array} $$ $$ \begin{array}{ccc} a & \mapright{p} & b \\ \mapupl{\\(i:I)\rightarrow a} & & \mapup{p} \\ a & \mapright{\\(i:I)\rightarrow a} & a \\ \end{array} $$

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)

Lemmas

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 $[0,1]$ that returns application of encode function to path application of the given path to lamda argument f (p @ i) in both cases.

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 $[]$ of a over a path p comp p a [].

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

$$ \begin{array}{ccc} a & \mapright{comp} & c \\ \mapupl{\\(i:I) \rightarrow a} & & \mapup{q} \\ a & \mapright{p\ @\ i} & b \\ \end{array} $$

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 comp (Path A a (q @ i)) p [].

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 (p @ i, p @ i/\j).

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

Beta Equality

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.

Function Extensionality

Introduction

funext (A B: U) (f g: A -> B)
       (p: (x:A) -> Path B (f x) (g x))
     : Path (A -> B) f g

Elimination

happly (A B: U) (f g: A -> B) (p: Path (A -> B) f g) (x: A)
     : Path B (f x) (g x)

Computation

funext_Beta (A B: U) (f g: A -> B)
            (p: (x:A) -> Path B (f x) (g x))
          : (x:A) -> Path B (f x) (g x)

Uniqueness

funext_Eta (A B: U) (f g: A -> B)
           (p: Path (A -> B) f g)
         : Path (Path (A -> B) f g) (funext A B f g (happly A B f g p)) p

Dependent Version

piext (A: U) (B: A -> U) (f g: (x: A) -> B x)
      (p: (x: A) -> Path (B x) (f x) (g x))
    : Path ((y: A) -> B y) f g