Cubical Sets

In which I try to write about semantics. This is not gonna go well, but I’m gonna try my best. I’ve heard it on good authority that the best way to learn something is to explain it to someone else, so in this post I’m going to use you, dear reader, as my rubber duck while I try to understand cubical sets. These are important (to me) because they provide a semantic model of cubical type theory (which I have written about previously), and since we have a semantic model, that theory is (semantically) consistent.

Personally, I like to think of a cubical set as.. a set that has opinions about cubes. You can ask some cubical set $F$ (the letter $F$ is meant to be indicative of its nature, as we will see) about its opinion on the 0-cube, and it’ll give us a set of points. We could ask it about the line, and it’ll give us a set of lines, and so on and so forth. There are also, as we shall see, maps between cubes, and asking $F$ about these will give us maps between what it thinks those cubes are.

A disclaimer (which I won’t put in one of the big red warning boxes like above) is that I am not a category theorist! Most of this stuff I absorbed from reading various papers about the semantics of cubical type theory. This post is not really what I would call “a good reference”.

The Category of Cubes 🧊

The category of cubes has a concise description in category-theoretic terms but I would rather describe it like this: It’s the category in which the objects are all powers of the set of booleans, $\{0,1\}^n$, which we abbreviate to $[n]$. To describe the maps in the category of cubes, I’m going to upset category theorists and describe them concretely, as functions of sets, written in a “pattern matching” notation similar to Haskell. However, we will only “pattern match” on products.

• The faces, which exhibit a cube as a face of a larger cube. Concretely, a face map inserts either a 0 or a 1 somewhere along the tuple, taking an $n$-cube to an $(n+1)$-cube. The two most basic face maps take the 0-cube (a point) to either endpoint of the 1-cube (a line), defined by $\delta^0(()) = 0$ and $\delta^1(()) = 1$.

  As further examples, we have functions $\delta^i_j$ (for $0 \le i, j \le 1$) which map the 1-cube (a line) into the 2-cube (a square), as any of its 4 faces. These are, explicitly, $\delta^0_0(j) = (0, j)$, $\delta^0_1(i) = (i, 0)$, $\delta^1_0(j) = (1, j)$, and $\delta^1_1(i) = (i, 1)$.

  These also compose. For instance, the map $\delta^0_0 \circ \delta^1 : [0] \to [2]$ exhibits the point () as (0, 1)-th corner of a square. If we take the first coordinate to be the left-right direction (0 = left) and the second coordinate to be the up-down (0 = up) direction, then this composite map can be pictured as follows:

  

  The actual, concrete effect of $\delta^0_0 \circ \delta^1 : [0] \to [2]$ can be seen by evaluating the composite at the unique inhabitant of $[0]$, which is $()$ (the empty tuple). We have $(\delta^0_0 \circ \delta^1)(()) = \delta^0_0(1) = (0, 1)$.

• The degeneracies, which “collapse” an $(n+1)$-cube to an $n$-cube by deleting a dimension. The most basic degeneracy is given by the unique map $\sigma : [1] \to [0]$. There are two degeneracies $[2] \to [1]$, mapping a square to a line, by deleting either coordinate. These… don’t have very nice pictoral representations, at least in the category of cubes. We’ll see that when it comes to a cubical set, though, they are quite easy to diagram.

We also have the trivial map $1_n : [n] \to [n]$ which returns its argument $n$-tuple (cube) unchanged. It’s easy to see that this is the identity for composition, which is as in $\mathbf{Set}$. Since 🧊 is a category, we can consider standard category-theoretical operations on 🧊, like taking its opposite category, $\cube^{op}$. The category $\cube^{op}$ has as its objects the same cubes $[n]$ as before, but all of the maps are backwards, so that the face maps in $\cube^{op}$ project a face and the degeneracies expand a cube, by inserting trivial faces.

