module 1Lab.Path where

open Prim.Extension public open Prim.Interval public open Prim.Kan public -- Slightly ugly type to demonstrate the algebraic properties of the -- interval. private data _β‘β±_ (i : I) : (j : I) β SSet where reflβ± : i β‘β± i infix 10 _β‘β±_ variable β : Level A B : Type β f g : A β B x y : A

# Paths and the intervalπ

One of the key observations behind HoTT is that the inductive *identity
type* can be given a *spatial* interpretation: if we
interpret a type
$A$
as a space, then for a pair of points
$a,b:A,$
the identity type
$aβ‘b$
behaves like the space of *paths* from
$a$
to
$b$
in
$A.$
There is a constant path
$refl:aβ‘a$
at each point; every path
$p:aβ‘b$
has an inverse
$p_{β1}:bβ‘a;$
paths
$p:aβ‘b$
and
$q:bβ‘c$
can be laid end-to-end, giving the composite
$pβq:aβ‘c.$
Even further, these operations can be shown to satisfy algebraic laws,
like the inverse law
$p_{β1}βpβ‘refl,$
but only up to paths-between-paths: *homotopies*.

In the homotopy theory of topological spaces, paths in a space
$A$
are defined to be continuous mappings
$f:[0,1]βA$
from the *interval* to our space. The key idea behind cubical
type theory, and thus our implementation Cubical Agda, is that by
axiomatizing the important properties of
$[0,1]$
as an **interval type**
$I,$
we could similarly define *paths* to be functions
$IβA.$
We donβt have to cut down to a type of βcontinuousβ functions; instead,
we arrange for the interval *type* to be so that all functions
from it are continuous.

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

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, i.e.Β when there can be
at most one
$p:aβ‘b.$

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.

While the type
$I$
is meant to represent the unit interval
$[0,1],$
we donβt have to bake an axiomatization of the real numbers into our
type theory. For the purposes of representing identifications, we can
get away with treating the interval as mostly featureless. To start
with, weβll see that the interval is equipped with
**endpoints**, the values
$i0,i1:I,$
its start and end. If we have an arbitrary
$f:IβA,$
we say that it is a path *from*
$f(i0)$
*to*
$f(i1).$
Of course, most of the time, weβre interested in identifying elements we
already know about: we talk not about paths, but about **paths
from
$a$
to
$b$**.

However, we can not internally *define* the type of βfunctions
$f:IβA$
which satisfy
$f(i0)=a$
and
$f(i1)=b$β;
not only can we not internally talk of definitional equality, but we
donβt even have a notion of sameness yet: thatβs what weβre trying to
define! Instead, cubical type theory is equipped with a
*primitive* type of **paths from
$a$
to
$b$**.

This type, like any other, has formation and elimination rules.
Informally, the formation rule says that any function
$f:IβA$
can be made into a path
$f(i0)β‘f(i1),$
and the elimination rule says that if we have
$i:I,$
and a path
$p:aβ‘b,$
we can apply
$p(i)$
and get out a value of
$A.$
In formal presentations of cubical type theory (e.g.Β CCHM (2016)),
paths are introduced and eliminated with their own syntax. In Agda, we
instead *overload* the lambda notation, and function application,
so that it can be used for both functions *and* paths.

Therefore, while we can define a helper that upgrades any function to
a path, it looks a lot like the identity function; we do not
*require* this helper, since we can always write paths using the
same syntax as for functions.

When we can infer the type
$A$
from the points
$a,b:A,$
we write the type of paths as
$aβ‘b,$
both in the formalisation and the prose. This is traditional in Agda,
but slightly breaks with the convention of type theory
*literature*, which traditionally uses
$aβ‘b$
to mean definitional equality.

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

The easiest path to construct is *reflexivity*, called `refl`

for short: Given a point
$a:A,$
there is a distinguished path
$refl_{a}:aβ‘a,$
which goes from
$a$
to
$a$
by ignoring the interval variable
$i$
entirely.

refl : β {β} {A : Type β} {x : A} β x β‘ x refl {x = x} i = x

Before we move on, we can also demonstrate the elimination rule for
paths *as functions from the interval*, that is, application.
Note that, when we apply
$p:aβ‘b$
to one of the endpoints of the interval, we *definitionally* get
back the endpoints of the path. Other than the circularity (needing
sameness to define paths, which are our notion of sameness), these
definitional equalities are the reason that paths are a primitive type
former.

module _ {β} {A : Type β} {a b : A} {p : a β‘ b} where private apply-path : (i : I) β A apply-path i = p i left-endpoint : p i0 β‘ a left-endpoint = refl right-endpoint : p i1 β‘ b right-endpoint = refl

## Dependent pathsπ

Since weβre working in dependent type theory, a sensible question to
ask is whether we can extend the idea that paths are functions
$IβA$
to *dependent* functions
$(i:I)βA(i).$
Indeed we can, and these turn out to be very useful: theyβre
**dependent paths**. Weβll have more to say on these later, to
connect them with another emergent notion of dependent path, but itβs
important to mention the primitive notion now.

If we have a *line* of types
$A:IβType,$
and inhabitants
$a:A(i0)$
and
$b:A(i1),$
we can form the **dependent** path space between them: the
type
$PathPΒAΒaΒb,$
which in the code is written `PathP A a b`

