The Univalence Axiom in Cubical Sets

We give a brief overview of the cubical set model, introducing some different notations, but will otherwise assume the reader is familiar with [2, 6].

As opposed to [2, 6] let us define cubical sets as contravariant presheaves on the opposite of the category used there, that is, the category of cubes \(\mathscr {C}\) contains as objects finite sets \(I = \{i_1,\ldots ,i_n\}\) (\(n \ge 0\)) of names and a morphism \(f {:}J \rightarrow I\) is given by a set-theoretic map \(I \rightarrow J \cup \{0,1\}\) which is injective when restricted to the preimage of J; we will write compositions in applicative order. The category of cubical sets is the category \([\mathscr {C}^\mathrm {op},\mathbf {Set}]\) of presheaves on \(\mathscr {C}\). A morphism \(f {:}J \rightarrow I\) in \(\mathscr {C}\) can be viewed as a substitution. If \(f(i) \in J\), we call fdefined oni. For \(i \notin I\), the face morphisms are denoted by \((i / 0), (i / 1) {:}I \rightarrow I,i\) and are induced by setting i to 0 and 1, respectively; degenerating along \(i \notin I\) is denoted by \(s_i {:}I,i \rightarrow I\) and is induced by the inclusion \(I \subseteq I,i\).

If \(\varGamma \) is a cubical set, we write \({{\mathrm{Ty}}}(\varGamma )\) for the collection/class of presheaves on the category of elements of \(\varGamma \) [2, 6]. Such a presheaf \(A \in {{\mathrm{Ty}}}(\varGamma )\) is given by a family of sets \(A (I,\rho )\) for \(I \in \mathscr {C}\) and \(\rho \in \varGamma (I)\) together with restriction functions. As \(\rho \in \varGamma (I)\) determines I we simply write \(A \rho \) for \(A (I,\rho )\). Given \(A \in {{\mathrm{Ty}}}(\varGamma )\) and a natural transformation (substitution) \(\sigma {:}\varDelta \rightarrow \varGamma \) we get \(A \sigma \in {{\mathrm{Ty}}}(\varDelta )\) defined as \((A \sigma ) \rho = A (\sigma \rho )\) which extends canonically to the restrictions. For \(A \in {{\mathrm{Ty}}}(\varGamma )\) we denote the set of sections of A by \({{\mathrm{Ter}}}(\varGamma , A)\); so \(a \in {{\mathrm{Ter}}}(\varGamma ,A)\) is given by a family \(a \rho \in A \rho \) for \(\rho \in \varGamma (I)\) such that \((a \rho ) f = a (\rho f)\) for \(f {:}J \rightarrow I\). Substitution also extends to terms via \((a\sigma ) \rho = a (\sigma \rho )\).

Let us recall the construction of \(\varPi \)-types: \(\varPi \,A\,B \in {{\mathrm{Ty}}}(\varGamma )\) for \(A \in {{\mathrm{Ty}}}(\varGamma )\) and \(B \in {{\mathrm{Ty}}}(\varGamma .A)\) is given by letting each element w of \((\varPi \,A\,B)\rho \) (with \(\rho \in \varGamma (I)\)) be a family of \(w_f\,a \in B (\rho f, a)\) for \(f {:}J \rightarrow I\) and \(a \in A\rho \) satisfying \((w_f\,a)g = w_{fg}\,(a g)\); the restriction of such a w is given by \((wf)_g = w_{fg}\). In the sequel we will however only have to refer to \(w_f\) when f is the identity, and will thus simply write \(w\,a\) for \(w_\mathrm {id}\,a\). We also occasionally switch between sections in \({{\mathrm{Ter}}}(\varGamma .A, B)\) and \({{\mathrm{Ter}}}(\varGamma ,\varPi A B)\) without warning the reader.