We can also consider functors which map out of $\cube$ — and its opposite category! — and that’s what we’re interested in today. The functors we will talk about, those $X : \cube^{op} \to \mathbf{Set}$, are called cubical sets, and we’ll talk about them shortly, but first, a note:

Crucially, the category of cubes does not have any maps other than the faces and degeneracies (and identities), and importantly, any map $p : [m] \to [n]$ factors as a series of degeneracies followed by a series of faces. This means we can specify a cubical set entirely by how it acts on the faces and the degeneracies.

Cubical Sets

• To each object $c$ in 🧊, a set $X(c)$. Since the objects of 🧊 are all $[n]$, these are alternatively notated $X_n$.

• To each map $f : [n] \to [m]$ in 🧊, an arrow $X(f) : X_m \to X_n$. Specifically, these are all composites of the faces $X(\delta^i_j) : X_{n + 1} \to X_n$ and the degeneracies $X(\sigma_j) : X_n \to X_{n + 1}$.

Hold up - aren’t those backwards? Yes, they are! Remember, a cubical set is not a functor out of the category 🧊, it’s a functor out of $\cube{}^{op}$, so all of the arrows are backwards. To work more conveniently with cubical sets (and, in fact, more concretely) we need to take a very abstract detour through even more category theory.

The Unit Interval

Being functors $[\cube^{op}, \mathbf{Set}]$, we can also form maps between cubical sets, which are natural transformations $\alpha : X \to Y$. Specifically, a map between cubical sets assigns to each cube $c \in \cube$ a map $\alpha_c : F(c) \to G(c)$, such that for any morphism $f : c \to c\prime \in \cube$, the equation $\alpha_{c} \circ F(f) = G(f) \circ \alpha_{c\prime}$ holds. This condition is captured by the following diagram:

A standard construction in category theory is the Yoneda embedding functor, written $\yo$ (the hiragana character for “yo”), which maps an object of (in our case) $\cube$ into the category of cubical sets. It maps objects $c \in \cube$ to the hom-set functor $\mathrm{Hom}_{\cube}(-, c)$, which takes each object $d \in \cube^{op}$ to the set of morphisms $d \to c$ in 🧊. It takes the morphism $f : c \to d$ to the natural transformation $\yo(f) : \mathrm{Hom}_{\cube}(-, c) \to \mathrm{Hom}_{\cube}(-, d)$.

Let’s look at $\yo(f)$ some more. It’s a natural transformation between $\mathrm{Hom}(-, c)$ and $\mathrm{Hom}(-, d)$, so we can read that as a set of maps indexed by some $e \in \cube^{op}$. Since $\yo(f)_e : \mathrm{Hom}(e, c) \to \mathrm{Hom}(e, d)$, we can understand that the value $\yo(f)_e(g)$ takes for $g \in \mathrm{Hom}(e, c)$ is $f \circ g$.

The $\yo$ functor gives us, for an object $[n]$ in the category of cubes, an object.. well, $\yo([n])$ in the category of cubical sets. We’ll abbreviate $\yo([n])$ as $\square^n$ for time, since, as we’ll see, this object is very special indeed. Let’s consider, for simplicity, the unit interval cubical set, $\square^1$. We know it’s a functor from $\cube^{op}$ to $\mathbf{Set}$ — and more, we know exactly what it maps each cube to. The set of all maps from other cubes to $[1]$. Turns out, above $[1]$ this set only contains trivial cubes, so let’s look at what $\square^1_0$ and $\square^1_1$ are:

• For $\square^1_0$ we have to consider all ways of mapping the $0$-cube to the $1$-cube. These are the two “base” face maps $\delta^0$ and $\delta^1$.

• For $\square^1_1$, we have to consider all ways of mapping the $1$-cube to itself. You might think that this set is trivial, but think again (if you do): Yes, we do have the identity map $1_{[1]} : [1] \to [1]$, but we also have the compositions $\delta^0 \circ \sigma$ and $\delta^1 \circ \sigma$. Since we know what the objects in the category of cubes look like, you can think of these as the constant function f(x) = 0 and g(x) = 1 respectively, since that’s what they work out to:

$$(\delta^0 \circ \sigma)(x) = (\delta^0)(\sigma(x)) = \delta^0(()) = (0)$$

• For $\square^1_j, j > 1$ we only have degeneracies (and compositions of degeneracies) mapping $[j] \to [1]$.

Now, the standard cubes $\square^n$ don’t look very interesting. But you see, this is where I pulled a sneaky on you! Because of a result about $\yo$ — the Yoneda lemma. Specialised to our case, it says that for any n and any X, the sets $X_n$ and $\mathrm{Hom}(\square^n, X)$ correspond exactly: we can probe the structure of a cubical set $X$ by examining the classes of maps $\square^n$ to $X$.

Cubes in Sets

Let’s look at what the maps $\square^n \to X$ impart on $X$, shall we? But first, let’s reason a bit to identify how we can represent diagramatically the cubical set $\square^n$, by extrapolating our knowledge about the unit interval cubical set. For that case, $\square^1_0$ was the set containing both “endpoints” of the unit interval, and the set $\square^1_1$ contained two degenerate lines (for either endpoint — we’ll see how to think about these in the next section) and one non-degenerate line, which we think of as “the” unit interval.

So, in general, we think of $\square^n$ as consisting of the set $\square^n_0$ of vertices of X, the set $\square^n_1$ of lines of X, the set $\square^n_2$ of squares of X, the set $\square^n_3$ of cubes of X (cube in the sense of high school geometry), etc, all the way up to the set $\square^n_n$ of $n$-cubes of X, and all $\square^n_m, m > n$ are degenerate. We can represent these using.. diagrams! Diagrams of points, lines, squares, cubes, etc. Let’s look at the first few:

Now we can investigate a particular $n$-cube in $X$ as being a diagram in $X$ with the same shape as one of the diagrams above!

• A $0$-cube in X is just a point in X.

• A $1$-cube in X can be parsed to mean an arrow $f : x_0 \to x_1$. The points $x_0$ and $x_1$ are understood to be the cubes $f \circ \yo(\delta^0)$ and $f \circ \yo(\delta^1)$, which we call the endpoints of $f$. By composing with the image of a face map under $\yo$, we can project a lower-dimensional cube from a higher dimensional cube, by the action of $\yo$ on morphisms.

• A $2$-cube in X is a square $\sigma$ like

  

  In this diagram too we can understand the lower-dimensional cubes contained in $\sigma$ to be compositions $\sigma \circ \yo(p)$ for some composition of face maps $p : [m] \to [2], m \le 2$. As an example (the same example as in the section on 🧊), the arrow $p$ is the map $\sigma \circ \yo(\delta^0_0)$, and the point $b$ is the map $\sigma \circ \yo(\delta^0_0) \circ \yo(\delta^1)$. By functoriality of $\yo$, that composite is the same thing as $\sigma \circ \yo(\delta^0_0 \circ \delta^1)$.

• A $3$-cube in X is a map $\aleph : \square^3 \to X$, which could be visualized as the proper cube below, and has 6 2-faces (squares), 12 1-faces (edges) and 8 0-faces (vertices). As an exercise, work out which sequence of face maps in the underlying cube category leads leads to each of the possible 24 faces you can project. Honestly, the drawing of the $3$-cube isn’t even that enlightening, I just wanted to be fancy.

  Like, check out this absolute flex of a diagram, it’s god damn useless. Wow.

  As an a quick aside, can we talk about how god damn confusing this projection is? I can never tell whether I’m looking top-down at a truncated square pyramid ($\kappa$ is the top face) or if I’m looking through a normal solid 3-cube whose front face is transparent ($\kappa$ is the back face).

  

  In case it’s not clear (it’s not clear, I know), the 2-cubes present in the 3-cube $\aleph$ – yes, $\aleph$, that’s how hard I’m running out of letters over here – are these:

  • $\kappa$ is the square spanned by $w \to x \to z \leftarrow y \leftarrow w$.
  • $\lambda$ is the square spanned by $a \to w \to y \leftarrow c \leftarrow a$.
  • $\mu$ is the square spanned by $a \to b \to x \leftarrow w \leftarrow a$.
  • $\nu$ is the square spanned by $b \to x \to z \leftarrow d \leftarrow b$.
  • $\epsilon$ is the square spanned by $c \to y \to z \leftarrow d \leftarrow g$.
  • There is one more square, obscured by $\kappa$, which is spanned by $a \to b \to d \leftarrow c \leftarrow a$.

  Yeah, this item is padding. Fight me.