. Here, inferring
the line
$A$
is basically always impossible, so weβll always write it explicitly. As
before, these correspond 1-1 to dependent functions which map the
endpoints to
$a$
and
$b.$
To avoid repetition, weβll take this opportunity to write out the typing
rules, if that helps.

Colloquially, we speak of a value
$p:PathPΒAΒaΒb$
as a path between
$a$
and
$b$
**over
$A$**.
Formally, the idea is that, while
$a$
and
$b$
may live in different types,
$A$
is an identification between them; and, *over* this
identification,
$a$
and
$b$
are identical. The generic situation for a path over a path is pictured
in the diagram below.

Above, we have a blob representing the type of types, `Type`

, which is on the bottom
of the image. The line of types
$A$
is drawn as a literal path between the points
$A(i0)$
and
$A(i1)$
in this space. On top, we have the points
$a$
and
$b,$
which βlie overβ their respective types. And finally, our
$p:PathPΒAΒaΒb$
is path from
$a$
to
$b$
*over* the path
$A.$

Even though we introduced `Path`

first, the `PathP`

connective, being more
general, is the actual *primitive* provided by Agda. The path
type
$aβ‘b,$
and its longhand
$PathΒAΒaΒb,$
are defined in terms of `PathP`

.

Path : β {β} (A : Type β) (x y : A) β Type β Path A x y = PathP (Ξ» i β A) x y

## Symmetryπ

Now that we have the notion of paths, weβll spend the rest of this
module setting up the structure *around* them that makes them
useful. A good place to start with are the **inverses**:
there should be an operation mapping paths
$p:aβ‘b$
to paths
$p_{β1}:bβ‘a.$
In Cubical Agda, we work in *de Morgan* cubical type theory. This
means that, in addition to the endpoints
$i0,i1,$
the interval is equipped with a few extra bits of algebraic structure,
to make working with paths more convenient.

The relevant operation here is the de Morgan
**negation**, written
$Β¬i$
in the prose and `~_`

in the
formalisation. In addition to interacting with the other operations, the
negation satisfies
$Β¬i0=i1$
and
$Β¬i1=i0,$
and
$Β¬(Β¬i)=i.$
The first two imply that we can use it to implement inverses: for if we
have
$p:aβ‘b,$
then
$q=Ξ»i.ΒpΒ(Β¬i)$
satisfies
$q(i0)=p(i1)=b$
and
$q(i0)=p(i1)=a.$

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

We can also invert *dependent* paths: if
$a:A(i0)$
and
$b:A(i1)$
are identified over a line
$A,$
then
$b$
and
$a$
are identified over the inverse of
$A.$

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)

Since we have
$Β¬Β¬i=i,$
these operations are both *definitional* involutions. Once we
implement path *composition*, weβll be able to show that
$p_{β1}$
is legitimately the inverse to
$p.$

_ : symP (symP p) β‘ p _ = refl

## Raising dimensionπ

To recap, in cubical type theory, a term in a context with
$n$
interval variables expresses a way of mapping the
$n-cube$
into that type. So far, we have been talking about mapping the
$1-cube,$
i.e.Β the line, into types, producing identifications. But the type of
paths
$aβ‘b$
is itself a type, so if we have
$p,q:aβ‘b,$
we can form the iterated path type
$pβ‘q.$
Cubically, weβre now talking about functions
$IβIβA,$
with *two* dimensions: a way of mapping the *square* into
a type.

If we consider a path
$p:aβ‘b$
as an object in its own right, we can consider the reflexivity path
$refl_{p}:pβ‘p,$
which by the paragraph above lives one dimension higher. In this
section, weβll explore the *other* ways in which we can lift
$n-cubes$
to
$n+1$
cubes, and to higher dimensions from there.

In a context with two interval variables, we can move in two
dimensions (call them
$i$
and
$j):$
to use our path
$p,$
which only varies along *one* dimension, we must either
*discard* one of
$i$
or
$j,$
or find a way to *combine* them. Discarding is the easier option.
Depending on what dimension we ignore, we get one of two squares, both
of which have two
$p$
faces *across* from eachother. Note that the square `drop-i`

is just the reflexivity
path `refl`

.

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

Letβs look at how to visualise these squares. First, we should note
the direction our axes go in:
$i$
varies from the left to the right, and
$j$
varies top-to-bottom. The `drop-i`

square is
*constant* in the
$i$
direction, but in the
$j$
direction, itβs
$p.$
This manifests in the diagram as having
$refl$
for both of its vertical faces: on the left, weβre looking at
$p(i0)=a$
*not* varying along the vertical axis, and respectively for
$p(i1)=b$
on the right. For the `drop-j`

square, the situation is
flipped, since weβre now ignoring the horizontal direction.

We can now introduce the two operators that go into making the interval a de Morgan algebra: minimum, written $iβ§j,$ and maximum, $iβ¨j.$ As weβll see below, these satisfy the familiar rules for conjunctions and disjunctions in logic, hence the notation. But keep in mind that $I$ is not like ${0,1},$ but rather more like $[0,1]:$ we do not have $(iβ§Β¬i)=i0,$ because there are points along the interval where the βminimumβ of $i$ and β$1βi$β is not zero.

