2.1 The type of paths

It is useful to have a type of paths. Certainly, the most obvious way of obtaining such a type is to use the function type itself. We shall often refer to the type of functions from the interval $\mathbb{I} \to A$ as the line type, and call its terms lines. It is convenient to work with paths with arbitrary endpoints using line types, but as soon as we start considering paths from a particular point to another point, the limitations of this strategy begin to become apparent. In order to better deal with paths with fixed endpoints, we need a slightly more sophisticated variant of the function type called the path type, an internalization of functions from the interval that makes their endpoints fully explicit. Hence given any type $A : \mathcal{U}$ and terms $a, b : A$ , we can form the type of paths starting from a to b in A, which we denote by $\mathsf{path}_{A}(a, b)$ and call the path type of A and a and b. ^{Footnote 1}

What can we do with paths in the path type? Given a path $p : \mathsf{path}_{A}(a, b)$ and an interval variable $i : \mathbb{I}$ , we can apply the path to obtain a term of the type A depending on i, denoted p (i) and called the value of p at position i. Moreover, applying a path to one of the interval endpoints should result in the corresponding endpoint of the path. This means that for every term $p : \mathsf{path}_{A}(a, b)$ , the following endpoint equalities hold definitionally:

\begin{equation*}p (\mathsf{0}) \equiv a : A \quad\text{and}\quad p (\mathsf{1}) \equiv b : A.\end{equation*}

The canonical way to construct paths is by abstraction: given a term $a : A$ which may depend on $i : \mathbb{I}$ , we write $\lambda{i}.{a}$ to indicate a path from $a [{{\mathsf{0}}}/{{i}}]$ to $a [{{\mathsf{1}}}/{{i}}]$ in A, where, by convention, the scope of the binding $\lambda{-}.{}$ extends over the entire expression to its right unless otherwise noted by the use of parentheses.

It should come as no surprise that paths require equalities similar to those common for functions in the lambda calculus. More specifically, when a path abstraction term is applied to an interval point, we require a computation that plays the role of $\beta$ -reduction:

\begin{equation*}(\lambda{i}.{a})( j) \equiv a [{{j}}/{{i}}].\end{equation*}

We also expect that “every path is a path abstraction”, the uniqueness principle for the path type, meaning that we also consider the following $\eta$ -expansion rule:

\begin{equation*}p \equiv \lambda{i}.{(p(i))} \qquad \text{(when} \, {i} \text{does not occur in} \, {p}).\end{equation*}

This identifies any path p with the “path that applies p on the interval”, thus endowing paths with an extensional aspect. The use of this equality is crucial to the derivation of path induction in Section 6.1.

2.2. How we should think of paths

The use of diagrams will play a key role in our visualization of paths, for many cubical type-theoretic problems can be rigorously stated and solved using diagrammatic arguments. How should we think of paths cubically? This view follows naturally from the conception of paths as functions from the interval and the homotopical intuition. First of all, we visualize a term $a : A$ as a point:

\begin{equation*} \cdot \; a\end{equation*}

In the first dimension, we think of a term $p : \mathbb{I} \to A$ as a path from the point $p(\mathsf{0})$ to the point $p(\mathsf{1})$ . Given an interval variable $i : \mathbb{I}$ , such a path can be visualized as an abstract line p(i) in the “direction” i that goes from the initial to the terminal point of the path, as shown in the following diagram:

Extending the interpretation to higher dimensions, it is natural to think of a function $h : \mathbb{I} \to \mathbb{I} \to A$ as a homotopy of paths. Such a homotopy consists of two simultaneous continuous deformations and it can be visualized as an abstract square having four paths at each edges, as shown in the following diagram, where the lines $h(\mathsf{0})$ and $h(\mathsf{1})$ are the bottom and top faces in the direction i, and $\lambda j.h(j, \mathsf{0})$ and $\lambda j.h(j, \mathsf{1})$ the left and right faces in the j-direction, respectively:

In the third dimension, we consider homotopies between homotopies, which, as expected can be pictured as cubes. It is hard enough to visualize paths at even higher dimensions, but, most certainly, the reader can already guess the general pattern here: at dimension $n+1$ , we have $n+1$ -dimensional paths, which can be visualized as hypercubes with $2{(n+1)}$ faces formed by n-dimensional cubes. Finally, it is worth noting that this cubical structure applies for types $A : \mathcal{U}$ as well, since types are just terms of a type of universes.

2.3 How can we use paths?

Already at this stage, we can see how this novel account of paths as functions out of the interval is a significant departure from the traditional approach taken in homotopy type theory (The Univalent Foundations Program 2013), in which the path type is defined as an inductive type generated by a single reflexivity constructor. The following lemmas will serve to show some fundamental differences of the cubical approach.

We start with the fact that a term analogous to this reflexivity constructor is definable by considering constant functions from the interval, thus providing us a way to trivially regard terms as degenerate paths.

Lemma 1. For every type A and every $a : A$ , there exists a path

\begin{equation*} \mathsf{path}_{A}(a, a) \end{equation*}

called the reflexivity path of a and denoted $\mathsf{refl}_{a}$ .

Proof. Suppose that $i : \mathbb{I}$ is a fresh interval variable. By assumption, a does not depend on i, meaning that $\lambda{i}.{a}$ gives us a path starting from a to a in A.

Since in the homotopy interpretation we view functions as continuous maps, it is natural to expect that functions preserve paths, as shown in the homotopy type theory book (The Univalent Foundations Program 2013, Section 2.2). Here, we state this property with the following lemma for nondependent functions:

Lemma 2 (Function application (Cohen et al. Reference Cohen, Coquand, Huber and Mörtberg2018; Bezem et al. Reference Bezem, Coquand and Huber2014)) Given a function $f : A \to B$ and terms $a, b : A$ , we have an operation

\begin{equation*} \mathsf{ap}_f : (\mathsf{path}_{A}(a, b)) \to (\mathsf{path}_{B}(f(a), f(b))) \end{equation*}

such that $\mathsf{ap}_f (\mathsf{refl}_{a}) \equiv \mathsf{refl}_{f(a)}$ .

Proof. Given $p : \mathsf{path}_{A}(a, b)$ and an interval variable $i : \mathbb{I}$ , we have $f(p (i)) : B$ , for we can apply $f : A \to B$ to $p(i) : A$ . By abstraction, we have a path

\begin{equation*} \mathsf{ap}_f (p) :\equiv \lambda{i}.{f(p (i))}.\end{equation*}

from f (a) to f (b) in B, since p is a path from a to b. Moreover, we have

\begin{align*} \mathsf{ap}_f (\mathsf{refl}_{a}) &\equiv \lambda{i}.{f(\mathsf{refl}_{a} (i))} \\ &\equiv \lambda{i}.{f(a)} \\ &\equiv \mathsf{refl}_{f(a)} \end{align*}

as requested.

We note that $\mathsf{ap}$ behaves strictly functorially in the sense that the following are definitional equalities for identity functions, compositions of functions, and constant functions (Cohen et al. Reference Cohen, Coquand, Huber and Mörtberg2018; Bezem et al. Reference Bezem, Coquand and Huber2014):

\begin{align*}\mathsf{ap}_{id_A} (p) &\equiv p \\\mathsf{ap}_{f \circ g} (p) &\equiv \mathsf{ap}_{f} (\mathsf{ap}_{g} (p)) \\\mathsf{ap}_{\lambda \_.a} (p) &\equiv \mathsf{refl}_{a}.\end{align*}

In homotopy type theory (The Univalent Foundations Program 2013), in which the path type is defined as an inductive family, those equalities only hold up to homotopy.