Now that we know we can represent particular cubes in a cubical set X by diagrams, I can also finally show you what a degeneracy actually looks like! For instance, we know $X(\sigma)$ maps from the set of points of $X$ to the set of lines of $X$ (since $X$ is contravariant, it inverts the direction of $\sigma$ – remember that).

If $x$ is a particular point in $X$, its image under $X(\sigma)$ is a degenerate line connecting $x \to x$. Connections on lines $l$ turn them into degenerate squares where two opposing faces are $l$ and the other two faces are degenerate, and so on.

In both diagrams above, the dashed arrow from the $n$-cube to the inside of $(n+1)$-cube is meant to be understood as $a \circ \yo(\sigma)$, where $a$ is a map $\square^n \to X$. $\sigma_0 \circ \sigma$ is the map which collapses a square to a point by first removing the first coordinate, which is understood to be left-right; Thus, the cells in the up-down direction in $f \circ \yo(\sigma_0) \circ \yo(\sigma)$ are thin, and the left-right cells are full.

More examples of Cubical Sets

The simplest way of making a cubical set is by taking a normal set, say $A$, and ignoring the cubes, thus making the discrete cubical set $K(A)$, which has $K_n = A$ for every $n$; $K(δ^i_j) = 1$ and $K(\sigma_i) = 1$.

It’s easy to see that $K(A)$ is a functor, since:

• $K(1) = 1$
• $K(g \circ f) = 1$, and $K(g) \circ K(f) = 1 \circ 1 = 1$.

And thus $K(A)$ is a cubical set. It doesn’t have a lot of interesting structure, but some discrete cubical sets will have important roles to play when discussing the category of cubical sets. For instance, $K(\mathbb{N})$ plays the same role in $\mathbf{cSet}$ as it does in $\mathbf{Set}$!

If $A$ and $B$ are cubical sets, we can form their product $A \times B$, which is also a cubical set. Every $(A \times B)_n$ is $A_n \times B_n$, and maps $(A \times B)(f) : A_n \times B_n \to A_m \times B_m$ are taken to products of morphisms $A(f) \times B(f)$.¹

Describing individual constructions on cubical sets (like their product) isn’t very enlightening, though, and it’s a lot more fruitful to describe most of them in one go. So, with that goal, I’ll describe..

The Category of Cubical Sets, $\mathbf{PSh}(\cube)$

Cubical sets are, of course, objects of a category, like all good things. We call a functor $X^{op} \to \mathbf{Set}$ a presheaf on $X$, and we denote the category of presheaves on $X$ by $\mathbf{PSh}(X)$. Thus, since a cubical set is a functor $\cube^{op} \to \mathbf{Set}$, we can also call it a presheaf on 🧊, and thus, an object of $\mathbf{PSh}(\cube)$. To reduce the number of ice cube emoji on the screen, we’ll denote this category by $\mathbf{cSet}$.

The word “presheaf”, rigorously, only means “contravariant functor into $\mathbf{Set}$.” However, it’s what the nLab calls a “concept with an attitude”: If you call something a “presheaf category” instead of a “functor category”, it’s likely that you’re interested in the properties of $\mathbf{PSh}(C)$ as a presheaf topos, and, indeed, that’s what we’re interested in.

