---
title: Cubical Sets
date: June 21th, 2021

abbreviations:
  cube: 🧊
  globe: 🌎
  yo: よ
---

<div class="warning">

Throughout this post I'll use the ice cube emoji, &cube;, to stand for the _category of cubes_, which is more traditionally written □ (a blank square). The reason for this is that I have a really convenient emoji picker, so when I write about cubes on Twitter, it's a lot easier to call the category &cube; (maybe 4 keystrokes to select) rather than looking up the proper symbol on Google.

If you can't see this symbol - &cube; - then you should probably download an emoji font.

</div>

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 &cube;
----------------------------

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:

  <figure>
  <img height=200px alt="A diagram meant to indicate the inclusion of a point as a 0-face in the 2-cube. Colours are used to indicate how the point is mapped to the endpoint of a line, and then the corner of a square." src="/diagrams/cubicalsets/delta10_delta0.svg" />
  <figcaption>Including the $\color{red}{\bullet}$ point as a 0-face in the 2-cube </figcaption>
  </figure>

  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 &cube; is a category, we can consider standard category-theoretical operations _on_ &cube;, 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 &cube;, a _set_ $X(c)$. Since the objects of &cube; are all $[n]$, these are alternatively notated $X_n$.

- To each map $f : [n] \to [m]$ in &cube;, 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 &cube;, 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:

<figure>
<img height=200px alt="A naturality square" src="/diagrams/cubicalsets/naturality.svg" />
<figcaption>Is it even possible to talk about category theory without drawing a naturality square?</figcaption>
</figure>

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 &cube;.
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$.

<details>
<summary>The Yoneda lemma</summary>

The Yoneda lemma is a result about an arbitrary category $C$, its category of _presheaves_ $\mathbf{PSh}(C) = [C^{op}, \mathbf{Set}]$, and the functor $\yo(c)$ we just defined. Its statement is as follows:

$$
\mathrm{Hom}(\yo(c), F) \simeq F(c)
$$

In our case, it's interesting particularly because it says that we can explore the structure of a cubical set --- a presheaf on $\cube$ --- by analysing the maps from the standard $n$-cube $\square^n$ into $X$. Furthermore, it implies the Yoneda embedding $\yo$ is _fully faithful_, by the following calculation:

$$
\mathrm{Hom}_{\mathbf{PSh}(C)}(\yo(c), \yo(d)) \simeq \yo(d)(c) \simeq \mathrm{Hom}_{C}(c, d)
$$

It thus realises $C$ as a full subcategory of $\mathbf{PSh}(C)$ - in our case, the category $\cube$ as a subcategory of the category of cubical sets. This is useful because $\mathbb{PSh}(C)$ is a category with a _lot_ of structure (as we shall see), even when $C$ doesn't have any structure.

This also means that we can study maps between cubes by studying maps of standard cubical sets, which is good, because degeneracies in the category of cubes confuse me to death!

</details>

### 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:

<figure>
<img height=200px alt="The image of the first 3 objects of the category of cubes under the Yoneda embedding are cubical sets representing familiar shapes: a point, a line, a square, and a (solid) cube." src="/diagrams/cubicalsets/first_ncubes.svg" />
<figcaption>The cubical sets $\square^0$, $\square^1$, $\square^2$, $\square^3$.</figcaption>
</figure>

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
  
  <figure>
  <img alt="A diagrammatic representation of a particular square in a cubical set." height=200px src="/diagrams/cubicalsets/asquare.svg" />
  <figcaption>A square $\sigma$.</figcaption>
  </figure>

  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 &cube;), 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).
  <figure class="wraparound">
  <img alt="A diagrammatic representation of a particular cube in a cubical set. The diagram is incredibly busy and not very helpful." height=200px src="/diagrams/cubicalsets/acube.svg" />
  <figcaption>A _proper_ cube, finally!</figcaption>
  </figure>

  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.

<figure>
<img height=200px alt="Diagrammatic representations of the degeneracy which expresses a point as a degenerate line, and one of the ways of expressing a line as a degenerate square." src="/diagrams/cubicalsets/degeneracies.svg" />
<figcaption>Some degeneracies in cubical sets, diagrammed.</figcaption>
</figure>

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)$.[^1]

