module 1Lab.Path where

# The intervalπ

In HoTT, the inductively-defined identity type gets a new meaning
explanation: continuous paths, in a topological sense. The βkey ideaβ of
cubical type theory β and thus, Cubical Agda β is that we can take this
as a new *definition* of the identity type, where we interpret a
`Path`

in a type by a function
where the domain is the *interval type*.

## A brief comment on the meanings of βequalβ, βidenticalβ and βidentifiedβ, and how we refer to inhabitants of path types.

Before getting started, itβs worth taking a second to point out the
terminology that will be used in this module (and most of the other
pages). In intensional type theory, there is both an external notion of
βsamenessβ (definitional equality), and an internal notion of
βsamenessβ, which goes by many names: identity type, equality type,
propositional equality, path type, etc.^{1}

In this module, we refer to the type `A β‘ B`

as either
(the type of) *paths from A to B* or (the type of)
*identifications between A and B*, but **never** as
βequalities between A and Bβ. In particular, the HoTT book comments that
we may say
β$a$
and
$b$
are equalβ when the type
$aβ‘b$
is inhabited, but in this development we reserve this terminology for
the case where
$a$
and
$b$
inhabit a set.

Instead, for general types, we use
β$a$
and
$b$
are **identical**β or
β$a$
and
$b$
are **identified**β (or even the wordier, and rather more
literal, βthere is a path between
$a$
and
$b$β).
Depending on the type, we might use more specific words: Paths are said
to be **homotopic** when theyβre connected by a
path-of-paths, and types are said to be **equivalent** when
they are connected by a path.

open import Prim.Extension public open import Prim.Interval public open import Prim.Kan public

The type `I`

is meant to represent the
(real, closed) unit interval
$[0,1],$
the same unit interval used in the topological definition of path.
Because the real unit interval has a least and greatest element β 0 and
1 β the interval *type* also has two global inhabitants, `i0`

and `i1`

. This is where
the analogy with the reals breaks down: Thereβs no such thing as
`i0.5`

(much less `i1/Ο`

). In reality, the
interval type internalises an abstract interval *object*.

Regardless, since all functions definable in type theory are
automatically continuous, we can take a path to be any value in the
function type `I β A`

. When working with paths, though, itβs
useful to mention the endpoints of a path in its type β that is, the
values the function takes when applied to `i0`

and to
`i1`

. We can βupgradeβ any function `f : I β A`

to
a `Path`

, using a definition that
looks suspiciously like the identity function:

private to-path : β {β} {A : Type β} β (f : I β A) β Path A (f i0) (f i1) to-path f i = f i refl : β {β} {A : Type β} {x : A} β x β‘ x refl {x = x} = to-path (Ξ» i β x)

The type `Path A x y`

is also written `x β‘ y`

,
when `A`

is not important - i.e.Β when it can be inferred from
`x`

and `y`

. Under this interpretation, proof that
identification is reflexive (i.e.Β that
$x=x)$
is given by a `Path`

which yields the same
element everywhere on `I`

: The function that is constantly
$x.$

If we have a `Path`

, we can apply it to a
value of the interval type to get an element of the underlying type.
When a path is applied to one of the endpoints, the result is the same
as declared in its type β even when weβre applying a path we donβt know
the definition of.^{2}

module _ {β} {A : Type β} {x y : A} {p : x β‘ y} where private left-endpoint : p i0 β‘ x left-endpoint i = x right-endpoint : p i1 β‘ y right-endpoint i = y

In addition to the two endpoints `i0`

and `i1`

, the interval
has the structure of a De Morgan algebra. All the following equations
are respected (definitionally), but they can not be expressed internally
as a `Path`

because `I`

is not in `Type`

.^{3}

- $xβ§i0=i0,$ $xβ§i1=x$
- $xβ¨i0=x,$ $xβ¨i1=i1$
- $Β¬(xβ§y)=Β¬xβ¨Β¬y$
- $Β¬i0=i1,$ $Β¬i1=i0,$ $Β¬Β¬x=x$
- $β§$ and $β¨$ are both associative, commutative and idempotent, and distribute over eachother.

Note that, in the formalisation,
$Β¬x$
is written `~ x`

. As a more familiar description, a De Morgan
algebra is a Boolean algebra that does not (necessarily) satisfy the law
of excluded middle. This is necessary to maintain type safety.

## Raising dimensionπ

To wit: In cubical type theory, a term in a context with
$n$
interval variables expresses a way of mapping an
$n-cube$
into that type. One very important class of these maps are the
$1-cubes$
β lines or * paths* β which represent
identifications between terms of that type.

Iterating this construction, a term in a context with 2 interval
variables represents a square in the type, which can be read as saying
that some *paths* (specialising one of the variables to
$i0$
or
$i1)$
in that space are identical: A path between paths, which we call a
*homotopy*.

The structural operations on contexts, and the $β§$ and $β¨$ operations on the interval, give a way of extending from $n-dimensional$ cubes to $n+k-dimensional$ cubes. For instance, if we have a path like the one below, we can extend it to any of a bunch of different squares:

module _ {β} {A : Type β} {a b : A} {p : Path A a b} where

The first thing we can do is introduce another interval variable and
ignore it, varying the path over the non-ignored variable. These give us
squares where either the top/bottom or left/right faces are the path
`p`

, and the other two are refl.

private drop-j : PathP (Ξ» i β p i β‘ p i) refl refl drop-j i j = p i drop-i : PathP (Ξ» i β a β‘ b) p p drop-i i j = p j

These squares can be drawn as below. Take a moment to appreciate how
the *types* of `drop-j`

and `drop-i`

specify the
*boundary* of the diagram β A
`PathP (Ξ» i β p i β‘ p i) refl refl`

corresponds to a square
whose top/bottom faces are both `p`

, and whose left/right
faces are both `refl`

(by convention).
Similarly, `PathP (Ξ» i β a β‘ b) p p`

has `refl`

as top/bottom faces
(recall that `refl`

is the constant function
regarded as a path), and `p`

as both left/right faces.

The other thing we can do is use one of the binary operators on the
interval to get squares called *connections*, where two adjacent
faces are `p`

and the other two are refl:

β§-conn : PathP (Ξ» i β a β‘ p i) refl p β§-conn i j = p (i β§ j) β¨-conn : PathP (Ξ» i β p i β‘ b) p refl β¨-conn i j = p (i β¨ j)

These correspond to the following two squares:

Since iterated paths are used *a lot* in homotopy type theory,
we introduce a shorthand for 2D non-dependent paths. A `Square`

in a type is exactly
what it says on the tin: a square.

Square : β {β} {A : Type β} {a00 a01 a10 a11 : A} β (p : a00 β‘ a01) β (q : a00 β‘ a10) β (s : a01 β‘ a11) β (r : a10 β‘ a11) β Type β Square p q s r = PathP (Ξ» i β p i β‘ r i) q s

SquareP : β {β} (A : I β I β Type β) {aββ : A i0 i0} {aββ : A i0 i1} {aββ : A i1 i0} {aββ : A i1 i1} (p : PathP (Ξ» i β A i i0) aββ aββ) (q : PathP (Ξ» j β A i0 j) aββ aββ) (s : PathP (Ξ» j β A i1 j) aββ aββ) (r : PathP (Ξ» i β A i i1) aββ aββ) β Type β SquareP A p q s r = PathP (Ξ» i β PathP (Ξ» j β A i j) (p i) (r i)) q s

The arguments to `Square`

are as in the following
diagram, listed in the order βPQSRβ. This order is a bit unusual (itβs
one off from being alphabetical, for instance) but it does have a
significant benefit: If you imagine that the letters are laid out in a
circle, *identical paths are adjacent*. Reading the square in the
left-right direction, it says that
$p$
and
$r$
are identical β these are adjacent if you βfold upβ the sequence
`p q s r`

