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  _≡ⁱ_

  variable
    ℓ : Level
    A B : Type ℓ
    f g : A → B
    x y : A

Paths and the interval🔗

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

In the homotopy theory of topological spaces, paths in a space $A$ are defined to be continuous mappings $f:[0,1]\to A$ from the interval to our space. The key idea behind cubical type theory, and thus our implementation Cubical Agda, is that by axiomatizing the important properties of $[0,1]$ as an interval type $\mathbb{I}\text{,}$ we could similarly define paths to be functions $\mathbb{I}\to A\text{.}$ 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.

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

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

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

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

private
  to-path : ∀ {ℓ} {A : Type ℓ} (f : I → A) → f i0 ≡ f i1
  to-path f = λ i → f i

The easiest path to construct is reflexivity, called refl for short: Given a point $a:A\text{,}$ there is a distinguished path ${\mathrm{refl}}_a:a\equiv a\text{,}$ which goes from $a$ to $a$ by ignoring the interval variable $i$ entirely.

refl : ∀ {ℓ} {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} i = x

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

module _ {ℓ} {A : Type ℓ} {a b : A} {p : a ≡ b} where private
  apply-path : (i : I) → A
  apply-path i = p i

  left-endpoint : p i0 ≡ a
  left-endpoint = refl

  right-endpoint : p i1 ≡ b
  right-endpoint = refl

Dependent paths🔗

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

If we have a line of types $A:\mathbb{I}\to \mathrm{Type}\text{,}$ and inhabitants $a:A(i0)$ and $b:A(i1)\text{,}$ we can form the dependent path space between them: the type $\mathrm{PathP}Aab\text{,}$ which in the code is written PathP A a b. Here, inferring the line $A$ is basically always impossible, so we’ll always write it explicitly. As before, these correspond 1-1 to dependent functions which map the endpoints to $a$ and $b\text{.}$ To avoid repetition, we’ll take this opportunity to write out the typing rules, if that helps.

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

Above, we have a blob representing the type of types, Type, which is on the bottom of the image. The line of types $A$ is drawn as a literal path between the points $A(i0)$ and $A(i1)$ in this space. On top, we have the points $a$ and $b\text{,}$ which “lie over” their respective types. And finally, our $p:\mathrm{PathP}Aab$ is path from $a$ to $b$ over the path $A\text{.}$

Even though we introduced Path first, the PathP connective, being more general, is the actual primitive provided by Agda. The path type $a\equiv b\text{,}$ and its longhand $\mathrm{Path}Aab\text{,}$ are defined in terms of PathP.

Path : ∀ {ℓ} (A : Type ℓ) (x y : A) → Type ℓ
Path A x y = PathP (λ i → A) x y

Symmetry🔗

Now that we have the notion of paths, we’ll spend the rest of this module setting up the structure around them that makes them useful. A good place to start with are the inverses: there should be an operation mapping paths $p:a\equiv b$ to paths $p^{-1}:b\equiv a\text{.}$ In Cubical Agda, we work in de Morgan cubical type theory. This means that, in addition to the endpoints $i0,i1\text{,}$ 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 $\neg i$ in the prose and ~_ in the formalisation. In addition to interacting with the other operations, the negation satisfies $\neg i0=i1$ and $\neg i1=i0\text{,}$ and $\neg (\neg i)=i\text{.}$ The first two imply that we can use it to implement inverses: for if we have $p:a\equiv b\text{,}$ then $q=\lambda i.p(\neg i)$ satisfies $q(i0)=p(i1)=b$ and $q(i0)=p(i1)=a\text{.}$

