From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

TL;DR

This paper introduces twisted cubes in type theory, extending cube categories to model non-invertible equalities, bridging properties of cubes, globes, and simplices for higher categorical structures.

Contribution

It develops a new category of twisted cubes by modifying the BCH cube category, enabling the modeling of directed type theories with non-invertible equalities.

Findings

Defined the category of twisted cubes.

Proved initial properties of twisted cubes.

Showed potential to unify properties of cubes, globes, and simplices.

Abstract

Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher groupoids. Bezem, Coquand, and Huber have presented a constructive model of univalence using a specific cube category, which we call the BCH category. The higher categories encoded with the BCH category have the property that all morphisms are invertible, mirroring the fact that equality is symmetric. This might not always be desirable: the field of directed type theory considers a notion of equality that is not necessarily invertible. This motivates us to suggest a category of twisted cubes which avoids built-in invertibility. Our strategy is to first develop several alternative (but equivalent) presentations of the BCH category using morphisms between suitably defined graphs. Starting from there, a minor modification allows us to define our category of twisted cubes. We prove several first results about this category, and our work suggests that twisted cubes combine properties of cubes with properties of globes and simplices (tetrahedra).

Equations

$$\mathsf{left}\text{-}\mathsf{inj}(f):\equiv \Pi (x,y:A,z:B).(f(x)=\mathsf{inl}(z))\to (f(y)=\mathsf{inl}(z))\to x=y.$$

$$(A\text{lhook}\text{joinrel}\stackrel{\mathsf{left}}{\to }B+C):\equiv \Sigma (f:A\to (B+C)).\mathsf{left}\text{-}\mathsf{inj}(f).$$

$$\left(\underline{m}\text{lhook}\text{joinrel}\stackrel{\mathsf{left}}{\to }\underline{n}+\underline{1}\right)\simeq \left(\underline{n}\text{lhook}\text{joinrel}\stackrel{\mathsf{left}}{\to }\underline{m}+\underline{1}\right).$$

$$\mathsf{obj}({\square }_{\mathsf{BCH}}):\equiv \mathbb{N}$$

$$\mathsf{prism}(V):\equiv$$

$$\mathsf{prism}(E):\equiv$$

$$\cup$$

$$C_0:\equiv (\underline{1},\{(0,0)\})C_{n+1}:\equiv \mathsf{prism}(C_n)$$

$$\mathsf{nodes}(C_n)$$

$$\mathsf{edges}(C_n)$$

$$\mathsf{src}(\mathsf{inl}(v)):\equiv \mathsf{trg}(\mathsf{inl}(v))$$

$$\mathsf{src}(\mathsf{inr}(i,x_0{x}_1\dots x_{n-2}))$$

$$\mathsf{trg}(\mathsf{inr}(i,x_0{x}_1\dots x_{n-2}))$$

$$\mathsf{grp}\text{-}\mathsf{hom}\left((V,E),(V^{\prime },E^{\prime })\right):\equiv \Sigma (f:V\to V^{\prime }).\Pi (v_0,v_1:V).E(v_0,v_1)\to E^{\prime }(f(v_0),f(v_1))$$

$$\mathsf{obj}({\square }_{\mathsf{grp}}):\equiv \mathbb{N}$$

$$\sqcap ,\bigsqcup :V\times V\to V$$

$$\mathsf{pres}\text{-}\mathsf{meet}(g):\equiv \Pi (u,v:{\underline{2}}^{\underline{m}}).g(u\sqcap v)=g(u)\sqcap g(v)$$

$$\mathsf{pres}\text{-}\mathsf{join}(g):\equiv \Pi (u,v:{\underline{2}}^{\underline{m}}).g(u\bigsqcup v)=g(u)\bigsqcup g(v)$$

$$\mathsf{obj}({\square }_{\mathsf{cont}}):\equiv \mathbb{N}$$

$${\square }_{\mathsf{cont}}(m,n):\equiv \Sigma (g:\mathsf{grp}\text{-}\mathsf{hom}\left(C_m,C_n\right)).\mathsf{pres}\text{-}\mathsf{meet}(g)\times \mathsf{pres}\text{-}\mathsf{join}(g)$$

$$e:\Pi (m,n:\mathbb{N}).{\square }_{\mathsf{BCH}}^{\mathrm{op}}(m,n)\simeq {\square }_{\mathsf{cont}}(m,n).$$

