Cubical Sets

Cubical Sets

Posted on June 21, 2021
Word count: 5196

Throughout this post I’ll use the ice cube emoji, 🧊, 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 🧊 (maybe 4 keystrokes to select) rather than looking up the proper symbol on Google.

If you can’t see this symbol - 🧊 - then you should probably download an emoji font.

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 FF (the letter FF 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 FF 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\{0,1\}^n, which we abbreviate to [n][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 nn-cube to an (n+1)(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 δ0(())=0\delta^0(()) = 0 and δ1(())=1\delta^1(()) = 1.

    As further examples, we have functions δji\delta^i_j (for 0i,j10 \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, δ00(j)=(0,j)\delta^0_0(j) = (0, j), δ10(i)=(i,0)\delta^0_1(i) = (i, 0), δ01(j)=(1,j)\delta^1_0(j) = (1, j), and δ11(i)=(i,1)\delta^1_1(i) = (i, 1).

    These also compose. For instance, the map δ00δ1:[0][2]\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:

    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.

    Including the \color{red}{\bullet} point as a 0-face in the 2-cube

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

  • The degeneracies, which “collapse” an (n+1)(n+1)-cube to an nn-cube by deleting a dimension. The most basic degeneracy is given by the unique map σ:[1][0]\sigma : [1] \to [0]. There are two degeneracies [2][1][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 1n:[n][n]1_n : [n] \to [n] which returns its argument nn-tuple (cube) unchanged. It’s easy to see that this is the identity for composition, which is as in Set\mathbf{Set}. Since 🧊 is a category, we can consider standard category-theoretical operations on 🧊, like taking its opposite category, 🧊op\cube^{op}. The category 🧊op\cube^{op} has as its objects the same cubes [n][n] as before, but all of the maps are backwards, so that the face maps in 🧊op\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:🧊opSetX : \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][n]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 cc in 🧊, a set X(c)X(c). Since the objects of 🧊 are all [n][n], these are alternatively notated XnX_n.

  • To each map f:[n][m]f : [n] \to [m] in 🧊, an arrow X(f):XmXnX(f) : X_m \to X_n. Specifically, these are all composites of the faces X(δji):Xn+1XnX(\delta^i_j) : X_{n + 1} \to X_n and the degeneracies X(σj):XnXn+1X(\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 🧊op\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 [🧊op,Set][\cube^{op}, \mathbf{Set}], we can also form maps between cubical sets, which are natural transformations α:XY\alpha : X \to Y. Specifically, a map between cubical sets assigns to each cube c🧊c \in \cube a map αc:F(c)G(c)\alpha_c : F(c) \to G(c), such that for any morphism f:cc🧊f : c \to c\prime \in \cube, the equation αcF(f)=G(f)αc\alpha_{c} \circ F(f) = G(f) \circ \alpha_{c\prime} holds. This condition is captured by the following diagram:

A naturality square
Is it even possible to talk about category theory without drawing a naturality square?

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🧊c \in \cube to the hom-set functor Hom🧊(,c)\mathrm{Hom}_{\cube}(-, c), which takes each object d🧊opd \in \cube^{op} to the set of morphisms dcd \to c in 🧊. It takes the morphism f:cdf : c \to d to the natural transformation (f):Hom🧊(,c)Hom🧊(,d)\yo(f) : \mathrm{Hom}_{\cube}(-, c) \to \mathrm{Hom}_{\cube}(-, d).

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

The \yo functor gives us, for an object [n][n] in the category of cubes, an object.. well, ([n])\yo([n]) in the category of cubical sets. We’ll abbreviate ([n])\yo([n]) as n\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, 1\square^1. We know it’s a functor from 🧊op\cube^{op} to Set\mathbf{Set} — and more, we know exactly what it maps each cube to. The set of all maps from other cubes to [1][1]. Turns out, above [1][1] this set only contains trivial cubes, so let’s look at what 01\square^1_0 and 11\square^1_1 are:

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

  • For 11\square^1_1, we have to consider all ways of mapping the 11-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][1]1_{[1]} : [1] \to [1], but we also have the compositions δ0σ\delta^0 \circ \sigma and δ1σ\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:

(δ0σ)(x)=(δ0)(σ(x))=δ0(())=(0) (\delta^0 \circ \sigma)(x) = (\delta^0)(\sigma(x)) = \delta^0(()) = (0)

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

Now, the standard cubes n\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 XnX_n and Hom(n,X)\mathrm{Hom}(\square^n, X) correspond exactly: we can probe the structure of a cubical set XX by examining the classes of maps n\square^n to XX.

The Yoneda lemma

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

Hom((c),F)F(c) \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 nn-cube n\square^n into XX. Furthermore, it implies the Yoneda embedding \yo is fully faithful, by the following calculation:

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

It thus realises CC as a full subcategory of PSh(C)\mathbf{PSh}(C) - in our case, the category 🧊\cube as a subcategory of the category of cubical sets. This is useful because PSh(C)\mathbb{PSh}(C) is a category with a lot of structure (as we shall see), even when CC 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!

Cubes in Sets

Let’s look at what the maps nX\square^n \to X impart on XX, shall we? But first, let’s reason a bit to identify how we can represent diagramatically the cubical set n\square^n, by extrapolating our knowledge about the unit interval cubical set. For that case, 01\square^1_0 was the set containing both “endpoints” of the unit interval, and the set 11\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 n\square^n as consisting of the set 0n\square^n_0 of vertices of X, the set 1n\square^n_1 of lines of X, the set 2n\square^n_2 of squares of X, the set 3n\square^n_3 of cubes of X (cube in the sense of high school geometry), etc, all the way up to the set nn\square^n_n of nn-cubes of X, and all mn,m>n\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:

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.
The cubical sets 0\square^0, 1\square^1, 2\square^2, 3\square^3.

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

  • A 00-cube in X is just a point in X.

  • A 11-cube in X can be parsed to mean an arrow f:x0x1f : x_0 \to x_1. The points x0x_0 and x1x_1 are understood to be the cubes f(δ0)f \circ \yo(\delta^0) and f(δ1)f \circ \yo(\delta^1), which we call the endpoints of ff. 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 22-cube in X is a square σ\sigma like

    A diagrammatic representation of a particular square in a cubical set.

    A square σ\sigma.

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

  • A 33-cube in X is a map :3X\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 33-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).

    A diagrammatic representation of a particular cube in a cubical set. The diagram is incredibly busy and not very helpful.

    A proper cube, finally!

    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 wxzyww \to x \to z \leftarrow y \leftarrow w.
    • λ\lambda is the square spanned by awycaa \to w \to y \leftarrow c \leftarrow a.
    • μ\mu is the square spanned by abxwaa \to b \to x \leftarrow w \leftarrow a.
    • ν\nu is the square spanned by bxzdbb \to x \to z \leftarrow d \leftarrow b.
    • ϵ\epsilon is the square spanned by cyzdgc \to y \to z \leftarrow d \leftarrow g.
    • There is one more square, obscured by κ\kappa, which is spanned by abdcaa \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(σ)X(\sigma) maps from the set of points of XX to the set of lines of XX (since XX is contravariant, it inverts the direction of σ\sigma – remember that).

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

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.
Some degeneracies in cubical sets, diagrammed.

In both diagrams above, the dashed arrow from the nn-cube to the inside of (n+1)(n+1)-cube is meant to be understood as a(σ)a \circ \yo(\sigma), where aa is a map nX\square^n \to X. σ0σ\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(σ0)(σ)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 AA, and ignoring the cubes, thus making the discrete cubical set K(A)K(A), which has Kn=AK_n = A for every nn; K(δji)=1K(δ^i_j) = 1 and K(σi)=1K(\sigma_i) = 1.

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

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

And thus K(A)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(N)K(\mathbb{N}) plays the same role in cSet\mathbf{cSet} as it does in Set\mathbf{Set}!

If AA and BB are cubical sets, we can form their product A×BA \times B, which is also a cubical set. Every (A×B)n(A \times B)_n is An×BnA_n \times B_n, and maps (A×B)(f):An×BnAm×Bm(A \times B)(f) : A_n \times B_n \to A_m \times B_m are taken to products of morphisms A(f)×B(f)A(f) \times B(f).1

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, PSh(🧊)\mathbf{PSh}(\cube)

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

The word “presheaf”, rigorously, only means “contravariant functor into Set\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 PSh(C)\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 cSet\mathbf{cSet} (and, indeed, any PSh(C)\mathbf{PSh}(C)) has for “free”:

  • Completeness Every small limit exists in cSet\mathbf{cSet}, and is computed pointwise as a limit in Set\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)K(1).

  • Cocompleteness Every small colimit exists in cSet\mathbf{cSet}. In particular, if CC is a category, PSh(C)\mathbf{PSh}(C) is often referred to as the “free cocompletion” of CC — C plus all small colimits thrown in. These are also computed pointwise as colimits in cSet\mathbf{cSet}. Don’t know what a colimit is? One particularly important example is the coproduct A+BA + B. In Set\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)K(0).

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

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

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

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

    HomcSet(y(c)×X,Y)HomcSet((c),[X,Y])[X,Y](c)\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, ev:X×[X,Y]Y\mathrm{ev} : X \times [X, Y] \to Y, and showing that for every f:X×AYf : X \times A \to Y there is a λ(f):A[X,Y]\lambda{}(f) : A \to [X, Y], we can prove that ev\mathrm{ev} is the counit of the tensor-hom adjunction we want in PSh(🧊)\mathbf{PSh}(\cube), and thus that the definition posed above is indeed the correct definition of [X,Y][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 cSet\mathbf{cSet} (resp. sSet\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 XX throughout. We define the boundary of an nn-cube xx, 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.

The same square in a cubical set as before.
The same ol’ square σ\sigma.
The square, but with its inside (σ) removed.
The boundary of the square σ\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 nn-cubes, which will be denoted n\partial \square^n. Considering that boundary, we can define a box open in n\square^n as being the subset of n\partial \square^n with one (the face in the image of δiε\delta^\varepsilon_i) of its n1n-1 faces removed. This we denote by n,i,ε\sqcap^{n,i,\varepsilon}.

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

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.
All of the open boxes in σ\sigma.

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 gg which factors the map ff through the inclusion from n,i\sqcap^{n,i} into n\square^n.

A commutative triangle representing the Kan condition.
The Kan condition on the cubical sets XX.

The Cubical Nerve

First, recall the definition of a groupoid. A groupoid G\mathcal{G} is a category in which for every arrow f:ABf : A \to B there exists an arrow f1f^{-1}, such that ff1=f1f=1{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, Grpd\mathbf{Grpd}, in which the objects are groupoids and the morphisms are functors (and the 2-morphisms are natural isos).

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

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

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

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

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

    Degenerate squares in the truncated cubical nerve of a category.

    Thin squares in N2(A)N^{\le 2}(A)

I claim: If AA is a groupoid, then its nerve N2(A)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 1,0,i\sqcap^{1,0,i} is just a point xix_i; We can extend this to a line 1xi:xixi1_{x_i} : x_i \to x_i, as desired.

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

    A particular open box in the truncated cubical nerve of a groupoid.

    A representative example of open boxes in ff.

    We’re looking for the map f:acf : 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 aa to bb through pp, then to dd through gg, and now we’re stuck. A priori, there’s no arrow dcd \to c we can follow, but since AA is a groupoid, we can invert qq to get q1:dcq^{-1} : d \to c. Thus the composite q1gpq^{-1} \circ g \circ p connects aa and cc, like we wanted.

    Moreover, this diagram must commute, i.e., we must check that gp=q(q1gp)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 qq1f=fq \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 N2N^{\le 2}, and, as the superscript implies, only have non degenerate cubes for levels 2 and below. We could consider an untruncated NN 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 N2(A)N^{\le 2}(A) of a category is Kan, then AA is a groupoid. Adapting the analogous argument from Kerodon about Kan complexes to our Kan cubical sets, we’re given an f:abAf : a \to b \in A, and we build left and right inverses g,h:bag, h : b \to a to ff.

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

The open box which computes the left inverse of a map f.
If this open box had a filler, it would witness in AA the equation gf=1g \circ f = 1.
The open box which computes the right inverse of a map f.
If this open box had a filler, it would witness in AA the equation fh=1f \circ h = 1.

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

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 nn-category might look like interpreted cubically:

A globular cell in a 2-category is an α with 0-cells a, b and 1-cells f, g as a boundary.
A globular cell in a 2-category is an α\alpha with 0-cells a,ba, b and 1-cells f,gf, g as a boundary.
The same globular cell, stretched into a square.
We can interpret it as a cubical 2-cell where two faces are thin.

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.

The same square you've read about 3 times now.
Our good friend σ\sigma.
Squishing the square into a globe by composing the adjacent morphisms.
We collapse it into a globular σ🌎\sigma_\globe by composing the composable arrows.

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)K(A) is Kan

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

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

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

By this argument, every open box oo of dimension nn in K(A)K(A) is made up of the same element bAb \in A in all of its faces. We can extend this box to an nn-cube which is just the element bb: It is a complete nn-cube of K(A)K(A), and it has all of the same faces as oo 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 cSet\mathbf{cSet} on the Kan complexes, which turns out to be equivalent to the (,1)(\infty,1)-topos of Grpd\mathbf{\infty{}Grpd} of \infty-groupoids. A recent result by Shulman shows that this category, which I guess can be called cSetKan\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):

By definition, a type in these theories is a Kan cubical set. A type in a context like i,j,k:IAi, j, k : \mathbb{I} \vdash A is roughly like the set A([3])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:

And connection
The square generated by λi j.p(ij)\lambda i\ j. p(i \land j)
Or connection
The square generated by λi j.p(ij)\lambda i\ j. p(i \lor j)

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 λi.p ik\lambda i. p\ ik faces in the diagram), and the two other faces are the 1-cube we degenerated (the line pp). Connections are a very natural extension to the theory of Kan cubical sets, since in a sense they say that an nn-cube is regarded as a degenerate (n+1)(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, sSet\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 (X0X_0), the equalities between elements of that type (X1X_1), the homotopies between equalities in that type (X2X_2), and so forth. In that sense it’s not surprising that Kan cubical sets can be used to (almost) model HoTT!


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.


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:

The following papers:

The following pages from Kerodon:

  1. Where (f×g)(x,y)=(f(x),g(y))(f \times g)(x, y) = (f(x), g(y)) in Set\mathbf{Set}.↩︎