Another crucial difference is that, with the cubical notion of path, we are able to prove that two pointwise equal functions are equal up to a path. This is known as function extensionality, a property that cannot be obtained without the use of axioms in homotopy type theory (The Univalent Foundations Program 2013, Section 2.9), Section 4.9. This lack of function extensionality is a common occurrence shared by many intensional forms of dependent type theory (except for observational type theory).

Theorem (Function extensionality (Cohen et al. Reference Cohen, Coquand, Huber and Mörtberg2018)) Suppose that $f, g : \prod_{(x : A)} B(x)$ are functions. There is an operation

\begin{equation*}\mathsf{funext}_{f,g} : \prod_{(x : A)} \mathsf{path}_{B(x)}(f(x), g(x)) \to \mathsf{path}_{\prod_{(x : A)} B(x)}(f, g) \end{equation*}

Proof. If we are given $H : \prod_{(x : A)} \mathsf{path}_{B(x)}(f(x), g(x))$ and an arbitrary $x : A$ , we have a path H(x) from f(x) to g(x) in B(x). For $i : \mathbb{I}$ , H(x) at i gives a path from $\lambda x.f(x)$ to $\lambda x.g(x)$ in $A \to B$ ,

\begin{equation*}\lambda i.\lambda x. (H(x) (i)) : \prod_{(x : A)} B(x). \end{equation*}

By $\eta$ -conversion, it can be seen that this path goes from f to g.

3.1 Transportation along paths

Transport is a cubical generalization of the transport lemma (The Univalent Foundations Program 2013, Lem 2.3.1). Recall that, due to univalence (Voevodsky Reference Voevodsky2009), a principle that characterizes the path space of the universe type $\mathcal{U}$ , a path between types is (equivalent to) a homotopy equivalence between spaces (The Univalent Foundations Program 2013). In the cubical setting, transport states that, given any path between types $A: \mathbb{I} \to \mathcal{U}$ and any term $a : A(i)$ , we have a term of the type A (j), called the transport of a from i to j along A, and denoted by $a^{{{i}} \rightsquigarrow {{j}}}_{A} : A( j)$ . We also require that static transportations have no effect, which means that, when i is j, we have $a^{{i} \rightsquigarrow {i}}_{A} \equiv a$ .

In general, transporting along a degenerate path is not strictly the same as doing nothing, meaning that $a^{{i} \rightsquigarrow {j}}_{\mathsf{refl}_{A}} \not\equiv a.$ This is in contrast with the transport operation of homotopy type theory (The Univalent Foundations Program 2013), in which transportation along reflexivity is taken to be the identity function. The following lemma shows in what sense a generalization of this operation is taking place:

Lemma 3. Given a type family $C : A \to \mathcal{U}$ , terms $a, b : A$ and a path $p : \mathsf{path}_{A}(a, b)$ , there is a function

\begin{equation*} p_* : C(a) \to C(b). \end{equation*}

Proof. Assume we have $c : C(a)$ . Note first that we have a path of types

\begin{equation*}D(p) :\equiv \lambda i.C(p(i)) : \mathbb{I} \to \mathcal{U}\end{equation*}

from C(a) to C(b). The transportation of c from $\mathsf{0}$ to $\mathsf{1}$ along D(p) gives us

\begin{equation*}c^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{D(p)} : C(b)\end{equation*}

as desired.

Although $p_*(\mathsf{refl}_{a})$ is not the identity function up to definitional equality, this can be shown to be the case up to a path.

Lemma 4. For a type family $C : A \to \mathcal{U}$ and $a : A$ , we have a path

\begin{equation*} \mathsf{path}_{C(a) \to C(a)}((\mathsf{refl}_{a})_*, \mathsf{Id}_{C(a)}). \end{equation*}

Proof. The idea is to use function extensionality. By Theorem 2.3, we may assume that $c : C(a)$ . It remains to find a path from $(\mathsf{refl}_{a})_*(c)$ to c. But by definition, $(\mathsf{refl}_{a})_*(c) \equiv c^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda \_.C(a)}$ . Now fix $i : \mathbb{I}$ . We observe that $c^{{i} \rightsquigarrow {\mathsf{1}}}_{\lambda \_.C(a)} : C(a)$ , since $(\lambda \_.C(a))( j) \equiv C(a)$ for any $j : \mathbb{I}$ . But recall that the static transportation $c^{{\mathsf{l}} \rightsquigarrow {\mathsf{1}}}_{\lambda \_.C(a)}$ has no effect, so this term is definitionally equal to c. In other words, $\lambda i. c^{{i} \rightsquigarrow {\mathsf{1}}}_{\lambda \_.C(a)}$ is the path we are looking for.

3.2 Composition of paths

Composition ensures that every open cube in a type can be filled. For example, at dimension one, if we are given adjacent lines $p , q, r : \mathbb{I} \to A$ such that the initial point of p matches the initial point of q and the terminal point of p matches the initial point of r, composition provides a new line, the composite, that goes from the terminal point of q to the terminal point of r.

In fact, composition states more than that. It asserts the existence of the whole square witnessing the filling of the open box (the square in the diagram above). This is called the filler of the composition. When j is $\mathsf{1}$ , the filler gives us the composite, the missing face of the open box. The remaining faces of the filler are the faces of the open box. So, when j is $\mathsf{0}$ , the filler equals p (which we may call the cap of the composition) and when i is $\mathsf{0}$ or $\mathsf{1}$ , it will be q (the left tube) or r (the right tube), respectively. More generally, we refer to any open shape satisfying the relevant adjacency conditions as a composition scenario.

To illustrate the use of composition, we shall now prove symmetry and transitivity for paths with the definition of inverse and concatenation functions. Let us consider the former first. In cubical type theories based on a De Morgan structure (Cohen et al. Reference Cohen, Coquand, Huber and Mörtberg2018; Coquand et al. Reference Coquand, Huber and Mörtberg2018), path inversion comes for free with a primitive (strict) reversal operator but in a cartesian account some work needs to be done to derive it from the Kan operations.

Lemma 5. For every type A and every $a, b : A$ , there is a function

\begin{equation*}\mathsf{path}_{A}(a, b) \to \mathsf{path}_{A}(b, a) \end{equation*}

called the inverse function and denoted $p \mapsto {p}^{-1}$ .

Proof. Suppose that $i, j : \mathbb{I}$ . The idea of the following proof is to observe that $p : \mathsf{path}_{A}(a, b)$ gives a “line” $p ( j) : A$ in the j-direction from a to b in A. Since its initial point is a, we have an open box whose faces are formed by the lines p(j) (left tube), $\mathsf{refl}_{a}(i)$ (cap) and $\mathsf{refl}_{a}( j)$ (right tube). Note that the latter two lines are degenerate, i.e. by definition, they are the same as a. Degeneracy is indicated using double bars in the following diagram:

By composition, this open box must have a lid (top), an i-line from b to a in A, which gives us, by path abstraction, the required path ${p}^{-1}$ .

Fillers of compositions will be relevant to our constructions later on, so it can be convenient to have a special symbolism to talk about them directly. That is the purpose of the following notation:

When no confusion occurs, we may also write it $\mathsf{fill}(p)$ . Thus, the (i,j)-square defined in the proof of Lemma 5 can be denoted by $\mathsf{fill}({p}^{-1}(i))$ .

The next lemma defines path concatenation:

Lemma 7. For every type A and every $a, b, c : A$ , there is a function

\begin{equation*}\mathsf{path}_{A}(a, b) \to \mathsf{path}_{A}(b, c) \to \mathsf{path}_{A}(a, c)\end{equation*}

denoted $ p \mapsto q \mapsto p : \;\mathbin{\tiny\blacksquare} \; q$ . We call $p : \;\mathbin{\tiny\blacksquare} \; q$ the concatenation of p and q.