A topos is a “particularly nice category to do mathematics”, in which “nice” means “has a lot of structure”. Let’s look at some of the structure $\mathbf{cSet}$ (and, indeed, any $\mathbf{PSh}(C)$) has for “free”:

• Completeness Every small limit exists in $\mathbf{cSet}$, and is computed pointwise as a limit in $\mathbf{Set}$. This is an extension of the product of cubical sets mentioned above: a product is just a small, discrete limit. In particular, this also includes a terminal object in cubical sets, which is the discrete cubical set $K(1)$.

• Cocompleteness Every small colimit exists in $\mathbf{cSet}$. In particular, if $C$ is a category, $\mathbf{PSh}(C)$ is often referred to as the “free cocompletion” of $C$ — C plus all small colimits thrown in. These are also computed pointwise as colimits in $\mathbf{cSet}$. Don’t know what a colimit is? One particularly important example is the coproduct $A + B$. In $\mathbf{Set}$, this is the disjoint union.

  Another important colimit is the initial object in cubical sets, which is the discrete cubical set $K(0)$.

• Cartesian closure This one merits a little more explanation than a paragraph. Fix a cubical set $X$. To say $\mathbf{cSet}$ is Cartesian closed is to say the functor $- \times X$ (“product with X”, called “tensor”) has a right adjoint functor $[X, -]$, called “hom” (also read “function from X”, at least by me) - That is, $\mathrm{Hom}(A \times X, B) \simeq \mathrm{Hom}(A, [X, B])$.

  We can try to imagine what a would-be $[A, B]$ would be like by fixing a third cubical set $Z$ and seeing that if $[A, B]$ exists, then it must satisfy the equation

  $$\mathrm{Hom}_{\mathbf{cSet}}(Z, [X, Y]) \simeq \mathrm{Hom}_{\mathbf{cSet}}(Z \times X, Y).$$

  This equation holds when $c \in \cube$ and $Z = \yo(c)$, so by the Yoneda lemma we have

  $$\mathrm{Hom}_{\mathbf{cSet}}(y(c) \times X, Y) \simeq \mathrm{Hom}_{\mathbf{cSet}}(\yo(c), [X, Y]) \simeq [X, Y](c)$$

  By defining an “evaluation” map, $\mathrm{ev} : X \times [X, Y] \to Y$, and showing that for every $f : X \times A \to Y$ there is a $\lambda{}(f) : A \to [X, Y]$, we can prove that $\mathrm{ev}$ is the counit of the tensor-hom adjunction we want in $\mathbf{PSh}(\cube)$, and thus that the definition posed above is indeed the correct definition of $[X, Y]$ for cubical sets. For the details of this construction, check out the nLab.

• And a wealth of other properties, like local cartesian closure (“has dependent products”), having a subobject classifier (a “type of propositions”), having power objects (a generalisation of power sets), among many others.

Kan Cubical Sets

The category of cubical sets is pretty neat by itself, but.. it’s kinda useless. I’m sure there exist applications of cubical sets by themselves, but I can’t think of any. The cubical sets, just like the simplicial sets, come into their own when we consider the subcategory of $\mathbf{cSet}$ (resp. $\mathbf{sSet}$) consisting of the Kan complexes. Since the term Kan complex is generally used to mean “Kan simplicial set”, we’re generally left to use either “Kan cubical set” or “Cubical complex” for the objects of our subcategory. Let’s go with the former.

Fix a cubical set $X$ throughout. We define the boundary of an $n$-cube $x$, $\partial x$, to be the union of all of its faces. This can be pictured diagramatically as below: The faces of $\sigma$ are all of the points and arrows spanning it, and the union of these is $\partial \sigma$.

We still have the same 0-cubes and 1-cubes spanning $\sigma$, but the 2-cube $\sigma$ itself is no longer under consideration. We are principally interested in the boundaries of the standard $n$-cubes, which will be denoted $\partial \square^n$. Considering that boundary, we can define a box open in $\square^n$ as being the subset of $\partial \square^n$ with one (the face in the image of $\delta^\varepsilon_i$) of its $n-1$ faces removed. This we denote by $\sqcap^{n,i,\varepsilon}$.