sym : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
sym p i = p (~ i)

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

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 $\neg \neg i=i\text{,}$ these operations are both definitional involutions. Once we implement path composition, we’ll be able to show that $p^{-1}$ is legitimately the inverse to $p\text{.}$

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 $n$ interval variables expresses a way of mapping the $n\text{-cube}$ into that type. So far, we have been talking about mapping the $1\text{-cube,}$ i.e. the line, into types, producing identifications. But the type of paths $a\equiv b$ is itself a type, so if we have $p,q:a\equiv b\text{,}$ we can form the iterated path type $p\equiv q\text{.}$ Cubically, we’re now talking about functions $\mathbb{I}\to \mathbb{I}\to A\text{,}$ with two dimensions: a way of mapping the square into a type.

If we consider a path $p:a\equiv b$ as an object in its own right, we can consider the reflexivity path ${\mathrm{refl}}_p:p\equiv p\text{,}$ which by the paragraph above lives one dimension higher. In this section, we’ll explore the other ways in which we can lift $n\text{-cubes}$ to $n+1$ 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 $i$ and $j\text{):}$ to use our path $p\text{,}$ which only varies along one dimension, we must either discard one of $i$ or $j\text{,}$ or find a way to combine them. Discarding is the easier option. Depending on what dimension we ignore, we get one of two squares, both of which have two $p$ faces across from eachother. Note that the square drop-i is just the reflexivity path refl.

  drop-i : PathP (λ i → a ≡ b) p p
  drop-i i j = p j

  _ : drop-i ≡ refl
  _ = refl

  drop-j : PathP (λ i → p i ≡ p i) refl refl
  drop-j i j = p i

Let’s look at how to visualise these squares. First, we should note the direction our axes go in: $i$ varies from the left to the right, and $j$ varies top-to-bottom. The drop-i square is constant in the $i$ direction, but in the $j$ direction, it’s $p\text{.}$ This manifests in the diagram as having $\mathrm{refl}$ for both of its vertical faces: on the left, we’re looking at $p(i0)=a$ not varying along the vertical axis, and respectively for $p(i1)=b$ on the right. For the drop-j square, the situation is flipped, since we’re now ignoring the horizontal direction.

  ∧-conn : PathP (λ i → a ≡ p i) refl p
  ∧-conn i j = p (i ∧ j)

  ∨-conn : PathP (λ i → p i ≡ b) p refl
  ∨-conn i j = p (i ∨ j)

These correspond to the following two squares, called connections. In the diagrams below, we do not have the space to include the computation for the faces that vary along $j\text{,}$ but we did include them for the faces varying along $i\text{,}$ e.g., in the $p(i\wedge j)$ square, the left face (varying along $j\text{,}$ with $i=i0\text{)}$ is $$p(i0\wedge j)=p(i0)=a\text{,}$$ while the right face in $p(i\vee j)$ is $$p(i1\vee j)=p(i1)=b\text{.}$$

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

Intuitively, we may read this square as saying that the composites $q\cdot r$ and $p\cdot s$ are identified.¹ In the 1Lab, we define the type Square so that the arguments are given in the order $p\text{-}$$q\text{-}$$s\text{-}$$r\text{,}$ i.e. top-left-right-bottom. This choice is basically arbitrary, but it matters when reading out the (graphical) boundary from the type of a term.

Square
  : ∀ {ℓ} {A : Type ℓ} {a00 a01 a10 a11 : A}
  → (p : a00 ≡ a01) (q : a00 ≡ a10) (s : a01 ≡ a11) (r : a10 ≡ a11)
  → Type ℓ
Square p q s r = PathP (λ i → p i ≡ r i) q s

To start building some intuition, we can rewrite the dimension-raising operations we named above so that their types are given in terms of Square. We also ask Agda to check that a square with top/bottom faces refl, but left/right faces $p\text{,}$ 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 $\alpha :\mathrm{Square}pqsr\text{,}$ 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 $f:A\to B\text{,}$ and $x=y:A\text{,}$ then also $f(x)=f(y)\text{.}$ In our homotopical setting, we must generalise this to talking about paths $p:x\equiv y\text{,}$ and we must also name the resulting $f(x)\equiv f(y)\text{.}$ In cubical type theory, our homotopical intuition for paths provides the both the interpretation and implementation of this principle: it is the composition of a path $p:x\equiv y$ with a continuous function $f:A\to B\text{.}$