[^1]: Where $(f \times g)(x, y) = (f(x), g(y))$ in $\mathbf{Set}$.

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 &cube;_, 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](https://ncatlab.org/nlab/show/closed+monoidal+structure+on+presheaves).

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

<div class=mathpar>
  <figure>
  <img height=200px alt="The same square in a cubical set as before." src="/diagrams/cubicalsets/asquare.svg" />
  <figcaption>The same ol' square $\sigma$.</figcaption>
  </figure>

  <figure>
  <img height=200px alt="The square, but with its inside (σ) removed." src="/diagrams/cubicalsets/del_asquare.svg" />
  <figcaption>The boundary of the square $\sigma$.</figcaption>
  </figure>
</div>

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.

<figure>
<img height=200px alt="All possible open boxes of the square σ, which you get by removing one of the faces. In the diagram, the missing face was replaced with a dotted line." src="/diagrams/cubicalsets/open_boxes.svg" />
<figcaption>All of the open boxes in $\sigma$.</figcaption>
</figure>

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

<figure>
<img height=200px alt="A commutative triangle representing the Kan condition." src="/diagrams/cubicalsets/kan_condition.svg" />
<figcaption>The Kan condition on the cubical sets $X$.</figcaption>
</figure>

### 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$:

  <figure>
  <img height=200px alt="Degenerate squares in the truncated cubical nerve of a category." src="/diagrams/cubicalsets/thin_squares.svg" />
  <figcaption>Thin squares in $N^{\le 2}(A)$</figcaption>
  </figure>

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

  <figure>
  <img height=200px alt="A particular open box in the truncated cubical nerve of a groupoid." src="/diagrams/cubicalsets/open_box.svg" />
  <figcaption>A representative example of open boxes in $f$.</figcaption>
  </figure>

  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](https://kerodon.net/tag/0037) 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:

<div class=mathpar>
  <figure style="width:48%;">
    <img height=200px alt="The open box which computes the left inverse of a map f." src="/diagrams/cubicalsets/left_inv.svg" />
    <figcaption>If this open box had a filler, it would witness in $A$ the equation $g \circ f = 1$.</figcaption>
  </figure>
  <figure style="width:48%;">
    <img height=200px alt="The open box which computes the right inverse of a map f." src="/diagrams/cubicalsets/right_inv.svg" />
    <figcaption>If this open box had a filler, it would witness in $A$ the equation $f \circ h = 1$.</figcaption>
  </figure>
</div>

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:  

<div class=mathpar>
  <figure style="width:48%;">
    <img height=200px alt="A globular cell in a 2-category is an α with 0-cells a, b and 1-cells f, g as a boundary." src="/diagrams/cubicalsets/globular_2cell.svg" />
    <figcaption>A globular cell in a 2-category is an $\alpha$ with 0-cells $a, b$ and 1-cells $f, g$ as a boundary.</figcaption>
  </figure>
  <figure style="width:48%;">
    <img height=200px alt="The same globular cell, stretched into a square." src="/diagrams/cubicalsets/cubical_2cell.svg" />
    <figcaption>We can interpret it as a cubical 2-cell where two faces are thin.</figcaption>
  </figure>
</div>

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.

<div class=mathpar>
  <figure style="width:48%;">
    <img height=200px alt="The same square you've read about 3 times now." src="/diagrams/cubicalsets/asquare.svg" />
    <figcaption>Our good friend $\sigma$.</figcaption>
  </figure>
  <figure style="width:48%;">
    <img height=200px alt="Squishing the square into a globe by composing the adjacent morphisms." src="/diagrams/cubicalsets/aglobe.svg" />
    <figcaption>We collapse it into a globular $\sigma_\globe$ by composing the composable arrows.</figcaption>
  </figure>
</div>

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](http://www.tac.mta.ca/tac/volumes/1999/n7/5-07abs.html) 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 <span class=together>$b$'s</span> 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](https://arxiv.org/abs/1904.07004) 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](http://www.cse.chalmers.se/~coquand/mod1.pdf) 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](https://arxiv.org/abs/1611.02108) by **C**ohen, **C**oquand, **H**uber 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](/posts/cubical-type-theory.html):

<blockquote>
<div class="mathpar">

<figure style="width: 48%;">
<img src="/diagrams/ctt/land_connection.svg" alt="And connection" style="min-width: 250px;" />
<figcaption>The square generated by $\lambda i\ j. p(i \land j)$</figcaption>
</figure>

<figure style="width: 48%;">
<img src="/diagrams/ctt/lor_connection.svg" alt="Or connection" style="min-width: 250px;" />
<figcaption>The square generated by $\lambda i\ j. p(i \lor j)$</figcaption>
</figure>

</div>
</blockquote>

_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](https://ncatlab.org/nlab/show/closed+monoidal+structure+on+presheaves) - Definition of $[X,Y]$
- [fundamental groupoid of a cubical set and the cubical nerve of a groupoid](https://ncatlab.org/nlab/show/fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#nerve_functor) - Direct definition of $N^{\le 2}$
- [cubical set](https://ncatlab.org/nlab/show/cubical+set#in_higher_category_theory) - guess :)

The following papers:

- [A Model of Type Theory in Cubical Sets](http://www.cse.chalmers.se/~coquand/mod1.pdf)
- [Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom](https://arxiv.org/abs/1611.02108)
- [An Elementary Illustrated Introduction to Simplicial Sets](https://arxiv.org/abs/0809.4221)
- [Varieties of Cubical Sets](https://www2.mathematik.tu-darmstadt.de/~buchholtz/varieties-of-cubical-sets.pdf)
- [All $(\infty,1)$-toposes have strict univalent universes](https://arxiv.org/abs/1904.07004)

The following pages from Kerodon:

- [The Homotopy Coherent Nerve](https://kerodon.net/tag/00KM)
- [The Nerve of a Groupoid](https://kerodon.net/tag/0035)
