nLab cubical set

Definition

Notation

We make use of the notation of category of cubes.

Definition

The category of cubical sets is the free co-completion of $\square$, the category of cubes.

Remark

The free co-completion of a small category can be constructed as the category of presheaves of sets on this category. Thus we can also think of the category of cubical sets as the category of presheaves of sets on $\square$.

Notation

We denote the category of cubical sets by $\mathsf{Set}^{\square^{op}}$.

Definition

A cubical set is an object of $\mathsf{Set}^{\square^{op}}$.

Remark

When we think of the category of cubical sets as the category of presheaves of sets on $\square$, we consequently think of a cubical set as a presheaf of sets on $\square$.

Definition

A morphism of cubical sets is an arrow of $\mathsf{Set}^{\square^{op}}$.

Monoidal structure

The strict monoidal structure of $\square$ gives rise to a (non-strict) monoidal structure on $\mathsf{Set}^{\square^{op}}$, by Day convolution. The unit of the monoidal structure is $\square^{0}$, in the notation of Notation . Whenever we use the symbol $\otimes$ when working with cubical sets or morphisms of cubical sets, we shall always refer to the functor $- \otimes -$ of this monoidal structure.

Notation

Free standing $n$-cube, and an $n$-cube of a cubical set

Notation

Let $y : \square \rightarrow \mathsf{Set}^{\square^{op}}$ denote the Yoneda embedding functor. Let $n \geq 0$ be an integer. We denote the cubical set $y(I^{n})$ by $\square^{n}$.

Terminology

We refer to $\square^{n}$ as the free-standing $n$-cube.

Terminology

Let $X$ be a cubical set. Let $n \geq 0$ be an integer. By an $n$-cube of $X$, we shall mean a morphism of cubical sets $\square^{n} \rightarrow X$.

Notation

Let $f$ be a 1-cube of $X$. We shall often depict $f$ as $f : x_{0} \rightarrow x_{1}$ or as follows.

$$\array{x_{0} & \overset{f}{\rightarrow} & x_{1}}$$

In this case, $x_{0}$ is to be understood to be the $0$-cube $f \circ y(i_{0})$ of $X$, and $x_{1}$ is to be understood to be the $1$-cube $f \circ y(i_{1})$ of $X$.

Notation

Let $\sigma$ be a 2-cube of $X$. We shall often depict $\sigma$ as follows.

$$\array{ x_{0} & \overset{f_{0}}{\rightarrow} & x_{1} \\ f_{2} \downarrow & \sigma & \downarrow f_{1} \\ x_{2} & \underset{f_{3}}{\rightarrow} & x_{3} }$$

In this case, $f_{0}$ is to be understood to be the $1$-cube $\sigma \circ y(i_{0} \otimes I^{1})$ of $X$, $f_{1}$ is to be understood to be the $1$-cube $\sigma \circ y(I^{1} \otimes i_{1})$ of $X$, $f_{2}$ is to be understood to be the $1$-cube $\sigma \circ y(I^{1} \otimes i_{0})$ of $X$, and $f_{3}$ is to be understood to be the 1-cube $\sigma \circ y(i_{1} \otimes I^{1})$ of $X$.

It can be checked that this notation is consistent with Notation .

Boundary of the free standing $n$-cube, and of an $n$-cube of a cubical set

Notation

Let $n \geq 1$ be an integer. We denote by $\partial : \mathsf{Set}^{\square^{op}} \rightarrow \mathsf{Set}^{\square^{op}}$ the functor given by defined by $sk_{n-1} \circ tr_{n-1}$, where $tr_{n-1}$ is the $(n-1)$- truncation functor for cubical sets, and $sk_{n-1}$ is the $(n-1)$- skeleton functor for cubical sets.

Terminology

Let $n \geq 0$ be an integer. We refer to $\partial \square^{n}$ as the boundary of $\square^{n}$.

Notation

We also denote by $\partial \square^{0}$ (recalling that $\mathsf{Set}^{\square^{op}}$ is, by construction, co-complete) the initial object of $\mathsf{Set}^{\square^{op}}$.

Notation