β§-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, called
**connections**. In the diagrams below, we do not have the
space to include the computation for the faces that vary along
$j,$
but we did include them for the faces varying along
$i,$
e.g., in the
$p(iβ§j)$
square, the left face (varying along
$j,$
with
$i=i0)$
is
$p(i0β§j)=p(i0)=a,$
while the right face in
$p(iβ¨j)$
is
$p(i1β¨j)=p(i1)=b.$

Iterated paths are used a *lot* in homotopy type theory, but
in cubical type theory, itβs best to have a type that lets us specify
the boundary of a complete 2-dimensional *square*. Pictorially,
we lay out a square with faces
$p,$
$q,$
$r,$
and
$s,$
as in the diagram below.

Intuitively, we may read this square as saying that the
*composites*
$qβr$
and
$pβs$
are identified.^{1} In the 1Lab, we define the type
`Square`

so that the arguments
are given in the order
$p-$$q-$$s-$$r,$
i.e.Β top-left-right-bottom. This choice is basically arbitrary, but it
matters when reading out the (graphical) boundary from the type of a
term.

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

To start building some intuition, we can rewrite the
dimension-raising operations we named above so that their types are
given in terms of `Square`

. We also ask Agda to
check that a square with top/bottom faces `refl`

, but left/right faces
$p,$
is the same thing as a path between paths.

drop-i : Square refl p p refl drop-i i j = p j drop-j : Square p refl refl p drop-j i j = p i β§-conn : Square refl refl p p β§-conn i j = p (i β§ j) β¨-conn : Square p p refl refl β¨-conn i j = p (i β¨ j)

_ : Square refl p q refl β‘ (p β‘ q) _ = refl

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

module _ {β} {A : Type β} {a00 a01 a10 a11 : A} {p : a00 β‘ a01} {q : a00 β‘ a10} {s : a01 β‘ a11} {r : a10 β‘ a11} where

The last operations we consider *preserve* dimension, rather
than altering it. If we have a square
$Ξ±:SquareΒpΒqΒsΒr,$
there are a few symmetry-like operations we can apply to it, which
correspond to inverting either axis, or swapping them.

flipβ : Square p q s r β Square (sym p) s q (sym r) flipβ Ξ± i j = Ξ± (~ i) j flipβ : Square p q s r β Square r (sym q) (sym s) p flipβ Ξ± i j = Ξ± i (~ j) transpose : Square p q s r β Square q p r s transpose Ξ± i j = Ξ± j i

### Summary of interval algebraπ

Weβll conclude this section with a complete listing of the rules that the algebraic operations on the interval satisfy. These all hold definitionally, so weβll omit the proofs.

-- Laws governing _β§_ β§-comm : i β§ j β‘β± j β§ i β§-idem : i β§ i β‘β± i β§-zero : i β§ i0 β‘β± i0 β§-one : i β§ i1 β‘β± i β§-abs-β¨ : i β§ (i β¨ j) β‘β± i -- Laws governing _β¨_ β¨-comm : i β¨ j β‘β± j β¨ i β¨-idem : i β¨ i β‘β± i β¨-zero : i β¨ i0 β‘β± i β¨-one : i β¨ i1 β‘β± i1 β¨-abs-β§ : i β¨ (i β§ j) β‘β± i -- Laws governing ~_ ~-invol : ~ (~ i) β‘β± i demorgan : ~ (i β§ j) β‘β± ~ i β¨ ~ j ~-zero : ~ i0 β‘β± i1 ~-one : ~ i1 β‘β± i0

β¨-idem = reflβ± β§-one = reflβ± β§-comm = reflβ± β§-zero = reflβ± β§-idem = reflβ± β¨-comm = reflβ± β¨-zero = reflβ± β¨-one = reflβ± ~-invol = reflβ± demorgan = reflβ± ~-zero = reflβ± ~-one = reflβ± β§-abs-β¨ = reflβ± β¨-abs-β§ = reflβ±

# Paths as βsamenessβπ

One of the fundamental features of equality is that it is respected
by all functions: if we have
$f:AβB,$
and
$x=y:A,$
then also
$f(x)=f(y).$
In our homotopical setting, we must generalise this to talking about
*paths*
$p:xβ‘y,$
and we must also name the resulting
$f(x)β‘f(y).$
In cubical type theory, our homotopical intuition for paths provides the
both the interpretation *and* implementation of this principle:
it is the *composition* of a path
$p:xβ‘y$
with a *continuous* function
$f:AβB.$

