Kubus

6. Transport and path induction

A path between types is a line of types, and composition along a line of types with an empty system moves an element from one end to the other. This is transport, and from it follows the induction principle for paths.

Transport

lib/basic.ktt
✓def transport {A B : U} (p : Path U A B) (a : A) : B := comp i (p i) [] a

comp i (p i) [] a composes along the line p with no sides at all: the result is a carried over to the other end. Transport along a family of types over a path is substitution, the principle that equal elements have the same properties:

import basic
✓def subst {A : U} (P : A -> U) {a b : A} (p : Path A a b) (x : P a) : P b :=
transport (\i -> P (p i)) x

What does transport along a constant line do? For a data type without parameters, like the booleans, it is the identity, by computation:

✓data Bool : U := false | true
#eval transport (\i -> Bool) true
true
  : Bool

For an arbitrary type A, transport along the constant line is not the identity by computation, but it is equal to it by a path. The filler of the composition gives that path, with the constant side at i = 1:

lib/basic.ktt
✓def transportRefl {A : U} (x : A) : Path A (transport (\i -> A) x) x :=
\i -> comp j A [i = 1 -> x] x

Path induction

The induction principle for paths, J, says: to prove something about every path p from a fixed a to some x, it suffices to prove it for refl a. In cubical type theory, J is not a primitive; it is transport along the contraction of singletons from chapter 4:

lib/basic.ktt
✓def singl {A : U} (a : A) : U := (x : A) × Path A a x
✓def contrSingl {A : U} {a b : A} (p : Path A a b) : Path (singl a) (a, refl a) (b, p) :=
\i -> (p i, \j -> p (i /\ j))
✓def J {A : U} {a : A} (C : (x : A) -> Path A a x -> U) (d : C a (refl a)) {x : A} (p : Path A a x) : C x p :=
transport (\i -> C (contrSingl p i).1 (contrSingl p i).2) d

Its computation rule holds up to a path, again by transportRefl:

lib/basic.ktt
✓def JRefl {A : U} {a : A} (C : (x : A) -> Path A a x -> U) (d : C a (refl a))
: Path (C a (refl a)) (J C d (refl a)) d :=
transportRefl d

J derives the usual properties of paths. Symmetry, for example:

✓def symJ {A : U} {a b : A} (p : Path A a b) : Path A b a :=
J (\x q -> Path A x a) (refl a) p

J takes the motive \x q -> Path A x a, a family of types over the end point x and the path q, and the case refl a. The implicit arguments A and a and the end point x are found by unification (higher-order pattern unification, for the motive's type).

In practice, the cubical operations are often more direct than J: sym is a one-line interval lambda, and many equations hold by computation that J would only give up to a path.

Transport in families computes

Transport is defined by cases on the line of types, so it computes in function types, pair types and path types too. Transporting a pair transports its components:

✓def Pair : U := Bool × Bool
#eval transport (\i -> Pair) (true, false)
(true, false)
  : Bool × Bool