open import 1Lab.Type

open import Prim.Data.Bool
open import Prim.Extension
open import Prim.Interval
open import Prim.Kan

module 1Lab.Path where

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

-- Slightly ugly type to demonstrate the algebraic properties of the
-- interval.
private
data _β‘β±_ (i : I) : (j : I) β SSet where
reflβ± : i β‘β± i

infix 10 _β‘β±_

variable
β : Level
A B : Type β
f g : A β B
x y : A


# Paths and the intervalπ

One of the key observations behind HoTT is that the inductive identity type can be given a spatial interpretation: if we interpret a type 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

module _ {β} {A : I β Type β} {x : A i0} {y : A i1} (p : PathP A x y) where

  _ : 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.

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


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.

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

  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)

module _ {β} {A : Type β} {a b : A} {p q : Path A a b} where private

  _ : 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.

module _ where private
variable
i j : I

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

private

  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

  variable
a a' : A i0
b b' : B i0


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)

inspect : β {a} {A : Type a} (x : A) β Singleton x
inspect x = x , refl


# Compositionπ

In βBook HoTTβ, the primitive operation from which the higher-dimensional structure of types is derived is the J eliminator, with J-refl as a definitional computation rule. This has the benefit of being very elegant: This one elimination rule generates an infinite amount of coherent data. However, itβs very hard to make 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

Note

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

private module _ {A : I β I β Type} {x : β i β A i i0} {y : β i β A i i1} where private

  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.

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!

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 PathPs 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  TODO: Explain these whiskerings _β_ : β {β} {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


1. 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.β©οΈ

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