ap : β {a b} {A : Type a} {B : A β Type b} β (f : β x β 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 type of the function above is perhaps a bit more general than
initially expected: we talk not about types
$A,B$
and a function
$f:AβB,$
but instead about a type
$A,$
a type family
$B(β)$
over
$A,$
and a *dependent* function
$(x:A)βB(x).$
While the values
$f(x)$
and
$f(y)$
live in different points of the family
$B,$
if we have a
$p:xβ‘y,$
the types
$B(x)$
and
$B(y)$
are *themselves* identical. Therefore, we can define the
composition of a *dependent* function with a path, producing a
*dependent* path in the codomain.

We can also define a corresponding operation for *dependent*
paths in the domain, as long as weβre given a *line* of
functions.

apd : β {a b} {A : I β Type a} {B : (i : I) β A i β Type b} β (f : β 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)

The type of `apd`

is another doozy, but it
makes a *bit* more sense when we write out the lines as paths. It
says that if we have (dependently) identical dependent functions, and we
apply them to identical arguments, we get identical results. Itβs a
natural principle, apart from the ludicrous amount of
quantification.

_ : β {a b} {A A' : Type a} {B : A β Type b} {B' : A' β Type b} {f : β x β B x} {g : β x β B' x} {x : A} {y : A'} β {pa : A β‘ A'} {pb : PathP (Ξ» i β pa i β Type b) B B'} β (pf : PathP (Ξ» i β β x β pb i x) f g) β (px : PathP (Ξ» i β pa i) x y) β PathP (Ξ» i β pb i (px i)) (f x) (g y) _ = Ξ» pf px β apd (Ξ» i β pf i) px

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)

Under the correspondence between homotopy theory and higher category
theory, we would say that `ap`

expresses that functions are *functors* from their domain to
their codomain. Accordingly, we would expect that `ap`

preserves identities
(i.e.Β $refl)$
and commutes with taking inverses. Since paths are implemented as
functions, these preservation laws are *definitional*, instead of
needing proof. Weβll revisit these functoriality laws later, when we
have defined composition.

ap-sym : {p : x β‘ y} β sym (ap f p) β‘ ap f (sym p) ap-sym = refl ap-refl : ap f (refl {x = x}) β‘ refl ap-refl = refl

The `ap`

operation is also functorial
in its *first* argument: it preserves identity and composition of
*functions*, too.

ap-β : {p : x β‘ y} β ap (Ξ» x β g (f x)) p β‘ ap g (ap f p) ap-β = refl ap-id : {p : x β‘ y} β ap (Ξ» x β x) p β‘ p ap-id = refl

## Transportπ

Weβve established that every function preserves paths, but this is
not *quite* enough for a notion of sameness. The key principle
that characterises identity among the relations is
**indiscernibility of identicals**: at the logical level,
this says that if
$P(x)$
and
$x=y,$
then also
$P(y).$
In type theory, this is generalised: weβre not only talking about
*predicates*
$P(β),$
but rather *type families*
$P(β),$
which have values; and we do not simply have
$x=y,$
but rather a specific *path*
$p:aβ‘b.$

In Cubical Agda, the relevant *primitive* is the function
`transp`

, whose type is a slight
generalisation of the `transport`

operation below.
Weβll focus on `transport`

for now. To start
with, this is where paths show their difference from the notion of
equality in set-level type theories: it says that we have a function
from paths
$p:Aβ‘B$
to functions
$AβB.$
However, itβs *not* the case that every
$p,q:Aβ‘B$
gives back the *same* function
$AβB.$
Which function you get depends on (and determines) the path you put
in!

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

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

has exactly two inhabitants (see here), which would be
traditionally be read as saying something like βthe set of booleans is
equal to itself in two waysβ. As mentioned before, we reserve the
terminology
β$a$
and
$b$
are equalβ for when there is *at most one*
$aβ‘b;$
instead, the situation with `Bool`

should be read as βthere
are two *identifications* of `Bool`

with itself.β

By composing our new `transport`

with the `ap`

from the last section, we
can derive the promised indiscernibility of identicals, which we call
`subst`

. Here, weβll note that
the function
$P(x)βP(y)$
you get depends on both the path
$p:aβ‘b$
*and* the type family
$P(β).$

subst : β {ββ ββ} {A : Type ββ} (P : A β Type ββ) {x y : A} β x β‘ y β P x β P y subst P p x = transport (ap P p) x

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

As we mentioned above, the primitive `transp`

slightly generalises
the `transport`

operation: weβll now
see how this generality is useful. In addition to letting us specify the
line (read: identification between types) to transport over, and the
thing to transport, it has an additional argument
$Ο:I.$
This is the first instance of the interval naming
**formulas**: rather than being an *endpoint*, the
argument
$Ο$
specifies *where the path is constant*. When an element
$Ο:I$
is taken to be a *formula*, we interpret it to be the proposition
$Ο=i1.$

The constancy of the path is a side-condition in the type of
`transp`

that is enforced by the type checker, but which we
do not (yet) have the tools to express. However, the function it serves
is simple: when
$Ο=i1$
says the path is constant, transporting is definitionally the
identity:

_ : β {β} {A : Type β} β transp (Ξ» i β A) i1 β‘ id _ = refl

To define the high-level `transport`

, we had to set
$Ο=i0,$
expressing that the path is *nowhere* constant. This constancy
information is simply not tracked in the type of paths, so itβs our only
choice. However, we know that transporting along a reflexivity path
should be the identity. We can use the
$Ο$
argument to prove this!

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

In the definition above,
$Ξ»i.ΒA$
is always a constant function, so the side-condition is satisfied.
Therefore, we can compute the endpoints of the path. When
$i=i0,$
we have exactly `transport refl x`

; but when
$i=i1,$
the entire `transp`

computes away, and
weβre left with just
$x.$
In fact, the proof of `transport-refl`

generalises to a
natural operation computing a dependent path: we call it the
*filler* of the transport, since it *fills* a line
$PathPΒpΒxΒtransportΒpΒx.$

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

This definition is well-formed because, when $Β¬i=i1$ (i.e.Β $i=i0),$ the line is $Ξ»j.ΒpΒ(i0β§j)=Ξ»j.ΒA,$ which is constant. Moreover, its body computes to $transpΒΞ»j.ΒAΒi1Βx=x$ on $i0$ and to $transpΒpΒi0Βx=transportΒpΒx$ on the right, so the endpoints are correct.

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

### Computationπ

In book HoTT, `transport`

is defined using path induction, and it computes
definitionally only when the path is `refl`

. By contrast, in cubical
type theory, the `transp`

primitive computes in
terms of the line of types. For the natural numbers, and other inductive
types without parameters, `transport`

is always the
identity function. This is justified because a type like `Nat`

is completely insensitive
to the interval:

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

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

and
`B`

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

and `B`

:

module _ {A0 A1 B0 B1 : Type} {A : A0 β‘ A1} {B : B0 β‘ B1} where private

If we have $A(i)$ and $B(i),$ we can form the product type $A(i)ΓB(i).$ The transport operation, in this case, is componentwise. There isnβt much else we could do!

_ : transport (Ξ» i β A i Γ B i) (a , b) β‘ (transport A a , transport B b) _ = refl

For non-dependent functions, the situation is similarly intuitive, but slightly more complicated. We want to produce an $A(i1)βB(i1),$ but the only way we have to get a $B(β)$ is by applying $f.$ We first transport $x:A(i1)$ along $A_{β1}$ to get $transportΒA_{β1}Βx:A(i0),$ then apply $f$ to get something in $B(i0),$ and finally transport along $B$ to get something in $B(i1).$ Check it out:

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

Itβs also illustrative to consider the case of a dependent function.
We start with a line of types
$A(i)$
and a line of type *families*
$B(i,β)$
over
$A(i).$
If we have
$f:(x:A(i0))βB(i0,x),$
how do we send an
$x:A(i1)$
to something in
$B(i1,x)?$

As before, we can start by producing something in $A(i0)$ by transporting $x$ backwards, and applying $f.$ This gives us the values

$x_{0}y_{0}β=transportΒA_{β1}Βx=f(x_{0})ββ:A(i0):B(i0,x_{0}).β$Weβre now faced with the conundrum of transporting
$y_{0}$
along
$B.$
But we canβt take the line to be
$Ξ»i.ΒB(i,x_{0})$
since
$x_{0}:A(i0),$
while the argument to
$B(i,β)$
should be in
$A(i)!$
The solution is to *generalise*
$x_{0}$
to a line

so that we may form
$Ξ»i.ΒB(i,x_{i})$
connecting
$B(i0,x_{0})$
and
$B(i1,x).$
While this construction seems to have come out of nowhere, note that
$x_{i}$
is the inverse of `transport-filler`

along
$A_{β1}!$
We can then obtain our return value by transporting
$y_{0}$
along this line.

_ : {f : (x : A i0) β B i0 x} β transport (Ξ» i β (x : A i) β B i x) f β‘ Ξ» (x : A i1) β let xi : β i β A i xi i = transport-filler (Ξ» i β A (~ i)) x (~ i) y0 = f (xi i0) in transport (Ξ» i β B i (xi i)) y0 _ = refl

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

types) also involves a filler, but no negations.