Proof. Given paths $p : \mathsf{path}_{A}(a, b)$ and $q : \mathsf{path}_{A}(b, c)$ , we can construct an i-line p(i) from a to b and a j-line q(j) from b to c. Once again, we note that we have an open square,

and the path ${p}: \;\mathbin{\tiny\blacksquare} \;{q}$ is obtained by path abstraction on its composite.

We shall make diagrams as explicit as possible throughout the remainder of this paper, but, for the sake of readability, we omit labels for degenerate lines, since the reader should be able to correctly guess the information by checking the endpoints of the line. It is also important to bear in mind that, while we only considered the simplest composition scenario where we compose lines to form squares in the examples above, we can also compose squares to form cubes and, more generally, n-cubes to form $(n+1)$ -cubes. We shall deal with compositions at dimension two in Section 4.1. Composition scenarios at even higher dimensions will not be discussed in this paper.

In addition to the specification of the cap and tubes of an open cube, we also have to admit the specification of diagonals to make composition work properly in a cartesian setting, thereby allowing the diagonal of the filler to be definitionally equal to the designated diagonal (Angiuli et al. Reference Angiuli, Brunerie, Coquand, Hou (Favonia), Harper and Licata2019, 2018). But, as we will not be using diagonals, we do not need to worry about this here.

3.3 The interval is not Kan

We suggested above that every type is Kan. In fact, the interval is the only exception to this rule, since we have been implicitly treating it as a “type”, but it actually does not support any Kan operations. Consider, for example, the identity path on the interval, which goes from $\mathsf{0}$ to $\mathsf{1}$ ,

\begin{equation*}\lambda i.i : \mathsf{path}_{\mathbb{I}}(\mathsf{0}, \mathsf{1}).\end{equation*}

If the interval were Kan, then the identity path would have an inverse. But what could that be in our cartesian setting? Given that the interval lacks some properties required by typehood in a cubical type theory, it is often referred to as a pretype. To deal with this fact, we adopt the convention that the interval can only occur as the antecedent of a function type.

4.1 Weak connections

In cubical type theory, it is useful to have extra kinds of degeneracies known as connections, which can be thought of as meets and joins on the interval. Just as reversals, connections are built-in in a De Morgan setting (Cohen et al. Reference Cohen, Coquand, Huber and Mörtberg2018; Coquand et al. Reference Coquand, Huber and Mörtberg2018). They are not hard to derive in cartesian cubical type theory, but some of the computation rules only hold up to a path (hence we call them “weak” connections).

Lemma 8 (Meet) For every type A and $a, b : A$ , there is an operation

\begin{equation*} - (- \land -) : \mathsf{path}_{A}(a, b) \to \mathbb{I} \to \mathbb{I} \to A \end{equation*}

such that, for any $p : \mathsf{path}_{A}(a, b)$ and any $i, j : \mathbb{I}$ , the following holds:

The proof of this lemma requires a two-extent composition and thus a few remarks are in order here before we proceed. In the one-dimensional case, as we have seen as far, we just have a pair of tubes, so an open square is enough to complete the composition. With two pairs of tubes, each pair corresponding to the dimension in question, we are required to form an open object of the next higher shape, i.e. a cube. In other words, assuming that we want to fill an open (i, j, k)-cube in the j direction, we are expected to determine its (i, k)-face (bottom), two (k, j)-faces (left and right) and two (i, j)-faces (back and front), and those squares must all be adjacent up to definitional equality. If this holds, then the composite is a (i, k)-square. (For the same reasons, performing an n-extent composition requires a construction of an $(n+1)$ -cube).

Finally, it is often convenient to illustrate two-extent compositions using a two-dimensional structure in the form of a cube seen from above. ^{Footnote 2} The following diagram indicates how we shall be drawing two-extent compositions in the paper:

When referring to such diagrams we may call the center and outer squares the top (composite) and the bottom faces of the cube (filler), the top and bottom squares the back and front faces, and the left and right squares the left and right faces, respectively.

Proof. Given $p : \mathsf{path}_{A}(a, b)$ , we are to find a (i,j)-square whose top face is p (i), right face is p (j), left and bottom faces are a. First, by composition, we obtain, for any $i, j : \mathbb{I}$ , a square that looks like a “halfway” connection, called $p(i \land^{*}j)$ .

Note that this square is not the one that we are looking for. Its top face is given by a certain path obtained by composition, which we denote $p^*$ , and this path needs not be definitionally equal to p.

But we are able to fix this mismatch in a higher dimension by attaching this square to the top corner of an otherwise degenerate open cube in such a way that $p(- \land^{*} -)$ forms the back and right faces and the back right edge is $p^*$ . This is depicted in the diagram below, where the bottom, front, and left faces of the open cube are a. We complete the proof with a two-extent composition, whose composite is shown as the shaded face in the diagram:

Before moving on to the next connection, it is worth pointing out that the connections derived here could be slightly improved by attaching squares to the diagonal face of the open cubes of their compositions, thereby making the diagonal of the connections definitionally equal to p.

Lemma 9 (Join) Given a type A and $a, b : A$ , we have an operation:

\begin{equation*} - (- \lor -) : \mathsf{path}_{A}(a, b) \to \mathbb{I} \to \mathbb{I} \to A \end{equation*}

such that, for $p : \mathsf{path}_{A}(a, b)$ and $i, j : \mathbb{I}$ , we have:

Proof. Using the halfway meet connection constructed as part of the previous proof, we perform a two-extent composition on an open cube given by halfway meets (front and left), degenerate squares formed from lines (back and right) and points (bottom). The composite gives us the desired square:

To check that this is a well-formed composition, note that we set a as the bottom (i, k)-face, $p(k \land^* j)$ as the left and $p^*( j)$ as the right (k, j)-faces, $p^* ( j)$ as the back and $p(i \land^* j)$ as the front (k, j)-faces. Those squares are adjacent.

We hope that the reader is starting to get a feel for proofs by composition and the interplay between two-dimensional paths and squares at this point, so we may omit uses of path abstraction without further comment, and we may also leave it up to the reader to show that the cap and tubes displayed in the composition diagrams respect the relevant adjacency conditions.

4.2 The groupoid laws

From the cubical perspective, path equality (homotopy) is always relative, since, viewed as squares, the only way to say that two lines are the same is modulo an identification of two other lines. By contrast, homotopy type theory (The Univalent Foundations Program 2013) has a globular approach. But we can simulate globular identifications of paths by considering certain squares whose remaining faces are degenerate lines.

The groupoid laws are stated using this globular representation. Put differently, when we state that reflexivity is a unit for path inversion and concatenation, that inversion is involutive, and concatenation is associative, for example, we mean that there exists a globular identification between them.

Because the proof is simpler, we start by showing that reflexivity is a right and left unit for path concatenation in the next two lemmas.

Lemma 10 For every A and every $a, b : A$ we have a path

\begin{equation*} \mathsf{ru}_p : \mathsf{path}_{\mathsf{path}_{A}(a, b)}(p, p : \;\mathbin{\tiny\blacksquare} \; \mathsf{refl}_{b}) \end{equation*}

for any $p : \mathsf{path}_{A}(a, b)$ .

Proof. We need to construct an (i, j)-square having p (i) and $(p : \;\mathbin{\tiny\blacksquare} \; \mathsf{refl}_{b}) (i)$ as i-lines and a and b as degenerate j-lines. But this already follows from the filler of concatenation defined in the proof of Lemma 7.

Lemma 11 For every A and every $a, b : A$ we have a path

\begin{equation*}\mathsf{lu}_p : \mathsf{path}_{\mathsf{path}_{A}(a, b)}(p, {\mathsf{refl}_{a}}: \;\mathbin{\tiny\blacksquare} \;{p})\end{equation*}

for any $p : \mathsf{path}_{A}(a, b)$ .