Let \(A \in {{\mathrm{Ty}}}(\varGamma )\), \(\rho \in \varGamma (I)\), and \(J \subseteq I\). A J-tube in A over \(\rho \) is given by a family \(\mathbf {u}\) of elements \(u_{jc} \in A \rho (j / c)\) for \((j,c) \in J \times \{0,1\}\) which is adjacent compatible, that is, \(u_{jc} (k / d) = u_{k d} (j / c)\) for \((j,c),(k,d) \in J \times \{0,1\}\). For \((i,a) \in (I - J) \times \{0,1\}\) we say that an element \(u_{ia} \in A \rho (i / a)\) is a lid of such a tube \(\mathbf {u}\) if \(u_{jc} (i / a) = u_{ia} (j / c)\) for all \((j,c) \in J \times \{0,1\}\). In this situation we call the pair \([J \mapsto \mathbf {u}; (i,a) \mapsto u_{ia}]\) an open box in A over \(\rho \). A filler for such an open box is an element \(u \in A \rho \) such that \(u (j / c) = u_{jc}\) for \((j,c) \in \{(i,a)\} \cup (J \times \{0,1\})\). In case J is empty, we simply write \([(i,a) \mapsto u_{ia}]\).

Given \(f {:}K \rightarrow I\) and an open box \(m = [J \mapsto \mathbf {u}; (i,a) \mapsto u_{ia}]\) in A over \(\rho \) we call f allowed for m if f is defined on J, i. In this case we define the open box mf in A in \(\rho f\) to be \([J f \mapsto \mathbf {u}f; (f (i), a) \mapsto u_{ia} (f - i)]\) where \(\mathbf {u}f\) is given by \((\mathbf {u}f)_{f(j)\, c} = u_{j c} (f - j)\) with \(f - i {:}K - {f (i)} \rightarrow I-i\) being like f but skipping i, and Jf is the image of J under f.

Recall from [2, Section 4] that a (uniform) Kan structure for a type \(A \in {{\mathrm{Ty}}}(\varGamma )\) is given by an operation \(\kappa \) which (uniformly) fills open boxes: for any \(\rho \in \varGamma (I)\) and open box m in A over \(\rho \) we get a filler \(\kappa \,\rho \,m\) of m subject to the uniformity conditionfor all \(f {:}K \rightarrow I\) allowed for m.

Any Kan structure \(\kappa \) defines a composition operation\(\bar{\kappa }\) which provides the missing lid of the open box, given by:We denote the set of all Kan structures on \(A \in {{\mathrm{Ty}}}(\varGamma )\) as \({{\mathrm{Fill}}}(\varGamma , A)\). If \(\sigma {:}\varDelta \rightarrow \varGamma \) and \(\kappa \) is an element in \({{\mathrm{Fill}}}(\varGamma , A)\), we get an element \(\kappa \sigma \) in \({{\mathrm{Fill}}}(\varDelta , A \sigma )\) defined by \((\kappa \sigma ) \, \rho = \kappa \, (\sigma \rho )\).

Given a cubical set \(\varGamma \) a Kan type is a pair \((A,\kappa )\) where \(A \in {{\mathrm{Ty}}}(\varGamma )\) and \(\kappa \in {{\mathrm{Fill}}}(\varGamma ,A)\). We denote the collection of all such Kan types by \({{\mathrm{KTy}}}(\varGamma )\). In [2] we showed that Kan types are closed under dependent products and sums constituting a model of type theory.

In [2] we introduced identity types which were however only “weak”, e.g., transport along reflexivity is only propositionally equal to the identity function but not necessarily judgmentally equal. For this reason we will call these types path types and reserve \(\mathsf {Id}_{A}\) for the identity type with the usual judgmental equality defined in Sect. 4.

Recall that the path type \(\mathsf {Path}_{A}\,u\,v \in {{\mathrm{Ty}}}(\varGamma )\) for \(A \in {{\mathrm{Ty}}}(\varGamma )\) and \(u,v \in {{\mathrm{Ter}}}(\varGamma ,A)\) is defined by the sets \((\mathsf {Path}_{A}\,u\,v)\rho \) containing equivalence classes \(\langle i \rangle w\) where \(i \notin I\) and \(w\in A\rho s_i\) with \(w(i / 0) = u \rho \) and \(w(i / 1) = v \rho \). Restrictions are defined as expected, and we showed that Kan types are closed under forming path types [2].