Just like in the case of an $n$-cube in $X$, we understand the phrase “$(n,i,\varepsilon)$-open box in $X$” to mean a map $\sqcap^{n,i,\varepsilon} \to X$. Here are diagrams of all the open boxes in the same $\sigma$ as before.

A cubical set satisfies the Kan condition if every open box in X can be extended to a cube, or, more formally, if there exists a dotted arrow $g$ which factors the map $f$ through the inclusion from $\sqcap^{n,i}$ into $\square^n$.

The Cubical Nerve

First, recall the definition of a groupoid. A groupoid $\mathcal{G}$ is a category in which for every arrow $f : A \to B$ there exists an arrow $f^{-1}$, such that ${f \circ f^{-1}} = {f^{-1} \circ f} = 1$. That is: a groupoid is a category in which every arrow is invertible. There is a (2-)category of groupoids, $\mathbf{Grpd}$, in which the objects are groupoids and the morphisms are functors (and the 2-morphisms are natural isos).

We specify a functor $N^{\le 2} : \mathbf{Cat} \to \mathbf{cSet}$, the truncated nerve functor, which assigns to every groupoid a cubical set in which every $n\ge{}3$-cube is degenerate, as follows:

• The points in $N^{\le 2}(A)$ are the objects in $A$,

• The lines $f : a_0 \to a_1$ in $N^{\le 2}(A)$ are the arrows $f : a_0 \to a_1$ in $A$; The lines induced by degeneracy maps are the identity arrows.

• The squares in $N^{\le 2}(A)$ are the squares with corners $a, b, c, d$ spanned by $f : a \to c$, $p : a \to b$, $q : c \to d$, $g : b \to d$, such that $g \circ p = q \circ f$ - that is, the commutative squares with that boundary.

  The degenerate squares in $N^{\le 2}(A)$ are the squares as below, and they exist for every $a, b$, and $f : a \to b$ in $A$:

  

I claim: If $A$ is a groupoid, then its nerve $N^{\le 2}(A)$ is always Kan. I will not show this with a lot of rigour, but to convince yourself of this fact, deliberate on what it means to fill boundaries of our non-degenerate cubes: the lines and squares.

• In the case of lines, an open box $\sqcap^{1,0,i}$ is just a point $x_i$; We can extend this to a line $1_{x_i} : x_i \to x_i$, as desired.

• In the case of squares, an open box $\sqcap^{2,i,\varepsilon}$ is a diagram like the one below, in which all of the corners are objects of $A$ and the lines are maps in $A$. The maps in $A$ are invertible, so if we have $q$, we also have $q^{-1}$ (for instance).

  

  We’re looking for the map $f : a \to c$. The strategy to use here is to try to “follow” the source of the missing arrow “around” the edges of the cube, and, if you get stuck, invert the arrow you got stuck on. We take $a$ to $b$ through $p$, then to $d$ through $g$, and now we’re stuck. A priori, there’s no arrow $d \to c$ we can follow, but since $A$ is a groupoid, we can invert $q$ to get $q^{-1} : d \to c$. Thus the composite $q^{-1} \circ g \circ p$ connects $a$ and $c$, like we wanted.

  Moreover, this diagram must commute, i.e., we must check that $g \circ p = q \circ (q^{-1} \circ g \circ p)$. But this is automatic from the axioms of a category (which say we can ignore the parentheses), and the axioms for a groupoid, which imply that $q \circ q^{-1} \circ f = f$ (for any f).

We have established that the truncated nerve of a groupoid is Kan. Why truncated? Because we only consider 1-categories in the construction of $N^{\le 2}$, and, as the superscript implies, only have non degenerate cubes for levels 2 and below. We could consider an untruncated $N$ functor from $\infty$-categories to cubical sets; In that case, the nerve of an $\infty$-groupoid is Kan, just like in the 1-categorical case.