ap : ∀ {a b} {A : Type a} {B : A → Type b}
   → (f : ∀ x → B x) {x y : A} (p : x ≡ y)
   → PathP (λ i → B (p i)) (f x) (f y)
ap f p i = f (p i)

{-# NOINLINE ap #-}

The type of the function above is perhaps a bit more general than initially expected: we talk not about types $A,B$ and a function $f:A\to B\text{,}$ but instead about a type $A\text{,}$ a type family $B(-)$ over $A\text{,}$ and a dependent function $(x:A)\to B(x)\text{.}$ While the values $f(x)$ and $f(y)$ live in different points of the family $B\text{,}$ if we have a $p:x\equiv y\text{,}$ the types $B(x)$ and $B(y)$ are themselves identical. Therefore, we can define the composition of a dependent function with a path, producing a dependent path in the codomain.

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

apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
    → (f : ∀ i (a : A i) → B i a) {x : A i0} {y : A i1}
    → (p : PathP A x y)
    → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
apd f p i = f i (p i)

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

_
  : ∀ {a b} {A A' : Type a} {B : A → Type b} {B' : A' → Type b}
      {f : ∀ x → B x} {g : ∀ x → B' x} {x : A} {y : A'}
  → {pa : A ≡ A'} {pb : PathP (λ i → pa i → Type b) B B'}
  → (pf : PathP (λ i → ∀ x → pb i x) f g)
  → (px : PathP (λ i → pa i) x y)
  → PathP (λ i → pb i (px i)) (f x) (g y)
_ = λ pf px → apd (λ i → pf i) px

ap₂
  : ∀ {a b c} {A : Type a} {B : A → Type b} {C : (x : A) → B x → Type c}
      (f : (x : A) (y : B x) → C x y) {x y : A} {α : B x} {β : B y}
  → (p : x ≡ y) (q : PathP (λ i → B (p i)) α β)
  → PathP (λ i → C (p i) (q i)) (f x α) (f y β)
ap₂ f p q i = f (p i) (q i)

Under the correspondence between homotopy theory and higher category theory, we would say that ap expresses that functions are functors from their domain to their codomain. Accordingly, we would expect that ap preserves identities (i.e. $\mathrm{refl}\text{)}$ 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 $P(x)$ and $x=y\text{,}$ then also $P(y)\text{.}$ In type theory, this is generalised: we’re not only talking about predicates $P(-)\text{,}$ but rather type families $P(-)\text{,}$ which have values; and we do not simply have $x=y\text{,}$ but rather a specific path $p:a\equiv b\text{.}$

In Cubical Agda, the relevant primitive is the function transp, whose type is a slight generalisation of the transport operation below. We’ll focus on transport for now. To start with, this is where paths show their difference from the notion of equality in set-level type theories: it says that we have a function from paths $p:A\equiv B$ to functions $A\to B\text{.}$ However, it’s not the case that every $p,q:A\to B$ gives back the same function $A\to B\text{.}$ Which function you get depends on (and determines) the path you put in!

transport : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A → B
transport p = transp (λ i → p i) i0

As a concrete example, it can be shown that the type Bool ≡ Bool has exactly two inhabitants (see here), which would be traditionally be read as saying something like “the set of booleans is equal to itself in two ways”. As mentioned before, we reserve the terminology “$a$ and $b$ are equal” for when there is at most one $a\equiv b\text{;}$ instead, the situation with Bool should be read as “there are two identifications of Bool with itself.”

By composing our new transport with the ap from the last section, we can derive the promised indiscernibility of identicals, which we call subst. Here, we’ll note that the function $P(x)\to P(y)$ you get depends on both the path $p:a\equiv b$ and the type family $P(-)\text{.}$

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 $\phi :\mathbb{I}\text{.}$ This is the first instance of the interval naming formulas: rather than being an endpoint, the argument $\phi$ specifies where the path is constant. When an element $\phi :\mathbb{I}$ is taken to be a formula, we interpret it to be the proposition $\phi =i1\text{.}$

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 $\phi =i1$ says the path is constant, transporting is definitionally the identity:

_ : ∀ {ℓ} {A : Type ℓ} → transp (λ i → A) i1 ≡ id
_ = refl

To define the high-level transport, we had to set $\phi =i0\text{,}$ 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 $\phi$ 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, $\lambda i.A$ is always a constant function, so the side-condition is satisfied. Therefore, we can compute the endpoints of the path. When $i=i0\text{,}$ we have exactly transport refl x; but when $i=i1\text{,}$ the entire transp computes away, and we’re left with just $x\text{.}$ 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 $\mathrm{PathP}px\mathrm{transport}px\text{.}$

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 $\neg i=i1$ (i.e. $i=i0\text{),}$ the line is $\lambda j.p(i0\wedge j)=\lambda j.A\text{,}$ which is constant. Moreover, its body computes to $\mathrm{transp}\lambda j.Ai1x=x$ on $i0$ and to $\mathrm{transp}pi0x=\mathrm{transport}px$ on the right, so the endpoints are correct.

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 $A(i)$ and $B(i)\text{,}$ we can form the product type $A(i)\times B(i)\text{.}$ The transport operation, in this case, is componentwise. There isn’t much else we could do!

  _ : transport (λ i → A i × B i) (a , b) ≡ (transport A a , transport B b)
  _ = refl

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

  _ : {f : A i0 → B i0}
    → transport (λ i → A i → B i) f
    ≡ λ x → transport B (f (transport (sym A) x))
  _ = refl

module _ {A : I → Type} {B : (i : I) → A i → Type} where private

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

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

We’re now faced with the conundrum of transporting $y_0$ along $B\text{.}$ But we can’t take the line to be $\lambda i.B(i,x_0)$ since $x_0:A(i0)\text{,}$ while the argument to $B(i,-)$ should be in $A(i)\text{!}$ The solution is to generalise $x_0$ to a line

so that we may form $\lambda i.B(i,x_i)$ connecting $B(i0,x_0)$ and $B(i1,x)\text{.}$ While this construction seems to have come out of nowhere, note that $x_i$ is the inverse of transport-filler along $A^{-1}\text{!}$ We can then obtain our return value by transporting $y_0$ along this line.

  _ : {f : (x : A i0) → B i0 x} → transport (λ i → (x : A i) → B i x) f ≡
    λ (x : A i1) →
      let
        xi : ∀ i → A i
        xi i = transport-filler (λ i → A (~ i)) x (~ i)

        y0 = f (xi i0)
      in transport (λ i → B i (xi i)) y0
  _ = refl

The case for dependent sums (i.e. general Σ types) also involves a filler, but no negations.

  _ : {x : A i0} {y : B i0 x} → transport (λ i → Σ (A i) (B i)) (x , y) ≡
    let
      xi : ∀ i → A i
      xi i = transp (λ j → A (j ∧ i)) (~ i) x
    in xi i1 , transport (λ i → B i (xi i)) y
  _ = refl

Path induction🔗

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

J : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {x : A}
  → (P : (y : A) → x ≡ y → Type ℓ₂)
  → P x refl → ∀ {y} p → P y p

Seen one way, this is a generalised version of subst, where the type family may also depend on the path — to the syntactically-minded, this is exactly the induction principle for identity qua inductive family; it says that the total space of the identity family ${\Sigma }_{y:A}(x\equiv y)$ is generated by the point $(x,\mathrm{refl})\text{.}$ 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 ${\Sigma }_{y:A}(x\equiv y)$ is the space of paths from $x$ with an endpoint free, the free endpoint being the first coordinate of the pair. Elements in this type are allowed to have whatever right endpoint, and we’re allowed to identify paths with different endpoints. The J rule says that every $(y,p)$ in this type is identical to $(x,\mathrm{refl})\text{.}$ 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 ${\Sigma }_{y:A}(x\equiv y)\text{:}$ the type of elements of $A$ which are identical to $y\text{.}$ Read set-theoretically, it makes sense that this would only have one inhabitant!

Singleton : ∀ {ℓ} {A : Type ℓ} → A → Type _
Singleton x = Σ[ y ∈ _ ] (x ≡ y)

We’re given an inhabitant $y:A$ and a path $p:x\equiv y\text{.}$ To identify $(x,\mathrm{refl})\equiv (y,p)\text{,}$ we have to produce an identification $x\equiv y$ (we can use $p\text{),}$ and, over this, an identification of $\mathrm{refl}$ and $p\text{.}$

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 $$\mathrm{PathP}(\lambda i.x\equiv p(i))\mathrm{refl}p\text{,}$$ which we’ve already seen: not only can it be expressed as a Square, but it is precisely the type of the connection square $p(i\wedge j)\text{:}$

  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 $\mathrm{prefl}:P(x,\mathrm{refl})$ but we want $P(y,p)\text{,}$ we can first identify $(x,\mathrm{refl})\equiv (y,p)\text{,}$ 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 $e:A$ in a context with $n$ interval variables can be pictured as an $n\text{-cube}$ drawn on the type $A\text{.}$ We’re also familiar with the idea that we can place constraints on the values that these cubes take at certain points along the interval: this is what PathP specifies. A value $p:\mathrm{PathP}Axy$ is a line $\lambda i.p(i)$ in $A\text{,}$ which is $x$ when $i=i0$ and $y$ when $i=i1\text{.}$

But what if we want to specify constraints on a cube in higher dimensions? We could iterate PathP types, as done in the definition of Square, but that forces us to specify values at every endpoint. What if we only particularly care about the value at one of the endpoints, or some more complicated sub-shape of an $n\text{-cube?}$ Enter the Partial type former.

When $A$ is a type and $\phi :\mathbb{I}$ is some interval expression, we can form the type $\mathrm{Partial}\phi A$ of partial elements of $A$ with extent $\phi \text{:}$ an element of $A\text{,}$ but which is only defined when $\phi =i1\text{.}$ You can think of a partial element as a function: if you have $p:\mathrm{Partial}\phi A\text{,}$ and you can come up with some evidence $v$ that $\phi =i1\text{,}$ then $p(v):A\text{.}$ Conversely, if you have some $x:A\text{,}$ you can pretend it is a partial element by ignoring the evidence. In Agda, we write IsOne for the type of such evidence, and we write 1=1 for the proof that $i1=i1\text{.}$

The key feature of partial elements is that we can introduce them by giving systems: If you want to define an $f:\mathrm{Partial}(\phi \vee \psi )A\text{,}$ it suffices to give $x:\mathrm{Partial}\phi A$ and $y:\mathrm{Partial}\psi A\text{,}$ as long as they agree when $(\phi =i1)\wedge (\psi =i1)\text{.}$

For instance, if we have a dimension $i:\mathbb{I}\text{,}$ then the type $\mathrm{Partial}(i\vee \neg i)A$ represents the endpoints of a line in $A\text{.}$ We do not have a complete line, just the endpoints! As an example, we can define a value of Bool which is true on the left endpoint of the interval, and false on the right endpoint.

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

Graphically, our not-a-path is represented by the following rather boring shape: two disconnected points, with completely unrelated values at each endpoint of the interval.

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

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

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

Extensibility🔗

The next type former we’ll introduce lets us turn a partial element into a constraint. Much like the Path type constrains its inhabitants to have matching endpoints definitionally, the extension types let us carve out the subtype of $A$ which definitionally agree with a given partial element. If we have a $p:\mathrm{Partial}\phi A\text{,}$ then we can form the type $A[\phi \mapsto p]\text{.}$

The introduction rule, internalized as the constructor inS, says that, if we have a totally-defined element $e:A$ which satisfies $\phi ⊢e=p$ (i.e. which agrees with $p$ wherever it is defined), then we can form $\mathrm{inS}e:A[\phi \mapsto p]\text{.}$ The elimination rule says that, if $e:A[\phi \mapsto p]\text{,}$ then we can obtain an element $\mathrm{outS}e:A\text{;}$ and moreover, $\phi ⊢\mathrm{outS}e=p\text{.}$

With the type theory aside, let’s get to examples. Suppose we have a partial element of Bool which is true on the left endpoint of the interval, and undefined elsewhere. This is a partial element with one interval variable, so it would be extended by a path — a 1-dimensional cube. The reflexivity path is a line in Bool, which is true on the left endpoint of the interval (in fact, it is true everywhere), so we say that refl extends this partial element.

Diagramatically, we’ll depict extensions by drawing the relevant partial element in red, and the total element in black. In Agda, we write extension types using the type former _[_↦_], which is written mixfix as A [ φ ↦ p ]. We can formalise the red-black extensibility diagram above by defining the partial element left-true, and giving refl to inS, the constructor for _[_↦_].

private
  left-true : (i : I) → Partial (~ i) Bool
  left-true i (i = i0) = true

  refl-extends : (i : I) → Bool [ (~ i) ↦ left-true i ]
  refl-extends i = inS (refl {x = true} i)

Slightly more preicsely, the constructor inS expresses that any totally-defined cube $u$ can be seen as a partial cube, which simply agrees with $u$ for any choice of formula $\phi \text{.}$ To introduce elements of specific extensions, we use the fact that partial elements are definitionally equal as long as they are definitionally equal on their intersections. This might be a bit abstract, so let’s diagram the case where we have some square $a\text{,}$ and the partial element has formula $i\vee j\text{.}$ 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.²

  not-extensible
    : ((i : I) → Bool [ (~ i ∨ i) ↦ not-a-path i ])
    → true ≡ false
  not-extensible ext i = outS (ext i)

This counterexample demonstrates the eliminator for _[_↦_], outS, which we have already mentioned. However, we can also demonstrate its computation rule. In the code below, even though x is abstract, we know that outS agrees with the partial element u.

  _ : ∀ {A : Type} {u : Partial i1 A} {x : A [ i1 ↦ u ]}
    → outS x ≡ u 1=1
  _ = refl

Box filling🔗

Using the notions of partial elements and extensibility, we can define a higher-dimensional generalisation of the notion of binary path composition: the homogeneous composition operation, hcomp. This is one of the fundamental tools for working with higher-dimensional types in cubical type theory: it lets us reduce many problems of path algebra to formulating partial elements expressing their solutions.

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

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

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

  composite : w ≡ z
  composite i = hcomp (i ∨ ~ i) (shape i)

In this situation, we picture hcomp as filling the face opposite $j=i0\text{.}$

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

then we can obtain an extension $A[\phi \mapsto e(i1)]\text{.}$ The idea of the extra $i$ dimension is that we’re forced to give a connected shape: $i$ is disjoint from any of the variables in $\phi \text{,}$ so we have to give at least something (the value $e(i0)\text{).}$ This means that we can’t use hcomp to produce an extension of our not-a-path system, for example, since it would be impossible to make it connected in the first place!

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

hfill : ∀ {ℓ} {A : Type ℓ} (φ : I) → I
      → ((i : I) → Partial (φ ∨ ~ i) A)
      → A
hfill φ i u = hcomp (φ ∨ ~ i) λ where
  j (φ = i1) → u (i ∧ j) 1=1
  j (i = i0) → u i0 1=1
  j (j = i0) → u i0 1=1

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 $p^{-1}\cdot (p\cdot \cdot q\cdot \cdot r)=q\cdot r\text{.}$

··-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 $\mathrm{refl}\cdot (p\cdot q)=p\cdot q\text{.}$

_∙_
  : ∀ {ℓ} {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  _∙_

We’ll leave this section with a composition operation that works for dependent paths. This is a nice combination of fillers and CCHM composition: it takes proofs that $x\equiv y$ over $p$ and $y\equiv z$ over $q\text{,}$ and produces a path witnessing that $x\equiv z$ over $p\cdot q\text{.}$ 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  _∙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 $p$ and $q$ are variables. But what does it reduce to? A natural attempt would be to say that, at a point $i:\mathbb{I}\text{,}$ the path $\mathrm{transport}(\lambda i..x\equiv q(i))p$ is $t=\mathrm{transport}(\lambda i..A)p(i)$ — i.e., transport of paths is, pointwise, transport along the base. But this can’t be the case, since $t$ has endpoints

which are both wrong! More saliently, this attempt makes no use of the path $q$ at all, so there’s no way it can be right. However, the endpoints are propositionally correct. What we need is a way to correct the endpoints after transporting the base, using an arbitrary path. But this is exactly what hcomp lets us do! The real normal form of our transport is the dashed path in the diagram below, where we abbreviate $\mathrm{transp}(\lambda i.A)\phi x$ as $\mathrm{tr}\phi x\text{:}$

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

_ : {x y z : A} {p : x ≡ y} {q : y ≡ z} →
  let
    tr : (φ : I) (a : A) → A
    tr φ a = transp (λ i → A) φ a

    the-hcomp : x ≡ z
    the-hcomp i = hcomp (∂ i) λ where
      j (j = i0) → tr i0 (p i)
      j (i = i0) → tr j x
      j (i = i1) → tr j (q j)
  in (p ∙' q) ≡ the-hcomp
_ = refl

More generally, we can demonstrate the computation rule in an arbitrary PathP. It’s a straightforward generalisation of the construction above: We have a square of types $A(i,j)\text{,}$ and lines of endpoints $x(i):A(i,i0)$ and $y(i):A(i,i1)\text{.}$ Writing

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

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 $p\neg j\text{)}$ is the $k=i0$ face, and the red face is the $k=i1$ face.

However, even though the diagram is very busy, most of the detail it contains can be ignored. Reading it in the left-right direction, it expresses an identification between α-filler j k and β-filler j k, lying over a homotopy α = β. That homotopy is what you get when you read the bottom square of the diagram in the left-right direction. Explicitly, here is that bottom square:

Note that, exceptionally, this diagram is drawn with the left/right edges going up rather than down. This is to match the direction of the 3D diagram above. The colours are also matching.

Readers who are already familiar with the notion of h-level will have noticed that the proof ··-unique expresses that the type of double composites p ·· q ·· r is a proposition, not that it is contractible. However, since it is inhabited (by _··_··_ and its filler), it is contractible:

··-contract : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
            → (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
            → (β : Σ[ s ∈ (w ≡ z) ] Square (sym p) q s r)
            → (p ·· q ·· r , ··-filler p q r) ≡ β
··-contract p q r β = ··-unique p q r _ β

∙-unique
  : ∀ {ℓ} {A : Type ℓ} {x y z : A} {p : x ≡ y} {q : y ≡ z}
  → (r : x ≡ z)
  → Square refl p r q
  → r ≡ p ∙ q
∙-unique {p = p} {q} r square i =
  ··-unique refl p q (_ , square) (_ , (∙-filler p q)) i .fst

··-unique' : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
           → {p : w ≡ x} {q : x ≡ y} {r : y ≡ z} {s : w ≡ z}
           → (β : Square (sym p) q s r)
           → s ≡ p ·· q ·· r
··-unique' β i = ··-contract _ _ _ (_ , β) (~ i) .fst