It will be convenient below to introduce paths using separated products.

Of particular interest is \(\varGamma *\mathbb {I}\) where \(\mathbb {I}\) is the interval defined by \(\mathbb {I}(J) = J \cup \{0,1\}\) (see [2, Section 6.1]). ThenIf \((\rho , i) \in (\varGamma * \mathbb {I}) (I)\) with \(i\in I\), then \(\rho = \rho ' s_i\) for a uniquely determined \(\rho '\) which we denote by \(\rho - i\).

We can use \(\varGamma *\mathbb {I}\) to formulate the following introduction rule for path types

where \([0],[1] {:}\varGamma \rightarrow \varGamma * \mathbb {I}\) are induced by the global elements 0 and 1 of \(\mathbb {I}\), respectively, and \(\mathsf {p}{:}\varGamma *\mathbb {I}\rightarrow \varGamma \) is the first projection. The binding operation is interpreted by \((\langle \rangle w) \rho = \langle i \rangle \, w (\rho s_i, i)\) with i a fresh name (see [2, Section 8.2]).

Given an element \(\langle i \rangle w \in (\mathsf {Path}_{A}\,u\,v) \rho \) with \(\rho \in \varGamma (I)\), we set \((\langle i \rangle w) \mathop {\varvec{@}}a = w (i / a)\) where a is 0, 1, or a fresh name.

We will now recall the definition of an equivalence as a map having contractible fibers and then derive an operation for contractible and Kan types. To enhance readability we define the following types using variable names:where A and B are types, \(t : A \rightarrow B\), and v : B (all in an ambient context \(\varGamma \)). This can of course also be formally written name-free: for example, the first type can be written as \(\varSigma A \varPi A\mathsf {p}\, (\mathsf {Path}_{A\mathsf {p}\mathsf {p}} \mathsf {q}\mathsf {p}~\mathsf {q}) \in {{\mathrm{Ty}}}(\varGamma )\) and the second one as \(\varSigma A\mathsf {p}\, (\mathsf {Path}_{B\mathsf {p}\mathsf {p}} \,\mathsf {app}(t\mathsf {p}\mathsf {p},\mathsf {q})\,\mathsf {q}\mathsf {p}) \in {{\mathrm{Ty}}}(\varGamma .B)\).

Note that given \(\mathsf {ext}\in {{\mathrm{Contr}}}(\varGamma ,A)\) and \(\sigma {:}\varDelta \rightarrow \varGamma \) we obtain \(\mathsf {ext}\, \sigma \in {{\mathrm{Contr}}}(\varDelta , A\sigma )\) via \((\mathsf {ext}\,\sigma )\, \rho = \mathsf {ext}\, (\sigma \rho )\).

Next we will define an operation \({{\mathrm{\mathsf {G}}}}\) which allows us to transform an equivalence into a “path”.¹ This operation was introduced in [4] and motivated the “glueing” operation of [3]. We will define it in such a way that the associated transport of this path is given by underlying map of the equivalence.

A useful analogy is provided by the notion of pathover, a heterogeneous path lying over another path. We shortly review this notion from type theory with inductive equality. Given a type family \(P{:}T \rightarrow \mathsf {U}\) and a path \(p{:}x=_T y\) with its transport function \(p_*{:}Px\rightarrow Py\). If Px and Py are different types, there is no ordinary path connecting \(u {:}Px\) and \(v {:}Py\). Therefore the pathovers connecting u and v are taken to be the paths of type \(p_* u =_{Py} v\) (in the fiber Py).

We apply the same idea to \({{\mathrm{\mathsf {G}}}}t\), which should be a path from A to B in \(\mathsf {U}\) such that transport along this path is \(t {:}A\rightarrow B\). For the type family P we take \(\mathrm {id}_{\mathsf {U}}\) such that A and B indeed are fibers of P. Intuitively, a path from A to B is a set of heterogeneous paths between elements a of A and b of B. We want t to be the transport function along the path from A to B. By analogy we would take \({{\mathrm{\mathsf {G}}}}t\) to be the set of pathovers connecting \(a{:}A\) and \(b{:}B\) defined as the set of paths in B connecting t a and b. However, since we must be able to recover the startpoint a, we define \({{\mathrm{\mathsf {G}}}}t\) to be the set of pairs consisting of \(a{:}A\) and a path connecting t a and b. (Unlike a, the endpoint b can be recovered from the pathover and need not be remembered.)