. Similarly, reading top-down, it says that
$q$
and
$s$
are identical - these are directly adjacent.

## Symmetryπ

The involution `~_`

on the
interval type gives a way of inverting paths β a proof that
identification is symmetric.

sym : β {ββ} {A : Type ββ} {x y : A} β x β‘ y β y β‘ x sym p i = p (~ i)

symP : β {ββ} {A : I β Type ββ} {x : A i0} {y : A i1} β PathP A x y β PathP (Ξ» i β A (~ i)) y x symP p i = p (~ i)

As a minor improvement over βBook HoTTβ, this operation is
*definitionally* involutive:

module _ {β} {A : Type β} {x y : A} {p : x β‘ y} where private sym-invol : sym (sym p) β‘ p sym-invol i = p

Given a `Square`

, we can βflipβ it along
either dimension, or along the main diagonal:

module _ {β} {A : Type β} {a00 a01 a10 a11 : A} {p : a00 β‘ a01} {q : a00 β‘ a10} {s : a01 β‘ a11} {r : a10 β‘ a11} (Ξ± : Square p q s r) where flipβ : Square (sym p) s q (sym r) flipβ = symP Ξ± flipβ : Square r (sym q) (sym s) p flipβ i j = Ξ± i (~ j) transpose : Square q p r s transpose i j = Ξ± j i

# Pathsπ

While the basic structure of the path type is inherited from its
nature as functions out of an internal De Morgan algebra, the structure
of *identifications* presented by paths is more complicated. For
starters, letβs see how paths correspond to identifications in that they
witness the logical principle of βindiscernibility of identicalsβ.

## Transportπ

A basic principle of identity is that *identicals are
indiscernible*: if
$x=y$
and
$P(x)$
holds, then
$P(y)$
also holds, for any choice of predicate
$P.$
In type theory, this is generalised, as
$P$
can be not only a predicate, but any type family.

The way this is incarnated is by an operation called `transport`

, which says that
every path between `A`

and `B`

gives rise to a
*function* `A β B`

.

transport : β {β} {A B : Type β} β A β‘ B β A β B transport p = transp (Ξ» i β p i) i0

The transport operation is the earliest case of when thinking of
`p : A β‘ B`

as merely saying βA and B are equalβ goes
seriously wrong. A path gives a *specific* identification of
`A`

and `B`

, which can be highly non-trivial.

As a concrete example, it can be shown that the type
`Bool β‘ Bool`

has exactly two inhabitants (see here), which is something like
saying βthe set of booleans is equal to itself in two waysβ. That phrase
is nonsensical, which is why βthere are two paths Bool β Boolβ is
preferred: itβs not nonsense.

In Cubical Agda, `transport`

is a derived notion,
with the actual primitive being `transp`

. Unlike `transport`

, which has two
arguments (the path, and the point to transport), `transp`

has *three*:

The first argument to

`transp`

is a*line*of types, i.e.Β a function`A : I β Type`

, just as for`transport`

.The second argument to

`transp`

has type`I`

, but itβs not playing the role of an endpoint of the interval. Itβs playing the role of a*formula*, which specifies*where the transport is constant*: In`transp P i1`

,`P`

is required to be constant, and the transport is the identity function:_ : β {β} {A : Type β} β transp (Ξ» i β A) i1 β‘ id _ = refl

The third argument is an inhabitant of

`A i0`

, as for`transport`

.

This second argument, which lets us control where `transp`

is constant, brings a
lot of power to the table! For example, the proof that transporting
along `refl`

is `id`

is as follows:

transport-refl : β {β} {A : Type β} (x : A) β transport (Ξ» i β A) x β‘ x transport-refl {A = A} x i = transp (Ξ» _ β A) i x

Since `Ξ» i β A`

is a constant function, the definition of
`transport-refl`

is well-typed,
and it has the stated endpoints because `transport`

is defined to be
`transp P i0`

, and `transp P i1`

is the identity
function.

In fact, this generalises to something called the *filler* of
`transport`

:
`transport p x`

and `x`

*are* identical,
but theyβre identical *over* the given path:

transport-filler : β {β} {A B : Type β} β (p : A β‘ B) (x : A) β PathP (Ξ» i β p i) x (transport p x) transport-filler p x i = transp (Ξ» j β p (i β§ j)) (~ i) x

##
We also have some special cases of `transport-filler`

which are very
convenient when working with iterated transports.

transport-filler-ext : β {β} {A B : Type β} (p : A β‘ B) β PathP (Ξ» i β A β p i) (Ξ» x β x) (transport p) transport-filler-ext p i x = transport-filler p x i transportβ»-filler-ext : β {β} {A B : Type β} (p : A β‘ B) β PathP (Ξ» i β p i β A) (Ξ» x β x) (transport (sym p)) transportβ»-filler-ext p i x = transp (Ξ» j β p (i β§ ~ j)) (~ i) x transportβ»transport : β {β} {A B : Type β} (p : A β‘ B) (a : A) β transport (sym p) (transport p a) β‘ a transportβ»transport p a i = transportβ»-filler-ext p (~ i) (transport-filler-ext p (~ i) a)

The path is constant when `i = i0`

because
`(Ξ» j β p (i0 β§ j))`

is `(Ξ» j β p i0)`

(by the
reduction rules for `_β§_`

).
It has the stated endpoints, again, because `transp P i1`

is
the identity function.

By altering a path `p`

using a predicate `P`

,
we get the promised principle of *indiscernibility of
identicals*:

subst : β {ββ ββ} {A : Type ββ} (P : A β Type ββ) {x y : A} β x β‘ y β P x β P y subst P p x = transp (Ξ» i β P (p i)) i0 x

substβ : β {ββ ββ ββ} {A : Type ββ} {B : Type ββ} (P : A β B β Type ββ) {a a' : A} {b b' : B} β a β‘ a' β b β‘ b' β P a b β P a' b' substβ P p q x = transp (Ξ» i β P (p i) (q i)) i0 x

### Computationπ

In βBook HoTTβ, `transport`

is defined using path
induction, and it computes definitionally on `refl`

. We have already seen that
this is not definitional in cubical type theory, which might lead you to
ask: When does `transport`

compute? The answer
is: By cases on the path. The structure of the path `P`

is
what guides reduction of `transport`

. Here are some
reductions:

For the natural numbers, and other inductive types without
parameters, transport is always the identity function. This is justified
because thereβs nothing to vary in `Nat`

, so we can just ignore the
transport:

_ : {x : Nat} β transport (Ξ» i β Nat) x β‘ x _ = refl

For other type formers, the definition is a bit more involved. Letβs
assume that we have two lines, `A`

and `B`

, to see
how transport reduces in types built out of `A`

and
`B`

:

module _ {A : I β Type} {B : I β Type} where private

For non-dependent products, the reduction rule says that β`transport`

is homomorphic over
forming productsβ:

_ : {x : A i0} {y : B i0} β transport (Ξ» i β A i Γ B i) (x , y) β‘ (transport (Ξ» i β A i) x , transport (Ξ» i β B i) y) _ = refl

For non-dependent functions, we have a similar situation, except one
of the transports is *backwards*. This is because, given an
`f : A i0 β B i0`

, we have to turn an `A i1`

into
an `A i0`

to apply f!

_ : {f : A i0 β B i0} β transport (Ξ» i β A i β B i) f β‘ Ξ» x β transport (Ξ» i β B i) (f (transport (Ξ» i β A (~ i)) x)) _ = refl module _ {A : I β Type} {B : (i : I) β A i β Type} where private

In the dependent cases, we have slightly more work to do. Suppose
that we have a line `A : I β Type β`

and a *dependent*
line `B : (i : I) β A i β Type β`

. Letβs characterise `transport`

in the lines
`(Ξ» i β (x : A i) β B i x)`

