open import 1Lab.Type 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*.

##
**Aside**: 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 \equiv 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 \land \id{i0} = \id{i0}$, $x \land \id{i1} = x$
- $x \lor \id{i0} = x$, $x \lor \id{i1} = \id{i1}$
- $\neg(x \land y) = \neg x \lor \neg y$
- $\neg\id{i0} = \id{i1}$, $\neg\id{i1} = \id{i0}$, $\neg\neg x = x$
- $\land$ and $\lor$ are both associative, commutative and idempotent, and distribute over eachother.

Note that, in the formalisation,
$\neg 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 $\land$ and $\lor$ 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

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)

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

# 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

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

# 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 \equiv x$,
$q : x \equiv y$,
and
$r : y \equiv 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 \equiv x$,
$x \equiv y$,
and
$y \equiv z$.
Note that in the left face of the diagram, the path was inverted; This
is because while we have a path
$w \equiv x$,
we need a path
$x \equiv 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 \equiv 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 \equiv 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*
$\varphi$,
and a *type*
$A$.
The idea is that a term of type
$\id{Partial}\ \varphi\ A$
in a context with
$n$
I-typed variables is a
$n$-cube
that is only defined when
$\varphi$
β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
$\neg i \lor i$.
Note that this is not the same thing as i1! Since elements of
`I`