With the above informal explanation in mind, we define the operation \({{\mathrm{\mathsf {G}}}}\) first on cubical sets and then explain how it lifts to Kan structures. It satisfies the rules:The latter rule expresses stability under substitutions. Here and below \({{\mathrm{\mathsf {G}}}}\) (and \(\mathsf {ug}\) below) have A and B as implicit arguments.

We have a map \(\mathsf {ug}\in {{\mathrm{Ter}}}(\varGamma * \mathbb {I}.{{\mathrm{\mathsf {G}}}}t, B \mathsf {p})\) given by:

The fact that a map \(t \in {{\mathrm{Ter}}}(\varGamma ,A \rightarrow B)\) is an equivalence can be represented as an element of \({{\mathrm{Contr}}}(\varGamma .B, \mathsf {fib}\,t)\). By Lemma 1 this is the case whenever A and B have Kan structures and the fibers of t are contractible.

Let us recall the definition of a universe \(\mathsf {U}\) of small Kan types (assuming a Grothendieck universe of small sets in the ambient set theory). A type \(A \in {{\mathrm{Ty}}}(\varGamma )\) is small if all the sets \(A \rho \) for \(\rho \in \varGamma (I)\) are so. A Kan type \((A,\kappa ) \in {{\mathrm{KTy}}}(\varGamma )\) is small if \(A \in {{\mathrm{Ty}}}(\varGamma )\) is small. We denote the set of all such small types and Kan types by \({{\mathrm{Ty}}}_0(\varGamma )\) and \({{\mathrm{KTy}}}_0(\varGamma )\), respectively. Substitution makes both \({{\mathrm{Ty}}}_0\) and \({{\mathrm{KTy}}}_0\) into presheaves on the category of cubical sets. The universe \(\mathsf {U}\) is now given as \(U = {{\mathrm{KTy}}}_0 \circ {{\mathrm{\mathbf {y}}}}\) where \({{\mathrm{\mathbf {y}}}}\) denotes the Yoneda embedding. For an I-cube \((A,\kappa ) \in \mathsf {U}(I) = {{\mathrm{KTy}}}_0({{\mathrm{\mathbf {y}}}}I)\) we have that A is a presheaf on the category of elements of \({{\mathrm{\mathbf {y}}}}I\), and A(J, f) is a small set for every element \((J,f{:}J \rightarrow I)\). Moreover, \(\kappa (J,f)\) is a filler function for open boxes in A over (J, f). Of particular interest are the small set \(A(I,\mathrm {id}_I)\) and filler function \(\kappa (I,\mathrm {id}_I)\).

Given \(a \in {{\mathrm{Ter}}}(\varGamma ,\mathsf {U})\) we can associate a small type \({{\mathrm{\mathsf {El}}}}a\) in \({{\mathrm{Ty}}}_0 (\varGamma )\) by \(({{\mathrm{\mathsf {El}}}}a) \rho = A(I,\mathrm {id}_I)\) where \(a \rho = (A,\kappa )\). We equip \({{\mathrm{\mathsf {El}}}}a\) with the Kan structure \({{\mathrm{\underline{\mathsf {El}}}}}\,a\) defined by \(({{\mathrm{\underline{\mathsf {El}}}}}\,a)\rho = \kappa (I,\mathrm {id}_I)\). This results in an isomorphism which is natural in \(\varGamma \):