Proof. By composition, we define a helper (i, j)-square that goes from ${p}^{-1} (i)$ to b in the i-direction and from b to p (j) in the j-direction. The composition uses the filler of the path inversion of p (front), meet (right), and degenerate squares formed from lines (back and left) and points (bottom). For future reference, we shall call it $\gamma$ :

Forming a new open cube, we set $\gamma$ at the right, the filler of the concatenation of $\mathsf{refl}_{a}$ and p at the back, the filler of the inversion of p at the bottom, and degenerate squares at the other faces.

Why is the unit property so much simpler to demonstrate in the right? If we look attentively at the filler of path concatenation (Lemma 7), for example,

we can see that it forms a simultaneous identification that can be pronounced “let there be a path from p to $p : \;\mathbin{\tiny\blacksquare} \; q$ just in case q is $\mathsf{refl}_{a}$ ”. Consequently, if we set $q :\equiv \mathsf{refl}_{b}$ , we immediately have a globular path from p to $p : \;\mathbin{\tiny\blacksquare} \; q$ . We can thus compare path concatenation with the transitivity operation defined in the homotopy type theory book by path induction on the second argument (The Univalent Foundations Program 2013, Lem. 2.1.2). The same idea applies to path inversion, “let there be a path from ${p}^{-1}$ to $\mathsf{refl}_{a}$ just in case p is $\mathsf{refl}_{a}$ ”, so it is related to the symmetry operation defined by path induction on p (The Univalent Foundations Program 2013, Lem. 2.1.1).

Next we prove that path inversion indeed is a right and left inverse with respect to concatenation:

Lemma 12 For every A and every $a, b : A$ we have a path

\begin{equation*}\mathsf{rc}_p : \mathsf{path}_{\mathsf{path}_{A}(a, a)}(\mathsf{refl}_{a}, {p}: \;\mathbin{\tiny\blacksquare} \;{{p}^{-1}})\end{equation*}

for any $p : \mathsf{path}_{A}(a, b)$ .

Proof. By composition, we must construct a cube whose composite is an (i, k)-square with $\mathsf{refl}_{a} (i)$ and ${p}: \;\mathbin{\tiny\blacksquare} \;{{p}^{-1}} (i)$ as i-lines and a in both degenerate k-lines. Now consider the following open (i, j, k)-cube

whose bottom, left and right faces are degenerate squares, and back and front squares are, respectively, the fillers for path inversion and concatenation.

Lemma 13. For every A and every $a, b : A$ we have a path

\begin{equation*}\mathsf{lc}_p : \mathsf{path}_{\mathsf{path}_{A}(b, b)}(\mathsf{refl}_{b}, {{p}^{-1}}: \;\mathbin{\tiny\blacksquare} \;{p})\end{equation*}

for any $p : \mathsf{path}_{A}(a, b)$ .

Proof. By composition on the following open cube, whose back face is the $\gamma$ square defined in the proof of Lemma 11.

The following lemma states that path inversion is involutive:

Lemma 14. For every A and every $a, b : A$ , we have a path

\begin{equation*}\mathsf{inv}_p : \mathsf{path}_{\mathsf{path}_{A}(a, b)}(p, {({p}^{-1})}^{-1})\end{equation*}

for any $p : \mathsf{path}_{A}(a, b)$ .

Proof. The proof follows by the use of meets, joins, and $\gamma$ to form the composite:

Last but not least, we want to show that path concatenation is associative.

Lemma 15. For every A and every $a, b, c, d : A$ , we have a path

\begin{equation*}\mathsf{assoc}_{p,q,r} : \mathsf{path}_{\mathsf{path}_{A}(a, d)}((p : \;\mathbin{\tiny\blacksquare} \; q) : \;\mathbin{\tiny\blacksquare} \; r, p : \;\mathbin{\tiny\blacksquare} \; (q : \;\mathbin{\tiny\blacksquare} \; r)) \end{equation*}

for any $p : \mathsf{path}_{A}(a, b)$ , $q : \mathsf{path}_{A}(b, c)$ , $r : \mathsf{path}_{A}(c, d)$ .

Proof. We use the fact that, for any two squares with the same three faces, there is a square showing that the fourth sides are equal. In particular, given the following two squares with definitionally equal bottom, right, and left faces

we can construct the desired path homotopy

Since $\alpha$ is just the filler of path concatenation ${p}: \;\mathbin{\tiny\blacksquare} \;{({q}: \;\mathbin{\tiny\blacksquare} \;{r})}$ , it remains to construct $\beta$ . But this is easy, because looking at the top and right sides of this square, the filler of path concatenation gives us a canonical construction:

What about the higher groupoid structure of types? What we have shown in this section is that types have a 1-groupoid structure, but since those laws do not hold “on the nose” as definitional equations, they must satisfy some equations of their own. We will not cover this here. Instead we give a proof of path induction in Section 6.1, which corresponds almost exactly to the elimination rule for the inductive path type in homotopy type theory (The Univalent Foundations Program 2013) (except that the computation rule here only holds up to a path), and conjecture that it should be possible to derive them with an approach similar to Lumsdaine (Reference Lumsdaine2010).

5.1 The dependent path type

Given a type line $A : \mathbb{I} \to \mathcal{U}$ and terms $a : A(\mathsf{0})$ and $b : A(\mathsf{1})$ , the type of dependent paths from a to b is written $\mathsf{pathd}_{A}(a, b)$ . If the underlying type line is a constant function, that is, the reflexivity path, then the dependent path type is the nondependent path type

\begin{equation*}\mathsf{pathd}_{\lambda \_.A}(a, b) \equiv \mathsf{path}_{A}(a, b).\end{equation*}

The only reason why this equality holds is because nondependent paths are actually defined in terms of dependent paths. So the rules for the dependent path type arise as straightforward generalizations of the ones stated before for path types in virtually the same way the dependent function type generalizes the nondependent function type. For instance, as with nondependent paths, we eliminate a term of this type by application, $p (i) : A(i)$ , where $p : \mathsf{pathd}_{A}(a, b)$ and $i : \mathbb{I}$ . The constructor of this type is path abstraction, and we say that $\lambda{i}.{a} : \mathsf{pathd}_{A}(a[{{\mathsf{0}}}/{{i}}], a[{{\mathsf{1}}}/{{i}}])$ if $a : A(i)$ assuming that $i : \mathbb{I}$ , where $a[{{\mathsf{0}}}/{{i}}] : A(\mathsf{0})$ and $a[{{\mathsf{1}}}/{{i}}] : A(\mathsf{1})$ . Moreover, we also require equalities that are no different from the ones for the ordinary path type. In particular, given $p : \mathsf{pathd}_{A}(a, b)$ and $i : \mathbb{I}$ , we have boundary rules $p (\mathsf{0}) \equiv a : A(\mathsf{0})$ and $p (\mathsf{1}) \equiv b : A(\mathsf{1})$ , and the uniqueness rule $\lambda{i}.{(p(i))} \equiv p$ when i does not occur in p.

We need a type for dependent paths in the cubical setting because in their most general form paths connect terms inhabiting the endpoints of a type line. Consider for example the meet operator defined in Lemma 8. What, exactly, is its type? Starting with an iterated function type

\begin{equation*}\lambda j. \lambda i. p (i \land j) : \mathbb{I} \to \mathbb{I} \to A\end{equation*}

we can obtain a path in the type of paths from a to p (j)

\begin{equation*}\lambda j. \lambda{i}.{p (i \land j)} : \prod_{({j} : {\mathbb{I}})}{{\mathsf{path}_{A}(a, p ( j))}},\end{equation*}

because, given a fixed j, $\lambda i.p(i \land j)$ varies from the point a to p (j). By repeating the process, we obtain a dependent path from $\mathsf{refl}_{a}$ to p in the type of paths from a to p (j)