Let $n \geq 1$ be an integer. We denote by $i_{n} : \partial \square^{n} \rightarrow \square^{n}$ the morphism of cubical sets corresponding, under the adjunction between $sk_{n-1}$ and $tr_{n-1}$ described at cubical truncation, skeleton, and co-skeleton, to the identity arrow $tr_{n}(\square^{n}) \rightarrow tr_{n}(\square^{n})$ in $\mathsf{Set}^{\square_{n-1}^{op}}$.

Terminology

Let $n \geq 0$ be an integer, and let $\sigma : \square^{n} \rightarrow X$ be an $n$-cube of a cubical set $X$. We refer to the morphism of cubical sets

$$\array{\partial \square^{n} & \overset{i_{n}}{\rightarrow} & \square^{n} & \overset{\sigma}{\rightarrow} & X }$$

as the boundary of $\sigma$.

Notation

Let $\sigma$ be a 2-cube of $X$ as follows.

$$\array{ x_{0} & \overset{f_{0}}{\to} & x_{1} \\ f_{2} \downarrow & \sigma & \downarrow f_{1} \\ x_{2} & \underset{f_{3}}{\to} & x_{3} }$$

We shall often depict the boundary of $\sigma$ as follows.

$$\array{ x_{0} & \overset{f_{0}}{\to} & x_{1} \\ f_{2} \downarrow & & \downarrow f_{1} \\ x_{2} & \underset{f_{3}}{\to} & x_{3} }$$

Horns of the free-standing $n$-cube

Notation

We define inductively, for any integer $n \geq 1$, any integer $1 \leq i \leq n$, and any integer $0 \leq \epsilon \leq 1$, a cubical set $\sqcap^{n,i,\epsilon}$ and a morphism of cubical sets $i_{i, \epsilon} : \sqcap^{n,i,\epsilon} \rightarrow \square^{n}$.

When $n=1$, we define both $\sqcap^{1,1,0}$ and $\sqcap^{1,1,1}$ to be $\square^{0}$. We define $i_{1,0} : \square^{0} \rightarrow \square^{1}$ to be $y(i_{0})$, and define $i_{1,1} : \square^{0} \rightarrow \square^{1}$ to be $y(i_{1})$.

Suppose that, for some integer $n \geq 1$, we have defined $\sqcap^{n,i,\epsilon}$ and a morphism of cubical sets $i_{i, \epsilon} : \sqcap^{n,i,\epsilon} \rightarrow \square^{n}$ for all integers $1 \leq i \leq n$, and all integers $0 \leq \epsilon \leq 1$. For $1 \leq i \leq n$, we define (recalling that $\mathsf{Set}^{\square^{op}}$ is co-complete by construction) $\sqcap^{n+1,i, \epsilon}$ to be a cubical set fitting into a co-cartesian square in $\mathsf{Set}^{\square^{op}}$ as follows.

$$\array{ \sqcap^{n,i,\epsilon} \sqcup \sqcap^{n,i,\epsilon} & \overset{\big( \sqcap^{n,i,\epsilon} \otimes y(i_{0}) \big) \sqcup \big( \sqcap^{n,i,\epsilon} \otimes y(i_{1}) \big)}{\rightarrow} & \sqcap^{n,i,\epsilon} \otimes \square^{1} \\ \mathllap{i_{i,\epsilon} \sqcup i_{i,\epsilon}} \downarrow & & \downarrow \mathrlap{r_{0}} \\ \square^{n} \sqcup \square^{n} & \underset{r_{1 }}{\rightarrow} & \sqcap^{n+1,i,\epsilon} }$$

We denote by $i_{i,\epsilon} : \sqcap^{n+1,i,\epsilon} \rightarrow \square^{n+1}$ the canonical arrow determined, by means of the universal property of $\sqcap^{n+1,i,\epsilon}$, by the following commutative square in $\mathsf{Set}^{\square^{op}}$.

$$\array{ \sqcap^{n,i,\epsilon} \sqcup \sqcap^{n,i,\epsilon} & \overset{\big( \sqcap^{n,i,\epsilon} \otimes y(i_{0}) \big) \sqcup \big( \sqcap^{n,i,\epsilon} \otimes y(i_{1}) \big)}{\rightarrow} & \sqcap^{n,i,\epsilon} \otimes \square^{1} \\ \mathllap{i_{i,\epsilon} \sqcup i_{i,\epsilon}} \downarrow & & \downarrow \mathrlap{i_{i,\epsilon} \otimes \square^{1}} \\ \square^{n} \sqcup \square^{n} & \underset{\big( \square^{n} \otimes y(i_{0}) \big) \sqcup \big( \square^{n} \otimes y(i_{1}) \big)}{\rightarrow} & \square^{n+1} }$$