$$\lambda g.i\circ ({\mathsf{proj}}_1(g)):\left(\Sigma (g:\mathsf{grp}\text{-}\mathsf{hom}\left(C_m,C_n\right).\mathsf{pres}\text{-}\mathsf{join}(g)\right)\to \mathsf{grp}\text{-}\mathsf{hom}\left(B_m,C_n\right)$$

$${\square }_{\mathsf{cont}}(m,n)$$

$$\equiv$$

$$\simeq$$

$$\equiv$$

$$\mathsf{dim}:\mathsf{edges}(C_n)\to \underline{n}+\underline{1}$$

$$\mathsf{dim}(\mathsf{inr}(i,x_0\dots x_{n-2}):\equiv \mathsf{inl}(i)$$

$$\mathsf{dim}\text{-}\mathsf{pres}(f):\equiv \Pi (e_1,e_2:\mathsf{edges}(C_n)).(\mathsf{dim}(e_1)=\mathsf{dim}(e_2))\to (\mathsf{dim}(f(e_1))=\mathsf{dim}(f(e_2))).$$

$$\mathsf{obj}({\square }_{\mathsf{dim}}):\equiv \mathbb{N}$$

$$\displaystyle\mathsf{dim\text{-}inj}(f):\equiv\Pi(e_{1},e_{2}:\mathsf{edges}(C_{m}),j:\underline{n}).\big{(}\mathsf{dim}(f(e_{1}))=\mathsf{inl}(j)\times\mathsf{dim}(f(e_{2}))=\mathsf{inl}(j)\big{)}$$

$$\to (\mathsf{dim}(e_1)=\mathsf{dim}(e_2)).$$

$$\mathsf{tw}\text{-}\mathsf{prism}(V):\equiv$$

$$\mathsf{tw}\text{-}\mathsf{prism}(E):\equiv$$

Full text

The higher categories encoded with the BCH cube category have the property that all morphisms are invertible, mirroring the fact that equality is symmetric. This might not always be desirable: the field of directed type theory considers a notion of equality that is not necessarily invertible.

This motivates us to suggest a category of twisted cubes which avoids built-in invertibility. Our strategy is to first develop several alternative (but equivalent) presentations of the BCH cube category using morphisms between suitably defined graphs. Starting from there, a minor modification allows us to define our category of twisted cubes. We prove several first results about this category, and our work suggests that twisted cubes combine properties of cubes with properties of globes and simplices (tetrahedra).

1 Introduction and Motivation

A cube category is a category whose objects are (or represent) finite-dimensional cubes, and whose morphisms are mappings of some sort between these cubes. There are many different cube categories [1, 5, 8, 9, 20], and they are used to encode higher categorical structures.

Homotopy type theory [28] is a variation of Martin-Löf’s intensional type theory. The characteristic and novel view adapted in homotopy type theory is that types carry the structure of higher categories, or, to be precise, higher groupoids (i.e. all morphisms are invertible). This view supports Voevodsky’s univalence principle which should be seen as a central concept of homotopy type theory. The first model of such a type theory, given by Voevodsky [29] (see also the presentation by Kapulkin and Lumsdaine [16]), uses simplicial sets. However, it is still an open question how simplicial sets can be used to build a constructive model of type theory with univalent universes [13]. Using cubical sets, this has been achieved by Bezem, Coquand, and Huber [8]. Starting from there, cubes have gathered a lot of attention in the type theory community, leading to various cubical type theories which have univalence not as an axiom but as a built-in derivable principle [3, 6, 12, 23]. Many different cube categories have been considered in this context.

The important cube category used by Bezem, Coquand, and Huber [8] (from now on referred to as the BCH cube category) uses finite sets of variable names as objects, and a morphism from a set $I$ to a set $J$ is a function $f:I\to J\cup\{0,1\}$ which is “injective on the left part”, i.e. $f(i_{1})=f(i_{2})=j$ with $j:J$ implies $i_{1}=i_{2}$. One goal of this paper is to develop several alternative presentations of this category, mainly using graph morphisms. We have two main motivations to do this. The first is that, as we hope, our alternative and intuitive (but equivalent) definitions enable new views on the category and facilitate the discovery of further observations. The second motivation is that a minor change in the definition will allow us to construct a new cube category, the twisted cubes from the title. We will come back to this in a moment.

The standard way to create models (of both higher categories and type theories) using simplicial or cubical index categories is to take presheaves and equip them with certain Kan-filling conditions. These filling conditions entail composition of morphisms as well as associativity and all higher coherence laws that one needs. A typical such Kan-filling condition for the $2$-cube111While Bezem, Coquand, and Huber [8] define their index category to have finite sets of variables as objects, it is possible to simply use natural numbers as objects. The $n$-cube, or $n$-dimensional cube, is then the object of the presheaf category that is represented by the object $n$ of the index category., as shown on the left of Figure 1, says that, given the “partial square” of three solid edges on the right, one can always find the dashed edge (together with an actual filler for the square).

One important observation here is that, in the case of the BCH cube category and other cube categories, invertibility of morphisms is built-in. Consider the partial square, as shown on the middle of Figure 1, where two of the three solid edges are identities and the third is an actual non-trivial morphism (or equality) $p$ from $x$ to $y$. Using the Kan filling operation described above, we get a morphism from $y$ to $x$, which serves as the inverse of $p$.

The invertibility of morphisms is useful for most forms of type theory, where equaliy is symmetric. This however is not always the case, cf. the proposals for directed type theories by Licata and Harper [18], Nuyts [22], Riehl and Shulman [25], North [21], and others. Their aim is to generalise type theory by replacing (higher) groupoids by general (higher) categories. In a nutshell, this means that “equality” (or whatever takes the place of equality) is not necessarily invertible.

We think that a very valuable long-term goal would be to make the connection of directed type theories with cubical type theories and create some sort of directed cubical type theory. This is at the moment certainly out of reach, and we do not know how such a type theory could be built. Nevertheless, it motivates us to explore variations of the BCH cube category which do not have the described built-in equality.

To avoid invertibility, we “twist” the left-most edge of the $2$-dimensional cube, as shown on the right of Figure 1, to ensure that the construction from before becomes impossible. This might seems artificial and specific to the $2$-dimensional case but by using our graph morphisms that we develop for the BCH cube category, it becomes very easy to define the twisting version for cubes of all dimensions.

To construct a twisted $n$-cube from a twisted $(n-1)$-cube, we first expand the original cube along a new dimension (we call this thickening): this is same as constructing a standard $n$-cube form a standard $(n-1)$-cube, which is just a construction of its cylinder object. We then reverse all dimensions at the starting point of the new dimension (we call this twisting). Figure 2 illustrates this thickening-and-twisting process up to dimension $3$, where the existing dimensions are shifted by one in order to allow the new dimension to be the first dimension.

One important property of standard cubes which twisted cubes retain is that every face of a [twisted] $n$-cube is a [twisted] $(n-1)$-cube. An interesting example is the case $n=3$: In order to construct a twisted $3$-cube, we thicken the twisted $2$-cube as illustrate in Figure 2 where the left and the right face are already twisted $2$-cubes, while the rest are thickened $1$-cubes. The right face is unaffected during the twisting, but the left face is reversed entirely. Nevertheless, it is still a $2$-cube (just flipped backwards).

Twisted cubes do not only remove the discussed source of invertibility, but they also change the way we view composition of morphisms. The filling of a “standard” square can be interpreted as saying that the composition of two edges equals the composition of the other two edges, and if we want to see the lid as the composite of the three other edges, then one has to be inverted. In contrast, in the twisted square, the lid can be seen directly as the single composite of the three other edges. The right half of Figure 3 shows the projection of the twisted $3$-cube, and the smallest square (011, 001, 101, 111) is the lid. As for the square, this lid should be seen as the composite of the other (here five) faces. Intuitively, one starts with the biggest square, composes it with the top and the bottom squares, then with the left and the right square, and thus arrives at the smallest square. Figure 4 shows the analogous situation for the $4$-dimensional twisted cube, where one starts with the inner $3$-cube, then extends to the front and the back, to the top and the bottom, and finally to the left and the right.

The “twisting” pattern also appears in the twisted arrow category [17], also known as the category of factorisations [7]. However, it is unclear how to generalise this idea to more than squares; it has been developed to solve a different problem.

In the main body of the paper, we first introduce the framework of graph morphisms for standard (non-twisted) cubes. We consider the properties of meet/join and dimension preservation of graph morphisms, and conclude that both of these are suitable refinements to ensure that the category of graph morphisms matches the BCH cube category. The proof of this is the main result of Section 2. We use this development to introduce and examine twisted cubes in Section 3. We will see that they have many characteristic properties that standard cubes are lacking. Some of them, such as a Hamiltonian path through the cube and the fact that vertices are totally ordered, are familiar from simplicial structures but not from cubical ones. Another interesting feature, neither familiar from cubical nor from simplicial but from globular structures, is that surjective maps are unique (i.e. there is only one way to degenerate a twisted cube). These and other observations allow us to define a further representation of the category of twisted cubes which does not make use of graphs.

Setting

We use a standard version of Martin-Löf’s dependent type theory as our meta-language. We assume function extensionality, but we do not require other axioms or features since we mostly work with finite sets, which are extremely well-behaved by default. In particular, it does not matter for us whether UIP/Axiom K is assumed or not, and the development would be identical in extensional dependent type theory.

Summary of Contributions

Our main contributions are as follows:

• •

We give several alternative but equivalent presentations of the BCH cube category.

• •

We introduce twisted cubes, a variation of the BCH cube category which allows for filling conditions without built-in invertibility.

• •

We show several results about twisted cubes. These include connections to simplices (a unique Humiliation path and the property of being a Reedy category) and to globes (unique surjective maps and degeneracies).

2 A Standard Cube Category

In this section, we discuss various representations of the cube category $\square_{\mathsf{BCH}}$. This category was used by Bezem, Coquand, and Huber to present a constructive model of univalence [8]. In Section 3, we will see how minimal modifications lead to a category of twisted cubes.

Keeping in mind that we use type theory as the language in which the results are presented (i.e. as our meta-theory), we use the following notations: $\mathbb{N}$ are the natural numbers, including [math]. For $n:\mathbb{N}$, the set $\underline{n}$ is the finite set with elements $\{0,1,\ldots,n-1\}$. In particular, $\underline{2}$ is the set of booleans. As usual, ${\underline{n}}^{\underline{m}}$ is simply the function set $\underline{m}\to\underline{n}$. We denote elements of ${\underline{2}}^{\underline{n}}$ by binary sequences as in $0\cdot 1\cdot 1\cdot 0$. This means such a function $f$ is denoted by $f(0)\cdot f(1)\cdot f(2)\ldots f(n-1)$. If there is no risk of confusion, we omit the $\cdot$ and simply use juxtaposition as in $0110$.

In several situations, we want to consider a type of functions into a coproduct which is injective “on the left part of the codomain”. To make this precise, we introduce a notation:

Definition 2.1** ($\lhook\joinrel\xrightarrow{\mathsf{left}}$).**

Assume $A$, $B$, and $C$ are given types. For a function $f:A\to(B+C)$, we say that $f$ is injective on the left part if

[TABLE]

We write the type of functions which are injective on the left part as

[TABLE]

In the next lemma, a function $f:A\to B+\underline{1}$ is called a partial function, with $\underline{1}$ being the “undefined” part.222Technically, these are of course only the partial functions from $A$ to $B$ with decidable support. Since we only work with finite types, it is not surprising that we only need to consider the decidable case. The following simple but useful (and well-known) result will be necessary. It could be formulated in higher generality, but a version which is sufficient for us is this:

Lemma 2.2**.**

Given $m,n:\mathbb{N}$, injective partial functions from $\underline{m}$ to $\underline{n}$ are in bijection with injective partial functions from $\underline{n}$ to $\underline{m}$. In other words, we have an equivalence

[TABLE]

Proof 2.3**.**

The equivalence can be constructed directly. Given an $f:\underline{m}\lhook\joinrel\xrightarrow{\mathsf{left}}\underline{n}+\underline{1}$, we have to construct a function $g:\underline{n}\lhook\joinrel\xrightarrow{\mathsf{left}}\underline{m}+\underline{1}$. For $i:\underline{n}$, we can decide whether there is a $k$ such that $f(k)=\mathsf{inl}(i)$. If so, then this $k$ is unique due to injectivity, and we set $g(i):\equiv\mathsf{inl}(k)$; otherwise, we set $g(i):\equiv\mathsf{inr}(0)$. Checking that this is an equivalence is routine.

The presentation of the cube category in question that we start with is the one given by Bezem, Coquand, and Huber [8] (which is the same as in Huber’s PhD thesis [15]). Since it is sufficient for our purposes, we use a skeletal variation: our objects are not finite sets but rather natural numbers.

Definition 2.4** **(category

$\square_{\mathsf{BCH}}$ [8, 15]).

The category $\square_{\mathsf{BCH}}$ has natural numbers as objects and, for $m,n:\mathbb{N}$, a morphism in $\square_{\mathsf{BCH}}(m,n)$ is a function $f:\underline{m}\to\underline{n}+\underline{2}$ which is injective on the $\underline{n}$-part. In type-theoretic notation:

[TABLE]

Composition $g\circ f$ is defined to be the set-theoretic composition $(g+\mathsf{id}_{2})\circ f$.

What we will need is the opposite of this category, $\square^{\mathrm{op}}_{\mathsf{BCH}}$. While the above definition is short and abstract, a description close to the intuitive idea of cubes is helpful for our later developments. Let us consider graphs $G=(V,E)$ of nodes (vertices) and edges, where $V$ is a set with decidable equality and $E$ is a subset of $V\times V$. A standard way to implement this is to let $E$ be a family of “mere propositions”333Recall that a mere proposition, or a subsingleton, is a type with at most one element., indexed twice over $V$. However, we write $(s,t):E$ for $E(s,t)$ and assume that $E$ is given in the “total space” formulation. Furthermore, in our cases $E$ will always be a decidable subset.

$E$ being a subset means that our graphs do not have multiple parallel edges, i.e. for any pair of vertices, there is at most one edge between them, and it is decidable whether there is an edge between two given vertices.

Given a graph, we construct a new graph as follows. Note that the “total space” of the edges of the new graph is $E+E+V$, but in order to make clear which vertices these new edges connect, we use “set theory style” notation:

Definition 2.5**.**

*Given $G=(V,E)$, the graph-prism of $G$, denoted as

$\mathsf{prism}\;(G):\equiv(\mathsf{prism}\;(V),\mathsf{prism}\;(E))$ is another graph where*

[TABLE]

This allows us to define the standard cube as a graph:444Most of graphs in this paper are reflexive graphs to support degeneracies as graph morphisms.

Definition 2.6**.**

Given $n:\mathbb{N}$, the standard cube $C_{n}$ is defined as follows:

[TABLE]

Another way of defining $C_{n}$, without recursion, is the following. Here, we give the “total space” of edges $\mathsf{edges}(C_{n})$ together with functions $\mathsf{src},\mathsf{trg}:\mathsf{edges}(C_{n})\to\mathsf{nodes}(C_{n})$:

Definition 2.7**.**

In the following, our convention is that $\underline{-1}$ is empty (i.e. the same as $\underline{0}$):

[TABLE]

The number of total edges in (11) comes from the following calculation. We have $n$ dimension, thus $2^{n}$ nodes, which come with self-loops giving rise to the summand $\underline{2}^{\underline{n}}$. For ever node, we further have an edge in each dimension. Avoiding double counting, this gives the summand $\underline{n}\times\underline{2}^{\underline{n-1}}$. Figure 5 shows drawings for $C_{0}$ to $C_{3}$.

Lemma 2.8**.**

Definition 2.6* and Definition 2.7 define isomorphic graph structures. ∎*

This observation allows us to use whichever is more convenient in any given situation.

A graph morphism from $G=(V,E)$ to $G^{\prime}=(V^{\prime},E^{\prime})$ is, as usual, a function between the node types which preserves the edges:

[TABLE]

We can now consider the following category:

Definition 2.9** (category $\square_{\mathsf{grp}}$).**

*The category $\square_{\mathsf{grp}}$ has natural numbers as objects.

A morphism between $m$ and $n$ is a graph morphism from $C_{m}$ to $C_{n}$, as in:*

[TABLE]

Composition is composition of graph morphisms.

The category $\square_{\mathsf{grp}}$ has more morphisms than $\square^{\mathrm{op}}_{\mathsf{BCH}}$. One example would be the morphism in $\mathsf{grp\text{-}hom}\left(C_{2},C_{1}\right)$ which maps the three nodes $00$, $01$, $10$ all to [math] and $11$ to $1$. Another example is the morphism which maps $00$ to [math], and $01$, $10$, $11$ all to $1$. Both of these morphisms do not have analogues in $\square^{\mathrm{op}}_{\mathsf{BCH}}$. In other words, $\square_{\mathsf{grp}}$ has connections. Since, in the current paper, we are looking for alternative definitions of the category $\square^{\mathrm{op}}_{\mathsf{BCH}}$, we refine the definition of the morphisms in $\square_{\mathsf{grp}}$ to resolve the mismatch. Let us formulate the following auxiliary definitions.

Definition 2.10** (free preorder on a graph).**

For a given graph $G=(V,E)$, we write $G^{*}=(V,E^{*})$ for the free preorder generated by it. $G^{*}$ has $V$ as objects and, for $v,u:V$, we have $v\leqslant u$ if there is a chain of edges starting in $v$ and ending in $u$.

When talking about nodes in $G$, we borrow the notions of meet (product) and join (coproduct) from preorders. If they exist in $G^{*}$, we write them as $v\sqcap u$ and $v\sqcup u$.

It is easy to see that, in the case of $C_{n}$, all meets and joins exist and can be calculated directly: From the programming perspective, they correspond to the bitwise operators ${}^{\prime}\texttt{\&}^{\prime}$ and ${}^{\prime}\texttt{|}^{\prime}$. Thus, when talking about $C_{n}$, we can view $\sqcap$ and $\sqcup$ as actual functions calculating the binary meet and join:

[TABLE]

Given a graph morphism $g:\mathsf{grp\text{-}hom}\left(C_{m},C_{n}\right)$, it is easy to define what it means that it preserves binary meets resp. joins:

[TABLE]

Note that preserving meets and joins is a property (a “mere proposition”) of morphisms. For general morphisms between graphs which might not have all meets or joins, the definition is more subtle but still straightforward; one can always define the property of being a meet (join) and then say that any vertex which has this property is mapped to one which also has it. We omit the precise type-theoretic formulation.

The two mentioned examples of morphisms which are “too much” in $\square_{\mathsf{grp}}$ do not preserve binary meets resp. joins.

Definition 2.11** (category $\square_{\mathsf{cont}}$).**

The category $\square_{\mathsf{cont}}$ has $\mathbb{N}$ as objects and, as morphisms, graph morphisms between standard cubes which preserve meets and joins ($\mathsf{cont}$ for continuous):

[TABLE]

This gives us a category which is indeed equivalent (in fact isomorphic) to $\square^{\mathrm{op}}_{\mathsf{BCH}}$:

Theorem 2.12**.**

The categories $\square^{\mathrm{op}}_{\mathsf{BCH}}$ and $\square_{\mathsf{cont}}$ are isomorphic. The isomorphism on the object part is the identity, i.e. the equivalence is given by a family $e$ as in:

[TABLE]

Before giving a proof, we formulate the following:

Lemma 2.13**.**

Consider the full subgraph of $C_{n}$ which has exactly $(n+1)$ vertices, namely the “origin” $00\ldots 0$ and the “base vectors” which have exactly one $1$. We call this subgraph $B_{n}$, where the $B$ stands for “base”, and it comes with the inclusion $i:B_{n}\hookrightarrow C_{n}$. For any $m$, “forgetting” the property of preserving the joins and composing with $i$ as in

[TABLE]

is an equivalence. Moreover, $g$ preserves meets if and only if $i\circ(\mathsf{proj}_{1}(g))$ does.

Proof 2.14**.**

The only binary joins that $B_{m}$ has are trivial, so every morphism $\mathsf{grp\text{-}hom}\left(B_{m},C_{n}\right)$ is join-preserving. Thus, the first claim of the lemma is that every such morphism can be extended in a unique way as shown in the diagram to the right. Every node of $C_{m}$ which is not in $B_{m}$, i.e. every node which is not the origin or a base vector, can be written as a join of base vectors. Since we need to preserve joins, it is therefore determined where the node has to be sent to. The map defined in this way preserves all binary joins, and it preserves binary meets if and only if the input does.

B_{m}$$C_{n}$$C_{m}

Proof 2.15** (Proof of Theorem 2.12).**

We first give the overview of the argument as a chain of equivalences, then we justify each step [S1 – S5].

[TABLE]

Step 1 holds by Lemma 2.13. Let us look at Step 2. Giving a graph homomorphism between $B_{m}$ and $C_{n}$ corresponds to choosing where the origin is mapped to, and choosing where each (non-trivial) edge of $B_{m}$ is mapped to. For the origin, we use the component $z:{\underline{2}}^{\underline{n}}$. There are $m$ non-trivial edges in $B_{m}$, and $z$ is an endpoint (or starting point) of $n$ non-trivial edges and one trivial edge in $C_{n}$. This gives us up to $\underline{m}\to\underline{n}+\underline{1}$ possible functions, but since we only consider meet-preserving morphisms, every function needs to be injective on the left part, leading to $d:\underline{m}\lhook\joinrel\xrightarrow{\mathsf{left}}\underline{n}+\underline{1}$. Moreover, if $d(i)=\mathsf{inl}(j)$ for some $i,j$, then the image of the origin must be the starting point of the edge in dimension $j$, i.e. $z(j)=0$. Step 3 is an application of Lemma 2.2 (it essentially swaps the roles of $m$ and $n$). Step 4 only unfolds the definition of $\lhook\joinrel\xrightarrow{\mathsf{left}}$.

In Step 5, the usual distributivity between $\Sigma$ and $\Pi$ (under the propositions-as-types view referred to as the “axiom of choice”) is used: $z$, $e$, and the unnamed last component can all be seen as (dependent) functions with domain $\underline{n}$. The dependent function $\alpha$ combines them into a single dependent function with domain $\underline{n}$ and a codomain that consists of multiple components which, again, are called $e$, $z$, with the last one being unnamed. Only the component expressing the “injectivity on the left part”-property cannot be seen as a function in $\underline{n}$. In Step 6, we massage the codomain of $\alpha$: We have $e:\underline{m}+\underline{1}$ and also $z:\underline{2}$, but the condition says that $z$ is determined unless $e=\mathsf{inr}(0)$; thus, the type is equivalent to $\underline{m}+\underline{2}$.

We omit the calculation which shows that the constructed equivalence preserves composition of morphisms in the categories.

In Section 3, we will switch from standard cubes to twisted cubes. The directions of some edges will be reversed. It is therefore an advantage to formulate a condition similar to the one about meets and joins without referring to the direction of edges. This is indeed possible:

Definition 2.22** **(dimension preserving morphisms; category

$\square_{\mathsf{dim}}$).

Given the standard cube $C_{n}$, where we use the non-recursive definition as in Definition 2.7, the dimension of an edge is defined as follows:

[TABLE]

We say that a morphism $f:\mathsf{grp\text{-}hom}\left(C_{m},C_{n}\right)$ is dimension-preserving if $f$ maps edges of the same dimension to edges of the same dimension,

[TABLE]

The category $\square_{\mathsf{dim}}$ makes use of these concepts:

[TABLE]

As $\mathsf{pres\text{-}meet}(g)$ and $\mathsf{pres\text{-}join}(g)$, preserving the dimension as in (26) is a proposition in the sense of homotopy type theory (has at most one proof).

Remark 2.23**.**

For a graph morphism $f$ as in the definition above, the following condition says that $f$ is “injective on dimensions” (on the non-trivial part):

[TABLE]

However, note that this follows directly from $\mathsf{dim\text{-}pres}(f)$: Assume $e_{1},e_{2}$ are edges such that $\mathsf{dim}(f(e_{1}))$ and $\mathsf{dim}(f(e_{2}))$ are equal and non-trivial. If $e_{1}$ and $e_{2}$ are not “parallel” (i.e. not in the same dimension), then we can find $e_{1}^{\prime}$ in the same dimension as $e_{1}$ such that $e_{1}^{\prime}$ and $e_{2}$ are adjacent (i.e. the endpoint of one is the starting point of the other). It is clear that $f(e_{1}^{\prime})$ and $f(e_{2})$ cannot go into the same non-trivial direction, since we can only go one step into a given direction before going back.

The connection to meet- and join-preserving is given by the following result:

Lemma 2.24**.**

A morphism $f:\mathsf{grp\text{-}hom}\left(C_{m},C_{n}\right)$ is join-and-meet-preserving exactly if it is dimension-preserving.

Proof 2.25**.**

This follows easily by going via morphisms $\mathsf{grp\text{-}hom}\left(B_{m},C_{n}\right)$ as in Lemma 2.13. The graph $B_{m}$ has exactly one edge for every non-trivial dimension, and the proof is analogous to the one of Lemma 2.13.

Corollary 2.26** (Section summary).**

The categories $\square^{\mathrm{op}}_{\mathsf{BCH}}$, $\square_{\mathsf{cont}}$, and $\square_{\mathsf{dim}}$ are isomorphic. ∎

3 A Category of Twisted Cubes

As discussed in the introduction, we build on our framework of graph morphisms to define a category of twisted cubes. A variation of Definition 2.5 gives us these twisted cubes. The critical change can be seen in (29), which should be compared with (6):

Definition 3.1**.**

*Given a graph $G=(V,E)$, the twisted graph-prism of $G$,

denoted as $\mathsf{tw\text{-}prism}\;(G):\equiv(\mathsf{tw\text{-}prism}\;(V),\;\mathsf{tw\text{-}prism}\;(E))$ is the graph defined by*

[TABLE]

We then define:

Definition 3.2**.**

Given $n:\mathbb{N}$, the twisted cube $T_{n}$ is defined as follows:

[TABLE]

Alternatively, we can tweak Definition 2.6 to get a non-recursive definition. As before, the convention is that $\underline{-1}$ is empty.

Definition 3.3**.**

The non-recursive definition of $T_{n}$ is as follows:

[TABLE]

where $b=1$ if the total number of zeros in $x_{0}x_{1}\ldots x_{i-1}$ is odd, and $b=0$ otherwise.

This means that an edge is reversed (compared to the standard cubes discussed before) exactly if the number of zeros in dimensions that come before the edge is odd (note that the condition talks about $x_{i-1}$, not $x_{n-2}$). The twisted cubes of dimension up to $3$ are illustrated in Figure 6; see also Figures 3 and 4 in the introduction.

Lemma 3.4**.**

Definition 3.2* and Definition 3.3 define isomorphic graph structures. ∎*

$T_{n}$ has an interesting property that the standard cube $C_{n}$ does not have: The induced preorder $T_{n}^{*}$ on the vertices is a total order. This observation was originally suggested by Paolo Capriotti and Jakob von Raumer in a discussion with the first author of this paper. Note that this observation should not be misunderstood to mean that $T_{n}$ itself is uninteresting. Its edges give it a unique structure, as visualised in Figure 7.

The idea behind this result is that $\mathsf{tw\text{-}prism}$ preserves the property of having a preorder that is total. To elaborate on this, if $G^{*}$ is a total order, then ${(\mathsf{tw\text{-}prism}\;G)}^{*}$ consists of two copies of $G^{*}$, where the first copy is “turned around”. One of the edges added in (31) links the largest node in the first copy to the smallest node in the second copy, thus every element of the second copy is larger than all the elements of the first copy. In other words, ${(\mathsf{tw\text{-}prism}\;G)}^{*}$ is the join of the two copies.555Join in the sense of the join of categories [19], which should not be confused with the join (coproduct) of objects in a preorder (cf. Definition 2.10).

Theorem 3.5**.**

For all $n:\mathbb{N}$, the preorder $T_{n}^{*}$ is isomorphic to the total order $({\underline{2}}^{\underline{n}},<)$.

Note that Theorem 3.5 is a property which one usually expects for simplicial structures, but not for cubical ones.

Remark 3.6**.**

There are two binary numbers for each node in Figure 7. The bottom one represents each node name according to Definition 3.3 whereas the top one represents the total order of $T_{3}$. It is impossible to unify these two binary numbers for $n\geqslant 2$ since, for each edge $e$, the numbers $\mathsf{src}(e)$ and $\mathsf{src}(e)$ only differ by (at most) one single bit by Definition 3.3, while incrementing a binary number can flip more than one bit.

Another related observation is that we can find a path from the smallest vertex to the largest vertex of $T_{n}$ which respects the direction of the edges, and which visits each vertex exactly once. Recall that such a path is called a Hamiltonian path. We record this:

Theorem 3.7**.**

For all $n:\mathbb{N}$, there is exactly one Hamiltonian path through $T_{n+1}$. This path contains exactly one edge in the first dimension (i.e. the one which is added when going from $T_{n}$ to $T_{n+1}$). Moreover, this single edge in the new dimension connects the Hamiltonian paths through the two copies of $T_{n}$ of which $T_{n+1}$ consists by definition, cf. (28).

Proof 3.8** (Proof of Theorem 3.5 and Theorem 3.7).**

As before, we denote elements of ${\underline{2}}^{\underline{n}}$ as sequences such as $00101$ (binary representation with most significant bit first) or, for clarity, by $0\cdot 0\cdot 1\cdot 0\cdot 1$. We use the endofunction $\mathsf{neg}$ on $\underline{2}^{\underline{n}}$, which simply replaces each [math] in a sequence by a $1$ and vice versa; i.e. it sends the number $i$ to $2^{n}-1-i$ (note that $\mathsf{neg}$ does not reverse the sequence, but the ordering on ${\underline{2}}^{\underline{n}}$).

Let us define endofunctions $f_{n}$ and $g_{n}$ on ${\underline{2}}^{\underline{n}}$, by induction on $n$. Note that, at this point, we do not talk about graph morphisms but only about functions between sets. The base cases of the induction are uniquely determined. We define $f$ and $g$ by

[TABLE]

It is easy to calculate that, by induction, $f$ and $g$ are inverse to each other. We want to show that they extend to morphisms between preorders,

[TABLE]

To construct $\hat{f}_{n}$ and the Hamiltonian path through the cube, it suffices to show: for $x,y:{\underline{2}}^{\underline{n}}$ with $x+1=y$, we have an edge $f_{n}(x)\to f_{n}(y)$.

We do induction on $n$. For $n=0$, this is vacuously true (such $x,y$ do not exist). For $n=n^{\prime}+1$, there are multiple cases:

• •

case $x=0\cdot x^{\prime}$ and $y=0\cdot y^{\prime}$: Then, the assumption gives us $x^{\prime}+1=y^{\prime}$ and we have to find an edge $0\cdot f_{n}(\mathsf{neg}(x^{\prime}))\to 0\cdot f_{n}(\mathsf{neg}(y^{\prime}))$. Looking at Definition 3.1, we can get this if we have $f_{n}(\mathsf{neg}(y^{\prime}))\to f_{n}(\mathsf{neg}(x^{\prime}))$. This holds by induction, since $\mathsf{neg}$ reverses the order which gives us $\mathsf{neg}(y^{\prime})+1=\mathsf{neg}(x^{\prime})$.

• •

case $x=1\cdot x^{\prime}$ and $y=1\cdot y^{\prime}$: Similar to the previous case, but nothing gets reversed.

• •

case $x=0\cdot x^{\prime}$ and $y=1\cdot y^{\prime}$: In this case, we have $x=0111\ldots$ and $y=1000\ldots$. We need to find an edge $0\cdot f(\mathsf{neg}(111\ldots))\to 1\cdot f(000\ldots)$, which simplifies to $0\cdot f(000\ldots)\to 1\cdot f(000\ldots)$. This edge is directly given in (31).

• •

case $x=1\cdot x^{\prime}$ and $y=0\cdot y^{\prime}$: Contradicts with the assumption $x+1=y$.

This shows that there is a Hamiltonian path, and it is given by $\hat{f}_{n}$. The definition of $f$ as in (38,39) also shows that $f_{n+1}$ consists of two copies of $f_{n}$, implying the last claim of Theorem 3.7. In order to prove Theorem 3.5, we need to construct $\hat{g}_{n}$. It is enough to show that, for an edge from $u$ to $v$ in $T_{n}$, we have $g(u)\leqslant g(v)$. This follows by straightforward induction, going through the edges in Definition 3.1. But Theorem 3.5 implies that there is at most one Hamiltonian path.

Remark 3.9**.**

Note that every vertex $v$ in $T_{n}$ is an endpoint of $n$ non-trivial edges. The number of zeros in the binary representation in the “order number” of $v$ (i.e. the value $g_{n}(v)$ in the proof of Theorem 3.5) equals the number of outgoing edges. Figure 7 shows this.

Analogously to Definition 2.9, we can now define the category of twisted graph morphisms:

Definition 3.10** (category $\Bowtie_{\mathsf{grp}}$).**

The category $\Bowtie_{\mathsf{grp}}$ has natural numbers as objects, and morphisms from $m$ to $n$ are graph morphisms between twisted cubes:

[TABLE]

It is easy to see that the category $\Bowtie_{\mathsf{grp}}$ has a version of connections. Since we are looking for a “twisted analogue” of $\square^{\mathrm{op}}_{\mathsf{BCH}}$, we need to refine it further. In Section 2, we have discussed the restriction to (meet and join)-preserving morphisms, and to dimension-preserving morphisms. It follows directly from Theorem 3.5 that every morphism in $\Bowtie_{\mathsf{grp}}$ preserves all binary meets and joins, so this condition becomes trivial; it does not avoid connections. However, preserving dimensions is still a non-trivial condition which does avoid connections. The definition of equation (26) still works.

Definition 3.11** (category $\Bowtie_{\mathsf{dim}}$).**

The category $\Bowtie_{\mathsf{dim}}$ has dimension-preserving maps between twisted cubes as morphisms:

[TABLE]

Note that the explanation of Remark 2.23 holds for the twisted cube category as well.

A consequence of Theorem 3.5 is that morphisms in $\Bowtie_{\mathsf{dim}}$ cannot “swap dimensions”. But an even stronger result holds, namely that surjective morphisms are unique:

Theorem 3.12**.**

*There is exactly one surjective morphism in $\Bowtie_{\mathsf{dim}}(m,n)$ for $m\geqslant n$.

(Clearly, there is none if $m<n$.)*

Proof 3.13**.**

The key to the proof is Theorem 3.7. Clearly, the Hamiltonian path in $T_{m}$ goes through all vertices. Due to surjectivity, its image has to go through all vertices of $T_{n}$. In other words, the $T_{m}$-Hamiltonian path has to be mapped to the $T_{n}$-Hamiltonian path. Since the graph morphisms that we consider preserve the dimension, the only edge in the $T_{m}$-path which can be mapped to the single edge in the first dimension in the $T_{n}$-path is just this single edge in the first dimension in the $T_{m}$-path; i.e. the middle edge has to be mapped to the middle edge. From here, it follows by induction that there can only be at most one surjective graph morphism.

What is left to show is that there actually is a surjective graph morphism if $m\geqslant n$. It is enough to construct a surjective graph morphism $f:\Bowtie_{\mathsf{dim}}(n+1,n)$, from where we get any other by $(m-n)$-fold composition ([math]-fold composition is the identity). Such a graph morphism is given by

[TABLE]

Since the directions of the edges do not depend on the very last dimension, this works (cf. Definition 3.3).

An important consequence of the above result is that there is a unique way to degenerate a twisted cube. We do not go into the details here, but see the conclusions at the end of the paper. For now, we go into a different direction.

Let us write $\mathsf{intv}$ (“interval”) for the finite set $\{0,1,\star\}$. Of course, $\mathsf{intv}$ is isomorphic to $\underline{3}$, but referring to the last element as $\star$ helps the intuition, we hope.

Definition 3.14**.**

A face of the twisted $n$-cube $T_{n}$ is a function $f:\underline{n}\to\mathsf{intv}$. The dimension of a face, written $\dim(f)$, equals the number of times $f$ takes $\star$ as value (i.e. the size of $f^{-1}(\star)$). The type of faces of dimension $k$ is written as $\mathsf{faces}(n,k)$.

The face $f:\underline{n}\to\mathsf{intv}$ represents the full subgraph of $T_{n}$ of vertices on which $f$ “matches” (a vertex $x_{0}x_{1}\ldots{}x_{n-1}$ is matched if, for every $i$, we have $f(i)=x_{i}$ or $f(i)=\star$).

Lemma 3.15**.**

The image of $f:\Bowtie_{\mathsf{dim}}(m,n)$ is a face.

Proof 3.16**.**

This follows from the property of preserving the dimension as defined in (26).

Lemma 3.17**.**

The $m$-faces are the only injective maps $\Bowtie_{\mathsf{dim}}(m,n)$:

[TABLE]

Proof 3.18**.**

Every face gives rise to a canonical injective dimension-preserving morphism in the sense of Definition 2.22, as dictated by the inclusion of the full subgraph that the face represents into $T_{n}$. The fact that these are the only ones follows from Theorem 3.5 (we cannot “swap dimensions”) and Lemma 3.15.

As with Theorem 3.5 before, Lemma 3.17 is a result which is usually found in simplicial structures, but not in cubical ones. In any case, we now easily get:

Lemma 3.19** **(factorisation of dimension preserving

morphisms).

Given a morphism $f:\Bowtie_{\mathsf{dim}}(m,n)$, there is exactly one way to write it as the composition $f=\mathsf{inj}(f)\circ\mathsf{surj}(f)$ of a surjective dimension preserving graph morphism followed by an injective one. This means that the map

[TABLE]

is an equivalence. Moreover, morphisms $\Bowtie_{\mathsf{dim}}(m,n)$ are in 1-to-1 correspondence with faces of $T_{n}$ of dimension $\leqslant m$.

Proof 3.20**.**

A consequence of Lemma 3.15 is that the factorisation on the level of sets of vertices works. The second claim follows from the first: In (45), the $k$ and the surjective map are uniquely determined (i.e. contractible components) by Theorem 3.12. By Lemma 3.17, injective maps correspond to faces.

Remark 3.21**.**

It follows from Lemma 3.19 and the proof of Theorem 3.12 that all the non-empty fibres of a dimension-preserving morphism between twisted cubes have the same size. The reverse is the case as well: a morphism between twisted graphs where all non-empty fibres have the same size is dimension-preserving.

Another consequence of the above results is that $\Bowtie_{\mathsf{dim}}$ can be given the structure of a Reedy category (cf. [14]). Recall that a Reedy category is a category $R$ with a degree function $d:\mathsf{obj}(\Bowtie_{\mathsf{dim}})\to\mathbb{N}$ and two subcategories $R^{+}$ and $R^{-}$, such that:666Degrees can more generally be arbitrary ordinals, but $\mathbb{N}$ is sufficient in our case.

• •

both subcategories are wide, i.e. contain all the objects of $R$;

• •

every nonidentity morphism in $R^{+}$ raises the degree;

• •

every nonidentity morphism in $R^{-}$ lowers the degree;

• •

and every morphism of $R$ can be written as a morphisms in $R^{-}$ followed by a morphism in $R^{+}$ in a unique way.

The reason why Reedy categories are interesting is that they enable certain inductive constructions. In the setting of type theory, they have been discussed by Shulman [26].

Theorem 3.22**.**

The category $\Bowtie_{\mathsf{dim}}$ is a Reedy category where the degree of an object is the object itself (recall that objects are natural numbers). $\Bowtie_{\mathsf{dim}}^{+}$ is the subcategory of injective morphisms, and $\Bowtie_{\mathsf{dim}}^{-}$ is the subcategory of surjective morphisms.

Proof 3.23**.**

The first three properties are clear, and the factorisation is given by Lemma 3.19.

Finally, let us record an alternative representation of the category $\Bowtie_{\mathsf{dim}}$ which does not go via graph morphisms.

Definition 3.24** (ternary notation: category $\Bowtie_{\mathsf{tri}}$).**

The category $\Bowtie_{\mathsf{tri}}$ has natural numbers as objects, and a morphism from $m$ to $n$ is a function $\underline{n}\to\mathsf{intv}$ which takes $\star$ at most $m$ times as image:

[TABLE]

The identity morphisms are the functions that are constantly $\star$. To define the composition of $f:\Bowtie_{\mathsf{tri}}(k,m)$ and $g:\Bowtie_{\mathsf{tri}}(m,n)$, we need to define a function $g\circ f:\underline{n}\to\mathsf{intv}$ (which is $\star$ at most $k$ times). We define $(g\circ f)(i)$ by recursion on $i$, simultaneously with the values $i^{\prime}$ and $b_{i}$, as follows:

[TABLE]

where

• •

$i^{\prime}$* is the number of occurrences of $\star$ in the sequence $g(0),g(1),\ldots,g(i-1)$;*

• •

$b_{i}$* is $1$ if the number of zeros in the sequence $(g\circ f)(0),(g\circ f)(1),\ldots,(g\circ f)(i-1)$ is odd, and [math] if it is even.*

Note that a morphism in $\Bowtie_{\mathsf{tri}}(m,n)$ can be represented as a sequence such as $01\!\star{}\!0\!\star{}\!10$ of length $n$ which contains the symbol $\star$ at most $m$ times, which is why we refer to it as ternary notation.

Remark 3.25**.**

There is a category of twisted semi-cubes, denoted by $\Bowtie_{\mathsf{tri}}^{+}$, which is exactly the same as $\Bowtie_{\mathsf{tri}}$ except that the number of $\star$ in the sequence must be exactly $m$, i.e. “$\leqslant$” is changed to “$=$” in the definition of $\Bowtie_{\mathsf{tri}}(m,n)$. This category is equivalent to the sub-category of $\Bowtie_{\mathsf{dim}}$, denoted as $\Bowtie_{\mathsf{dim}}^{+}$, which consists of injective dimension-preserving graph homomorphisms. Note that this injectivity condition is equivalent to removing the reflexive edges from Definition 3.2.

If we remove the expression ($\mathsf{xor}\,b_{i}$) in the definition of morphisms of $\Bowtie_{\mathsf{tri}}^{+}$, then the category becomes equivalent to the category of standard cubes but without degeneracies and swapping dimensions. In other words, the expression ($\mathsf{xor}\,b_{i}$) characterises “twisted-ness”.

Theorem 3.26**.**

The categories $\Bowtie_{\mathsf{dim}}$, and $\Bowtie_{\mathsf{tri}}$ are isomorphic, with the object part being the identity. In particular, we have:

[TABLE]

Proof 3.27**.**

As the following chain of equivalences:

[TABLE]

When transported along this isomorphism, the composition of $\Bowtie_{\mathsf{dim}}$ gets mapped to the composition of $\Bowtie_{\mathsf{tri}}$, as required.

4 Conclusions and Future Directions

We have suggested new representations of the BCH cube category and introduced a category of twisted cubes. It is natural to further study the similarities and differences between standard and twisted cube categories, and some new results will be presented in the upcoming PhD thesis of the first author.

As future work, we plan to examine algebraic descriptions via generators and relations. Such presentations exist for many different cube categories in the literature but, as far as we are aware, not for the BCH cube category. The closest suggestions available are the presentations by Antolini [5] and Newstead [20], which seem to be fairly easy to adapt to the BCH cube category. Interestingly, further adapting the generators to the twisted setting simplifies them significantly, which mirrors the fact that morphisms between twisted cubes cannot swap dimensions. Moreover, our Theorem 3.12 implies that degeneracies are unique: there is only one single way in which a twisted $n$-cube can be degenerated to get a twisted $(n+1)$-cube. A consequence is that we do not need to impose relations between different degeneracies.

This, we hope, will make it possible to develop the higher categorical structures that can be encoded as presheaves on the category of twisted cubes. An ultimate goal would be to model some form of directed cubical type theory mirroring the model by Bezem, Coquand, and Huber [8].

Another possible application of our twisted cube categories might be building a syntax for a parametric type theory or cubical type theory without an interval as suggested by Altenkirch and Kaposi [2]. A major difficulty in their development was the presence of multiple degeneracies, a problem which does not occur in the current work.

A further direction which may be worth exploring is to not consider set-valued presheaves, but type-valued presheaves instead. To facilitate this, we can consider the category of twisted semi-cubes mentioned in Remark 3.25. From there, type-valued presheaves can be encoded as Reedy-fibrant diagrams in a known style [27]. We can then add a condition reminiscent of Rezk’s Segal-condition [24] by stating that the projection from twisted semi-cubical types to the sequence of types along the Hamiltonian path is an equivalence. This corresponds to saying that the partial $n$-cube with missing inner part and lid (cf. Figure 3) have a contractible type of fillers. It seems that this could be a first step towards the construction of composition and higher coherences, although further conditions seem to be necessary. The relation to the (complete) semi-Segal types by Capriotti and others  [4, 10, 11] remains to be studied.

Acknowledgements

We would like to thank Paolo Capriotti and Jakob von Raumer. Both offered many suggestions during fruitful exchanges. In particular, the initial observation on which Theorem 3.5 is based was suggested by them, and the idea of considering graph morphisms was found in one of our many interesting discussions. The first author would like to thank his PhD supervisor, Thorsten Altenkirch, for helpful discussions. We are also grateful to the participants of TYPES’19 in Oslo and the summer school on HTT/UF in Leeds. We thank in particular Emily Riehl, Christian Sattler, and Steve Awodey for their help and their comments. Special thanks go to Andreas Nuyts, who has pointed out a mistake in an earlier draft of this paper, and to the anonymous reviewers for their careful reading and comments.