_ : {x : A i0} {y : B i0 x} β transport (Ξ» i β Ξ£ (A i) (B i)) (x , y) β‘ let xi : β i β A i xi i = transp (Ξ» j β A (j β§ i)) (~ i) x in xi i1 , transport (Ξ» i β B i (xi i)) y _ = refl

## Path inductionπ

In Martin-LΓΆf type theory, the identity type is not characterised by
indiscernibility of identicals (its *recursion* principle), but
rather by its *induction* principle, known simply as βJβ.
Internalised, the J rule has the following type:

J : β {ββ ββ} {A : Type ββ} {x : A} β (P : (y : A) β x β‘ y β Type ββ) β P x refl β β {y} p β P y p

Seen one way, this is a generalised version of `subst`

, where the type family
may also depend on the path β to the syntactically-minded, this is
exactly the induction principle for identity *qua* inductive
family; it says that the total space of the identity family
$Ξ£_{y:A}(xβ‘y)$
is generated by the point
$(x,refl).$
This rule is not purely syntactically motivated: it has a natural
homotopical interpretation, which leads to a nice *visual*
explanation.

In this analogy, the total space
$Ξ£_{y:A}(xβ‘y)$
is the space of paths from
$x$
*with an endpoint free*, the *free* endpoint being the
first coordinate of the pair. Elements in this type are allowed to have
whatever right endpoint, and weβre allowed to identify paths with
different endpoints. The J rule says that every
$(y,p)$
in this type is identical to
$(x,refl).$
How can that be? If we think of paths as *ropes* that can shrink,
and of identifications between them as deformations over time, then this
rule states that, as long as one endpoint is *free*, weβre
allowed to *coil in* the rope, reducing its length until it is
trivial. In this analogy, we can see why one endpoint has to be free: if
it werenβt, our path might get snagged on something!

This identification comes up very often when working in homotopy type
theory, so it has its own name: **contractibility of
singletons**. A type of singletons is something like
$Ξ£_{y:A}(xβ‘y):$
the type of elements of
$A$
which are identical to
$y.$
Read set-theoretically, it makes sense that this would only have one
inhabitant!

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