\begin{equation*}\lambda{j}.{\lambda{i}.{p (i \land j)}} : \mathsf{pathd}_{\lambda i.\mathsf{path}_{A}(a, p (i))}(\mathsf{refl}_{a}, p)\end{equation*}

since $\lambda j.\lambda{i}.{p(i \land j)}$ goes from

\begin{align*}\lambda{i}.{p(i \land \mathsf{0})} \equiv & \ \lambda{i}.{a}\end{align*}

to

\begin{align*}\lambda{i}.{p(i \land \mathsf{1})} \equiv & \ \lambda{i}.{p (i)} \\\equiv & \ p.\end{align*}

In homotopy type theory (The Univalent Foundations Program 2013), a type for dependent paths is definable using the nondependent and inductively defined path type. The advantage of the cubical approach to dependent paths is that they are naturally built-in. It is also worth noting that a type for dependent paths can be defined as multidimensional extension types instead (Angiuli Reference Angiuli2019, p. 67), a generalization of path types that avoid the intricacies that are innate to the use of iterative path types.

5.2 Heterogeneous composition

As soon as we start considering dependent paths, it becomes clear that the path inversion and concatenation operations defined in Section 3.2 are not general enough. Let us consider the limitations of nondependent path inversion first. Assuming that $\mathsf{pathd}_{A}(a, b)$ is a type, where $a : A(\mathsf{0})$ and $b : A(\mathsf{1})$ , the type $\mathsf{pathd}_{A}(b, a)$ of inverse paths from b to a will not be well-formed unless it is also the case that $b : A(\mathsf{0})$ and $a : A(\mathsf{1})$ . For nondependent paths, this condition turns out to be trivially satisfied since the relevant type line is a constant function, meaning that $A(\mathsf{0}) \equiv A \equiv A(\mathsf{1})$ . But as this is not true in general, the operation defined in Lemma 5 fails to produce inverses for dependent paths.

Fortunately, there is a way to deal with this problem using type universes. Suppose we are given a type line $A : \mathbb{I} \to \mathcal{U}$ , that is, a nondependent path from the type $A(\mathsf{0})$ to $A(\mathsf{1})$ in the universe $\mathcal{U}$ ,

\begin{equation*}A : \mathsf{path}_{\mathcal{U}}(A(\mathsf{0}), A(\mathsf{1})).\end{equation*}

We can assume that this is a nondependent path because type universes never depend on interval variables, so we have both $A(\mathsf{0}), A(\mathsf{1}) : \mathcal{U}$ .

Now it can be shown by Lemma 5 that the following inverse exists:

In particular, we have

\begin{equation*}{A}^{-1} : \mathsf{path}_{\mathcal{U}}(A(\mathsf{1}), A(\mathsf{0})),\end{equation*}

which corresponds precisely to the “inverse” type of A, for the initial and terminal points of ${A}^{-1}$ are, respectively, $A(\mathsf{1})$ and $A(\mathsf{0})$ . Put differently, we have two inferences that hold top/bottom and bottom/top,

\begin{equation*}\frac{a : {A}^{-1} (1)}{a : A(\mathsf{0})} \quad\text{and}\quad \frac{a : {A}^{-1} (0)}{a : A(\mathsf{1})}.\end{equation*}

Thus, assuming that $\mathsf{pathd}_{A}(a, b)$ is a type, it is now easy to see that $\mathsf{pathd}_{{A}^{-1}}(b, a)$ will always be a type as well, regardless of whether A is a degenerate line or not: if $\mathsf{pathd}_{A}(a, b)$ is a type then we have $a : A(\mathsf{0})$ and $b : A(\mathsf{1})$ , meaning that $a : {A}^{-1} (1)$ and $b : {A}^{-1} (0)$ must be the case.

This motivates the definition of a dependent path inversion operation:

Lemma 16. For every type $A : \mathbb{I} \to \mathcal{U}$ and every $a : A(\mathsf{0})$ and $b : A(\mathsf{1})$ , there is a function

\begin{equation*}\mathsf{pathd}_{A}(a, b) \to \mathsf{pathd}_{{{A}^{-1}}}(b, a)\end{equation*}

called the (dependent) inverse path and denoted $p \mapsto {p}^{-1}$ .

Proof. Dependent operations are typically introduced by repeating, mutatis mutandis, the proofs of their nondependent counterparts. So, the results which were previously proven by composition will now follow from a “heterogeneous” variant of composition based on the same open cubes. This adaptation is required because we are dealing with nondegenerate type lines and dependent paths, and, for a valid composition, all the faces of an open cube, that is, all the terms of the composition scenario, must have the same type.

More concretely, the open box used in the definition of nondependent path inversion (the one used in the proof of Lemma 5) is ill-formed in this context since $p ( j) : A( j)$ and $a : A(\mathsf{0})$ are lines with different types:

The solution is not to form an open box living in A, but rather to perform a composition taking place in ${A}^{-1}$ , using transport on the type line $\lambda j.\mathsf{fill}_{j}({A}^{-1}(i))$ , the filler of the inverse of A, to adjust the type of the faces of open box.

For the cap, we want to transport a from $\mathsf{0}$ to $\mathsf{1}$ . This gives us the correct type because $\mathsf{fill}_{\mathsf{1}}({A}^{-1}(i))\equiv {A}^{-1}(i)$ . Now we observe that $a : \mathsf{fill}_{\mathsf{0}}({A}^{-1}(i))\equiv {A}(0)$ , so we have

\begin{equation*}{a}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(i))} : {A}^{-1}(i).\end{equation*}

Now for the left tube, i.e. assuming that $i=\mathsf{0}$ , we transport p from j to $\mathsf{1}$ . More specifically, since $p ( j) : \mathsf{fill}_{j}({A}^{-1}(\mathsf{0}))\equiv {A}( j)$ , and, again, $\mathsf{fill}_{\mathsf{1}}({A}^{-1}(\mathsf{0}))\equiv {A}^{-1}(\mathsf{0})$ , we have

\begin{equation*}{(p ( j))}^{{\mathsf{j}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{ j}({A}^{-1}(\mathsf{0}))} : {A}^{-1}(\mathsf{0}).\end{equation*}

The right tube is treated similarly, except that we transport a (and $i=\mathsf{1}$ ),

\begin{equation*}{a}^{{\mathsf{j}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{ j}({A}^{-1}(\mathsf{1}))} : {A}^{-1}(\mathsf{1}).\end{equation*}

It is not hard to show that those lines are adjacent. We want to form a composition from $\mathsf{0}$ to $\mathsf{1}$ , so the initial point of the left tube should match the initial point of the cap,

\begin{align*} (\lambda j. {(p ( j))}^{{\mathsf{j}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{ j}({A}^{-1}(\mathsf{0}))})(\mathsf{0}) &\equiv {(p (\mathsf{0}))}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(\mathsf{0}))} \\ &\equiv {a}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(\mathsf{0}))} \\ &\equiv {a}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(i))} \end{align*}

and the initial point of the right tube should be the terminal point of the cap,

\begin{align*} (\lambda j. {a}^{{\mathsf{j}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{ j}({A}^{-1}(\mathsf{1}))})(\mathsf{0}) &\equiv {a}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(\mathsf{1}))} \\ &\equiv {a}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(i))}. \end{align*}

By composition, we have a line from b to a in ${A}^{-1}(i)$ . This composite has the correct endpoints because