More surprising, the converse implication is also true! If the nerve $N^{\le 2}(A)$ of a category is Kan, then $A$ is a groupoid. Adapting the analogous argument from Kerodon about Kan complexes to our Kan cubical sets, we’re given an $f : a \to b \in A$, and we build left and right inverses $g, h : b \to a$ to $f$.

This can be done by defining a pair of partial squares in $N^{\le 2}(A)$, in which the missing faces represent left and right inverses to our map $f \in A$. Here they are:

By assumption, $N^{\le 2}(A)$ is Kan, which means these open boxes do have fillers, and thus the equations $g \circ f = 1$ and $f \circ h = 1$ hold in $A$. We calculate: $g = 1 \circ g = h \circ f \circ g = h \circ 1 = 1$, leaving implicit the applications of associativity of $\circ$, thus concluding that $g = h$ is an inverse to $f$.

In either case, we’re considering a globular construction (a groupoid) as a cubical construction. This consideration can be interpreted for any “level” of higher structure which you might want: above, we only had 1-cells in our groupoid, but, for example, here’s what a two-cell $\alpha$ in a globular $n$-category might look like interpreted cubically:

Similarly, if we take our good old square $\sigma$, we can interpret that as a globular 2-cell, by “stretching” the diagram vertically, inserting degenerate cells where appropriate.

For more details on the connection between thin cubes and globes, in the particular case of double categories and 2-categories, the paper Double categories, 2-categories, thin structures and connections by Brown and Mosa is excellent. It also contains pictorial represntations of the equations which have to hold between faces, degeneracies and connections, which I have entirely neglected!

The discrete cubical set $K(A)$ is Kan

This follows from the name, it’s a $K(A)_n$ complex, duh!

That was a joke, but it was a bad one. As a quick reminder, every $K(A)_n$ is taken to be the set $A$, and all of the restrictions (faces and degeneracies) are the identity on $A$. We want to show that every open box $\sqcap^{n,i,\varepsilon}$ in $K(A)$ has a unique filler. But consider (by way of handwaving) what an open box $\sqcap^{n,i,\varepsilon}$ is: A cube $\square^n \to K(A)$ with “one of its faces removed”.

Any cube $b : \square^n \to K(A)$ is an element of $K(A)_n$ (by the Yoneda lemma), which is the set $A$, by definition. The cube $b$ has however many $(n - 1)$-dimensional faces, which we can compute by applying the appropriate face maps. Since the face maps in $K(A)$ are all the identity function, we learn that all of $b$’s faces have to be the same element $b \in A$, regarded as $(n-1)$-dimensional cubes.

By this argument, every open box $o$ of dimension $n$ in $K(A)$ is made up of the same element $b \in A$ in all of its faces. We can extend this box to an $n$-cube which is just the element $b$: It is a complete $n$-cube of $K(A)$, and it has all of the same faces as $o$ where both are defined.

We can consider the category made up of only those cubical sets which are Kan complexes. This turns out to be a very interesting category! Specifically, I’m talking about the full subcategory of $\mathbf{cSet}$ on the Kan complexes, which turns out to be equivalent to the $(\infty,1)$-topos of $\mathbf{\infty{}Grpd}$ of $\infty$-groupoids. A recent result by Shulman shows that this category, which I guess can be called $\mathbf{cSet}_{\mathrm{Kan}}$, models… Homotopy Type Theory.

Cubical Types

Aha! That paragraph was a twist, but it wouldn’t be a post on this blog if I didn’t manage to write in type theory somehow! However, if you went back to the first paragraph, you’d have seen this coming. My interest in Kan cubical sets is entirely due to, well, these two papers, in which a model of MLTT + the univalence axiom (modulo the computation rule for J only holding up to a path):