Weβre given an inhabitant $y:A$ and a path $p:xβ‘y.$ To identify $(x,refl)β‘(y,p),$ we have to produce an identification $xβ‘y$ (we can use $p),$ and, over this, an identification of $refl$ and $p.$

Singleton-is-contr : β {β} {A : Type β} {x : A} (y : Singleton x) β Path (Singleton x) (x , refl) y Singleton-is-contr {x = x} (y , p) =

Writing out the dependency explicitly, we see that the second
component should inhabit the dependent path type
$PathPΒ(Ξ»i.Βxβ‘p(i))ΒreflΒp,$
which weβve already seen: not only can it be expressed as a
`Square`

, but it is precisely the type of the connection square
$p(iβ§j):$

let q : Square refl refl p p q = Ξ» i j β p (i β§ j) in Ξ» i β p i , q i

We then obtain the definition of J: If we have $prefl:P(x,refl)$ but we want $P(y,p),$ we can first identify $(x,refl)β‘(y,p),$ then transport our assumption over that.

J {x = x} P prefl {y} p = let pull : (x , refl) β‘ (y , p) pull = Singleton-is-contr (y , p) in substβ P (ap fst pull) (ap snd pull) prefl

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 this rule work 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, we trade off the computation rule `J-refl`

for a smooth
implementation of these higher-dimensional principles. The result is,
undeniably, a more complicated type theory: we now have to explain how
to reduce `transp`

in arbitrary lines of
types. Weβve made some progress, considering things like universes,
inductive data types, dependent products, and dependent sums. However,
we have not yet explained how to compute `transp`

in path types, much
less in `PathP`

. To have a functioning
type theory, weβll need computation rules to handle these; but for that,
we first need to introduce the higher-dimensional generalisation of path
types: **partial elements** and
**extensibility**.

## Partial elementsπ

In our discussion of the
interval, we became acquainted with the idea that a value
$e:A$
in a context with
$n$
interval variables can be pictured as an
$n-cube$
drawn on the type
$A.$
Weβre also familiar with the idea that we can place *constraints*
on the values that these cubes take at certain points along the
interval: this is what `PathP`

specifies. A value
$p:PathPΒAΒxΒy$
is a line
$Ξ»i.Βp(i)$
in
$A,$
which is
$x$
when
$i=i0$
and
$y$
when
$i=i1.$

But what if we want to specify constraints on a cube in higher
dimensions? We could iterate `PathP`

types, as done in the
definition of `Square`

, but that forces us to
specify values at *every* endpoint. What if we only particularly
care about the value at *one* of the endpoints, or some more
complicated sub-shape of an
$n-cube?$
Enter the `Partial`

type former.

When
$A$
is a type and
$Ο:I$
is some interval expression, we can form the type
$PartialΒΟΒA$
of **partial elements** of
$A$
with **extent**
$Ο:$
an element of
$A,$
but which is only defined when
$Ο=i1.$
You can think of a partial element as a function: if you have
$p:PartialΒΟΒA,$
and you can come up with some evidence
$v$
that
$Ο=i1,$
then
$p(v):A.$
Conversely, if you *have* some
$x:A,$
you can pretend it is a partial element by *ignoring* the
evidence. In Agda, we write `IsOne`

for the type of such evidence, and we write `1=1`

for the proof that
$i1=i1.$

The key feature of partial elements is that we can introduce them by
giving **systems**: If you want to define an
$f:PartialΒ(Οβ¨Ο)ΒA,$
it suffices to give
$x:PartialΒΟΒA$
and
$y:PartialΒΟΒA,$
*as long as they agree when
$(Ο=i1)β§(Ο=i1).$*

For instance, if we have a dimension
$i:I,$
then the type
$PartialΒ(iβ¨Β¬i)ΒA$
represents the *endpoints* of a line in
$A.$
We do not have a *complete* line, just the endpoints! As an
example, we can define a value of `Bool`

which is `true`

on the left
endpoint of the interval, and `false`

on the right
endpoint.

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

Graphically, our `not-a-path`

is represented by
the following rather boring shape: two disconnected points, with
completely unrelated values at each endpoint of the interval.

As a further example, we could imagine piecing together
*three* paths into a partial element that is defined on three
faces, resulting in something like an upside-down drinking glass. Note
that each of the faces in the system below only constrains *one*
of the dimensions, as written between parentheses on the left-hand-side.
This means the right-hand-side can, and does, still vary along the
*other* dimension. This is in contrast to our `not-a-path`

example above, in
which the *only* dimension is constrained, so there can be no
variation.

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

Note that this element is valid *only because* we laid out the
paths with their common vertices are aligned. This is the side condition
we have to fulfill when defining a system: on common edges, the faces of
the partial element *must* agree.

## Extensibilityπ

The next type former weβll introduce lets us turn a partial element
into a *constraint*. Much like the `Path`

type constrains its inhabitants to have matching endpoints
definitionally, the **extension types** let us carve out
the subtype of
$A$
which *definitionally* agree with a given partial element. If we
have a
$p:PartialΒΟΒA,$
then we can form the type
$A[Οβ¦p].$

The introduction rule, internalized as the constructor `inS`

