path

Path package contains basic theorems about general homotopy path types. In the core cubical has heterogenous PathP type, so you can easily define homogenous Path:

Path (A : U) (a b : A) : U = PathP (<i> A) a b

The Path identity type defines a Path space. Elements of that space are functions from interval $[0,1]$ to a values of that path space.

Intro

Reflexivity Path Space

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 <i> a.

Lemmas

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

Map

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

Maps a given path space between values of one type to path space of another type by an encode function between types. Implemented as lambda defined on $[0,1]$ that returns application of encode function to path application of the given path to lamda argument <i> f (p @ i).

Eliminators

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

J by Paulin-Mohring

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

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

Dependent Eliminator

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.

Function Extensionality

Non-dependent

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

Inverse

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

Dependent

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