We define $\sqcap^{n+1, n+1, \epsilon}$ to be a cubical set fitting into a co-cartesian square in $\mathsf{Set}^{\square^{op}}$ as follows.

$$\array{ \sqcap^{n,n,\epsilon} \sqcup \sqcap^{n,n,\epsilon} & \overset{\big( y(i_{0}) \otimes \sqcap^{n,n,\epsilon} \big) \sqcup \big( y(i_{1}) \otimes \sqcap^{n,n,\epsilon} \big)}{\rightarrow} & \square^{1} \otimes \sqcap^{n,n,\epsilon} \\ \mathllap{i_{n,\epsilon} \sqcup i_{n,\epsilon}} \downarrow & & \downarrow \mathrlap{r_{0}} \\ \square^{n} \sqcup \square^{n} & \underset{r_{1}}{\rightarrow} & \sqcap^{n+1,n+1,\epsilon} }$$

We denote by $i_{n+1,\epsilon} : \sqcap^{n+1,n+1,\epsilon} \rightarrow \square^{n+1}$ the canonical arrow determined, by means of the universal property of $\sqcap^{n+1,n+1,\epsilon}$, by the following commutative square in $\mathsf{Set}^{\square^{op}}$.

$$\array{ \sqcap^{n,n,\epsilon} \sqcup \sqcap^{n,n,\epsilon} & \overset{\big( y(i_{0}) \otimes \sqcap^{n,n,\epsilon} \big) \sqcup \big( y(i_{1}) \otimes \sqcap^{n,n,\epsilon} \big)}{\rightarrow} & \square^{1} \otimes \sqcap^{n,n,\epsilon} \\ \mathllap{i_{n,\epsilon} \sqcup i_{n,\epsilon}} \downarrow & & \downarrow \mathrlap{\square^{1} \otimes i_{n,\epsilon}} \\ \square^{n} \sqcup \square^{n} & \underset{\big( y(i_{0}) \otimes \square^{n} \big) \sqcup \big( y(i_{1}) \otimes \square^{n} \big)}{\rightarrow} & \square^{n+1} }$$

Terminology

We refer to $\sqcap^{n, i, \epsilon}$ together with the morphism $i_{i,\epsilon}$ as a horn of $\square^{n}$.

Morphism from $\square^{n}$ to $\square^{0}$

Notation

We denote by $p : \square^{n} \rightarrow \square^{0}$ the arrow $y(\underbrace{p \otimes p \otimes \cdots p}_{n})$ of $\mathsf{Set}^{\square^{op}}$, making use of the fact that $\underbrace{\square^{0} \otimes \square^{0} \otimes \cdots \square^{0}}_{n}$ is $\square^{0}$, since $\square^{0}$ is the unit of the monoidal structure of $\mathsf{Set}^{\square^{op}}$.

Model structure

The category of cubical sets admits a Cisinski model structure, which admits a Quillen equivalence to the Kan–Quillen model structure on simplicial sets. See the article model structure on cubical sets for more information.

The category of cubical sets also admits a Joyal-type model structure, which admits a Quillen equivalence to the Joyal model structure on simplicial sets. See the article model structure for cubical quasicategories for more information.

Expository material

For Expository and other material, see cubical set - exposition.

Related entries

General

• bicubical sets

Applications of cubical sets

• cubical type theory

In higher category theory

• fundamental groupoid of a cubical set and the cubical nerve of a groupoid

• homotopy hypothesis for 1-types

Theory of cubical sets

• category of cubes

• cubical geometric realisation

• cubulation

• cubical truncation, skeleton, and co-skeleton

• homotopy groups of a cubical Kan complex

• model structure on cubical sets

References

The original reference for cubical sets (based on the 1950 paper by Samuel Eilenberg and J. A. Zilber on simplicial sets) is

• Daniel M. Kan, Abstract homotopy. I, Proceedings of the National Academy of Sciences 41:12 (1955), 1092–1096. doi.

Kan switched to simplicial sets in Part III of the series.