, says that, if we have a
totally-defined element
$e:A$
which satisfies
$Οβ’e=p$
(i.e.Β which agrees with
$p$
wherever it is defined), then we can form
$inSe:A[Οβ¦p].$
The elimination rule says that, if
$e:A[Οβ¦p],$
then we can obtain an element
$outSe:A;$
and moreover,
$Οβ’outSe=p.$

With the type theory aside, letβs get to examples. 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* this
partial element.

Diagramatically, weβll depict extensions by drawing the relevant
partial element in red, and the total element in black. In Agda, we
write extension types using the type former `_[_β¦_]`

,
which is written mixfix as `A [ Ο β¦ p ]`

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

Slightly more preicsely, the constructor `inS`

expresses
that *any* totally-defined cube
$u$
can be seen as a partial cube, which simply agrees with
$u$
for any choice of formula
$Ο.$
To introduce elements of *specific* extensions, we use the fact
that partial elements are definitionally equal as long as they are
definitionally equal on their intersections. 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 wedge 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 many partial elements that can not be
extended at all. Take `not-a-path`

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

at `i0`

and `false`

at `i1`

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

β a contradiction.^{2}

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 we have already
mentioned. However, we can also demonstrate its *computation*
rule. In the code below, even though `x`

is abstract, we know
that `outS`

agrees with the partial element
`u`

.

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

## Box fillingπ

Using the notions of partial elements and extensibility, we can
define a higher-dimensional generalisation of the notion of binary path
composition: the **homogeneous composition** operation,
`hcomp`

. This is one of the
fundamental tools for working with higher-dimensional types in cubical
type theory: it lets us reduce many problems of path algebra to
formulating partial elements expressing their solutions.

Since this is the second hardest construction to grok in cubical type theory, weβll start with a very concrete example. Recall the partial element we drew by gluing three paths together, and its formalisation:

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

If we consider this open square as a sequence of three paths to
follow, then our intuition that types are spaces (or groupoids) says
that there should be a *fourth* path, the composite, whose
βeffectβ is to follow each of the paths in turn. We donβt yet know how
to compute such a path, but it should very well exist! This is one of
the many things that `hcomp`

can do for us:

composite : w β‘ z composite i = hcomp (i β¨ ~ i) (shape i)

In this situation, we picture `hcomp`

as filling the face opposite
$j=i0.$

In general, `hcomp`

allows us to build an
$n-dimensional$
cube, with a boundary of our choice, by expressing it as the missing
face in some
$(n+1)-dimensional$
shape. Its actual interface says that, if we have some shape
$Ο:I,$
and a partial element

then we can obtain an extension
$A[Οβ¦e(i1)].$
The idea of the extra
$i$
dimension is that weβre forced to give a *connected* shape:
$i$
is disjoint from any of the variables in
$Ο,$
so we have to give at least *something* (the value
$e(i0)).$
This means that we canβt use `hcomp`

to produce an extension of our `not-a-path`

system, for example,
since it would be impossible to make it connected in the first
place!

Note that `hcomp`

gives us the missing
$(nβ1)-dimensional$
face of the open
$n-box,$
but the semantics guarantees the existence of the
$n-box$
*itself*. Using the De Morgan structure on the interval, we can
*define* this βfillingβ operation in terms of composition: we
express the *entire* original shape as the βmissing faceβ of an
$(n+1)-dimensional$
problem.

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. Since `Square`

expresses an equation
between paths, we can read the type of `Β·Β·-filler`

as saying that
$p_{β1}β(pββqββr)=qβr.$

Β·Β·-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. Any of paths would have led to
the same definition, but for definiteness we choose `p`

. Note
that we can also define a filler for the single composition, whose type
we read as saying that
$reflβ(pβq)=pβq.$

_β_ : β {β} {A : Type β} {x y z : A} β x β‘ y β y β‘ z β x β‘ z p β q = refl Β·Β· p Β·Β· q β-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 infixr 30 _β_

Weβll leave this section with a composition operation that works for
*dependent* paths. This is a nice combination of fillers and CCHM
composition: it takes proofs that
$xβ‘y$
over
$p$
and
$yβ‘z$
over
$q,$
and produces a path witnessing that
$xβ‘z$
over
$pβq.$
The definition is exactly analogous to that of single composition, but
with extreme amounts of extra quantification.

_β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

β-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) _ββ_ : β {β} {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_ _ββ_

## The need for hcompπ

At the start of this section, our goal was to explain how to compute
`transp`

in a line of
*paths* (or `PathP`

s). Towards this, we
introduced the higher-dimensional composition operation, `hcomp`

, and weβve shown that it
can be used to recover ordinary path composition β but we have not
explained how that connects to reduction of `transp`

in path types. Let us
do so now. Readers familiar with MLTT will know that composition of
paths can be defined in terms of path induction, or, more clearly, `transport`

:

_β'_ : {x y z : A} (p : x β‘ y) (q : y β‘ z) β x β‘ z _β'_ {x = x} p q = transport (Ξ» i β x β‘ q i) p

Since we know that `transport`

reduces when applied
to type formers, the definition above is *not* neutral, even when
$p$
and
$q$
are variables. But what does it reduce *to*? A natural attempt
would be to say that, at a point
$i:I,$
the path
$transportΒ(Ξ»i.Β.xβ‘q(i))Βp$
is
$t=transportΒ(Ξ»i.Β.A)Βp(i)$
β i.e., transport of paths is, pointwise, transport along the base. But
this canβt be the case, since
$t$
has endpoints

which are *both* wrong! More saliently, this attempt makes no
use of the path
$q$
at all, so thereβs no way it can be right. However, the endpoints are
*propositionally* correct. What we need is a way to correct the
endpoints after transporting the base, using an arbitrary path. But this
is exactly what `hcomp`

lets us do! The
*real* normal form of our transport is the dashed path in the
diagram below, where we abbreviate
$transpΒ(Ξ»i.ΒA)ΒΟΒx$
as
$trΒΟΒx:$

We can ask Agda to verify this, by writing out the diagram as an
`hcomp`

:

_ : {x y z : A} {p : x β‘ y} {q : y β‘ z} β let tr : (Ο : I) (a : A) β A tr Ο a = transp (Ξ» i β A) Ο a the-hcomp : x β‘ z the-hcomp i = hcomp (β i) Ξ» where j (j = i0) β tr i0 (p i) j (i = i0) β tr j x j (i = i1) β tr j (q j) in (p β' q) β‘ the-hcomp _ = refl

More generally, we can demonstrate the computation rule in an
arbitrary `PathP`

. Itβs a straightforward
generalisation of the construction above: We have a *square* of
types
$A(i,j),$
and lines of endpoints
$x(i):A(i,i0)$
and
$y(i):A(i,i1).$
Writing

we can ask Agda to check that transporting a $p:C(i0)$ to something in $C(i1)$ is done by computing the composition below:

C : I β Type C j = PathP (Ξ» i β A j i) (x j) (y j) the-hcomp : C i0 β C i1 the-hcomp p i = hcomp (β i) Ξ» where j (j = i0) β transp (Ξ» j β A j i) i0 (p i) j (i = i0) β transp (Ξ» i β A (j β¨ i) i0) j (x j) j (i = i1) β transp (Ξ» i β A (j β¨ i) i1) j (y j) _ : {p : C i0} β transp C i0 p β‘ the-hcomp p _ = refl

## Uniqueness of compositionsπ

Since weβre defining composition of paths as the missing face in a
particular square, we have to wonder: can paths have *multiple*
composites, i.e.Β multiple faces that fit into the same square? The
answer, fortunately, is no: we can show that any triple of paths has a
*unique* double composite, by drawing a *cube* whose
missing face is a *square* whose boundary includes the two
*lines* weβre comparing.

Β·Β·-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

Finally, we note that the uniqueness results from this section let us
prove that path composition as defined directly through `hcomp`

agrees with path
composition as defined through transport. The key observation is that
the `transport-filler`

along
$Ξ»i.Βxβ‘q(i)$
is *precisely* the square analogous to `β-filler`

:

_ : (x : A) {y z : A} (p : x β‘ y) (q : y β‘ z) β p β' q β‘ p β q _ = Ξ» x p q β let filler : Square refl p (p β' q) q filler = transport-filler (Ξ» i β x β‘ q i) p in β-unique (p β' q) filler

### Functoriality of apπ

This is a very short section: when we introduced `ap`

, we promised to
show that it also preserves path composition, to complete the
requirements of functoriality. Using the uniqueness result from the
previous section, this becomes mostly straightforward. First, we
introduce the operation `ap-square`

, which, as the name
implies, shows that every function preserves squares:

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)

Despite the nightmare type (to allow `f`

to be a dependent
function), the definition is just as straightforward as that of `ap`

. Using this with `Β·Β·filler`

, we get a square with
boundary

but note that our lemma `Β·Β·-unique'`

says precisely that,
for every square with this boundary, we can get a square connecting the
red path
$apΒfΒ(pββqββr)$
and the composition
$apΒfΒpββapΒfΒqββapΒfΒr.$

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

## Dependent paths, continuedπ

Armed with the transport and composition operations, we can continue
the development of the notion of dependent
path. The `transport`

operation gives rise
to an *emergent* notion of dependent path, in addition to the
primitive `PathP`

. If we have a line of
types
$P(i),$
and points
$x:P(i0),y:P(i1),$
then we can say that they are βidentified over
$P$β
to mean either
$PathPΒPΒxΒy$
*or*
$transportΒPΒxβ‘y.$

Itβs possible to directly construct paths in the universe that witness the agreement between these:

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 that the first definition is well-formed 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 connection between dependent paths and transport 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 these operations, we can define maps that convert between `PathP`

s and βbook-styleβ
dependent paths, which are more efficient than transporting along `PathPβ‘Path`

.

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)

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

# Basics of groupoid structureπ

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 _$β_ #-} _β _ : β {β} {A : Type β} β A β A β Type β x β y = Β¬ x β‘ y

At this point in the formalisation, we have not yet introduced the machinery necessary to define composition of paths, let alone prove that squares correspond to identities between composites.

However, itβs instructive to keep this intuition in mind for when we

*do*define composition, and for when we can prove this correspondence.β©οΈAlthough it is not proven to be a contradiction in

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

## References

- Cohen, Cyril, Thierry Coquand, Simon Huber, and Anders MΓΆrtberg. 2016. βCubical Type Theory: A Constructive Interpretation of the Univalence Axiom.β https://arxiv.org/abs/1611.02108.