are meant to represent real numbers
$r \in [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 a 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 : \id{Partial}\ \varphi\ A$.
We could represent this very generically as a *lifting problem*,
i.e.Β trying to find a map
$\square^n$
which agrees with
$e$
when restricted to
$\varphi$,
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
$\varphi$.
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 \lor 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
$\partial i \lor \neg 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 $\phi$ and a partial element $u$ defined along $\phi \lor \neg j$ (for $j$ disjoint from $\phi$; we call it the βdirection of compositionβ, sometimes), then we can extend it to a totally-defined element, which agrees with $u$ along $\phi$.

The idea is that the $\neg j$, being in some sense βorthogonal toβ the dimensions in $\phi$, will βconnectβ the tube given by $\phi$. This is a slight generalization of the classical Kan condition, which would insist $\phi = \bigvee_i \partial 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 \to 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

**Note**: While every inhabitant of Type has a composition operation, not every
*type* (something that can be on the right of 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
`_[_β¦_]`

^{7}.

Definition: A type isfibrantif it supports hcomp. This word comes up a lot when discussing not only the semantics of Cubical type theory, but also its practice! For instance, the fibrancy of Type is what powers univalence.

Agda also provides a *heterogeneous* version of composition
(sometimes referred to as β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 PathPs 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

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 \bullet 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)

## 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\ \neg j$) is the $k = \id{i0}$ face, and the red face is the $k = \id{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 _ Ξ²

# Functorial Actionπ

This composition structure on paths makes every type into an $\infty$-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)

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-comp : {x y : A} {p : x β‘ y} β ap (Ξ» x β g (f x)) p β‘ ap g (ap f p) ap-comp = 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-comp-path : (f : A β B) {x y z : A} (p : x β‘ y) (q : y β‘ z) β ap f (p β q) β‘ ap f p β ap f q ap-comp-path f p q i = Β·Β·-unique refl (ap f p) (ap f q) (ap f (p β q) , Ξ» k j β f (β-filler p q k j)) (ap f p β ap f q , β-filler _ _) i .fst

# 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 30 _β_ 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
$\id{Bool} \equiv \id{Bool}$
that switches the points around, `true`

and
`false`

can be identified!

## Coercionπ

In Cubical Agda, the interval is given the structure of a De Morgan
algebra. This is not the only choice of structure on the interval that
gives a model of univalent type theory: We could also subject the
interval to *no* additional structure other than what comes from
the structural rules of type theory (introducing variables, ignoring
variables, swapping variables, etc). This is a different cubical type
theory, called *Cartesian cubical type theory*.

In Cartesian cubical type theory, instead of having a transp operation which takes
$A(\id{i0}) \to A(\id{i1})$,
there is a βmore powerfulβ *coercion* operation, written
$\id{coe}^A_{i \to j}$,
which takes
$A(i) \to A(j)$,
as in the subscript. However, despite the seeming added power, the
coercion operation can be implemented in Cubical Agda: First, we
introduce alternative names for several uses of transp.

coe0β1 : β {β} (A : I β Type β) β A i0 β A i1 coe0β1 A a = transp (Ξ» i β A i) i0 a -- ^ This is another name for transport coe1β0 : β {β} (A : I β Type β) β A i1 β A i0 coe1β0 A a = transp (Ξ» i β A (~ i)) i0 a -- ^ This is equivalent to transport β sym

There are also βmore excitingβ operations, which transport from one of the endpoints to a path which can vary over the interval. These generalise the transport-filler operation.

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

We visualise coe0βi and coe1βi as being
βspreadβ operations, since they take a value from one endpoint of the
interval (0 or 1, respectively) and βspread itβ to a line varying over
the variable `i`

. Similarly, we have βsqueezeβ operations,
which take a line varying over `i`

to one of the
endpoints:

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

Using the filler of a square, we can put together the
`0βi`

and `1βi`

coercions to get the βmaster
coercionβ operation. That square is drawn as the diagram below, where
the edges are more important than the corners, and the dashed line is
`coe A i i1`

.

coe : β {β : I β Level} (A : β i β Type (β i)) (i j : I) β A i β A j coe A i j a = fill A (β i) j Ξ» where j (i = i0) β coe0βi A j a j (i = i1) β coe1βi A j a j (j = i0) β coeiβ0 A i a

As the square implies, when `j = i1`

, we have the squeeze
operation opposite to coeiβ0, which we call coeiβ1.

coeiβ1 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i1 coeiβ1 A i a = coe A i i1 a

**Sidenote**: The boundary for the square implies that
we can give a more verbose type for coe, one which
mentions all of the spreads and squeezes. Note that this is a
*dependent path between functions
$A\ i \to A\ j$*,
a very complicated construction indeed!

private coe-verbose : β {β} (A : I β Type β) β PathP (Ξ» i β PathP (Ξ» j β A i β A j) (coeiβ0 A i) (coeiβ1 A i)) (Ξ» j β coe0βi A j) (Ξ» j β coe1βi A j) coe-verbose A i j = coe A i j

This operation satisfies, *definitionally*, a whole host of
equations. For starters, we have that the
$\id{coe}^A_{i\to1}$
(resp
$i \to 0$)
specialises to transport when
$i = 0$
(resp.
$i = 1$),
and to the identity when
$i = 1$
(resp.
$i = 0$):

coei0β1 : β {β} (A : I β Type β) (a : A i0) β coeiβ1 A i0 a β‘ coe0β1 A a coei0β1 A a = refl coei1β1 : β {β} (A : I β Type β) (a : A i1) β coeiβ1 A i1 a β‘ a coei1β1 A a = refl coei1β0 : β {β} (A : I β Type β) (a : A i1) β coeiβ0 A i1 a β‘ coe1β0 A a coei1β0 A a = refl coei0β0 : β {β} (A : I β Type β) (a : A i0) β coeiβ0 A i0 a β‘ a coei0β0 A a = refl

Then we have paths connecting the βmaster coercionβ coe and its several faces:

coeiβi0 : β {β} (A : I β Type β) (i : I) (a : A i) β coe A i i0 a β‘ coeiβ0 A i a coeiβi0 A i a = refl coei0βi : β {β} (A : I β Type β) (i : I) (a : A i0) β coe A i0 i a β‘ coe0βi A i a coei0βi A i a = refl coeiβi1 : β {β} (A : I β Type β) (i : I) (a : A i) β coe A i i1 a β‘ coeiβ1 A i a coeiβi1 A i a = refl coei1βi : β {β} (A : I β Type β) (i : I) (a : A i1) β coe A i1 i a β‘ coe1βi A i a coei1βi A i a = refl

In Cartesian cubical type theory, the following equation is definitional. It says that the top right and bottom left corners of the diagram are indeed what I said they were! However, in Cubical Agda, it is only propositional:

coeiβi : β {β} (A : I β Type β) (i : I) (a : A i) β coe A i i a β‘ a coeiβi A i = coe0βi (Ξ» i β (a : A i) β coe A i i a β‘ a) i (Ξ» _ β refl)

Using the Cartesian coercions, we define maps that convert between PathPs and Book dependent paths. These maps could also be defined in terms of transp and PathPβ‘Path, but this definition is more efficient.

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

These definitions illustrate how using the named squeezes and spreads β coe0βi, coeiβ1 β can be a lot more elegant than trying to work out what particular connection soup to use in a transp.

# 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 b} {A : Type a} {B : A β Type b} β {x y : Ξ£ A B} β (p : x .fst β‘ y .fst) β PathP (Ξ» i β B (p i)) (x .snd) (y .snd) β 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 (i = i1) β β-filler (H x) (ap g p) k j 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:

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

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.β©οΈIn Agda 2.6.2, function types

`I β A`

are*not*fibrant, even though they correspond to paths with βunmarkedβ endpoints. In Agda 2.6.3 (in development at the time of writing),`I`

was moved to its own universe,`IUniv`

, with a typing rule for functions saying that`A β B`

is fibrant whenever`B : Type`

and`A : Type`

*or*`A : IUniv`

- i.e. function types`I β A`

were made fibrant whenever`A`

is.β©οΈ