. A first attempt would be to
repeat the non-dependent construction: Given an
`f : (x : A i0) β B i0 x`

and an argument
`x : A i1`

, we first get `x' : A i0`

by
transporting along `Ξ» i β A (~ i)`

, compute
`f x' : B i0 x`

, then transport along
`(Ξ» i β B i x')`

to g- Wait.

_ : {f : (x : A i0) β B i0 x} β transport (Ξ» i β (x : A i) β B i x) f β‘ Ξ» (x : A i1) β let x' : A i0 x' = transport (Ξ» i β A (~ i)) x

We canβt βtransport along `(Ξ» i β B i x')`

β, thatβs not
even a well-formed type! Indeed, `B i : A i β Type`

, but
`x' : A i1`

. What we need is some way of connecting our
original `x`

and `x'`

, so that we may get a
`B i1 x'`

. This is where `transport-filler`

comes in:

xβ‘x' : PathP (Ξ» i β A (~ i)) x x' xβ‘x' = transport-filler (Ξ» i β A (~ i)) x

By using `Ξ» i β B i (xβ‘x' (~ i))`

as our path, we a) get
something type-correct, and b) get something with the right endpoints.
`(Ξ» i β B i (xβ‘x' (~ i)))`

connects `B i0 x`

and
`B i1 x'`

, which is what we wanted.