\begin{equation*}{(p (\mathsf{1}))}^{{\mathsf{l}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{ j}({A}^{-1}(\mathsf{0}))}\equiv p(\mathsf{1}) \equiv b\end{equation*}

and

\begin{align*}{a}^{{\mathsf{l}} \rightsquigarrow {\mathsf{1}}}_{\lambda j.\mathsf{fill}_{j}({A}^{-1}(\mathsf{1}))} \equiv a.\\[-35pt]\end{align*}

It is important to stress that the proof of the previous lemma is based on heterogeneous composition, a particular kind of composition in which the types of the cap and composite may differ. As indicated in the proof above, a heterogeneous composition can be obtained from composition and transport. For instance, given a type line $A : \mathbb{I} \to \mathcal{U}$ , a heterogeneous composition in A with cap $a : \mathbb{I} \to A(\mathsf{0})$ and tubes $a_0, a_1 : \prod_{(i : \mathbb{I})} A(i)$ is just an abbreviation for a compound composition which combines the two Kan operations into one, a composition with cap $\lambda i.{(a(i))}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{A} : \mathbb{I} \to A(\mathsf{1})$ and tubes $\lambda j.{(a_0( j))}^{{\mathsf{j}} \rightsquigarrow {\mathsf{1}}}_A : \mathbb{I} \to A(\mathsf{1})$ and $\lambda j.{(a_1( j))}^{{\mathsf{j}} \rightsquigarrow {\mathsf{1}}}_A : \mathbb{I} \to A(\mathsf{1})$ . The composite is a term of type $\mathbb{I} \to A(\mathsf{1})$ .

So we have already covered the case of path inversion and showed how we can invert dependent paths using heterogeneous composition. One natural question is whether a similar strategy can be used to concatenate dependent paths. It is easier to see the limitations of the nondependent operation of path concatenation when we consider two-dimensional paths such as

\begin{equation*}\alpha : \mathsf{pathd}_{\lambda j.\mathsf{path}_{A}(s ( j), t ( j))}(p, q) \qquad\text{and}\qquad \beta : \mathsf{pathd}_{\lambda j.\mathsf{path}_{A}(u ( j), v ( j))}(q, r),\end{equation*}

which correspond to two (i,j)-squares in A such as the following:

It is clear that we should be able to concatenate the paths $\alpha$ and $\beta$ vertically, using the bottom and top faces of the squares, if we concatenate their left and right faces using nondependent path concatenation. This should give us a j-dependent path from p to r in the type of paths from $s : \;\mathbin{\tiny\blacksquare} \; u( j)$ to $t : \;\mathbin{\tiny\blacksquare} \; v( j)$ in A. This construction is illustrated in the following composition, whose left and right squares can be easily obtained by composition using the fillers of path concatenation and inversion, and meets and joins:

This two-dimensional concatenation is not an instance of the nondependent operation derived in Lemma 7: from our definition, it follows that to form the concatenated path ${\alpha}: \;\mathbin{\tiny\blacksquare} \;{\beta}$ , first $\alpha$ and $\beta$ must be terms of the same type and that type must be a degenerate line. In this example, the concatenation fails for both reasons, for the equality $\mathsf{path}_{A}(s ( j), t ( j)) \equiv \mathsf{path}_{A}(u ( j), v ( j))$ need not be the case and those types may depend on the interval variable j.

To overcome this problem, we need a dependent path concatenation operation. Following the definition of dependent path inversion, we consider the nondependent path concatenation of line types first. Suppose that $A,B : \mathbb{I} \to \mathcal{U}$ such that $A(\mathsf{1}) \equiv B (0)$ . The diagram

illustrates the path concatenation of A and B,

\begin{equation*} A : \;\mathbin{\tiny\blacksquare} \; B \; : \; \mathsf{path}_{\mathcal{U}}(A(\mathsf{0}), B(\mathsf{1})).\end{equation*}

We also have two important inferences that hold top/bottom and bottom/top,

\begin{equation*}\frac{a : (A : \;\mathbin{\tiny\blacksquare} \; B) (0)}{a : A(\mathsf{0})} \quad\text{and}\quad \frac{b : (A : \;\mathbin{\tiny\blacksquare} \; B) (1)}{b : B (1)}.\end{equation*}

With this, we have all we need to define concatenation for dependent paths:

Lemma 17. Suppose that $A, B : \mathbb{I} \to \mathcal{U}$ such that $A(\mathsf{1}) \equiv B (0)$ . Given any $a : A(\mathsf{0})$ , $b : A(\mathsf{1})$ and $c : B (1)$ , there is a function

\begin{equation*}\mathsf{pathd}_{A}(a, b) \to \mathsf{pathd}_{B}(b, c) \to \mathsf{pathd}_{{A}: \;\mathbin{\tiny\blacksquare} \;{B}}(a, c)\end{equation*}

written $p \mapsto q \mapsto p \,: \;\mathbin{\tiny\blacksquare} \; q$ and called the dependent path concatenation function.

Proof. By heterogeneous composition on the open box from Lemma 7.

Dependent path concatenation allows us to concatenate $\alpha$ and $\beta$ from our example above, but it is worth noting that the resulting path need not be definitionally equal to the operation $\alpha ? \beta$ we described. However, it is easy to show by path induction that they are equal up to globular identification.

5.3 The groupoid laws for dependent paths

Now that we are in possession of a new pair of dependent path inverse and concatenation operations, it is possible for us to revisit the groupoid structure from Section 4.2 and derive more general laws that hold for dependent paths as well. It is helpful to understand how this generalization works with an example.

As a case in point, let us examine the involution law from Lemma 14. This law actually expresses a fact about paths in degenerate line types. To be exact, given a degenerate $A : \mathbb{I} \to \mathcal{U}$ , it states that, for every $a : A(\mathsf{0})$ , $b : A(\mathsf{1})$ and $p : \mathsf{pathd}_{A}(a, b)$ , there is a path

\begin{equation*}\mathsf{pathd}_{\lambda \_. \mathsf{pathd}_{A}(a, b)}({({p}^{-1})}^{-1}, p).\end{equation*}

If we were to drop the restriction that the type line A be degenerate, meaning that the law would then be founded on dependent path inversion instead, the desired type would have to be stated as something like

\begin{equation*}\mathsf{pathd}_{\lambda j.\mathsf{pathd}_{\lambda i. ?( j)(i)}(a, b)}({({p}^{-1})}^{-1}, p).\end{equation*}

Because we are dealing with dependent paths and their operations, which often result in paths living in a different type line, we run into a problem at this point: we need a path from ${({p}^{-1})}^{-1} : \mathsf{pathd}_{{({A}^{-1})}^{-1}}(a, b)$ to $p : \mathsf{pathd}_{A}(a, b)$ , and we must specify in what type line this path lives in. Now, considering that generally ${({A}^{-1})}^{-1} \not\equiv A$ , this type line cannot be degenerate. But recall that, by the non-dependent involution law from Lemma 14, there is a path

\begin{equation*}\mathsf{inv}_A : \mathsf{path}_{\mathsf{path}_{\mathcal{U}}(A(\mathsf{0}), A(\mathsf{1}))}({({A}^{-1})}^{-1}, A),\end{equation*}

so the law we are looking for can be stated as follows:

Lemma 18. For every $A : \mathbb{I} \to \mathcal{U}$ with $a : A(\mathsf{0})$ and $b : A(\mathsf{1})$ , we have

\begin{equation*}\mathsf{pathd}_{\lambda j.\mathsf{pathd}_{\lambda i. \mathsf{inv}_A( j) (i)}(a, b)}({({p}^{-1})}^{-1}, p)\end{equation*}

for any dependent path $p : \mathsf{pathd}_{A}(a, b)$ .

The proof argument is similar to those given in the definition of dependent path inversion and composition from Lemmas 16 and 17, respectively. It thus follows from a straightforward heterogeneous composition on the open cube constructed for the proof of the nondependent version of the involution law from Lemma 14. In fact, all dependent counterparts of the laws proven in Section 4.2 follow the same pattern: they can all be stated by using their nondependent counterparts and proven by a heterogeneous filling of their open cubes. For this reason, we will simply omit those results.

6.1 Path induction

We now present a derivation of path induction (The Univalent Foundations Program 2013, Section 1.12.1), a key property that informally states that paths with a free endpoint can be deformed and retracted without changing their essential characteristics. As mentioned before, path induction serves as the elimination rule for the inductive path type in homotopy type theory, where it is taken as primitive. The result considered here corresponds to what is sometimes called based path induction (The Univalent Foundations Program 2013):

Theorem (Path induction) Given a type $A : \mathcal{U}$ , a term $a : A$ and a type family $C : \prod_{(x : A)} \mathsf{path}_{A}(a, x) \to \mathcal{U}$ , we have a function

\begin{equation*}\mathsf{pathrec} : \prod_{(x : A)} \prod_{(p : \mathsf{path}_{A}(a, x))} \prod_{(c : C(a,\mathsf{refl}_{a}))} C(x,p).\end{equation*}

Proof. We want to construct, for every $x : A $ , $p : \mathsf{path}_{A}(a, x)$ and $c : C(a,\mathsf{refl}_{a})$ , a term of type C(x,p). To obtain such a term, we shall transport c along a type line $D : \mathbb{I} \to \mathcal{U}$ that goes from $D(\mathsf{0}) :\equiv C(a,\mathsf{refl}_{a})$ to $D(\mathsf{1}) :\equiv C(x,p)$ . For the construction of the desired type line D, it suffices to consider the halfway meet connection derived in our proof of Lemma 8:

Now it suffices to define our type line as:

\begin{equation*}D :\equiv \lambda {i}. C(p (i \land^* \mathsf{1}), \lambda{j}.{p (i \land^* j)}) : \mathbb{I} \to \mathcal{U}\end{equation*}

because it goes from

\begin{align*} D(\mathsf{0}) &\equiv (\lambda {i}. C(p (i \land^* \mathsf{1}), \lambda{j}.{p (i \land^* j)})) \mathsf{0} \\ &\equiv C(p (\mathsf{0} \land^* \mathsf{1}), \lambda{j}.{p (\mathsf{0} \land^* j)}) \\ &\equiv C(a,\mathsf{refl}_{a}) \end{align*}

to

\begin{align*} D(\mathsf{1}) &\equiv (\lambda {i}. C(p (i \land^* \mathsf{1}), \lambda{j}.{p (i \land^* j)})) \mathsf{1} \\ &\equiv C(p (\mathsf{1} \land^* \mathsf{1}), \lambda{j}.{p (\mathsf{1} \land^* j)}) \\ &\equiv C(x, \lambda{j}.{p ( j)}) \\ &\equiv C(x, p). \end{align*}

To complete the proof, we transport $c : D(\mathsf{0})$ from $\mathsf{0}$ to $\mathsf{1}$ .

Note that, in the above proof, the $\eta$ -rule for the path type discussed in Section 2.1, that is, the requirement that $p \equiv \lambda{j}.{(p ( j))}$ , is crucial to the correct specification of endpoints of the type line we are doing the transportation over. Without this rule, it would not be possible to show that $D(\mathsf{1}) \equiv C(x, p)$ and the transportation would give us a term of the wrong type.

In cubical type theory, the computation rule for path induction does not hold “on the nose” like in the case of the eliminator of the inductive path type (The Univalent Foundations Program 2013). Put differently, for a fixed type family $C : \prod_{(x : A)} \mathsf{path}_{A}(a, x) \to \mathcal{U}$ , given $a : A $ and $c : C(a,\mathsf{refl}_{a})$ , in general,

\begin{equation*}\mathsf{pathrec}(a,\mathsf{refl}_{a},c) \not\equiv c.\end{equation*}

But this equality can be shown to hold up to a path:

Lemma 19 (Path computation (Angiuli Reference Angiuli2019)) For every $a : A $ and $c : C(a,\mathsf{refl}_{a})$ , we have a path of type

\begin{equation*}\mathsf{path}_{C(a, \mathsf{refl}_{a})}(\mathsf{pathrec}(a,\mathsf{refl}_{a},c), c).\end{equation*}

Proof. By the definition of path induction, we have a definitional equality

\begin{equation*}\mathsf{pathrec}(a, \mathsf{refl}_{a}, c) \equiv {c}^{{\mathsf{0}} \rightsquigarrow {\mathsf{1}}}_{\lambda {i}. C(\mathsf{refl}_{a} (i \land^* \mathsf{1}), \lambda{j}.{\mathsf{refl}_{a} (i \land^* j)})}.\end{equation*}

We are to find a path from this transported term to c in the type $C(a, \mathsf{refl}_{a})$ . First, we note that the transportation induces a path

\begin{equation*}\lambda{i}.{{c}^{{\mathsf{i}} \rightsquigarrow {\mathsf{1}}}_{\lambda {i}. C(\mathsf{refl}_{a} (i \land^* \mathsf{1}), \lambda{j}.{\mathsf{refl}_{a} (i \land^* j)})}}.\end{equation*}

This path has the right endpoints, since the static transportation from $\mathsf{1}$ to $\mathsf{1}$ has no effect, being therefore definitionally equal to c. But we need a path in the type $C(a, \mathsf{refl}_{a})$ and when we consider the type line the transportation in the constructed path occurs along, it can be seen that this induced path is actually in the type $C(\mathsf{refl}_{a} (i \land^* \mathsf{1}), \lambda{j}.{\mathsf{refl}_{a} (i \land^* j)})$ . This is not the type $C(a, \mathsf{refl}_{a})$ we are looking for because $a \not\equiv \mathsf{refl}_{a} (i \land^* \mathsf{1})$ and $\mathsf{refl}_{a} \not\equiv \lambda{j}. \mathsf{refl}_{a} (i \land^* j)$ .

To conclude this proof, we will fix this type mismatch with a heterogeneous composition based on the following composition scenario, where the composite is intended to give us the desired path in the type $C(a, \mathsf{refl}_{a})$ :

However, before this can be viewed as a valid heterogeneous composition, we must specify in what type line the operation takes place. We therefore have to define a $D_i : \mathbb{I} \to \mathcal{U}$ containing the cap and composite as terms inhabiting its initial and terminal endpoints. More explicitly, we need to satisfy the endpoint conditions that $D_i(\mathsf{0}) \equiv C(a, \mathsf{refl}_{a}) \equiv D_i(\mathsf{1})$ . In the i-direction, however, we need $D_\mathsf{0} \equiv \lambda{j}. C({\mathsf{refl}_{a}(j \land^* \mathsf{1})}, \lambda{k}.{\mathsf{refl}_{a} (j \land^* k)}) $ and $D_\mathsf{1} \equiv \lambda{j}.C(a, \mathsf{refl}_{a})$ .

First we construct by composition an otherwise degenerated square with $\mathsf{refl}_{a}(k \land^* \mathsf{1})$ as the right face. The composition scenario consists of degenerate squares in the bottom, front, back, and left and $\mathsf{refl}_{a}(k \land^* \mathsf{1})$ in the right:

Finally, we set $D_i :\equiv \lambda {k}. C(\alpha(k)(i), \lambda{j}.\mathsf{fill}_{j}(\alpha(k)(i)))$ . Now, to check that the type line $D_i$ has the correct endpoints we observe that for either $\mathsf{\varepsilon}=\mathsf{0}$ or $\mathsf{\varepsilon}=\mathsf{1}$ :

\begin{align*} D_i(\mathsf{\varepsilon}) &\equiv (\lambda{i}. C(\alpha(k)(i), \lambda{j}.\mathsf{fill}_{j}(\alpha(k)(i))))(\mathsf{\varepsilon}) \\ &\equiv C(\alpha(\mathsf{\varepsilon})(i), \lambda{j}.\mathsf{fill}_{j}(\alpha(\mathsf{\varepsilon})(i))) \\ &\equiv C(a, \lambda{j}.a). \\ \end{align*}

In the i-direction, for $i=\mathsf{0}$ we have

\begin{align*} D_\mathsf{0} &\equiv \lambda{k}. C(\alpha(k)(\mathsf{0}), \lambda{j}.\mathsf{fill}_{j}(\alpha(k)(\mathsf{0}))) \\ &\equiv \lambda{k}. C(\mathsf{refl}_{a}(k \land^* \mathsf{1}), \lambda{j}. \mathsf{refl}_{a}(k \land^* j)), \end{align*}

and for $i=\mathsf{1}$

\begin{align*} D_\mathsf{1} &\equiv \lambda{k}. C(\alpha(k)(\mathsf{1}), \lambda{j}.\mathsf{fill}_{j}(\alpha(k)(\mathsf{1}))) \\ &\equiv \lambda{k}. C(a, \lambda{j}.a). \\[-40pt] \end{align*}

The proof above is inspired by an argument given by Angiuli (Angiuli Reference Angiuli2019, pp. 54–56), who considered a slightly different definition of path induction based on the folklore result that $\sum_{(x:A)} \mathsf{path}_{A}(a, x)$ is contractible with center $\langle a, \mathsf{refl}_{a} \rangle$ and that type families respect paths in their indexing type.

In the presence of higher inductive types (Cavallo and Harper Reference Cavallo and Harper2018; Coquand et al. Reference Coquand, Huber and Mörtberg2018), the inductive path type from homotopy type theory (The Univalent Foundations Program 2013) can be recovered as a higher inductive type freely generated by reflexivity (Cavallo and Harper Reference Cavallo and Harper2018). Path induction then acts strictly on reflexivity, since it is given as a specific generator that can be recognized by the eliminator, and this allows for a strict computation rule. This inductive path type can be shown to be equivalent to the path type (Cavallo and Harper Reference Cavallo and Harper2018), meaning that, by univalence, the inductive path type is the path type up to a path.

6.2 The Eckmann–Hilton argument

In homotopy type theory, paths from a point to itself are called loops. Thus, given a type A and a point $a : A$ , the loop space $\Omega(A,a)$ is defined to be the type of loops $\mathsf{path}_{A}(a, a)$ . When the loop space of a loop space is considered, we have the second loop space $\Omega^2(A,a)$ , which is the type $\mathsf{path}_{\mathsf{path}_{A}(a, a)}(\mathsf{refl}_{a}, \mathsf{refl}_{a})$ .

The Eckmann–Hilton argument is one interesting result about the second loop space that states that path concatenation is commutative. It is inspired by a classical result in homotopy theory and proven by path induction in homotopy type theory (The Univalent Foundations Program 2013, Thm. 2.1.6). We adapt this proof in what follows:

Theorem (Eckmann–Hilton) For any $\alpha, \beta : \Omega^2(A,a)$ , there is a path

\begin{equation*}\mathsf{path}_{\Omega^2(A,a)}({\alpha}: \;\mathbin{\tiny\blacksquare} \;{\beta}, {\beta}: \;\mathbin{\tiny\blacksquare} \;{\alpha})\end{equation*}

Proof. It is easier to prove a stronger statement that holds more generally for any two-dimensional globular paths by path induction, and then derive the intended claim as a special case. So, given paths $\alpha : \mathsf{path}_{\mathsf{path}_{A}(a, b)}(p, q)$ and $\beta : \mathsf{path}_{\mathsf{path}_{A}(b, c)}(r, s)$ , first we define a right whiskering operation

\begin{equation*}{\alpha}\; : \;\mathbin{\tiny\blacksquare} \;_{\mathsf{r}} \;{r} : \mathsf{path}_{\mathsf{path}_{A}(a, c)}({p}: \;\mathbin{\tiny\blacksquare} \;{r}, {q}: \;\mathbin{\tiny\blacksquare} \;{r})\end{equation*}

in the obvious way such that the following composition holds, with $\alpha$ at the bottom:

then we define left whiskering

\begin{equation*}{p}\; : \;\mathbin{\tiny\blacksquare} \;_{\mathsf{l}} \;{\beta} : \mathsf{path}_{\mathsf{path}_{A}(a, c)}({p}: \;\mathbin{\tiny\blacksquare} \;{r}, {p}: \;\mathbin{\tiny\blacksquare} \;{s})\end{equation*}

by composition on a similar open cube but with $\beta$ at the right:

It is easy to see by path induction on $\alpha$ , $\beta$ , p, and r that there exists a path

\begin{equation*} \mathsf{path}_{\mathsf{path}_{\mathsf{path}_{A}(a, c)}({p}: \;\mathbin{\tiny\blacksquare} \;{r}, {q}: \;\mathbin{\tiny\blacksquare} \;{s})}({({\alpha}: \;\mathbin{\tiny\blacksquare} \;_{\mathsf{r}}{r})}: \;\mathbin{\tiny\blacksquare} \;{({q}: \;\mathbin{\tiny\blacksquare} \;_{\mathsf{l}}{\beta})}, {({p}: \;\mathbin{\tiny\blacksquare} \;_{\mathsf{l}}{\beta})}: \;\mathbin{\tiny\blacksquare} \;{({\alpha}: \;\mathbin{\tiny\blacksquare} \;_{\mathsf{r}}{s})}). \end{equation*}

Now let $p \equiv q \equiv r \equiv s \equiv \mathsf{refl}_{a}$ . Since reflexivity is both a right and left unit for path concatenation (as shown in Lemmas 10 and 11), the above proposition demonstrates our intended claim.

The Eckmann–Hilton argument has been proved very recently for De Morgan cubes in a purely cubical way that avoids path induction (Brunerie et al. Reference Brunerie, Ljungström and Mörtberg2021). The key element that makes this proof possible is a transportation from $\mathsf{0}$ to $\mathsf{1}$ along a j-type line of paths from ${\alpha_{\mathsf{r}}( j)}: \;\mathbin{\tiny\blacksquare} \;{\beta_{\mathsf{l}}( j)}$ to ${\beta_{\mathsf{l}}( j)}: \;\mathbin{\tiny\blacksquare} \;{\alpha_{\mathsf{r}}( j)}$ in $\Omega(A,a)$ , constructed using function application, path concatenation, and the right and left unit, where

\begin{align*}\alpha_{\mathsf{r}}( j) :\equiv & \ \mathsf{ap}_{\lambda{p}. \mathsf{ru}_p^{-1}( j)} (\alpha) : \mathsf{path}_{\Omega(A,a)}(\mathsf{ru}_{\mathsf{refl}_{a}}^{-1}( j), \mathsf{ru}_{\mathsf{refl}_{a}}^{-1}( j)) \\\beta_{\mathsf{l}}( j) :\equiv & \ \mathsf{ap}_{\lambda{p}. \mathsf{lu}_p^{-1}( j)} (\beta) : \mathsf{path}_{\Omega(A,a)}(\mathsf{lu}_{\mathsf{refl}_{a}}^{-1}( j), \mathsf{lu}_{\mathsf{refl}_{a}}^{-1}( j)).\end{align*}

This type is actually well-formed for De Morgan cubes because it can be shown that $\mathsf{ru}_{\mathsf{refl}_{x}} \equiv \mathsf{lu}_{\mathsf{refl}_{x}}$ , for all $x : A$ , using proofs of the right and left unit laws based on essentially the same compositions, except that they make use of the built-in connections that act strongly on reflexivity terms. This definitional equality, however, does not hold for cartesian cubes and their weak connections, so a direct cubical proof would have to rely on a different strategy.