• A Model of Type Theory in Cubical Sets by Bezem, Coquand and Huber in which they exhibit a model, which was later refined to

• Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom by Cohen, Coquand, Huber and Mörtberg.

By definition, a type in these theories is a Kan cubical set. A type in a context like $i, j, k : \mathbb{I} \vdash A$ is roughly like the set $A([3])$, if you ignore that their cube category is completely different from the one presented here! They’re (roughly) equivalent, though, except for the cube category of CCHM having operations called reversals (which invert one dimension) and special kinds of degeneracies called connections. A connection is a degeneracy like in the diagram below, which I am stealing from my own post about CCHM:

Ahem, please forgive past-me’s type theoretic accent. These are, like the normal degeneracies, 2-cubes in which 2 faces are thin (these are the $\lambda i. p\ ik$ faces in the diagram), and the two other faces are the 1-cube we degenerated (the line $p$). Connections are a very natural extension to the theory of Kan cubical sets, since in a sense they say that an $n$-cube is regarded as a degenerate $(n+1)$-cube in all of the possible ways.

This extra structure of connections turns out to be very important when considering a category of cubical sets as an alternative to the category of simplicial sets, $\mathbf{sSet}$, when doing homotopy theory. This is because cubes without connection are not a strict test category, a property which is… complicated to describe. But very roughly, it says that the canonical way of mapping between cubical sets and homotopy types does not preserve products.

The perspective we can get that from this particular application of (Kan) cubical sets is that they provide a systematic way to represent the elements of a type ($X_0$), the equalities between elements of that type ($X_1$), the homotopies between equalities in that type ($X_2$), and so forth. In that sense it’s not surprising that Kan cubical sets can be used to (almost) model HoTT!

Conclusion

I don’t know why I write conclusions; These aren’t high school essays. However, in this case I do feel compelled to apologise for how technical and disjointed this post was, and how it seems like I needlessly elaborated on things which (to some) might be trivial while not going into enough detail about highly non-trivial things.

Like I said in the first paragraph, I was writing this to learn more about cubical sets. So, unlike my other posts, which are explaining concepts I already had an understanding of — for instance, my last proper post was talking about my implementation of cubical type theory, not cubical type theory in general — this post is explaining something I had a fuzzy understanding of, and touches on some category-theoretical concepts I didn’t have the faintest clue about, like the Yoneda embedding.

Several people had tried to explain the Yoneda embedding to me before, but it had never stuck. It was only when I actually wrote out the definition, worked through its effect on objects and maps, and explored a bit of the structure of the unit interval cubical set. I guess explaining something really is the best way to learn it!

This was my shortest interval between blog posts maybe.. ever. Don’t get used to it! This is the blog post I should’ve written instead of whatever filler about Axiom J I wrote about last time, but motivation works in mysterious ways when you struggle with depression. In reality, it’s not that mysterious — I’m writing this on the last week of the first academic semester of 2021, which means the deadline anxiety has finally been lifted. God damn, I hate university.

References

Since this post is a lot more technical than my others, and it’s about something I don’t know a lot about, I figured I should cite my sources so you can know I’m not spewing complete baloney. I don’t know how people cite things in English-speaking countries, and, to be perfectly honest, I’ve done a terrible job of keeping track of where I got all this stuff, but here are the papers and pages and textbooks I consulted along the way:

The nLab. Seriously. So many nLab pages. I think these three are the ones I visited most often while writing this post, though:

• closed monoidal structure on presheaves - Definition of $[X,Y]$
• fundamental groupoid of a cubical set and the cubical nerve of a groupoid - Direct definition of $N^{\le 2}$
• cubical set - guess :)

The following papers:

• A Model of Type Theory in Cubical Sets
• Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom
• An Elementary Illustrated Introduction to Simplicial Sets
• Varieties of Cubical Sets
• All $(\infty,1)$-toposes have strict univalent universes

The following pages from Kerodon:

• The Homotopy Coherent Nerve
• The Nerve of a Groupoid