where \(\ulcorner X \urcorner \rho = X \hat{\rho }\in \mathsf {U}(I)\) for \(X \in {{\mathrm{KTy}}}_0 (\varGamma )\). Here \(\hat{\rho }{:}{{\mathrm{\mathbf {y}}}}I \rightarrow \varGamma \) is the associated substitution of \(\rho \in \varGamma (I)\), that is, \(\hat{\rho }f = \rho f \in \varGamma (J)\) for any \(f {:}J \rightarrow I\). Since moreover \({{\mathrm{Hom}}}(\varGamma ,\mathsf {U}) \cong {{\mathrm{Ter}}}(\varGamma ,\mathsf {U})\), we get that \({{\mathrm{KTy}}}_0\) is representable.

We are now ready for the first main result of this paper.

We will now describe the identity type which justifies the usual judgmental equality for its eliminator following Swan [7].

Let \(\varGamma \) be a cubical set and \(A,B\in {{\mathrm{Ty}}}(\varGamma )\), i.e., A and B are presheaves on the category of elements of \(\varGamma \). For natural transformations²\(\alpha {:}A \rightarrow B\) we are going to define a factorization as \(\alpha = p_\alpha \, i_\alpha \) with \(i_\alpha {:}A \rightarrow M_\alpha \) and \(p_\alpha {:}M_\alpha \rightarrow B\). Furthermore, \(i_{\alpha }\) will be a cofibration (i.e., has the lifting property w.r.t. any acyclic fibration as formulated in Corollary 2) and \(p_{\alpha }\) will be equipped with an acyclic-fibration structure. This factorization corresponds to Garner’s factorization using the refined small object argument [5] specialized to cubical sets.

For \(\rho \) in \(\varGamma (I)\) we will define the sets \(M_\alpha \rho \) together with the restriction maps \(M_\alpha \rho \rightarrow M_\alpha (\rho f)\) (for \(f {:}J \rightarrow I\)) and the components \(M_\alpha \rho \rightarrow B \rho \) of the natural transformation \(p_\alpha \) by an inductive process (see Remark 2 below). The elements of \(M_\alpha \rho \) are either of the form \(\mathsf {i}\, u\) with u in \(A \rho \) (and \(\mathsf {i}\) considered as a constructor) and we set in this case \((\mathsf {i}\, u) f = \mathsf {i}(u \, f)\) and \(p_\alpha (\mathsf {i}\, u) = \alpha \,u\). Or the elements are of the form \((v, [J \mapsto \mathbf {u}])\) where \(v \in B\rho \), \(J \subseteq I\), and \(\mathbf {u}\) is a J-tube in \(M_\alpha \rho \) over v (meaning \(p_\alpha \, u_{jb} = v (j / b)\)). In the latter case we set \(p_\alpha (v, [J \mapsto \mathbf {u}]) = v\) and for the restrictions \((v,[J\mapsto \mathbf {u}])f = u_{jb}(f-j)\) if \(f(j)=b\in \{0,1\}\) for some \(j\in J\), and \((v,[J\mapsto \mathbf {u}])f = (vf,[Jf\mapsto \mathbf {u}f])\) if f is defined on J. Note that restrictions do not increase the syntactic complexity of an element \(m \in M_\alpha \rho \). This defines \(M_\alpha \in {{\mathrm{Ty}}}(\varGamma )\) and we set \(i_\alpha \,u = \mathsf {i}\,u\).

We use \(M_\alpha , i_\alpha , p_\alpha \) in the following way. Let A be a Kan type and let \(B=\mathsf {Path}_{A}\) be the Kan type of paths over A without specified endpoints. (The Kan structure on A induces the Kan structure on B, much in the same way as shown in [2] for types \(\mathsf {Path}_{A}\,a\,b\).) As mentioned in Sect. 2, transport along reflexivity paths is not necessarily the identity function. One could solve this problem if one could recognize the reflexivity paths, which is not possible in \(\mathsf {Path}_{A}\). Swan’s [7] solution to this problem is to define a type equivalent to \(\mathsf {Path}_{A}\) in which one can recognize (representations of) reflexivity paths. This is the type \(M_\alpha \) with \(\alpha {:}A \rightarrow \mathsf {Path}_{A}\) mapping each a in A to its reflexivity path. The representation of the reflexivity path of a in \(M_\alpha \) is \(\mathsf {i}\,a\), with \(\mathsf {i}\) a constructor of the inductively defined type \(M_\alpha \), and recognizing \(\mathsf {i}\,a\) is done through pattern matching. All the rest of the complicated definition above is to make sure that \(M_\alpha \) has the right Kan structure (Lemma 2), and that elimination generally has the right properties (Corollary 1).

