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
β
and
are equalβ when the type
is inhabited, but in this development we reserve this terminology for
the case where
and
inhabit a set.
Instead, for general types, we use β and are identicalβ or β and are identifiedβ (or even the wordier, and rather more literal, βthere is a path between and β). 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
,
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
)
is given by a Path which yields the same element
everywhere on I
: The function that is constantly
.
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
- ,
- ,
- , ,
- and are both associative, commutative and idempotent, and distribute over eachother.
Note that, in the formalisation,
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 interval variables expresses a way of mapping an -cube into that type. One very important class of these maps are the -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 or ) in that space are identical: A path between paths, which we call a homotopy.
The structural operations on contexts, and the and operations on the interval, give a way of extending from -dimensional cubes to -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
and
are identical β these are adjacent if you βfold upβ the sequence
p q s r
. Similarly, reading top-down, it says that
and
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 and holds, then also holds, for any choice of predicate . In type theory, this is generalised, as 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 complexes4, 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 by an -cube is a term of type in a context with 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 , , and . 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 , , and . Note that in the left face of the diagram, the path was inverted; This is because while we have a path , we need a path , 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 . The interpretation of types as Kan cubical sets guarantees that the open box above extends to a complete square, and thus the line exists.
Partial Elementsπ
The definition of Kan cubical sets as those having fillers for all open boxes is all well and good, but to use this from within type theory we need a way of reflecting the idea of βopen boxβ as syntax. This is done is by using the Partial type former.
The Partial type former takes two arguments: A
formula
,
and a type
.
The idea is that a term of type
in a context with
I-typed variables is a
-cube
that is only defined when
βis trueβ. In Agda, formulas are represented using the De Morgan
structure of the interval, and they are βtrueβ when they are equal to 1.
The predicate IsOne
represents
truth of a formula, and there is a canonical inhabitant 1=1 which says i1
is i1.
For instance, if we have a variable i : I
of interval
type, we can represent disjoint endpoints of a Path by a partial element with formula
.
Note that this is not the same thing as i1! Since elements of
I
are meant to represent real numbers
,
it suffices to find one for which
is not
β 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 -variables gives us a way of mapping some subobject of the -cube into a type. A natural question to ask, then, is: Given a partial element of , can we extend that to a honest-to-god element of , which agrees with where it is defined?
Specifically, when this is the case, we say that extends . We could represent this very generically as a lifting problem, i.e.Β trying to find a map which agrees with when restricted to , but I believe a specific example will be more helpful.
Suppose we have a partial element of Bool which is
true on the left endpoint of the
interval, and undefined elsewhere. This is a partial element with one
interval variable, so it would be extended by a path β a
1-dimensional cube. The reflexivity path is a line in Bool
,
which is true on the left endpoint of the
interval (in fact, it is true everywhere), so we say that
refl extends the partial
element.
In the diagram, we draw the specific partial element being extended
in red, and the total path extending it in black. In Agda, extensions
are represented by the type former _[_β¦_]
.5
We can formalise the red-black extensibility diagram above by
defining the partial element left-true and
giving refl to inS, the
constructor for _[_β¦_]
.
private left-true : (i : I) β Partial (~ i) Bool left-true i (i = i0) = true refl-extends : (i : I) β Bool [ (~ i) β¦ left-true i ] refl-extends i = inS (refl {x = true} i)
The constructor inS
expresses that any
totally-defined cube
can be seen as a partial cube, one that agrees with
for any choice of formula
.
This might be a bit abstract, so letβs diagram the case where we have
some square
,
and the partial element has formula
.
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
β where
represents the left/right direction, and
the up/down direction, as is done below. So, this is an element that is
defined almost everywhere: all three out of four faces of the
square exist, but weβre missing the fourth face and an inside.
module _ {A : Type} {w x y z : A} {p : w β‘ x} {q : x β‘ y} {r : y β‘ z} where private double-comp-tube : (i j : I) β Partial (~ i β¨ i β¨ ~ j) A double-comp-tube i j (i = i0) = sym p j double-comp-tube i j (i = i1) = r j double-comp-tube i j (j = i0) = q i
The Kan condition on types says that, whenever we have some formula and a partial element defined along (for disjoint from ; we call it the βdirection of compositionβ, sometimes), then we can extend it to a totally-defined element, which agrees with along .
The idea is that the , being in some sense βorthogonal toβ the dimensions in , will βconnectβ the tube given by . This is a slight generalization of the classical Kan condition, which would insist , where 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 . 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 -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 is fibrant if 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 and 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 and . 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 ) is the face, and the red face is the 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 -groupoid, which is discussed in a different module.
It is then reasonable to expect that every function behave like a functor, 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
and
where the types
and
are not definitionally equal, but only identified in some
specified way. We call these βpaths over
ppathsβ, 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 path) 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 havePathP (Ξ» j β P j) p q
, by the endpoint rule for transport-filler.When
i = i1
, we havePathP (Ξ» 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
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 .
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 to or .
coeiβ0 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i0 coeiβ0 A i a = transp (Ξ» j β A (i β§ ~ j)) (~ i) a coeiβ1 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i1 coeiβ1 A i a = transp (Ξ» l β A (i β¨ l)) i a
Using squeezes and spreads, we can define maps that convert between PathPs and βbook-styleβ dependent paths. These conversions could also be defined in terms of PathPβ‘Path, but the following definitions are more efficient.
module _ {β} {A : I β Type β} {x : A i0} {y : A i1} where to-pathp : coe0β1 A x β‘ y β PathP A x y to-pathp p i = hcomp (β i) Ξ» where j (j = i0) β coe0βi A i x j (i = i0) β x j (i = i1) β p j from-pathp : PathP A x y β coe0β1 A x β‘ y from-pathp p i = transp (Ξ» j β A (i β¨ j)) i (p i)
Note that by composing the functions to-pathp and to-pathp with the reversal on the interval, we obtain a correspondence PathP and paths with a backwards transport on the right-hand side.
module _ {β} {A : I β Type β} {x : A i0} {y : A i1} where to-pathpβ» : x β‘ coe1β0 A y β PathP A x y to-pathpβ» p = symP $ to-pathp {A = Ξ» j β A (~ j)} (Ξ» i β p (~ i)) from-pathpβ» : PathP A x y β x β‘ coe1β0 A y from-pathpβ» p = sym $ from-pathp (Ξ» i β p (~ i))
Itβs actually fairly complicated to show that the functions to-pathp and from-pathp are inverses. The statements of the theorems are simple:
to-from-pathp : β {β} {A : I β Type β} {x y} (p : PathP A x y) β to-pathp (from-pathp p) β‘ p from-to-pathp : β {β} {A : I β Type β} {x y} (p : coe0β1 A x β‘ y) β from-pathp {A = A} (to-pathp p) β‘ p
The proof is a bit hairy, since it involves very high-dimensional hcomps. We leave it under this fold for the curious reader, but we encourage you to take to-from-pathp and from-to-pathp on faith otherwise.
to-from-pathp {A = A} {x} {y} p i j = hcomp-unique (β j) (Ξ» { k (k = i0) β coe0βi A j x ; k (j = i0) β x ; k (j = i1) β coeiβ1 A k (p k) }) (Ξ» k β inS (transp (Ξ» l β A (j β§ (k β¨ l))) (~ j β¨ k) (p (j β§ k)))) i from-to-pathp {A = A} {x} {y} p i j = hcomp (β i β¨ β j) Ξ» where k (k = i0) β coeiβ1 A (j β¨ ~ i) $ transp (Ξ» l β A (j β¨ (~ i β§ l))) (i β¨ j) $ coe0βi A j x k (j = i0) β slide (k β¨ ~ i) k (j = i1) β p k k (i = i0) β coeiβ1 A j $ hfill (β j) k Ξ» where k (k = i0) β coe0βi A j x k (j = i0) β x k (j = i1) β p k k (i = i1) β hcomp (β k β¨ β j) Ξ» where l (l = i0) β slide (k β¨ j) l (k = i0) β slide j l (k = i1) β p (j β§ l) l (j = i0) β slide k l (j = i1) β p (k β§ l) where slide : coe0β1 A x β‘ coe0β1 A x slide i = coeiβ1 A i (coe0βi A i x)
Path Spacesπ
A large part of the study of HoTT is the characterisation of path
spaces. Given a type A
, what does
Path A x y
look like? Hedbergβs theorem says that for
types with decidable equality, itβs boring. For the circle, we can prove its loop
space is the integers β we have
Path SΒΉ base base β‘ Int
.
Most of these characterisations need machinery that is not in this module to be properly stated. Even then, we can begin to outline a few simple cases:
Ξ£ Typesπ
For Ξ£ types, a path between
(a , b) β‘ (x , y)
consists of a path
p : a β‘ x
, and a path between b
and
y
laying over p
.
Ξ£-pathp : β {a 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 (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 universeSSetΟ
, 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 thatA β B
is fibrant wheneverB : Type
andA : Type
orA : IUniv
- i.e. function typesI β A
were made fibrant wheneverA
is.β©οΈ