fx' : B i0 x' fx' = f x' in transport (Ξ» i β B i (xβ‘x' (~ i))) fx' _ = refl

The case for dependent products (i.e.Β general `Ξ£`

types) is analogous, but without any inverse transports.

## Path inductionπ

The path induction principle, also known as βaxiom Jβ, essentially breaks down as the following two statements:

Identicals are indiscernible (

`transport`

)Singletons are contractible. The type

`Singleton A x`

is the βsubtype of A of the elements identical to xβ:

Singleton : β {β} {A : Type β} β A β Type _ Singleton x = Ξ£[ y β _ ] (x β‘ y)

There is a canonical inhabitant of `Singleton x`

, namely
`(x, refl)`

. To say that `singletons`

are contractible is
to say that every other inhabitant has a path to
`(x, refl)`

:

Singleton-is-contr : β {β} {A : Type β} {x : A} (y : Singleton x) β Path (Singleton x) (x , refl) y Singleton-is-contr {x = x} (y , path) i = path i , square i where square : Square refl refl path path square i j = path (i β§ j)

Thus, the definition of `J`

:
`transport`

+ `Singleton-is-contr`

.

J : β {ββ ββ} {A : Type ββ} {x : A} (P : (y : A) β x β‘ y β Type ββ) β P x (Ξ» _ β x) β {y : A} (p : x β‘ y) β P y p J {x = x} P prefl {y} p = transport (Ξ» i β P (path i .fst) (path i .snd)) prefl where path : (x , refl) β‘ (y , p) path = Singleton-is-contr (y , p)

This eliminator *doesnβt* definitionally compute to
`prefl`

when `p`

is `refl`

, again since
`transport (Ξ» i β A)`

isnβt definitionally the identity.
However, since it *is* a transport, we can use the `transport-filler`

to get a path
expressing the computation rule.

J-refl : β {ββ ββ} {A : Type ββ} {x : A} (P : (y : A) β x β‘ y β Type ββ) β (pxr : P x refl) β J P pxr refl β‘ pxr J-refl {x = x} P prefl i = transport-filler (Ξ» i β P _ (Ξ» j β x)) prefl (~ i)

inspect : β {a} {A : Type a} (x : A) β Singleton x inspect x = x , refl record Recall {a b} {A : Type a} {B : A β Type b} (f : (x : A) β B x) (x : A) (y : B x) : Type (a β b) where constructor βͺ_β« field eq : f x β‘ y recall : β {a b} {A : Type a} {B : A β Type b} β (f : (x : A) β B x) (x : A) β Recall f x (f x) recall f x = βͺ refl β«

# Compositionπ

In βBook HoTTβ, the primitive operation from which the
higher-dimensional structure of types is derived is the `J`

eliminator, with `J-refl`

as a
*definitional* computation rule. This has the benefit of being
very elegant: This one elimination rule generates an infinite amount of
coherent data. However, itβs very hard to make compute in the presence
of higher inductive types and univalence, so much so that, in the book,
univalence and HITs only compute up to paths.

In Cubical Agda, types are interpreted as objects called *cubical
Kan complexes*^{4}, which are a *geometric*
description of spaces as βsets we can probe by cubesβ. In Agda, this
βprobingβ is reflected by mapping the interval into a type: A βprobeβ of
$A$
by an
$n-cube$
is a term of type
$A$
in a context with
$n$
variables of type `I`

β points, lines, squares,
cubes, etc. This structure lets us βexploreβ the higher dimensional
structure of a type, but it does not specify how this structure
behaves.

Thatβs where the βKanβ part of βcubical Kan complexβ comes in:
Semantically, *every open box extends to a cube*. The concept of
βopen boxβ might make even less sense than the concept of βcube in a
typeβ initially, so it helps to picture them! Suppose we have three
paths
$p:wβ‘x,$
$q:xβ‘y,$
and
$r:yβ‘z.$
We can pictorially arrange them into an open box like in the diagram
below, by joining the paths by their common endpoints:

In the diagram above, we have a square assembled of three lines
$wβ‘x,$
$xβ‘y,$
and
$yβ‘z.$
Note that in the left face of the diagram, the path was inverted; This
is because while we have a path
$wβ‘x,$
we need a path
$xβ‘w,$
and all parallel faces of a cube must βpointβ in the same direction. The
way the diagram is drawn strongly implies that there is a face missing β
the line
$wβ‘z.$
The interpretation of types as *Kan* cubical sets guarantees that
the open box above extends to a complete square, and thus the line
$wβ‘z$
exists.

## Partial elementsπ

The definition of Kan cubical sets as those having fillers for all
open boxes is all well and good, but to use this from within type theory
we need a way of reflecting the idea of βopen boxβ as syntax. This is
done is by using the `Partial`

type former.

The `Partial`

type former takes two
arguments: A *formula*
$Ο,$
and a *type*
$A.$
The idea is that a term of type
$PartialΒΟΒA$
in a context with
$n$
`I`

-typed variables is a
$n-cube$
that is only defined when
$Ο$
βis trueβ. In Agda, formulas are represented using the De Morgan
structure of the interval, and they are βtrueβ when they are equal to 1.
The predicate `IsOne`

represents
truth of a formula, and there is a canonical inhabitant `1=1`

which says `i1`

is `i1`

.

For instance, if we have a variable `i : I`

of interval
type, we can represent *disjoint endpoints* of a `Path`

by a partial element with
formula
$Β¬iβ¨i.$
Note that this is not the same thing as `i1`

! Since elements
of `I`

are meant to represent real numbers
$rβ[0,1],$
it suffices to find one for which
$max(x,1βx)$
is not
$1$
β like 0.5.

private not-a-path : (i : I) β Partial (~ i β¨ i) Bool not-a-path i (i = i0) = true not-a-path i (i = i1) = false

This represents the following shape: Two disconnected points, with completely unrelated values at each endpoint of the interval.

More concretely, an element of `Partial`

can be understood as a
function where the domain is the predicate `IsOne`

, which has an inhabitant `1=1`

, stating that one is one.
Indeed, we can *apply* a `Partial`

to an argument of type
`IsOne`

to get a value of the
underlying type.

_ : not-a-path i0 1=1 β‘ true _ = refl

Note that if we *did* have `(~i β¨ i) = i1`

(i.e.Β our De Morgan algebra was a Boolean algebra), the partial element
above would give us a contradiction, since any
`I β Partial i1 T`

extends to a path:

_ : (f : I β Partial i1 Bool) β Path Bool (f i0 1=1) (f i1 1=1) _ = Ξ» f i β f i 1=1

## Extensibilityπ

A partial element in a context with
$n-variables$
gives us a way of mapping some subobject of the
$n-cube$
into a type. A natural question to ask, then, is: Given a partial
element
$e$
of
$A,$
can we extend that to an honest-to-god *element* of
$A,$
which agrees with
$e$
where it is defined?

Specifically, when this is the case, we say that
$x:A$
*extends*
$e:PartialΒΟΒA.$
We could represent this very generically as a *lifting problem*,
i.e.Β trying to find a map
$β‘_{n}$
which agrees with
$e$
when restricted to
$Ο,$
but I believe a specific example will be more helpful.

Suppose we have a partial element of `Bool`

which is `true`

on the left
endpoint of the interval, and undefined elsewhere. This is a partial
element with one interval variable, so it would be extended by a
*path* β a 1-dimensional cube. The reflexivity path is a line in
`Bool`

, which is `true`

on the left
endpoint of the interval (in fact, it is `true`

everywhere),
so we say that `refl`

*extends* the
partial element.

In the diagram, we draw the specific partial element being extended
in red, and the total path extending it in black. In Agda, extensions
are represented by the type former `_[_β¦_]`

.^{5}

We can formalise the red-black extensibility diagram above by
defining the partial element `left-true`

and giving `refl`

to `inS`

, the constructor for `_[_β¦_]`

.

private left-true : (i : I) β Partial (~ i) Bool left-true i (i = i0) = true refl-extends : (i : I) β Bool [ (~ i) β¦ left-true i ] refl-extends i = inS (refl {x = true} i)

The constructor `inS`

expresses that *any*
totally-defined cube
$u$
can be seen as a partial cube, one that agrees with
$u$
for any choice of formula
$Ο.$
This might be a bit abstract, so letβs diagram the case where we have
some square
$a,$
and the partial element has formula
$iβ¨j.$
This extension can be drawn as in the diagram below: The red βbackwards
Lβ shape is the partial element, which is βextended byβ the black lines
to make a complete square.

_ : β {β} {A : Type β} {Ο : I} (u : A) β A [ Ο β¦ (Ξ» _ β u) ] _ = inS

Note that since an extension must agree with the partial element
*everywhere*, there are elements that can not be extended at all.
Take `notAPath`

from before β since
there is no path that is `true`

at `i0`

and `false`

at `i1`

, it is not
extensible. If it were extensible, we would have
`true β‘ false`

β a contradiction.^{6}

not-extensible : ((i : I) β Bool [ (~ i β¨ i) β¦ not-a-path i ]) β true β‘ false not-extensible ext i = outS (ext i)

This counterexample demonstrates the eliminator for `_[_β¦_]`

,
`outS`

, which turns an
`A [ Ο β¦ u ]`

to `A`

, with a computation rule
saying that, for `x : A [ i1 β¦ u ]`

, `outS x`

computes to `u 1=1`

:

_ : β {A : Type} {u : Partial i1 A} {x : A [ i1 β¦ u ]} β outS x β‘ u 1=1 _ = refl

The notion of partial elements and extensibility captures the
specific interface of the Kan operations, which can be summed up in the
following sentence: *If a partial path is extensible at i0, then it is
extensible at i1*. Letβs
unpack that a bit:

A *partial path* is anything of type
`I β Partial Ο A`

β letβs say we have an `f`

in
that type. It takes a value at `i0`

(thatβs
`f i0`

), and a value at `i1`

. The Kan
condition expresses that, if there exists an
`A [ Ο β¦ f i0 ]`

, then we also have an
`A [ Ο β¦ f i1 ]`

. In other words: Extensibility is preserved
by paths.

Recall the open box we drew by gluing paths together at the start of
the section (on the left). It has a *top face* `q`

,
and it has a *tube* β its left/right faces, which can be
considered as a partial (in the left-right direction) path going in the
top-down direction.

We can make this the construction of this βopen boxβ formal by giving
a `Partial`

element of
`A`

, which is defined on
$βiβ¨Β¬j$
β where
$i$
represents the left/right direction, and
$j$
the up/down direction, as is done below. So, this is an element that is
defined *almost* everywhere: all three out of four faces of the
square exist, but weβre missing the fourth face and an inside.

module _ {A : Type} {w x y z : A} {p : w β‘ x} {q : x β‘ y} {r : y β‘ z} where private double-comp-tube : (i j : I) β Partial (~ i β¨ i β¨ ~ j) A double-comp-tube i j (i = i0) = sym p j double-comp-tube i j (i = i1) = r j double-comp-tube i j (j = i0) = q i

The Kan condition on types says that, whenever we have some formula $Ο$ and a partial element $u$ defined along $Οβ¨Β¬j$ (for $j$ disjoint from $Ο;$ we call it the βdirection of compositionβ, sometimes), then we can extend it to a totally-defined element, which agrees with $u$ along $Ο.$

The idea is that the $Β¬j,$ being in some sense βorthogonal toβ the dimensions in $Ο,$ will βconnectβ the tube given by $Ο.$ This is a slight generalization of the classical Kan condition, which would insist $Ο=β_{i}βi,$ where $i$ ranges over all dimensions in the context.

extensible-at-i1 : (i : I) β A [ (i β¨ ~ i) β¦ double-comp-tube i i1 ] extensible-at-i1 i = inS $β hcomp (β i) (double-comp-tube i)

Unwinding what it means for this element to exist, we see that the
`hcomp`

operation guarantees the
existence of a path
$wβz.$
It is the face that is hinted at by completing the open box above to a
complete square.

double-comp : w β‘ z double-comp i = outS (extensible-at-i1 i)

Note that `hcomp`

gives us the missing face
of the open box, but the semantics guarantees the existence of the box
itself, as an
$n-cube.$
From the De Morgan structure on the interval, we can derive the
existence of the cubes themselves (called **fillers**) from
the existence of the missing faces:

hfill : β {β} {A : Type β} (Ο : I) β I β ((i : I) β Partial (Ο β¨ ~ i) A) β A hfill Ο i u = hcomp (Ο β¨ ~ i) Ξ» where j (Ο = i1) β u (i β§ j) 1=1 j (i = i0) β u i0 1=1 j (j = i0) β u i0 1=1

While every inhabitant of `Type`

has a composition operation, not every *type* (something that can
be on the right of a type signature `e : T`

) does. We call
the types that *do* have a composition operation βfibrantβ, since
these are semantically the cubical sets which are Kan complices.
Examples of types which are *not* fibrant include the interval
`I`

, the partial elements `Partial`

, and the extensions
`_[_β¦_]`

.

Agda also provides a *heterogeneous* version of composition
(which we sometimes call βCCHM compositionβ), called `comp`

. It too has a
corresponding filling operation, called `fill`

. The idea behind CCHM
composition is β by analogy with `hcomp`

expressing that βpaths preserve extensibilityβ β that `PathP`

s preserve extensibility.
Thus we have:

fill : β {β : I β Level} (A : β i β Type (β i)) (Ο : I) (i : I) β (u : β i β Partial (Ο β¨ ~ i) (A i)) β A i fill A Ο i u = comp (Ξ» j β A (i β§ j)) (Ο β¨ ~ i) Ξ» where j (Ο = i1) β u (i β§ j) 1=1 j (i = i0) β u i0 1=1 j (j = i0) β u i0 1=1

Given the inputs to a composition β a family of partial paths
`u`

and a base `u0`

β `hfill`

connects the input of the
composition (`u0`

) and the output. The cubical shape of
iterated identifications causes a slight oddity: The only unbiased
definition of path composition we can give is *double
composition*, which corresponds to the missing face for the square at the start of this
section.

_Β·Β·_Β·Β·_ : β {β} {A : Type β} {w x y z : A} β w β‘ x β x β‘ y β y β‘ z β w β‘ z (p Β·Β· q Β·Β· r) i = hcomp (β i) Ξ» where j (i = i0) β p (~ j) j (i = i1) β r j j (j = i0) β q i

Since it will be useful later, we also give an explicit name for the filler of the double composition square.

Β·Β·-filler : β {β} {A : Type β} {w x y z : A} β (p : w β‘ x) (q : x β‘ y) (r : y β‘ z) β Square (sym p) q (p Β·Β· q Β·Β· r) r Β·Β·-filler p q r i j = hfill (β j) i Ξ» where k (j = i0) β p (~ k) k (j = i1) β r k k (k = i0) β q j

We can define the ordinary, single composition by taking
`p = refl`

, as is done below. The square associated with the
binary composition operation is obtained as the same open box at the
start of the section, the same `double-comp-tube`

, but by
setting any of the faces to be reflexivity. For definiteness, we chose
the left face:

_β_ : β {β} {A : Type β} {x y z : A} β x β‘ y β y β‘ z β x β‘ z p β q = refl Β·Β· p Β·Β· q infixr 30 _β_

The ordinary, βsingle compositeβ of
$p$
and
$q$
is the dashed face in the diagram above. Since we bound `Β·Β·-filler`

above, and defined
`_β_`

in terms of `_Β·Β·_Β·Β·_`

, we can reuse
the latterβs filler to get one for the former:

β-filler : β {β} {A : Type β} {x y z : A} β (p : x β‘ y) (q : y β‘ z) β Square refl p (p β q) q β-filler {x = x} {y} {z} p q = Β·Β·-filler refl p q

The single composition has a filler βin the other directionβ, which
connects
$q$
and
$pβq.$
This is, essentially, because the choice of setting the left face to
`refl`

was completely arbitrary
in the definition of `_β_`

: we could just as
well have gone with setting the *right* face to `refl`

.

β-filler' : β {β} {A : Type β} {x y z : A} β (p : x β‘ y) (q : y β‘ z) β Square (sym p) q (p β q) refl β-filler' {x = x} {y} {z} p q j i = hcomp (β i β¨ ~ j) Ξ» where k (i = i0) β p (~ j) k (i = i1) β q k k (j = i0) β q (i β§ k) k (k = i0) β p (i β¨ ~ j)

We can use the filler and heterogeneous composition to define
composition of `PathP`

s and `Square`

s:

_βP_ : β {β β'} {A : Type β} {B : A β Type β'} {x y z : A} {x' : B x} {y' : B y} {z' : B z} {p : x β‘ y} {q : y β‘ z} β PathP (Ξ» i β B (p i)) x' y' β PathP (Ξ» i β B (q i)) y' z' β PathP (Ξ» i β B ((p β q) i)) x' z' _βP_ {B = B} {x' = x'} {p = p} {q = q} p' q' i = comp (Ξ» j β B (β-filler p q j i)) (β i) Ξ» where j (i = i0) β x' j (i = i1) β q' j j (j = i0) β p' i _ββ_ : β {β} {A : Type β} {a00 a01 a02 a10 a11 a12 : A} {p : a00 β‘ a01} {p' : a01 β‘ a02} {q : a00 β‘ a10} {s : a01 β‘ a11} {t : a02 β‘ a12} {r : a10 β‘ a11} {r' : a11 β‘ a12} β Square p q s r β Square p' s t r' β Square (p β p') q t (r β r') (Ξ± ββ Ξ²) i j = ((Ξ» i β Ξ± i j) β (Ξ» i β Ξ² i j)) i infixr 30 _βP_ _ββ_

## Uniquenessπ

A common characteristic of *geometric* interpretations of
higher categories β like the one we have here β when compared to
algebraic definitions is that there is no prescription in general for
how to find composites of morphisms. Instead, we have that each triple
of morphism has a *contractible space* of composites. We call the
proof of this fact `Β·Β·-unique`

:

Β·Β·-unique : β {β} {A : Type β} {w x y z : A} β (p : w β‘ x) (q : x β‘ y) (r : y β‘ z) β (Ξ± Ξ² : Ξ£[ s β (w β‘ z) ] Square (sym p) q s r) β Ξ± β‘ Ξ²

Note that the type of `Ξ±`

and `Ξ²`

asks for a
path `w β‘ z`

which *specifically* completes the open
box for double composition. We would not in general expect that
`w β‘ z`

is contractible for an arbitrary `a`

! Note
that the proof of this involves filling a cube in a context that
*already* has an interval variable in scope - a hypercube!

Β·Β·-unique {w = w} {x} {y} {z} p q r (Ξ± , Ξ±-fill) (Ξ² , Ξ²-fill) = Ξ» i β (Ξ» j β square i j) , (Ξ» j k β cube i j k) where cube : (i j : I) β p (~ j) β‘ r j cube i j k = hfill (β i β¨ β k) j Ξ» where l (i = i0) β Ξ±-fill l k l (i = i1) β Ξ²-fill l k l (k = i0) β p (~ l) l (k = i1) β r l l (l = i0) β q k square : Ξ± β‘ Ξ² square i j = cube i i1 j

The term `cube`

above has the following cube as a
boundary. Since it is a filler, there is a missing face at the bottom
which has no name, so we denote it by `hcomp...`

in the
diagram.

This diagram is quite busy because it is a 3D commutative diagram, but it could be busier: all of the unimportant edges were not annotated. By the way, the lavender face (including the lavender $pΒΒ¬j)$ is the $k=i0$ face, and the red face is the $k=i1$ face.

However, even though the diagram is very busy, most of the detail it
contains can be ignored. Reading it in the left-right direction, it
expresses an identification between `Ξ±-filler j k`

and
`Ξ²-filler j k`

, lying over a homotopy `Ξ± = Ξ²`

.
That homotopy is what you get when you read the bottom square of the
diagram in the left-right direction. Explicitly, here is that bottom
square:

Note that, exceptionally, this diagram is drawn with the left/right edges going up rather than down. This is to match the direction of the 3D diagram above. The colours are also matching.

Readers who are already familiar with the notion of h-level will have
noticed that the proof `Β·Β·-unique`

expresses that the
type of double composites `p Β·Β· q Β·Β· r`

is a
*proposition*, not that it is contractible. However, since it is
inhabited (by `_Β·Β·_Β·Β·_`

and its
filler), it is contractible:

Β·Β·-contract : β {β} {A : Type β} {w x y z : A} β (p : w β‘ x) (q : x β‘ y) (r : y β‘ z) β (Ξ² : Ξ£[ s β (w β‘ z) ] Square (sym p) q s r) β (p Β·Β· q Β·Β· r , Β·Β·-filler p q r) β‘ Ξ² Β·Β·-contract p q r Ξ² = Β·Β·-unique p q r _ Ξ²

β-unique : β {β} {A : Type β} {x y z : A} {p : x β‘ y} {q : y β‘ z} β (r : x β‘ z) β Square refl p r q β r β‘ p β q β-unique {p = p} {q} r square i = Β·Β·-unique refl p q (_ , square) (_ , (β-filler p q)) i .fst Β·Β·-unique' : β {β} {A : Type β} {w x y z : A} β {p : w β‘ x} {q : x β‘ y} {r : y β‘ z} {s : w β‘ z} β (Ξ² : Square (sym p) q s r) β s β‘ p Β·Β· q Β·Β· r Β·Β·-unique' Ξ² i = Β·Β·-contract _ _ _ (_ , Ξ²) (~ i) .fst

# Functorial actionπ

This composition structure on paths makes every type into an $β-groupoid,$ which is discussed in a different module.

It is then reasonable to expect that every function behave like a
funct**or**, in that it has an action on objects (the
actual computational content of the function) and an action on
*morphisms* β how that function acts on paths. Reading paths as
identity, this is a proof that functions take identical inputs to
identical outputs.

ap : β {a b} {A : Type a} {B : A β Type b} (f : (x : A) β B x) {x y : A} β (p : x β‘ y) β PathP (Ξ» i β B (p i)) (f x) (f y) ap f p i = f (p i) {-# NOINLINE ap #-}

The following function expresses the same thing as `ap`

, but for binary functions.
The type is huge! Thatβs because it applies to the most general type of
2-argument dependent function possible:
`(x : A) (y : B x) β C x y`

. Even then, the proof is
beautifully short:

apβ : β {a b c} {A : Type a} {B : A β Type b} {C : (x : A) β B x β Type c} (f : (x : A) (y : B x) β C x y) {x y : A} {Ξ± : B x} {Ξ² : B y} β (p : x β‘ y) β (q : PathP (Ξ» i β B (p i)) Ξ± Ξ²) β PathP (Ξ» i β C (p i) (q i)) (f x Ξ±) (f y Ξ²) apβ f p q i = f (p i) (q i)

apd : β {a b} {A : I β Type a} {B : (i : I) β A i β Type b} β (f : (i : I) β (a : A i) β B i a) β {x : A i0} β {y : A i1} β (p : PathP A x y) β PathP (Ξ» i β B i (p i)) (f i0 x) (f i1 y) apd f p i = f i (p i) ap-square : β {β β'} {A : Type β} {B : A β Type β'} {a00 a01 a10 a11 : A} {p : a00 β‘ a01} {q : a00 β‘ a10} {s : a01 β‘ a11} {r : a10 β‘ a11} β (f : (a : A) β B a) β (Ξ± : Square p q s r) β SquareP (Ξ» i j β B (Ξ± i j)) (ap f p) (ap f q) (ap f s) (ap f r) ap-square f Ξ± i j = f (Ξ± i j)

This operation satisfies many identities definitionally that are only
propositional when `ap`

is defined in terms of `J`

. For instance:

module _ where private variable β : Level A B C : Type β f : A β B g : B β C ap-β : {x y : A} {p : x β‘ y} β ap (Ξ» x β g (f x)) p β‘ ap g (ap f p) ap-β = refl ap-id : {x y : A} {p : x β‘ y} β ap (Ξ» x β x) p β‘ p ap-id = refl ap-sym : {x y : A} {p : x β‘ y} β sym (ap f p) β‘ ap f (sym p) ap-sym = refl ap-refl : {x : A} β ap f (Ξ» i β x) β‘ (Ξ» i β f x) ap-refl = refl

The last lemma, that `ap`

respects composition of
*paths*, can be proven by uniqueness: both
`ap f (p β q)`

and `ap f p β ap f q`

are valid
βlidsβ for the open box with sides `refl`

,
`ap f p`

and `ap f q`

, so they must be equal:

ap-Β·Β· : (f : A β B) {x y z w : A} (p : x β‘ y) (q : y β‘ z) (r : z β‘ w) β ap f (p Β·Β· q Β·Β· r) β‘ ap f p Β·Β· ap f q Β·Β· ap f r ap-Β·Β· f p q r = Β·Β·-unique' (ap-square f (Β·Β·-filler p q r)) ap-β : (f : A β B) {x y z : A} (p : x β‘ y) (q : y β‘ z) β ap f (p β q) β‘ ap f p β ap f q ap-β f p q = ap-Β·Β· f refl p q

# Syntax sugarπ

When constructing long chains of identifications, itβs rather helpful
to be able to visualise *what* is being identified with more
βpriorityβ than *how* it is being identified. For this, a handful
of combinators with weird names are defined:

β‘β¨β©-syntax : β {β} {A : Type β} (x : A) {y z} β y β‘ z β x β‘ y β x β‘ z β‘β¨β©-syntax x q p = p β q β‘β¨β©β‘β¨β©-syntax : β {β} {A : Type β} (w x : A) {y z} β (p : w β‘ x) β (q : x β‘ y) β (r : y β‘ z) β w β‘ z β‘β¨β©β‘β¨β©-syntax w x p q r = p Β·Β· q Β·Β· r infixr 2 β‘β¨β©-syntax syntax β‘β¨β©-syntax x q p = x β‘β¨ p β© q _β‘Λβ¨_β©_ : β {β} {A : Type β} (x : A) {y z : A} β y β‘ x β y β‘ z β x β‘ z x β‘Λβ¨ p β©β‘Λ q = (sym p) β q _β‘β¨β©_ : β {β} {A : Type β} (x : A) {y : A} β x β‘ y β x β‘ y x β‘β¨β© xβ‘y = xβ‘y _β : β {β} {A : Type β} (x : A) β x β‘ x x β = refl infixr 2 _β‘β¨β©_ _β‘Λβ¨_β©_ infix 3 _β along : β {β} {A : I β Type β} {x : A i0} {y : A i1} β (i : I) β PathP A x y β A i along i p = p i

These functions are used to make *equational reasoning
chains*. For instance, the following proof that addition of naturals
is associative is done in equational reasoning style:

private +-associative : (x y z : Nat) β x + (y + z) β‘ (x + y) + z +-associative zero y z = refl +-associative (suc x) y z = suc (x + (y + z)) β‘β¨ ap suc (+-associative x y z) β©β‘ suc ((x + y) + z) β

If your browser runs JavaScript, these equational reasoning chains,
by default, render with the *justifications* (the argument
written between `β¨ β©`

) hidden; There is a checkbox to display
them, either on the sidebar or on the top bar depending on how narrow
your screen is. For your convenience, itβs here too:

Try pressing it!

# Dependent pathsπ

Surprisingly often, we want to compare inhabitants
$a:A$
and
$b:B$
where the types
$A$
and
$B$
are not *definitionally* equal, but only identified in some
specified way. We call these β**paths** over
**p**pathsβ, or `PathP`

for short. In the same
way that a `Path`

can be understood as a
function `I β A`

with specified endpoints, a `PathP`

(*path* over
*p*ath) can be understood as a *dependent* function
`(i : I) β A i`

.

In the Book, paths over paths are implemented in terms of the `transport`

operation: A path
`x β‘ y`

over `p`

is a path
`transport p x β‘ y`

, thus defining dependent identifications
using non-dependent ones. Fortunately, a cubical argument shows us that
these notions coincide:

PathPβ‘Path : β {β} (P : I β Type β) (p : P i0) (q : P i1) β PathP P p q β‘ Path (P i1) (transport (Ξ» i β P i) p) q PathPβ‘Path P p q i = PathP (Ξ» j β P (i β¨ j)) (transport-filler (Ξ» j β P j) p i) q PathPβ‘Pathβ» : β {β} (P : I β Type β) (p : P i0) (q : P i1) β PathP P p q β‘ Path (P i0) p (transport (Ξ» i β P (~ i)) q) PathPβ‘Pathβ» P p q i = PathP (Ξ» j β P (~ i β§ j)) p (transport-filler (Ξ» j β P (~ j)) q i)

We can see this by substituting either `i0`

or
`i1`

for the variable `i`

.

When

`i = i0`

, we have`PathP (Ξ» j β P j) p q`

, by the endpoint rule for`transport-filler`

.When

`i = i1`

, we have`PathP (Ξ» j β P i1) (transport P p) q`

, again by the endpoint rule for`transport-filler`

.

The existence of paths over paths gives another βcounterexampleβ to
thinking of paths as *equality*. For instance, itβs hard to
imagine a world in which `true`

and `false`

can be
equal in any interesting sense of the word *equal* β but over the
identification
$Boolβ‘Bool$
that switches the points around, `true`

and
`false`

can be identified!

## Squeezing and spreadingπ

Using the De Morgan algebra structure on the interval, together with
the
β$Ο$β
argument to `transp`

, we can implement
operations that move a point between the concrete endpoints (i0, i1) and
arbitrary points on the interval, represented as variables. First, we
introduce the following names for transporting forwards and backwards
along a path.

coe0β1 : β {β} (A : I β Type β) β A i0 β A i1 coe0β1 A a = transp (Ξ» i β A i) i0 a coe1β0 : β {β} (A : I β Type β) β A i1 β A i0 coe1β0 A a = transp (Ξ» i β A (~ i)) i0 a

These two operations will βspreadβ a value which is concentrated at one of the endpoints to cover the entire path. They are named after their type: they move a value from i0/i1 to an arbitrary $i.$

coe0βi : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i0 β A i coe0βi A i a = transp (Ξ» j β A (i β§ j)) (~ i) a coe1βi : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i1 β A i coe1βi A i a = transp (Ξ» j β A (i β¨ ~ j)) i a

In the converse direction, we have βsqueezeβ operations, which take a value from $A(i)$ to $A(i0)$ or $A(i1).$

coeiβ0 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i0 coeiβ0 A i a = transp (Ξ» j β A (i β§ ~ j)) (~ i) a coeiβ1 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i1 coeiβ1 A i a = transp (Ξ» l β A (i β¨ l)) i a

Using squeezes and spreads, we can define maps that convert between
`PathP`

s and βbook-styleβ
dependent paths. These conversions could also be defined in terms of
`PathPβ‘Path`

, but the following
definitions are more efficient.

module _ {β} {A : I β Type β} {x : A i0} {y : A i1} where to-pathp : coe0β1 A x β‘ y β PathP A x y to-pathp p i = hcomp (β i) Ξ» where j (j = i0) β coe0βi A i x j (i = i0) β x j (i = i1) β p j from-pathp : PathP A x y β coe0β1 A x β‘ y from-pathp p i = transp (Ξ» j β A (i β¨ j)) i (p i)

Note that by composing the functions `to-pathp`

and `to-pathp`

with the reversal on
the interval, we obtain a correspondence `PathP`

and paths with a
backwards transport on the right-hand side.

module _ {β} {A : I β Type β} {x : A i0} {y : A i1} where to-pathpβ» : x β‘ coe1β0 A y β PathP A x y to-pathpβ» p = symP $ to-pathp {A = Ξ» j β A (~ j)} (Ξ» i β p (~ i)) from-pathpβ» : PathP A x y β x β‘ coe1β0 A y from-pathpβ» p = sym $ from-pathp (Ξ» i β p (~ i))

Itβs actually fairly complicated to show that the functions `to-pathp`

and `from-pathp`

are inverses. The
statements of the theorems are simple:

to-from-pathp : β {β} {A : I β Type β} {x y} (p : PathP A x y) β to-pathp (from-pathp p) β‘ p from-to-pathp : β {β} {A : I β Type β} {x y} (p : coe0β1 A x β‘ y) β from-pathp {A = A} (to-pathp p) β‘ p

hcomp-unique : β {β} {A : Type β} Ο (u : β i β Partial (Ο β¨ ~ i) A) β (h2 : β i β A [ _ β¦ (Ξ» { (i = i0) β u i0 1=1 ; (Ο = i1) β u i 1=1 }) ]) β hcomp Ο u β‘ outS (h2 i1) hcomp-unique Ο u h2 i = hcomp (Ο β¨ i) Ξ» where k (k = i0) β u i0 1=1 k (i = i1) β outS (h2 k) k (Ο = i1) β u k 1=1

##
The proof is a bit hairy, since it involves very high-dimensional
hcomps. We leave it under this fold for the curious reader, but we
encourage you to take `to-from-pathp`

and `from-to-pathp`

on faith
otherwise.

to-from-pathp {A = A} {x} {y} p i j = hcomp-unique (β j) (Ξ» { k (k = i0) β coe0βi A j x ; k (j = i0) β x ; k (j = i1) β coeiβ1 A k (p k) }) (Ξ» k β inS (transp (Ξ» l β A (j β§ (k β¨ l))) (~ j β¨ k) (p (j β§ k)))) i from-to-pathp {A = A} {x} {y} p i j = hcomp (β i β¨ β j) Ξ» where k (k = i0) β coeiβ1 A (j β¨ ~ i) $ transp (Ξ» l β A (j β¨ (~ i β§ l))) (i β¨ j) $ coe0βi A j x k (j = i0) β slide (k β¨ ~ i) k (j = i1) β p k k (i = i0) β coeiβ1 A j $ hfill (β j) k Ξ» where k (k = i0) β coe0βi A j x k (j = i0) β x k (j = i1) β p k k (i = i1) β hcomp (β k β¨ β j) Ξ» where l (l = i0) β slide (k β¨ j) l (k = i0) β slide j l (k = i1) β p (j β§ l) l (j = i0) β slide k l (j = i1) β p (k β§ l) where slide : coe0β1 A x β‘ coe0β1 A x slide i = coeiβ1 A i (coe0βi A i x)

# Path spacesπ

A large part of the study of HoTT is the *characterisation of path
spaces*. Given a type `A`

, what does
`Path A x y`

look like? Hedbergβs theorem says that for
types with decidable equality, itβs boring. For the circle, we can prove its loop
space is the integers β we have
`Path SΒΉ base base β‘ Int`

.

Most of these characterisations need machinery that is not in this module to be properly stated. Even then, we can begin to outline a few simple cases:

## Ξ£ typesπ

For `Ξ£`

types, a path between
`(a , b) β‘ (x , y)`

consists of a path
`p : a β‘ x`

, and a path between `b`

and
`y`

laying over `p`

.

Ξ£-pathp : β {β β'} {A : I β Type β} {B : β i β A i β Type β'} β {x : Ξ£ _ (B i0)} {y : Ξ£ _ (B i1)} β (p : PathP A (x .fst) (y .fst)) β PathP (Ξ» i β B i (p i)) (x .snd) (y .snd) β PathP (Ξ» i β Ξ£ (A i) (B i)) x y Ξ£-pathp p q i = p i , q i

We can also use the book characterisation of dependent paths, which
is simpler in the case where the `Ξ£`

represents a subset β i.e., `B`

is a family of
propositions.

Ξ£-path : β {a b} {A : Type a} {B : A β Type b} β {x y : Ξ£ A B} β (p : x .fst β‘ y .fst) β subst B p (x .snd) β‘ (y .snd) β x β‘ y Ξ£-path {A = A} {B} {x} {y} p q = Ξ£-pathp p (to-pathp q)

## Ξ typesπ

For dependent functions, the paths are *homotopies*, in the
topological sense: `Path ((x : A) β B x) f g`

is the same
thing as a function `I β (x : A) β B x`

β which we could turn
into a product if we really wanted to.

happly : β {a b} {A : Type a} {B : A β Type b} {f g : (x : A) β B x} β f β‘ g β (x : A) β f x β‘ g x happly p x i = p i x

With this, we have made definitional yet another principle which is
propositional in the HoTT book: *function extensionality*.
Functions are identical precisely if they assign the same outputs to
every input.

funext : β {a b} {A : Type a} {B : A β Type b} {f g : (x : A) β B x} β ((x : A) β f x β‘ g x) β f β‘ g funext p i x = p x i

Furthermore, we know (since types are groupoids, and functions are functors) that, by analogy with 1-category theory, paths in a function type should behave like natural transformations (because they are arrows in a functor category). This is indeed the case:

homotopy-natural : β {a b} {A : Type a} {B : Type b} β {f g : A β B} β (H : (x : A) β f x β‘ g x) β {x y : A} (p : x β‘ y) β H x β ap g p β‘ ap f p β H y homotopy-natural {f = f} {g = g} H {x} {y} p = β-unique _ Ξ» i j β hcomp (~ i β¨ β j) Ξ» where k (k = i0) β H x (j β§ i) k (i = i0) β f (p (j β§ k)) k (j = i0) β f x k (j = i1) β H (p k) i

## Pathsπ

The groupoid structure of *paths* is also interesting. While
the characterisation of `Path (Path A x y) p q`

is
fundamentally tied to the characterisation of `A`

, there are
general theorems that can be proven about *transport* in path
spaces. For example, transporting both endpoints of a path is equivalent
to a ternary composition:

double-composite : β {β} {A : Type β} β {x y z w : A} β (p : x β‘ y) (q : y β‘ z) (r : z β‘ w) β p Β·Β· q Β·Β· r β‘ p β q β r double-composite p q r i j = hcomp (i β¨ β j) Ξ» where k (i = i1) β β-filler' p (q β r) k j k (j = i0) β p (~ k) k (j = i1) β r (i β¨ k) k (k = i0) β β-filler q r i j

transport-path : β {β} {A : Type β} {x y x' y' : A} β (p : x β‘ y) β (left : x β‘ x') β (right : y β‘ y') β transport (Ξ» i β left i β‘ right i) p β‘ sym left β p β right transport-path {A = A} {x} {y} {x'} {y'} p left right = lemma β double-composite _ _ _

The argument is slightly indirect. First, we have a proof (omitted for space) that composing three paths using binary composition (twice) is the same path as composing them in one go, using the (ternary) double composition operation. This is used in a second step, as a slight endpoint correction.

The first step, the lemma below, characterises transport in path
spaces in terms of the double composite: This is *almost*
definitional, but since Cubical Agda implements only composition
**for PathP**, we need to adjust the path by a
bunch of transports:

where lemma : _ β‘ (sym left Β·Β· p Β·Β· right) lemma i j = hcomp (~ i β¨ β j) Ξ» where k (k = i0) β transp (Ξ» j β A) i (p j) k (i = i0) β hfill (β j) k Ξ» where k (k = i0) β transp (Ξ» i β A) i0 (p j) k (j = i0) β transp (Ξ» j β A) k (left k) k (j = i1) β transp (Ξ» j β A) k (right k) k (j = i0) β transp (Ξ» j β A) (k β¨ i) (left k) k (j = i1) β transp (Ξ» j β A) (k β¨ i) (right k)

Special cases can be proven about substitution. For example, if we hold the right endpoint constant, we get something homotopic to composing with the inverse of the adjustment path:

subst-path-left : β {β} {A : Type β} {x y x' : A} β (p : x β‘ y) β (left : x β‘ x') β subst (Ξ» e β e β‘ y) left p β‘ sym left β p subst-path-left {y = y} p left = subst (Ξ» e β e β‘ y) left p β‘β¨β© transport (Ξ» i β left i β‘ y) p β‘β¨ transport-path p left refl β©β‘ sym left β p β refl β‘β¨ ap (sym left β_) (sym (β-filler _ _)) β©β‘ sym left β p β

If we hold the left endpoint constant instead, we get a respelling of composition:

subst-path-right : β {β} {A : Type β} {x y y' : A} β (p : x β‘ y) β (right : y β‘ y') β subst (Ξ» e β x β‘ e) right p β‘ p β right subst-path-right {x = x} p right = subst (Ξ» e β x β‘ e) right p β‘β¨β© transport (Ξ» i β x β‘ right i) p β‘β¨ transport-path p refl right β©β‘ sym refl β p β right β‘β¨β© refl β p β right β‘β¨ sym (β-filler' _ _) β©β‘ p β right β

Finally, we can apply the same path to both endpoints:

subst-path-both : β {β} {A : Type β} {x x' : A} β (p : x β‘ x) β (adj : x β‘ x') β subst (Ξ» x β x β‘ x) adj p β‘ sym adj β p β adj subst-path-both p adj = transport-path p adj adj

_β_ : β {β} {A : I β Type β} {aβ aβ' : A i0} {aβ : A i1} β aβ β‘ aβ' β PathP A aβ' aβ β PathP A aβ aβ (p β q) i = hcomp (β i) Ξ» where j (i = i0) β p (~ j) j (i = i1) β q i1 j (j = i0) β q i _β·_ : β {β} {A : I β Type β} {aβ : A i0} {aβ aβ' : A i1} β PathP A aβ aβ β aβ β‘ aβ' β PathP A aβ aβ' (p β· q) i = hcomp (β i) Ξ» where j (i = i0) β p i0 j (i = i1) β q j j (j = i0) β p i infixr 31 _β_ infixl 32 _β·_ Squareβ‘double-composite-path : β {β} {A : Type β} β {w x y z : A} β {p : x β‘ w} {q : x β‘ y} {s : w β‘ z} {r : y β‘ z} β Square p q s r β‘ (sym p Β·Β· q Β·Β· r β‘ s) Squareβ‘double-composite-path {p = p} {q} {s} {r} k = PathP (Ξ» i β p (i β¨ k) β‘ r (i β¨ k)) (Β·Β·-filler (sym p) q r k) s J' : β {ββ ββ} {A : Type ββ} (P : (x y : A) β x β‘ y β Type ββ) β (β x β P x x refl) β {x y : A} (p : x β‘ y) β P x y p J' P prefl {x} p = transport (Ξ» i β P x (p i) Ξ» j β p (i β§ j)) (prefl x) Jβ : β {βa βb βp} {A : Type βa} {B : Type βb} {xa : A} {xb : B} β (P : β ya yb β xa β‘ ya β xb β‘ yb β Type βp) β P xa xb refl refl β β {ya yb} p q β P ya yb p q Jβ P prr p q = transport (Ξ» i β P (p i) (q i) (Ξ» j β p (i β§ j)) (Ξ» j β q (i β§ j))) prr invert-sides : β {β} {A : Type β} {x y z : A} (p : x β‘ y) (q : x β‘ z) β Square q p (sym q) (sym p) invert-sides {x = x} p q i j = hcomp (β i β¨ β j) Ξ» where k (i = i0) β p (k β§ j) k (i = i1) β q (~ j β§ k) k (j = i0) β q (i β§ k) k (j = i1) β p (~ i β§ k) k (k = i0) β x sym-β-filler : β {β} {A : Type β} {x y z : A} (p : x β‘ y) (q : y β‘ z) β I β I β I β A sym-β-filler {A = A} {z = z} p q i j k = hfill (β i) k Ξ» where l (i = i0) β q (l β¨ j) l (i = i1) β p (~ l β§ j) l (l = i0) β invert-sides q (sym p) i j sym-β : β {β} {A : Type β} {x y z : A} (p : x β‘ y) (q : y β‘ z) β sym (p β q) β‘ sym q β sym p sym-β p q i j = sym-β-filler p q j i i1 infixl 45 _$β_ _$β_ : β {ββ ββ} {A : Type ββ} {B : A β Type ββ} {f g : β x β B x} β f β‘ g β β x β f x β‘ g x (f $β x) i = f i x {-# INLINE _$β_ #-}

The distinction between these two is elaborated on in the Intro to HoTT page.β©οΈ

For the semantically inclined, these correspond to face inclusions (including the inclusions of endpoints into a line) being monomorphisms, and thus

*cofibrations*in the model structure on cubical sets.β©οΈSince

`I`

is not Kan (that is β it does not have a*composition*structure), it is not an inhabitant of the βfibrant universeβ`Type`

. Instead it lives in`SSet`

, or, in Agda 2.6.3, its own universe β`IUniv`

.β©οΈI (AmΓ©lia) wrote a blog post explaining the semantics of them in a lot of depth.β©οΈ

`Sub`

lives in the universe`SSetΟ`

, which we do not have a binding for, so we can not name the type of`_[_β¦_]`

.β©οΈAlthough it is not proven to be a contradiction in

*this*module, see Data.Bool for that construction.β©οΈ