Constructors of the form \((v,[J\mapsto \mathbf {u}])\) equip \(p_\alpha {:}M_\alpha \rightarrow B\) with an acyclic-fibration structure which (uniformly) fills tubes \([J \mapsto \mathbf {u}]\) in \(M_\alpha \rho \) over a filled cube v in \(B \rho \). Thus to, say, construct a path between specified endpoints in \(M_\alpha \) it is enough to give a path in B between the images of the endpoints under \(p_\alpha \).

There are two important observations to make at this point: First, this construction preserves smallness, i.e., \(M_\alpha \in {{\mathrm{Ty}}}_0 (\varGamma )\) whenever \(A, B \in {{\mathrm{Ty}}}_0 (\varGamma )\). And, second, this construction is stable under substitution: given \(\sigma {:}\varDelta \rightarrow \varGamma \) we have \(M_\alpha \sigma = M_{\alpha \sigma }\), \(i_\alpha \sigma = i_{\alpha \sigma }\), and \(p_\alpha \sigma = p_{\alpha \sigma }\). Neither of these properties holds for the corresponding factorization into an acyclic cofibration followed by a fibration (sketched in [6, Section 3.5] for a special case).

If the Kan structure is an acyclic-fibration structure as in Definition 2, that is, if we can fill tubes without a closing lid, the above proof can be carried out without \(s'\). This implies the following result, which expresses that \(i_{\alpha } {:}A \rightarrow M_{\alpha }\) is a cofibration.

This also implies the following result, which expresses that \(i_{\alpha } {:}A \rightarrow M_{\alpha }\) is a acyclic cofibration as soon as \(\alpha \) has a well-behaved homotopy inverse. Recall that application \(\mathsf {ap}\,\alpha \,p \in {{\mathrm{Ter}}}(\varGamma , \mathsf {Path}_{B}\, (\alpha \,u)\,(\alpha \,v))\) of \(\alpha {:}A \rightarrow B\) to a path \(p \in {{\mathrm{Ter}}}(\varGamma ,\mathsf {Path}_{A}\,u\,v)\) is given by \((\mathsf {ap}\,\alpha \,p)\rho = \langle i \rangle \, \alpha (p \rho \mathop {\varvec{@}}i)\) (see [6, Section 3.3.2]).

The representation of the identity type with the usual judgmental equality for its eliminator follows from these results by considering the case where B is the type of paths without specified endpoints \(\mathsf {Path}_{A}\) over a type A and \(\alpha \,a\) is the constant path a. We get a factorization with \(\mathsf {Id}_{A} := M_\alpha \), \({{\mathrm{\mathsf {refl}}}}:= i_\alpha \), and where the right vertical map is given by taking endpoints:

This \(\alpha \) satisfies the hypothesis of Corollary 2 using the properties of path-types from [2, Section 8.2], and hence \({{\mathrm{\mathsf {refl}}}}{:}A \rightarrow \mathsf {Id}_{A}\) has diagonal lifts against types with Kan structure. These diagonal lifts serve as the interpretation of the eliminator (cf. [1, p. 52]) and their choice is stable under substitution, allowing us thus to interpret identity types.

One can also explain \(\mathsf {Id}_{A}\) with fixed endpoints as Kan type in context \(\varGamma .A.A\mathsf {p}\) and then show that \(\mathsf {Id}_{A}\,u\,v\) is \(\mathsf {Path}\)-equivalent to \(\mathsf {Path}_{A}\,u\,v\). It follows that a type is \(\mathsf {Path}_{}\)-contractible if, and only if, it is \(\mathsf {Id}_{}\)-contractible. The univalence axiom for \(\mathsf {Path}_{}\)-types (Theorem 4) hence also holds formulated with \(\mathsf {Id}_{}\)-types.

We can summarize the results of this section as: