module 1Lab.Path where
open Prim.Extension public open Prim.Interval public open Prim.Kan hiding (module hcomp-sys ; module comp-sys) 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 as a space, then for a pair of points the identity type behaves like the space of paths from to in There is a constant path at each point; every path has an inverse paths and can be laid end-to-end, giving the composite Even further, these operations can be shown to satisfy algebraic laws, like the inverse law but only up to paths-between-paths: homotopies.
In the homotopy theory of topological spaces, paths in a space are defined to be continuous mappings 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 as an interval type we could similarly define paths to be functions 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
“
and
are equal” when the type
is inhabited, but in this development we reserve this terminology for
the case where
and
inhabit a set,
i.e. when there can be at most one
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.
While the type is meant to represent the unit interval 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 its start and end. If we have an arbitrary we say that it is a path from to 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 to .
However, we can not internally define the type of “functions which satisfy and ”; 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 to .
This type, like any other, has formation and elimination rules. Informally, the formation rule says that any function can be made into a path and the elimination rule says that if we have and a path we can apply and get out a value of 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 from the points we write the type of paths as 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 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
there is a distinguished path
which goes from
to
by ignoring the interval variable
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 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 to dependent functions 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
and inhabitants
and
we can form the dependent path space between them: the
type
which in the code is written PathP A a b
. Here, inferring
the line
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
and
To avoid repetition, we’ll take this opportunity to write out the typing
rules, if that helps.
Colloquially, we speak of a value as a path between and over . Formally, the idea is that, while and may live in different types, is an identification between them; and, over this identification, and 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
is drawn as a literal path between the points
and
in this space. On top, we have the points
and
which “lie over” their respective types. And finally, our
is path from
to
over the path
Even though we introduced Path
first, the PathP
connective, being
more general, is the actual primitive provided by Agda. The
path type
and its longhand
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 to paths In Cubical Agda, we work in de Morgan cubical type theory. This means that, in addition to the endpoints 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
in the prose and ~_
in the
formalisation. In addition to interacting with the other operations, the
negation satisfies
and
and
The first two imply that we can use it to implement inverses: for if we
have
then
satisfies
and
sym : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x sym p i = p (~ i)
We can also invert dependent paths: if and are identified over a line then and are identified over the inverse of
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 these operations are both definitional involutions. Once we implement path composition, we’ll be able to show that is legitimately the inverse to
_ : symP (symP p) ≡ p _ = refl
Raising dimension🔗
To recap, in cubical type theory, a term in a context with interval variables expresses a way of mapping the into that type. So far, we have been talking about mapping the i.e. the line, into types, producing identifications. But the type of paths is itself a type, so if we have we can form the iterated path type Cubically, we’re now talking about functions with two dimensions: a way of mapping the square into a type.
If we consider a path as an object in its own right, we can consider the reflexivity path which by the paragraph above lives one dimension higher. In this section, we’ll explore the other ways in which we can lift to cubes, and to higher dimensions from there.
In a context with two interval variables, we can move in two
dimensions (call them
and
to use our path
which only varies along one dimension, we must either
discard one of
or
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
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:
varies from the left to the right, and
varies top-to-bottom. The drop-i
square is
constant in the
direction, but in the
direction, it’s
This manifests in the diagram as having
for both of its vertical faces: on the left, we’re looking at
not varying along the vertical axis, and respectively for
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 and maximum, As we’ll see below, these satisfy the familiar rules for conjunctions and disjunctions in logic, hence the notation. But keep in mind that is not like but rather more like we do not have because there are points along the interval where the “minimum” of and “” 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 but we did include them for the faces varying along e.g., in the square, the left face (varying along with is while the right face in is
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 and as in the diagram below.
Intuitively, we may read this square as saying that the
composites
and
are identified.1 In the 1Lab, we define the type
Square
so that the
arguments are given in the order
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
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 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 and then also In our homotopical setting, we must generalise this to talking about paths and we must also name the resulting 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 with a continuous function
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 and a function but instead about a type a type family over and a dependent function While the values and live in different points of the family if we have a the types and 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.
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 and then also In type theory, this is generalised: we’re not only talking about predicates but rather type families which have values; and we do not simply have but rather a specific path
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
to functions
However, it’s not the case that every
gives back the same function
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
“
and
are equal” for when there is at most one
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
you get depends on both the path
and the type family
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
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
is taken to be a formula, we interpret it to be the proposition
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
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
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,
is always a constant function, so the side-condition is satisfied.
Therefore, we can compute the endpoints of the path. When
we have exactly transport refl x
; but when
the entire transp
computes away, and we’re left with just
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
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.e. the line is which is constant. Moreover, its body computes to on and to 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 and we can form the product type 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 but the only way we have to get a is by applying We first transport along to get then apply to get something in and finally transport along to get something in 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 and a line of type families over If we have how do we send an to something in
As before, we can start by producing something in by transporting backwards, and applying This gives us the values
We’re now faced with the conundrum of transporting along But we can’t take the line to be since while the argument to should be in The solution is to generalise to a line
so that we may form
connecting
and
While this construction seems to have come out of nowhere, note that
is the inverse of transport-filler
along
We can then obtain our return value by transporting
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
is generated by the point
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 is the space of paths from 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 in this type is identical to 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 the type of elements of which are identical to 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 and a path To identify we have to produce an identification (we can use and, over this, an identification of and
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
which we’ve already seen: not only can it be expressed as a
Square
, but it is precisely the type of the connection
square
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 but we want we can first identify 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
in a context with
interval variables can be pictured as an
drawn on the type
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
is a line
in
which is
when
and
when
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
Enter the Partial
type former.
When
is a type and
is some interval expression, we can form the type
of partial elements of
with extent
an element of
but which is only defined when
You can think of a partial element as a function: if you have
and you can come up with some evidence
that
then
Conversely, if you have some
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
The key feature of partial elements is that we can introduce them by giving systems: If you want to define an it suffices to give and as long as they agree when
For instance, if we have a dimension
then the type
represents the endpoints of a line in
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
which definitionally agree with a given partial element. If we
have a
then we can form the type
The introduction rule, internalized as the constructor inS
, says that, if we have
a totally-defined element
which satisfies
(i.e. which agrees with
wherever it is defined), then we can form
The elimination rule says that, if
then we can obtain an element
and moreover,
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
can be seen as a partial cube, which simply agrees with
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
and the partial element has formula
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
In general, hcomp
allows us to build an
cube, with a boundary of our choice, by expressing it as the missing
face in some
shape. Its actual interface says that, if we have some shape
and a partial element
then we can obtain an extension
The idea of the extra
dimension is that we’re forced to give a connected shape:
is disjoint from any of the variables in
so we have to give at least something (the value
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
face of the open
but the semantics guarantees the existence of the
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
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) sys module ··-sys where sys : ∀ j → Partial (∂ i ∨ ~ j) _ sys j (i = i0) = p (~ j) sys j (i = i1) = r j sys j (j = i0) = q i
{-# DISPLAY hcomp _ (··-sys.sys {ℓ} {A} {w} {x} {y} {z} p q r i) = _··_··_ {ℓ} {A} {w} {x} {y} {z} p q r 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
··-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
_∙_ : ∀ {ℓ} {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 over and over and produces a path witnessing that over 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
and
are variables. But what does it reduce to? A natural attempt
would be to say that, at a point
the path
is
— i.e., transport of paths is, pointwise, transport along the base. But
this can’t be the case, since
has endpoints
which are both wrong! More saliently, this attempt makes no
use of the path
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
as
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
and lines of endpoints
and
Writing
we can ask Agda to check that transporting a to something in 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 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 _ β
∙-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
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
and the composition
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
and points
then we can say that they are “identified over
”
to mean either
or
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 havePathP (λ j → P j) p q
, by the endpoint rule fortransport-filler
.When
i = i1
, we havePathP (λ j → P i1) (transport P p) q
, again by the endpoint rule fortransport-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
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 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 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.