2.1 Type theories: notations and categorical semantics

We establish the terminology and conventions that are used throughout this article to manipulate type theories. Note that our method consists in formulating a type theory to describe a structure, as opposed to developing said structure internally to Martin–Löf type theory.

Expressions. A type theory manipulates various kind of objects, that we present here along with the convention we use for naming them.

• variables are elements of a given infinite countable set of variables, we denote them $x,y,z,\ldots$ ,

• terms, which are built out of variables and constructors, we denote them $t,u,\ldots$ ,

• types, which are built out of terms and constructors, we denote them $A,B,\ldots$ ,

• contexts are supported by association lists of the form $x:A$ , they are denoted $\Gamma,\Delta,\ldots$ ,

• substitutions are supported by lists of mappings of the form $x\mapsto t$ where x is a variable and t a term, we denote them $\gamma,\delta,\ldots$ .

The constructors for terms and type depend on the theory we consider, and we introduce them individually. These all come with associated set of variables, $\operatorname{Var}$ and that is the set of variables needed to build it out. We denote $\operatorname{Var}({t:A})$ for the union of $\operatorname{Var}(t)$ and $\operatorname{Var}(A)$ . For contexts and substitutions, we always have the following formulas

\begin{align*} \operatorname{Var}({\varnothing}) &= \emptyset & \operatorname{Var}({\Gamma,x:A}) &= \operatorname{Var}(\Gamma) \cup \left\{{x}\right\} & \operatorname{Var}({\langle{}\rangle}) &= \emptyset & \operatorname{Var}({\langle{\gamma,x\mapsto t}\rangle}) &= \operatorname{Var}({\gamma})\cup \operatorname{Var}({t})\end{align*}

Action of substitutions. We define the action of a substitution $\gamma$ on a type A (resp. on a term t) denoted $A[\gamma]$ (resp. $t[\gamma]$ ). These are defined separately on each theory, but share the variable case in common:

\begin{equation*} x[\langle{}\rangle] = x \qquad\qquad x[\langle{\gamma,y\mapsto t}\rangle] = \left\{ \begin{array}{ll} t & \text{If $x = y$} \\ x[\gamma] & \text{Otherwise} \end{array} \right.\end{equation*}

This action provides a composition of substitutions given inductively by

\begin{align*} \langle{}\rangle\circ\delta &= \langle{}\rangle & \langle{\gamma,x\mapsto t}\rangle\circ\delta &= \langle{\gamma\circ\delta,x\mapsto t[\delta]}\rangle\end{align*}

Judgments. There are four kinds of judgments that are commons to all of our type theories, they express the well-definedness of the previously introduced objects:

\begin{equation*} \begin{array}{l@{\quad \rightsquigarrow \quad}l@{\qquad\quad}l@{\quad \rightsquigarrow \quad}l} \Gamma\vdash & \text{$\Gamma$ is a valid context} & \Gamma\vdash t:A & t \, \text{is a valid term of type} \, A \, \text{in} \, \Gamma\\ \Gamma\vdash A & A \, \text{is a valid type in} \, \Gamma & \Delta\vdash \gamma:\Gamma & \gamma \, \text{is a valid substitution from $\Delta$ to $\Gamma$} \end{array}\end{equation*}

In order to distinguish, we sometimes refer to the raw syntax, or to expressions for a syntactic entity which is not assumed to satisfy any of the above judgment.

Basic rules. The following rules are common to all the type theories that we consider

Where in the rules ce and se we assume that $x\notin\operatorname{Var}(\Gamma)$ .

Syntactic category. We admit that for all the theories that we consider, the action of substitution makes the following rules admissible

and that the action of substitutions is compatible with the composition, thus making the composition associative

\begin{align*} A[\gamma][\delta] &= A [\gamma\circ\delta] & t[\gamma][\delta] &= t[\gamma\circ\delta] & \gamma\circ(\delta\circ\delta) &= (\gamma\circ\delta)\circ\delta\end{align*}

Moreover, we can define an identity substitution, defined on a context $\Gamma = (x_i:A_i)_{i\in I}$ by $\operatorname{id}_{\Gamma} = \langle{x_i\mapsto x_i}\rangle_{i\in I}$ . One can show that whenever $\Gamma\vdash$ is derivable, then so is $\Gamma\vdash \operatorname{id}_{\Gamma}: \Gamma$ and that whenever $\Delta\vdash\gamma:\Gamma$ , $\Gamma\vdash A$ and $\Gamma\vdash t:A$ hold, the following equalities are satisfied.

\begin{align*} A[\operatorname{id}_{\Gamma}] &= A & t [\operatorname{id}_{\Gamma}] &= t & \gamma \circ \operatorname{id}_{\Gamma} &= \gamma & \operatorname{id}_{\Delta} \circ \gamma &= \gamma\end{align*}

Hence one can construct a syntactic category $\operatorname{\mathcal{S}}_{\mathfrak{T}}$ associated to a type theory $\mathfrak{T}$ , whose objects are the contexts of the type theory $\mathfrak{T}$ , and whose morphisms are the substitutions.

Properties. We admit that all our type theories also satisfy the following properties, that one can prove by induction on the derivation trees. We refer the reader to a formalization in Agda ^{Footnote 1} where we define prove these properties for some of the theories.

Category with families. We use the formalism of categories with families, introduced by Dybjer (Reference Dybjer1996) as our categorical axiomatization of dependent type theories. Denote Fam the category of families, where objects are families of sets $(A_i)_{i\in I}$ , and morphisms $f:(A_i)_{i\in I}\to (B_j)_{j\in J}$ are pairs consisting of a function $f:I\to J$ and a family of functions $(f_i:A_i\to B_{f(i)})_{i\in I}$ . Given a category C equipped with a functor T : C ^op → Fam. Given an object $\Gamma$ of C, its image will be denoted

\begin{equation*} T\Gamma = \left({\operatorname{Tm}^\Gamma_A}\right)_{A\in\operatorname{Ty}^\Gamma}\end{equation*}

i.e., $\operatorname{Ty}^\Gamma$ is the index set and $\operatorname{Tm}^\Gamma_A$ is an element of the family. By analogy with a type theory, for a morphism $\gamma : \Delta \to \Gamma$ an element $A\in\operatorname{Ty}^\Gamma$ and an element $t\in\operatorname{Tm}^\Gamma_A$ , we write $A[\gamma] = T\gamma(A)$ the image of A in $\operatorname{Ty}^\Delta$ , and $t[\gamma] = T_A\gamma(t)$ the image of t in $\operatorname{Tm}^\Delta_{A[\gamma]}$ . With those notations, the functoriality of T can be written as, for all composable morphisms $\gamma$ , $\delta$ in C,

\begin{align*} A[\gamma\circ\delta] &= A[\gamma][\delta] & A[\operatorname{id}]&=A & t[\gamma\circ\delta] &= t[\gamma][\delta] & t[\operatorname{id}]&=t\end{align*}

A category with families (or CwF) consists of a category C equipped with a functor as above T : C ^op → Fam, such that C has a terminal object, denoted $\varnothing$ , and that there is a context comprehension operation: given a context $\Gamma$ and type $A\in\operatorname{Ty}^\Gamma$ , there is a context $\left({\Gamma,A}\right)$ , together with a projection morphism $\pi:\left({\Gamma,A}\right) \to \Gamma$ and a term $p\in\operatorname{Tm}^{\left({\Gamma,A}\right)}_{A[\pi]}$ , such that for every morphism $\sigma : \Delta\to\Gamma$ in C together with a term $t \in\operatorname{Tm}^{\Delta}_{A[\sigma]}$ , there exists a unique morphism $\langle{\sigma,t}\rangle : \Delta\to\left({\Gamma,A}\right)$ such that $p[\langle{\sigma,t}\rangle] = t$ :

We call an arrow of the form $\pi:(\Gamma,A)\to\Gamma$ a display map. The following result is well-known and allow for giving structure to the syntactic category of a type theory.

Models of a category with families. The structure of category with families enforces some compatibility between context comprehension and the action of morphisms on the type.

This is essentially a reformulation of the universal property of the context comprehension and was observed by Dybjer (Reference Dybjer1996). The entire formalism of categories with families can be seen as an axiomatization of a category with a split choice of pullbacks along the display maps.

Morphisms of category with families. We call a morphism of categories with families a functor that preserves the terminal object and the context comprehension on the nose. Since the pullbacks are computed from this structure, the morphisms of categories with families preserve the pullbacks along display maps.

2.2 Globular sets

Globular weak $\omega$ -categories are supported by globular sets, which are presheaves over the category of globes G, generated by (with $ts = ss$ and $st = tt$ ). We denote $\operatorname{GSet} = \widehat{\operatorname{G}}$ the category of globular sets, and in this category, we call the n-dimensional disk the representable object represented by n and denote it $D^n$ .

Type theory for globular sets. Following Finster and Mimram (Reference Finster and Mimram2017), we first give a type theoretic description of the theory $\mathfrak{G}$ describing globular sets. This theory has two type constructors $\star$ and $\to$ and no term constructor. Intuitively, $\star$ is the types of the objects of the set, and given a type A and two terms t, u, the type ${t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ is the type of higher cells from t to u. Define the variables of a type, as well as the action of substitutions as follows

\begin{align*} \operatorname{Var}(\star) &= \emptyset & \operatorname{Var}({{t}\underset{A}{\xrightarrow{\phantom{A}}}{u}}) &= \operatorname{Var}(A) \cup \operatorname{Var}(t) \cup \operatorname{Var}(u) & \star[\gamma] &= \star & ({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})[\gamma] &= {t[\gamma]}\underset{A[\gamma]}{\xrightarrow{\phantom{A[\gamma]}}}{u[\gamma]}\end{align*}

These constructors are subject to the following introduction rules

Since there are no term constructors, the only terms in the theory $\mathfrak{G}$ are variables. A self-contained description of this theory is provided in Appendix A.1.

Semantics of the theory $\mathfrak{G}$ . Here, we present results about the theory $\mathfrak{G}$ without proofs; a detailed presentation can be found in Finster and Mimram (Reference Finster and Mimram2017), Benjamin et al. (Reference Benjamin, Finster and Mimram2021). The following result characterizes the syntactic category of $\mathfrak{G}$ and is illustrated in Figure 1.

Figure 1.

A context and its corresponding globular set.

Disk contexts. The category of finite globular sets contains in particular the representable objects $D^n$ , we also denote $D^n$ , and call disk contexts, the corresponding contexts in $\mathfrak{G}$ given by Proposition 5. In low dimensions, they are given (up to renaming of their variables), by

\begin{align*} D^0 &= (x : \star)& D^1 &= (x:\star,y:\star,f:x\to y) & D^2 &= (x:\star,y:\star,f:x\to y, g:x\to y, \alpha : f\to g)\end{align*}

2.3 The type theory $\mathsf{CaTT}$

In order to axiomatize the weak $\omega$ -category structure, we add new terms, that we call operations and coherences. This can be done by adding term constructors to the theory $\mathfrak{G}$ . To express the rules for these constructors, we introduce the ps-contexts, which are a particular class of ps-contexts.

Ps-contexts. We define ps-contexts to be a particular class of contexts in the theory $\mathfrak{G}$ that we describe using rules of a type-theoretic flavor. We thus introduce two new judgment kinds

The second judgment is just a convenient auxiliary, where the dangling variable indicates the unique variable on which one is allowed to glue a cell at the next step. These two judgments are subject to the following rules

A ps-context $\Gamma$ comes equipped with notion of i-source $\partial^-(i) \Gamma$ and i-target $\partial^+(i) \Gamma$ for every number $i\in\mathbb{N}$ , defined inductively on its structure:

\begin{equation*} \partial^-(i) {(x:\star)} = (x:\star) \qquad\qquad\partial^-_i(\Gamma,y:A,f:x\to y) = \left\{ \begin{array}{l@{\quad}l} \partial^-_i\Gamma & \text{if $\dim A \geq i$}\\ \partial^-_i\Gamma,y:A,f:x\to y & \text{otherwise} \end{array} \right.\end{equation*}

\begin{equation*} \partial^+(i) {(x:\star)} = (x:\star) \qquad\qquad \partial^+_i(\Gamma,y:A,f:x\to y) = \left\{ \begin{array}{l@{\quad}l} \partial^+_i\Gamma & \text{if $\dim A > i$}\\ \operatorname{drop}(\partial^+_i\Gamma),y:A & \text{if $\dim A = i$}\\ \partial^+_i\Gamma,y:A,f:x\to y & \text{otherwise} \end{array} \right.\end{equation*}

where $\operatorname{drop}(\Gamma)$ is the context $\Gamma$ with its last variable removed, i.e., $\operatorname{drop}(\Gamma,x:A)=\Gamma$ . We write $\partial^{\pm} \Gamma = \partial^{\pm}_{\dim\Gamma - 1}$ . With these conventions, $\partial^-(x:\star)$ and $\partial^+(x:\star)$ are not defined.

Syntax of the theory CaTT. The syntax is obtained by adding two term constructors $\mathsf{op}$ and $\mathsf{coh}$ , do the theory $\mathfrak{G}$ . A term expression in this theory is thus defined to be either a variable or of the form $\mathsf{op}_{\Delta,A}[\delta]$ or $\mathsf{coh}_{\Delta,A}[\delta]$ , where in both the latter cases $\Delta$ is a context, A is a type and $\delta$ is a substitution. To simplify the notations, we denote $\mathsf{constr}$ to be either $\mathsf{op}$ or $\mathsf{coh}$ .The set of variables and the application of substitutions are defined by the formulas

\begin{align*} \operatorname{Var}({\mathsf{constr}_{\Gamma,A}[\gamma]}) &= \operatorname{Var}({\gamma}) &\mathsf{constr}_{\Gamma,A}[\gamma][\delta] &= \mathsf{constr}_{\Gamma,A}[\gamma\circ\delta]\end{align*}

Side conditions. The introduction rules for the term constructors $\mathsf{op}$ and $\mathsf{coh}$ have to verify some side conditions regarding the variables that are used in the type that we derive. Intuitively the introduction rule for the constructor $\mathsf{op}$ creates witnesses for operations, for instance the composition, or whiskering, which a priori have no reason to be invertible, whereas the introduction rule for the constructor $\mathsf{coh}$ creates witnesses for coherences, as for instance the associators, which are always weakly invertible. In order to simplify the notations, we encapsulate the requirements for these rules along with their side conditions in new judgments $\Gamma\vdash_{\mathsf{op}} A$ and $\Gamma\vdash_{\mathsf{coh}} A$ that we interpret as stating that A defines a valid operation (resp. coherence) in the context $\Gamma$ . These two judgments are subject to the following derivation rules, which express all the requirements for the introduction rules of the constructors $\mathsf{op}$ and $\mathsf{coh}$

Note that whenever $\Gamma\vdash_{\mathsf{op}} A$ is derivable, then a top-dimensional variable of $\Gamma$ cannot appear in A, whereas whenever $\Gamma\vdash_{\mathsf{coh}} A$ is derivable, a top-dimensional variable of $\Gamma$ has to appear in A, hence these two rules are mutually exclusive.

Operations and coherences. We can now give the introduction rules for the new term constructors $\mathsf{coh}$ and $\mathsf{op}$ .

The resulting type theory obtained by adding these rules is called $\mathsf{CaTT}$ . We present all the rules of the type theory $\mathsf{CaTT}$ together in Appendix A.2.

Interpretation. The ps-contexts intuitively represent all the context in which there ought to be an essentially unique definition (in a weak situation, they have a contractible set worth of composition). The rule ( $\mathsf{op}-$ intro) enforces a composition to exist for every ps-context, while the rule ( $\mathsf{coh}-$ intro) enforces that any two composition of a ps-context are related, together, they provide a directed formulation of the idea of contractibility. Note that our formulation of the rule ( $\mathsf{coh}-$ intro) is slightly different than the one introduced by Finster and Mimram (Reference Finster and Mimram2017). Actually the two can be proven equivalent, but the proof is surprisingly involved Benjamin (Reference Benjamin2020), Coro. 103.

Examples. We give a few examples of derivations in this system illustrating how it describes weak $\omega$ -categories. This shows the introduction of a new operation and a new coherence and emphasizes the role of the substitutions taken as their arguments.

• Composition: In $\mathsf{CaTT}$ one can use an operation to derive a witness for composition of 1-cells. Start by considering the context $\Gamma_ {\texttt{comp}} = (x:\star,y:\star,f:x\to y,z:\star,g:y\to z)$ . One can check that $\Gamma_{\texttt{comp}}\vdash_{\mathsf{ps}}$ , and compute its source $\partial^-({\Gamma_{\texttt{comp}}}) = (x:\star)$ and target $\partial^+({\Gamma_{\texttt{comp}}}) = (z:\star)$ . Thus, the judgment $\Gamma_{\texttt{comp}}\vdash_{\mathsf{op}} x\to z$ is derivable. Now considering with two terms v,w in a context $\Gamma$ such that $\Gamma\vdash v:u\to u'$ and $\Gamma\vdash w:u'\to u''$ (i.e., two composable 1-cells u and v), we define the substitution $\gamma = \langle{x\mapsto u,y\mapsto u',f\mapsto v,z\mapsto u'',g\mapsto w}\rangle$ . The judgment $\Gamma\vdash \gamma:\Gamma_{\texttt{comp}}$ is then derivable, thus so it $\Gamma\vdash\mathsf{op}_{\Gamma_{\texttt{comp},x\to z}}[\gamma] : u\to u''$ . We denote this term with the simpler and more usual notation $\Gamma\vdash \texttt{comp}\ v\ w : u\to u''$ .

• Associativity: Similarly, one can define the context

  \begin{equation*} \Gamma_ {\texttt{assoc}} = (x:\star,y:\star,f:x\to y,z:\star,g:y\to z,w:\star,h:z\to w) \end{equation*}
  and check that $\Gamma_{\texttt{assoc}}\vdash_{\mathsf{ps}}$ , and $\Gamma_{\texttt{assoc}} \vdash_{\mathsf{coh}} {\texttt{comp}\ (\texttt{comp}\ f\ g)\ h} \to {\texttt{comp}\ f\ (\texttt{comp}\ g\ h)} $ are both derivable. Whenever a context $\Gamma$ defines three terms u,v,w that are composable 1-cells, the rule $\mathsf{coh}$ -intro provides a witness for the associativity of their compositions, denoted
  \begin{equation*} \Gamma\vdash\texttt{assoc}\ u\ v\ w : {\texttt{comp}\ (\texttt{comp}\ u\ v)\ w} \to {\texttt{comp}\ u\ (\texttt{comp}\ v\ w)} \end{equation*}

Models. For the purpose of this article, we define the category of weak $\omega$ -categories to be the category of models of $\mathsf{CaTT}$ , and we refer the reader to Benjamin et al. (Reference Benjamin, Finster and Mimram2021) for a formal exploration of how they relate to other known definitions of weak $\omega$ -categories. We can however explain informally why this definition is sensible: Considering a model $F:\operatorname{\mathcal{S}}_{\mathsf{CaTT}}\to{\operatorname{Set}}$ , we define its set of objects to be $F(D^0)$ , and given two objects $x,y\in F(D^0)$ , the set of 1-cells between x and y in F to be $\operatorname{Hom}_F(x,y) = \left\{{f\in F(D^1), F(s)(f)=x, F(t)(f)=y}\right\}$ where $D^1\vdash s:D^0$ is the source substitution and $D^1\vdash t:D^0$ is the target substitution. Two 1-cells $f\in\operatorname{Hom}_F(x,y)$ and $g\in\operatorname{Hom}_F(y,z)$ define a unique element of $F(\Gamma_{\texttt{comp}})$ . Then, the constructor comp defines a substitution $\Gamma_{\texttt{comp}}\to D^1$ , which induces the element of $F(D^1)$ corresponding to the composition of f and g. This observation can be generalized, so that all derivable terms correspond to additional algebraic structure on the globular set induced by F.

Syntactic category. We have seen that the category ${\operatorname{\mathcal{S}}_{\mathfrak{G}}}^{\text{op}}$ consists in the finite globular sets, which are also the finitely generated ones since the representable are finite. Similarly the category ${\operatorname{\mathcal{S}}_{\mathsf{CaTT}}}^{\text{op}}$ can be conceived as the full subcategory of $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ whose objects are the computads with finitely many generators for the weak $\omega$ -category monad. Making this statement precise requires adapting the notion of computad (Burroni Reference Burroni1993; Street Reference Street1976) to this case, or working with a monadic formulation of the theory such as Leinster’s (2004). This formulation is equivalent to the Grothendieck–Maltsiniotis definition, pas proved by Ara (Reference Ara2010). We leave the details about these computads for further work, but still mention it here in order to draw the connection with the Gabriel–Ulmer duality (Gabriel and Ulmer Reference Gabriel and Ulmer2006).

3.1 Globular sets with a unit type

We first define a variant of the type theory $\mathfrak{G}$ , that we call $\mathfrak{G}_{{1}}$ , in order to handle the dimension shift that happens.

Unit type. The type theory $\mathfrak{G}_{{1}}$ is obtained from the theory $\mathfrak{G}$ by formally replacing the type $\star$ by a unit type that we denote 1, together with a constant that we denote (), which represent a term of this unit type. We keep the constructor $\to$ . These new constructors have the following set of variables and action under substitutions

\begin{align*} \operatorname{Var}(1) &= \emptyset & \operatorname{Var}({\texttt{()}}) &= \emptyset & 1[\gamma] &= 1 & \texttt{()}[\gamma] &= \texttt{()}\end{align*}

The type introduction rules for the theory $\mathfrak{G}_{1}$ are the following:

We also add a computation rule to this theory, that postulates a new definitional equality. We use the symbol $\equiv$ to denote such definitional equalities. We require the two following rules, so that typing respects definitional equality and that 1 is a unit type.

We refer the reader to Appendix A.3 for a summary of all the rules of the theory

Theories with definitional equalities The addition of definitional equality complicates the theory quite substantially in general. A slight technical problem is that the rule ( $\eta_{1}$ ) makes the set of variables of a term not invariant. This is easily solved since we do not use this set in the presence of the unit type. A more profound issue is that one needs to account for this equality in the definition of the syntactic category. This is why we now take the set of objects to be the contexts up to definitional equality, and the morphisms to be substitutions up to definitional equality. We also consider the set of terms and types associated to a context to be up to definitional equality. The last difficulty is that adding definitional equality may break the decidability of type checking. We admit that in our case, we can actually define a normal form by rewriting any term $\Gamma\vdash t:{1}$ into the term (). This ensures that the type checking is decidable. From now on, we always implicitly normalize all the expression we consider and thus eliminate all the difficulties due to definitional equality.

Notations for mixing theories. When it is ambiguous, we write $\vdash_{\mathcal{T}}$ for judgments that are derivable in the type theory $\mathcal{T}$ . In order to simplify the formulation, we allow for rules that combine judgments coming from different theory, in particular, we may say for example that any of the following rule is admissible to express the fact that we can construct a derivation of the lower judgment in the theory $\mathcal{T}'$ from a derivation of the upper judgment in the theory $\mathcal{T}$ .

Dimension and type of terms. We define the dimension of a type in the theory $\mathfrak{G}_{1}$ by induction: dim 1 = −2 and $\dim{{t}\underset{A}{\xrightarrow{\phantom{A}}}{u}} = \dim A + 1$ . The dimension of a term $\Gamma\vdash t:A$ is $\dim t = 1 + \dim A$ . Note that for every context $\Gamma$ , there is only ever one type of dimension $-1$ that is in normal form, the type $\Gamma\vdash{()}\underset{{1}}{\xrightarrow{\phantom{{1}}}}{()}$ , we denote this type $\star$ by analogy with the theory $\mathfrak{G}$ . When we define operations acting on $\mathfrak{G}_{{1}}$ , we always ensure that they respect the definitional equality by defining them only in normal form. That means that in practice, we may treat $\star$ as a separate case if needed, keeping in mind that it is simply a short form for ${()}\underset{{1}}{\xrightarrow{\phantom{{1}}}}{()}$ .

Semantics. We now show that the semantics of the theory $\mathfrak{G}_{{1}}$ is the same as the semantics of the theory $\mathfrak{G}$ .

The desuspension operation. In order to express the theory $\mathsf{MCaTT}$ , we need an operation that we call the desuspension, that we first describe as associating, to every context $\Gamma$ of $\mathfrak{G}$ , the context $\big\downarrow{\Gamma}$ in $\mathfrak{G}_{{1}}$ . It is defined by induction on the raw syntax of the theory $\mathfrak{G}$ , together with the corresponding operation on types of $\mathfrak{G}$

Induction case for contexts:

• A derivable context obtained by the rule ec is necessarily the context $\varnothing\vdash_{\mathfrak{G}}$ . The rule ec gives a derivation of $\big\downarrow{\varnothing} \vdash_{\mathfrak{G}_{1}}$

• A derivable context obtained by the rule ce is of the form $(\Gamma,x:A)\vdash_{\mathfrak{G}}$ , by the induction case on types we have $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}} \big\downarrow{A}$ . The rule ce yields a derivation for $\big\downarrow{\Gamma},x:\big\downarrow{A}\vdash_{\mathfrak{G}_{1}}$ .

Induction for types:

• A derivable type obtained by the rule $\star$ -intro is of the form $\Gamma\vdash_{\mathfrak{G}} \star$ , we necessarily have $\Gamma\vdash_{\mathfrak{G}}$ . The induction case for contexts implies $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}}$ . The rule 1-intro then provides a derivation for $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}}{1}$ .

• A derivable type obtained by the rule $\to$ -intro is of the form $\Gamma\vdash_{\mathfrak{G}} {t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ . The induction cases for types and variables provide derivations for $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}} A$ , $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}} t:\big\downarrow{A}$ and $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}} u:\big\downarrow{A}$ . The rule $\to$ -intro then gives a derivation for $\big\downarrow{\Gamma}\vdash {t}\underset{\big\downarrow{A}}{\xrightarrow{\phantom{\big\downarrow{A}}}}{u}$ .

Induction for variables: A term obtained by the rule Var is a variable $\Gamma\vdash_{\mathfrak{G}} x:A$ , and we have $\Gamma\vdash_{\mathfrak{G}}$ . The induction for contexts implies $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}}$ . Moreover, $(x:A)\in\Gamma$ implies $(x:\big\downarrow{A})\in\big\downarrow{\Gamma}$ . The rule var lets us construct a derivation for $\big\downarrow{\Gamma}\vdash_{\mathfrak{G}_{1}} x:\big\downarrow{A}$ .

From now on, when we perform proofs by induction on the derivation tree, we rely on the form of the judgment, for instance, we may write: “For the context $\varnothing\vdash$ ” to mean that we discriminate on the rule ec and that in this case the context is necessarily $\varnothing$ . This is justified since the rule ec is the only one that allows to derive $\varnothing\vdash$ , and more generally each syntactic constructor corresponds to exactly one introduction rule.

Examples. We illustrate the desuspension with a few examples. Intuitively merely consists in rewriting the type $\star$ into the type 1. For each of the context in $\mathfrak{G}_{{1}}$ , we also give a simpler context to which it is isomorphic.

3.2 The theory $\mathsf{MCaTT}$

The type theory $\mathsf{MCaTT}$ relies on the theory $\mathsf{CaTT}$ on a fundamental level. Its inference rules use the derivability of judgments in $\mathsf{CaTT}$ . To express these rules, we need to generalize the desuspension as an operation from the raw syntax of $\mathsf{CaTT}$ to the raw syntax of $\mathsf{MCaTT}$ . The raw syntax of $\mathsf{MCaTT}$ is obtained from the one of $\mathfrak{G}_{{1}}$ by adding two term constructors $\mathsf{mop}$ and $\mathsf{mcoh}$ . A term expression is either a variable, or of the form $\mathsf{mop}_{\Gamma,A}[\gamma]$ or $\mathsf{mcoh}_{\Gamma,A}[\Gamma]$ with $\Gamma$ a ps-context and A a type and $\delta$ a substitution. We sometimes unite these two cases under the notation $\mathsf{mconstr}$ which means either one of $\mathsf{mop}$ or $\mathsf{mcoh}$ . The variable set of these terms is not well defined (since not invariant under definitional equality), but the action of substitution is, and it is defined by $\mathsf{mconstr}_{\Gamma,A}[\gamma][\delta] = \mathsf{mconstr}_{\Gamma,A}[\gamma\circ\delta]$ . By convention, whenever we use $\mathsf{constr}$ and $\mathsf{mconstr}$ in the same equality, they are corresponding constructors, so either $\mathsf{op}$ and $\mathsf{mop}$ or $\mathsf{coh}$ and $\mathsf{mcoh}$ .

The general desuspension operation. We generalize the desuspension operation to contexts, types, terms and substitutions expressions of the theory $\mathsf{CaTT}$ as follows:

\begin{align*} \big\downarrow{\varnothing} &= \varnothing & \big\downarrow{(\Gamma,x:A)} &= \big\downarrow{\Gamma} , x:\big\downarrow{A}\\ \big\downarrow{\star} &= {1} & \big\downarrow{({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})} &= {\big\downarrow{t}}\underset{\big\downarrow{A}}{\xrightarrow{\phantom{\big\downarrow{A}}}}{\big\downarrow{u}} \\ \big\downarrow{x} &= x & \big\downarrow{\mathsf{constr}_{\Gamma,A}[\gamma]} &= \mathsf{mconstr}_{\Gamma,A}[\big\downarrow{\gamma}]\\ \big\downarrow{\langle{}\rangle} &= \langle{}\rangle & \big\downarrow{\langle{\gamma,x\mapsto t}\rangle} &= \langle{\big\downarrow{\gamma}, x\mapsto \big\downarrow{t}}\rangle\end{align*}

The theory $\mathsf{MCaTT}$ . The introduction rules for the constructors $\mathsf{mop}$ and $\mathsf{mcoh}$ reuse a lot of the machinery that we have developed for the theory $\mathsf{CaTT}$ . We use the desuspension operation to transfer this machinery to the theory $\mathsf{MCaTT}$ .

In the above rules, the judgments $\Gamma\vdash_{\mathsf{ps}}$ , $\Gamma\vdash_{\mathsf{op}} A$ and $\Gamma\vdash_{\mathsf{coh}} A$ are the judgments defined for the theory $\mathsf{CaTT}$ . In particular, although A is used as an index for the terms of the theory $\mathsf{MCaTT}$ , it may not be a valid type in this theory, but it has to be a valid type in the theory $\mathsf{CaTT}$ . For instance in the second of our following example, the type A uses the expression $\texttt{comp}$ that we have defined as a constructor of $\mathsf{CaTT}$ and not of $\mathsf{MCaTT}$ . All the rules of the theory $\mathsf{MCaTT}$ are summarized in Appendix A.4 to provide a self-contained overview.

Examples. We do not provide an implementation for this theory, but we can check by hand a few examples of derivations as a sanity check for our definition of monoidal weak $\omega$ -categories.

• Monoidal product: First consider the ps-context $\Gamma_{\texttt{comp}}$ , that we have defined in Section 2.3. We have $\big\downarrow{\Gamma_{\texttt{comp}}} \simeq (f:\star,g:\star)$ , thus for any context $\Delta$ , a pair of terms t,u of type $\star$ in $\Delta$ define a unique substitution $\Delta\vdash \gamma : \big\downarrow{\Gamma}_{\texttt{comp}}$ . The rule $\mathsf{mop}$ -intro gives a derivation of the product of t and u as $\Delta\vdash \mathsf{mop}_{\Gamma_{\texttt{comp},x\to\ z}} [\gamma]: \star$ . We simplify this notation as $\Delta\vdash\texttt{prod}\ t\ u : \star$ .

• Associativity of monoidal product: Similarly, consider the context $\Gamma_{\texttt{assoc}}$ defined in Section 2.3. A context $\Delta$ in $\mathsf{MCaTT}$ equipped with three terms t,u,v of type $\star$ define a unique substitution $\Delta\vdash \gamma:\big\downarrow{\Gamma}_{\texttt{assoc}}$ . Hence, the rule $\mathsf{mcoh}$ -intro provides an associator for the monoidal product $\Delta\vdash \mathsf{mop}_{\Gamma_{\texttt{assoc}},{\texttt{comp}\ (\texttt{comp}\ f\ g)\ h \to }{\texttt{comp}\ f (\texttt{comp}\ g\ h)}} : {\texttt{prod}\ (\texttt{prod}\ t\ u )\ v} \to {\texttt{prod}\ t\ (\texttt{prod}\ u\ v)}$ . We simplify this notation as $\Delta\vdash \texttt{passoc}\ t\ u\ v: {\texttt{prod}\ (\texttt{prod}\ t\ u )\ v} \to {\texttt{prod}\ t\ (\texttt{prod}\ u\ v)}$ .

• Neutral element: Consider the ps-context $\Gamma_{\texttt{neutral}}=(x:\star)$ . Then $\big\downarrow{\Gamma_{\texttt{neutral}}}$ is terminal. The rule ( $\mathsf{mcoh}$ -intro) allows to derive the unit in any context $\Delta$ as $\Delta\vdash \mathsf{mcoh}_{\Gamma_{\texttt{neutral}},x\to\ x} : \star$ .

4.1 The desuspension functor

We have already defined the desuspension operation, that we have used freely on the raw syntax of the theory. We now lift this operation to the syntactic categories by showing that it respects the derivability of judgments. We first prove following result about the interaction of the desuspension with the application of substitutions on a raw syntax level.

Induction for types:

• In the case of the type $\star$ , we have $\big\downarrow{(\star[\gamma])} = {1}$ and $\big\downarrow{\star}[\big\downarrow{\gamma}] = {1}$ .

• In the case of a type of the form ${t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ , we have the following equalities

  \begin{align*} \big\downarrow{(({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})[\gamma])} &= {\big\downarrow{(t[\gamma])}}\underset{{\big\downarrow{(A[\gamma])}}}{\xrightarrow{\phantom{{\big\downarrow{(A[\gamma])}}}}}{\big\downarrow{(u[\gamma])}} & \big\downarrow{({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})}[\big\downarrow{\gamma}] &= {\big\downarrow{t}[\big\downarrow{\gamma}]}\underset{{\big\downarrow{A}[\big\downarrow{\gamma}]}}{\xrightarrow{\phantom{\big\downarrow{A}[\big\downarrow{\gamma}]}}} {\big\downarrow{u} [\big\downarrow{\gamma}]} \end{align*}
  and we conclude by induction on types and terms.

Induction for terms:

• In the case of a variable $\Gamma\vdash x:A$ , denote $t = x[\gamma]$ . Then the association $x\mapsto \big\downarrow{t}$ appears in $\big\downarrow{\gamma}$ . Hence, $x[\big\downarrow{\gamma}] = \big\downarrow{(x[\gamma])}$ .

• In the case of a term of the form $\mathsf{constr}_{\Gamma,A}[\delta]$ , the following equalities hold

  \begin{align*} \big\downarrow{(\mathsf{constr}_{\Gamma,A}[\delta][\gamma])} &= \mathsf{mconstr}_{\Gamma,A}[\big\downarrow{(\delta\circ\gamma)}] & \big\downarrow{(\mathsf{constr}_{\Gamma,A}[\delta])}[\big\downarrow{\gamma}] &= \mathsf{mconstr}_{\Gamma,A}[\big\downarrow{\delta}\circ\big\downarrow{\gamma}] \end{align*}
  The induction case for substitution then provides the equality between these two expressions.

Induction for substitutions:

• In the case of the empty substitution $\langle{}\rangle$ , we have $\langle{}\rangle\circ\gamma = \langle{}\rangle$ , and hence $\big\downarrow{\left({\langle{}\rangle\circ \gamma}\right)} = \langle{}\rangle$ . But we also have $\big\downarrow{\langle{}\rangle}\circ \gamma = \langle{}\rangle$ .

• In the case of a substitution of the form $\langle{\theta,x\mapsto t}\rangle$ , we have the following equalities

  \begin{align*} \big\downarrow{(\langle{\theta,x\mapsto t}\rangle\circ\gamma)} &= \langle{\big\downarrow{(\theta\circ\gamma)},x\mapsto \big\downarrow{(t[\gamma])}}\rangle & \big\downarrow{\langle{\theta,x\mapsto t}\rangle}\circ\big\downarrow{\gamma} &= \langle{\big\downarrow{\theta}\circ\big\downarrow{\gamma},x\mapsto\big\downarrow{t} [\big\downarrow{\gamma}]}\rangle \end{align*}
  Then the induction case for substitutions proves that $\big\downarrow{(\theta\circ\gamma)} = \big\downarrow{\theta}\circ\big\downarrow{\gamma}$ , and the induction case for terms applies and shows that $\big\downarrow{(t[\gamma])} = \big\downarrow{t}[\big\downarrow{\gamma}]$ . This proves the equality between the two above expressions.

• For the empty context $\varnothing\vdash_{\mathsf{CaTT}}$ , we have $\big\downarrow{\varnothing} = \varnothing$ and the rule ec gives a derivation of $\big\downarrow{\varnothing}\vdash_{\mathsf{MCaTT}}$ .

• For the context $(\Gamma,x:A)\vdash_{\mathsf{CaTT}}$ , we necessarily have $\Gamma\vdash_{\mathsf{CaTT}}$ and $\Gamma\vdash_{\mathsf{CaTT}} A$ . By induction, we have $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}}$ and $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}} \big\downarrow{A}$ . Hence, the rule ce gives a derivation for $(\big\downarrow{\Gamma},x:\big\downarrow{A})\vdash$ . We conclude by noticing that $\big\downarrow{(\Gamma,x:A)} = (\big\downarrow{\Gamma},x:\big\downarrow{A})$ .

Induction for types:

• For the type $\Gamma\vdash_{\mathsf{CaTT}}\star$ , we necessarily have $\Gamma\vdash_{\mathsf{CaTT}}$ . By induction, this implies $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}}$ . The rule 1-intro gives a derivation for $\big\downarrow{\Gamma}\vdash\big\downarrow{\star}$ .

• For the type $\Gamma\vdash_{\mathsf{CaTT}} {t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ , we have a derivation of $\Gamma\vdash_{\mathsf{CaTT}} A$ , $\Gamma\vdash_{\mathsf{CaTT}}t:A$ and $\Gamma\vdash_{\mathsf{CaTT}}u:A$ . By induction, we get a derivation of $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}}\big\downarrow{A}$ , $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}} \big\downarrow{t}: \big\downarrow{A}$ and $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}}\big\downarrow{u} : \big\downarrow{A}$ . The rule $\to$ -intro then provides a derivation of $\big\downarrow{\Gamma}\vdash{\big\downarrow{t}}\underset{\big\downarrow{A}}{\xrightarrow{\phantom{\big\downarrow{A}}}}{\big\downarrow{u}}$ .

Induction for terms:

• For a variable $\Gamma\vdash_{\mathsf{CaTT}} x:A$ , we necessarily have $\Gamma\vdash_{\mathsf{CaTT}}$ . By induction, it provides a derivation of $\big\downarrow{\Gamma}\vdash_{\mathsf{MCaTT}}$ . Moreover, we have the condition $(x:A)\in\Gamma$ , hence $(x:\big\downarrow{A})\in\big\downarrow{\Gamma}$ . The rule var then proves $\big\downarrow{\Gamma}\vdash x:\big\downarrow{A}$ .

• For a term of the form $\Delta\vdash_{\mathsf{CaTT}}\mathsf{constr}_{\Gamma,A}[\gamma]:A[\gamma]$ , we have a derivation of $\Delta\vdash_{\mathsf{CaTT}}\gamma:\Gamma$ . By induction, provides a derivation for $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}} \big\downarrow{\gamma}:\big\downarrow{\Gamma}$ . The rule $\mathsf{mop}$ -intro or ( $\mathsf{mcoh}$ -intro) then gives a derivation of $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}} \mathsf{mconstr}_{\Gamma,A}[\big\downarrow{\gamma}]:\big\downarrow{A}[\big\downarrow{\gamma}]$ .

Induction for substitutions:

• For the empty substitution $\Delta\vdash_{\mathsf{CaTT}}\langle{}\rangle:\varnothing$ , we have a derivation of $\Delta\vdash_{\mathsf{CaTT}}$ . By induction, it provides a derivation of $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}}$ . The rule es then proves $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}}\langle{}\rangle:\varnothing$ .

• For the substitution $\Delta\vdash_{\mathsf{CaTT}}\langle{\gamma,x\mapsto t}\rangle:(\Gamma,x:A)$ , we have derivations of $\Delta\vdash_{\mathsf{CaTT}}\gamma:\Gamma$ , $\Gamma,x:A\vdash_{\mathsf{CaTT}}$ and $\Delta\vdash_{\mathsf{CaTT}}t:A[\gamma]$ . By induction those provide derivations of $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}} \big\downarrow{\gamma}:\big\downarrow{\Gamma}$ , $\big\downarrow{\Gamma},x:\big\downarrow{A} \vdash_{\mathsf{MCaTT}}$ and $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}} \big\downarrow{t} : \big\downarrow{(A[\gamma])}$ . Moreover, by Lemma 12, the last judgment rewrites as $\big\downarrow{\Delta} \vdash \big\downarrow{t}: \big\downarrow{A}[\big\downarrow{\gamma}]$ . Hence, the rule es provides a derivation of the judgment $\big\downarrow{\Delta}\vdash_{\mathsf{MCaTT}}\langle{\big\downarrow{\gamma}, x\mapsto \big\downarrow{t}}\rangle : (\big\downarrow{\Gamma},x:\big\downarrow{A})$ .

Categorical reformulation. We reformulate Lemma 12 and Proposition 13 in a categorical fashion, taking advantage of the formalism of categories with families.

• For the empty context $\varnothing$ , the identity is the empty substitution $\operatorname{id}_{\varnothing} = \langle{}\rangle$ , and we have $\big\downarrow{\langle{}\rangle} = \langle{}\rangle$ .

• For the context $(\Gamma,x:A)$ , the identity is $\langle{\operatorname{id}_{\Gamma},x\mapsto x}\rangle$ , whose image is $\langle{\big\downarrow{\operatorname{id}_{\Gamma}},x\mapsto x}\rangle$ . By induction, we have $\big\downarrow{\operatorname{id}_{\Gamma}} = \operatorname{id}_{\big\downarrow{\Gamma}}$ , which gives the equality $\big\downarrow{\operatorname{id}_{(\Gamma,x:A)}} = \operatorname{id}_{\big\downarrow{(\Gamma,x:A)}}$ .

We now show that this functor is a morphism of categories with families, be defining the image of a type $\Gamma\vdash A$ to be $\big\downarrow{A}$ and the image of a term $\Gamma\vdash t:A$ to be $\big\downarrow{t} $ . Proposition 13 shows that these elements live in the adequate set, and Lemma 12 moreover ensures that this association is functorial, so $\big\downarrow{}$ defines a morphism in the slice category $\operatorname{Cat}/\operatorname{Fam}$ . Since moreover the operation $\big\downarrow{}$ is defined to preserve the terminal context and the context comprehension (by definition, we have $\big\downarrow{\varnothing} = \varnothing$ and $\big\downarrow{(\Gamma,x:A)} = (\big\downarrow{\Gamma},x:\big\downarrow{A})$ and $\big\downarrow{\langle{\gamma,x\mapsto t}\rangle} = \langle{\big\downarrow{\gamma},x\mapsto \big\downarrow{t}}\rangle$ ), it is a morphism of categories with families.

4.2 The reduced suspension functor

We define another translation going in the opposite direction called the reduced suspension. It is an operation associating an expression of the theory $\mathsf{CaTT}$ to every expression of the theory $\mathsf{MCaTT}$ . This operation is not however purely syntactic, and even though it outputs a raw expression of $\mathsf{CaTT}$ , it is only properly defined on the derivable expression of $\mathsf{MCaTT}$ .

The reduced suspension operation. In order to define the reduced suspension, we assume the existence of a variable name that is completely fresh and call it $\bullet_{}$ . This could be achieved by extending the set of variables that we use with the variable $\bullet_{}$ .

In the case of a variable $\Gamma\vdash x:A$ , we have to assume that A ≠ 1 to ensure that the term is in normal form so that definitional equality is respected.

Syntactic properties of the reduced suspension. We show a few technical results, that are useful to prove that the reduced suspension preserves the judgments.

• for any type $\Gamma\vdash_{\mathsf{MCaTT}} A$ we have the equality $\big\uparrow{(A[\gamma])}=\big\uparrow{A}[\big\uparrow{\gamma}]$

• for any term $\Gamma\vdash_{\mathsf{MCaTT}} t:A$ , we have the equality $\big\uparrow{(t[\gamma])} = \big\uparrow{t}[\big\uparrow{\gamma}]$

• for any substitution $\Gamma\vdash_{\mathsf{MCaTT}}\delta:\Delta$ , we have the equality $\big\uparrow{\delta\circ \gamma} = \big\uparrow{\delta}\circ\big\uparrow{\gamma}$ .

Induction for types:

• For the type 1, we have ${1}[\gamma] = {1}$ , hence $\big\uparrow{\left({{1}[\gamma]}\right)} = \big\uparrow{1} = \star$ . But we also have $\big\uparrow{1}[\big\uparrow{\gamma}] = \star[\big\uparrow{\gamma}]=\star$ .

• For the type ${t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ , we have the two following equalities

  \begin{align*} \big\uparrow{(({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})[\gamma])} &= {\big\uparrow{(t[\gamma])}}\underset{\big\uparrow{(A[\gamma])}}{\xrightarrow{\phantom{\big\uparrow{(A[\gamma])}}}}{\big\uparrow{(u[\gamma])}} & (\big\uparrow{({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})})[\big\uparrow{\gamma}] &={(\big\uparrow{t})[\big\uparrow{\gamma}]}\underset{(\big\uparrow{A})[\big\uparrow{\gamma}]}{\xrightarrow{\phantom{(\big\uparrow{A})[\big\uparrow{\gamma}]}}}{(\big\uparrow{u})[\big\uparrow{\gamma}]} \end{align*}
  and by induction, we have $\big\uparrow{(A[\gamma])} = (\big\uparrow{A})[\big\uparrow{\gamma}]$ , $\big\uparrow{(t[\gamma])} = (\big\uparrow{t})[\big\uparrow{\gamma}]$ and $\big\uparrow{(u[\gamma])} = (\big\uparrow{u})[\big\uparrow{\gamma}]$ .

Induction for terms:

• For the term $\texttt{()}$ , we have $\big\uparrow{\left({\texttt{()}[\gamma]}\right)} = \bullet_{}$ . and also $\big\uparrow{\texttt{()}}[\big\uparrow{\gamma}] = \bullet_{}[\big\uparrow{\gamma}]$ . Lemma 16 shows $\big\uparrow{\texttt{()}}[\big\uparrow{\gamma}] = \bullet_{}$ .

• For the term $\Gamma\vdash x:A$ ( $\neq {1}$ ), by definition, $\big\uparrow{\gamma}$ defines the mapping $x\mapsto \big\uparrow{(x[\gamma])}$ , so $x[\big\uparrow{\gamma}] = \big\uparrow{(x[\gamma])}$ .

• For a term of the form $\mathsf{mop}_{\Gamma,A}[\delta]$ , we have the following equalities

  \begin{align*} \big\uparrow{(\mathsf{mconstr}_{\Gamma,A}[\delta][\gamma])} &= \mathsf{constr}_{\Gamma,A}[\bullet_{\Gamma\circ\big\uparrow{(\delta\circ\gamma)}}] \\ (\big\uparrow{\mathsf{mconstr}_{\Gamma,A}[\delta]})[\big\uparrow{\gamma}] &= \mathsf{constr}_{\Gamma,A}[(\bullet_{\Gamma\circ\big\uparrow{\delta})\circ\big\uparrow{\gamma}}] \end{align*}
  By induction and associativity of composition, these two terms are equal.

Induction for substitutions:

• For the substitution $\langle{}\rangle$ , we have $\big\uparrow{(\langle{}\rangle\circ\gamma)} = \langle{\bullet {}\mapsto\bullet {}}\rangle$ and $\big\uparrow{\langle{}\rangle}\circ\big\uparrow{\gamma} = \langle{\bullet {}\mapsto\bullet {}[\big\uparrow{\gamma}]}\rangle$ . Lemma 16 this shows that $\big\uparrow{\langle{}\rangle}\circ\big\uparrow{\gamma} = \langle{\bullet {}\mapsto\bullet {}}\rangle$ .

• For the substitution $\Gamma\vdash\langle{\theta,x\mapsto t}\rangle:(\Theta,x:{1})$ , we have the following equalities

  \begin{align*} \big\uparrow{(\langle{\theta,x\mapsto t}\rangle\circ\gamma)} &= \langle{\big\uparrow{(\theta\circ\gamma)}}\rangle & \big\uparrow{\langle{\theta,x\mapsto t}\rangle}\circ\big\uparrow{\gamma} &= \langle{\big\uparrow{\theta}\circ\big\uparrow{\gamma}}\rangle \end{align*}
  and we conclude by the induction case for substitutions.

• For a substitution of the form $\Gamma\vdash\langle{\theta,x\mapsto t}\rangle:(\Theta,x:A)$ with $$A \ne 1$$ , we have the equalities

  \begin{align*} \big\uparrow{(\langle{\theta,x\mapsto t}\rangle\circ\gamma)} &= \langle{\big\uparrow{(\theta\circ\gamma)},x\mapsto\big\uparrow{(t[\gamma])}}\rangle &\big\uparrow{\langle{\theta,x\mapsto t}\rangle}\circ\big\uparrow{\gamma} &= \langle{\big\uparrow{\theta}\circ\big\uparrow{\gamma},x\mapsto(\big\uparrow{t})[\big\uparrow{\gamma}]}\rangle \end{align*}
  and by conclude by the induction cases for substitutions and terms.

Reduced suspension on the theory $\mathfrak{G}$ . Note that the theory $\mathfrak{G}$ can be included in the theory $\mathsf{MCaTT}$ , by sending any expression in the theory $\mathfrak{G}$ to the same expression, seen as an expression of $\mathsf{MCaTT}$ . The only difference is that the type $\star$ is primitive in $\mathfrak{G}$ while it is interpreted as ${\texttt{()}}\to{\texttt{()}}$ in $\mathsf{MCaTT}$ . We first focus on the restriction of the reduced suspension to the theory $\mathfrak{G}$ . Since the reduced suspension sends variables on variables, it preserves the expressions of $\mathfrak{G}$ . We show that this transformation respects the derivation. This is a technical intermediate for generalizing the reduced suspension as a transformation from $\mathsf{MCaTT}$ to $\mathsf{CaTT}$ .

• For the empty context $\varnothing$ , we have $\big\uparrow{\varnothing} = (\bullet {}:\star)$ , and we can construct a derivation of $\big\uparrow{\varnothing}\vdash$ by applying successively the rules ec, $\star$ -intro and ce.

• For the context $(\Gamma,x:A)\vdash$ ( $$A \ne 1$$ since we are in the theory $\mathfrak{G}$ ), we have $\Gamma\vdash A$ . By induction this gives a derivation for $\big\uparrow{\Gamma}\vdash \big\uparrow{A}$ . The rule ce provides a derivation for $(\big\uparrow{\Gamma},x:\big\uparrow{A})\vdash$

Induction for types:

• For the type $\Gamma\vdash \star$ , we have a derivation of $\Gamma\vdash$ . By the induction, this shows $\big\uparrow{\Gamma}\vdash$ . Since $(\bullet {}:\star)\in\big\uparrow{\Gamma}$ , we can construct a derivation of $\big\uparrow{\Gamma}\vdash\big\uparrow{\star}$ as follows

• For the type $\Gamma\vdash {t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ , we have derivations of $\Gamma\vdash A$ , $\Gamma\vdash t:A$ and $\Gamma\vdash u:A$ . By induction, those give derivations of $\big\uparrow{\Gamma}\vdash\big\uparrow{A}$ , $\big\uparrow{\Gamma}\vdash \big\uparrow{t} : \big\uparrow{A}$ and $\big\uparrow{\Gamma}\vdash \big\uparrow{u} : \big\uparrow{A}$ . The rule $\to$ -intro then provides a derivation of $\big\uparrow{\Gamma}\vdash {\big\uparrow{t}}\underset{\big\uparrow{A}}{\xrightarrow{\phantom{\big\uparrow{A}}}}{\big\uparrow{u}}$ .

Induction for terms: A term in $\mathfrak{G}$ is a variable $\Gamma\vdash x:A$ . For such a variable, we have a derivation of $\Gamma\vdash$ , and by induction it gives a derivation of $\big\uparrow{\Gamma}\vdash$ . Moreover, the condition $(x:A)\in\Gamma$ is satisfied, and since we are the in the theory $\mathfrak{G}$ , $A \neq {1}$ . So we have $(x:\big\uparrow{A})\in\big\uparrow{\Gamma}$ . The rule var then yields a derivation of $\big\uparrow{\Gamma}\vdash x:\big\uparrow{A}$ .

Induction for substitutions:

• For the substitution $\Delta\vdash\langle{}\rangle:\varnothing$ , we have a derivation of $\Delta\vdash$ . By induction, this gives a derivation of $\big\uparrow{\Delta}\vdash$ . Moreover, we also have by definition that $(\bullet {}:\star)\in\big\uparrow{\Delta}$ , and we have already constructed a derivation of $(\bullet_{}:\star)\vdash$ . This lets us construct a derivation for $\big\uparrow{\Delta} \vdash \big\uparrow{\langle{}\rangle}:\big\uparrow{\varnothing}$ as follows

• For the substitution $\Delta\vdash\langle{\gamma,x\mapsto t}\rangle:(\Gamma,x:A)$ , we have $$A \ne 1$$ since we are in $\mathfrak{G}$ . Then we necessarily have derivations of $\Delta\vdash \gamma:\Gamma$ , $(\Gamma,x:A)\vdash$ and $\Delta\vdash t:A[\gamma]$ . By induction, those give derivations of the judgments $\big\uparrow{\Delta}\vdash\big\uparrow{\gamma}:\big\uparrow{\Gamma}$ , $\big\uparrow{\Gamma},x:\big\uparrow{A}\vdash$ and $\big\uparrow{\Delta}\vdash \big\uparrow{t}: \big\uparrow{A[\gamma]}$ . Lemma 17 allows to rewrite the last of these judgments as $\big\uparrow{\Delta}\vdash \big\uparrow{t}:\big\uparrow{A}[\big\uparrow{\gamma}]$ . The rule se then provides a derivation of $\big\uparrow{\Delta}\vdash\big\uparrow{\langle{\gamma,x\mapsto t}\rangle}:\big\uparrow{(\Gamma,x:A)}$ .

Properties of the substitution $\bullet_{\Delta}$ . The definition of the reduced suspension relies on the substitution $\bullet_{\Delta}$ . We prove syntactic properties about this substitution.

• For any type $\Delta\vdash_{\mathsf{CaTT}} A$ , we have $A[\bullet_{\Delta}] = \big\uparrow{\big\downarrow{A}}$

• For any term $\Delta\vdash_{\mathsf{CaTT}} t:A$ , we have $t[\bullet_{\Delta}] = \big\uparrow{\big\downarrow{t}}$ .

• For any substitution $\Delta\vdash_{\mathsf{CaTT}} \gamma:\Gamma$ , we have $\gamma\circ\bullet_{\Delta} = \bullet_{\Gamma\circ\big\uparrow{\big\downarrow{\gamma}}}$ .

Induction on types:

• For the type $\Delta\vdash_{\mathsf{CaTT}}\star$ , we have $\big\uparrow{\big\downarrow{\star}} = \star$ and by definition, $\star[\bullet_{\Delta}] = \star$ .

• For the type $\Delta\vdash_{\mathsf{CaTT}}{t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ , we have the equalities

  \begin{align*} ({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})[\bullet_\Delta] &= {t[\bullet_\Delta]}\underset{A[\bullet_\Delta]}{\xrightarrow{\phantom{A[\bullet_\Delta]}}} {u[\bullet_\Delta]} & \big\uparrow{\big\downarrow{({t}\underset{A}{\xrightarrow{\phantom{A}}}{u})}} &= {\big\uparrow{\big\downarrow{t}}}\underset{\big\uparrow{\big\downarrow{A}}}{\xrightarrow{\phantom{\big\uparrow{\big\downarrow{A}}}}} {\big\uparrow{\big\downarrow{u} }} \end{align*}
  and by induction $A[\bullet_\Delta] = \big\uparrow{\big\downarrow{A}}$ , $t[\bullet_\Delta]=\big\uparrow{\big\downarrow{t}}$ and $u[\bullet_\Delta] = \big\uparrow{\big\downarrow{u}}$ .

Induction on terms:

• For a variable $\Delta\vdash x:A$ , by definition the mapping $x\mapsto \big\uparrow{\big\downarrow{x}}$ is the only mapping for x in $\bullet_{\Delta}$ , hence $x[\bullet_{\Delta}] = \big\uparrow{\big\downarrow{x}}$ .

• For a term of the form $\Delta\vdash\mathsf{constr}_{\Gamma,A}[\gamma]:A[\gamma]$ , we have the following equations

  \begin{align*} \mathsf{constr}_{\Gamma,A}[\gamma][\bullet_{\Delta}] &= \mathsf{constr}_{\Gamma,A}[\gamma\circ\bullet_{\Delta}] & \big\uparrow{\big\downarrow{\mathsf{constr}}_{\Gamma,A}[\gamma]} &= \mathsf{constr}_{\Gamma,A}[\bullet_{\Gamma\circ\big\uparrow{\big\downarrow{\gamma}}}] \end{align*}
  and the induction case for substitutions then gives the equality.

Induction case for substitutions:

• For the empty substitution $\Delta\vdash\langle{}\rangle:\varnothing$ , since $\bullet_{\varnothing} = \langle{}\rangle$ , we have the equalities

  \begin{align*} \langle{}\rangle\circ\bullet_{\Delta} &= \langle{}\rangle & \bullet_{\varnothing\circ \big\uparrow{\big\downarrow{\langle{}\rangle}}} &= \langle{}\rangle \end{align*}

• For of the substitution $\Delta\vdash\langle{\gamma,x\mapsto t}\rangle : (\Gamma,x:A)$ , since the substitution $\bullet_{\Gamma}$ has source $\big\uparrow{\big\downarrow{\Gamma}}$ that do not use the variable x, we have $\bullet_{\Gamma\circ\langle{\big\uparrow{\big\downarrow{\gamma}},x\mapsto\big\uparrow{\big\downarrow{t}}}\rangle} = \bullet_{\Gamma\circ\big\uparrow{\big\downarrow{\gamma}}}$ . Moreover, if x is of type $\star$ we have $\big\uparrow{\big\downarrow{x}}[\langle{\big\uparrow{\big\downarrow{\gamma}},x\mapsto\big\uparrow{\big\downarrow{t} }}\rangle] = \bullet_{} = \big\uparrow{\big\downarrow{t}}$ , and if x is not of type $\star$ , the expression $x[\langle{\big\uparrow{\big\downarrow{\gamma}},x\mapsto\big\uparrow{\big\downarrow{t} }}\rangle]=\big\uparrow{\big\downarrow{t}}$ . Using the two previously shown equalities to simplify the expressions yields

  \begin{align*} \langle{\gamma,x\mapsto t}\rangle\circ\bullet_{\Delta} &= \langle{\gamma\circ\bullet_{\Delta},x\mapsto t[\bullet_{\Delta}]}\rangle& \bullet_{(\Gamma,x:A)}\circ\langle{\big\uparrow{\big\downarrow{\gamma}},x\mapsto \big\uparrow{\big\downarrow{t}}}\rangle &= \langle{\bullet_{\Gamma\circ \big\uparrow{\big\downarrow{\gamma}},x\mapsto \big\uparrow{\big\downarrow{t}}}}\rangle \end{align*}
  By induction we have $\gamma\circ\bullet_{\Delta} = \bullet_{\Gamma\circ\big\uparrow{\big\downarrow{\gamma}}}$ and $t[\bullet_{\Delta}] = \big\uparrow{\big\downarrow{t}}$

• For the context $\varnothing$ , we have already proven that $\big\uparrow{\big\downarrow{\varnothing}}\vdash$ . The rule es proves that $\big\uparrow{\big\downarrow{\varnothing}}\vdash \langle{}\rangle:\varnothing$ .

• For the context $(\Gamma,x:A)\vdash$ , we have by induction $\big\uparrow{\big\downarrow{\Gamma}}\vdash \bullet_{\Gamma} : \Gamma$ . By Proposition 1, this gives a derivation of $\big\uparrow{\big\downarrow{(\Gamma,x:A)}}\vdash \bullet_{\Gamma:\Gamma}$ . Moreover, by Lemma 18, we have that $\big\uparrow{\big\downarrow{(\Gamma,x:A)}}\vdash x:\big\uparrow{\big\downarrow{A}}$ , and Lemma 19 then shows that we have $\big\uparrow{\big\downarrow{(\Gamma,x:A)}}\vdash x:A[\bullet_\Gamma]$ . The rule se then gives a derivation of $\big\uparrow{\big\downarrow{(\Gamma,x:A)}}\vdash\bullet_{(\Gamma,x:A)}:(\Gamma,x:A)$ .

Correctness of the reduced suspension. We are now equipped to generalize the reduced suspension as an operation from the theory $\mathsf{MCaTT}$ to the theory $\mathsf{CaTT}$ . We prove the following correctness result showing that this operation is a well-defined translation between these two theories.

Induction for contexts:

• For the empty context $\varnothing$ , we have $\big\uparrow{\varnothing} = (\bullet {}:\star)$ , and we can construct a derivation of $\big\uparrow{\varnothing}\vdash$ by applying successively the rules ec, $\star$ -intro and ce.

• For the context $(\Gamma,x:{1})\vdash$ , we have $\big\uparrow{(\Gamma,x:{1})} = \big\uparrow{\Gamma}$ and by induction $\big\uparrow{\Gamma}\vdash$ .

• For the context $(\Gamma,x:A)\vdash$ with $$A \ne 1$$ , we have $\Gamma\vdash A$ . By induction this gives a derivation for $\big\uparrow{\Gamma}\vdash \big\uparrow{A}$ . The rule ce, provides a derivation for $(\big\uparrow{\Gamma},x:\big\uparrow{A})\vdash$

Induction for types:

• For the type $\Gamma\vdash{1}$ , we have a derivation of $\Gamma\vdash$ . By induction, we have a derivation of $\big\uparrow{\Gamma}\vdash$ . The rule $\star$ -intro then applies to provide a derivation of $\big\uparrow{\Gamma}\vdash\star$ .

• For the type $\Gamma\vdash {t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ , we have derivations of $\Gamma\vdash A$ , $\Gamma\vdash t:A$ and $\Gamma\vdash u:A$ . By induction, those give derivations of $\big\uparrow{\Gamma}\vdash\big\uparrow{A}$ , $\big\uparrow{\Gamma}\vdash \big\uparrow{t} : \big\uparrow{A}$ and $\big\uparrow{\Gamma}\vdash \big\uparrow{u} : \big\uparrow{A}$ . The rule $\to$ -intro then provides a derivation of $\big\uparrow{\Gamma}\vdash{\big\uparrow{t}}\underset{\big\uparrow{A}}{\xrightarrow{\phantom{\big\uparrow{A}}}}{\big\uparrow{u}}$ .

Induction for terms:

• For the term $\Gamma\vdash \texttt{()}:{1}$ , we have $\big\uparrow{\texttt{()}} = \bullet_{}$ . By induction, we have $\big\uparrow{\Gamma}\vdash$ . Since moreover $(\bullet_{}:\star)\in\big\uparrow{\Gamma}$ , the rule var gives a derivation of $\big\uparrow{\Gamma}\vdash \bullet_{} : \star$ .

• For a variable $\Gamma\vdash x:A$ , since we consider normal forms, $$A \ne 1$$ . We have a derivation of $\Gamma\vdash$ , and by induction it gives a derivation of $\big\uparrow{\Gamma}\vdash$ . Moreover, the condition $(x:A)\in\Gamma$ is satisfied, hence so is $(x:\big\uparrow{A})\in\big\uparrow{\Gamma}$ . The rule var then yields a derivation of $\big\uparrow{\Gamma}\vdash x:\big\uparrow{A}$ .

• For a term of the form $\mathsf{mconstr}_{\Gamma,A}[\gamma]$ , we have a derivation of $\Delta\vdash \gamma:\big\downarrow{\Gamma}$ . By induction, this gives a derivation for $\big\uparrow{\Delta}\vdash \big\uparrow{\gamma}:\big\uparrow{\big\downarrow{\Gamma}}$ . Moreover, Lemma 20 ensures that we have $\big\uparrow{\big\downarrow{\Gamma}}\vdash \bullet_{\Gamma : \Gamma}$ , hence we have a substitution $\big\uparrow{\Delta}\vdash \bullet_{\Gamma\circ\big\uparrow{\gamma} : \Gamma}$ . By applying the rule $\mathsf{op}$ -intro or $\mathsf{coh}$ -intro, this provides a derivation for the judgment $\big\uparrow{\Delta}\vdash\mathsf{constr}_{\Gamma,A}[\bullet_{\Gamma\circ\big\uparrow{\gamma}}] : A[\bullet_{\Gamma\circ\big\uparrow{\gamma}}]$ . The following equalities then prove that the type is the one we expect

  \begin{align*} A[\bullet_{\Gamma\circ \big\uparrow{\gamma}}] &= \big\uparrow{\big\downarrow{A}}[\big\uparrow{\gamma}] & \text{By Lemma 19} \\ &= \big\uparrow{((\big\downarrow{A})[\gamma])} & \text{By Lemma 17} \end{align*}

Induction for substitutions:

• For the substitution $\Delta\vdash\langle{}\rangle:\varnothing$ , we have a derivation of $\Delta\vdash$ . By induction, this gives a derivation of $\big\uparrow{\Delta}\vdash$ . Moreover, we also have by definition that $(\bullet {}:\star)\in\big\uparrow{\Delta}$ , and we have already constructed a derivation of $(\bullet_{}:\star)\vdash$ . This lets us construct a derivation for $\big\uparrow{\Delta} \vdash \big\uparrow{\langle{}\rangle}:\big\uparrow{\varnothing}$ as follows

• For the substitution $\Delta\vdash\langle{\gamma,x\mapsto t}\rangle:(\Gamma,x:{1})$ , we have the equalities

  \begin{align*} \big\uparrow{(\Gamma,x:{1})} &= \big\uparrow{\Gamma} & \big\uparrow{\langle{\gamma,x\mapsto t}\rangle} &= \big\uparrow{\gamma} \end{align*}
  Since we have $\Delta\vdash \gamma:\Gamma$ , by induction we deduce $\big\uparrow{\Delta}\vdash\big\uparrow{\gamma}:\big\uparrow{\Gamma}$ .

• For the substitution $\Delta\vdash\langle{\gamma,x\mapsto t}\rangle:(\Gamma,x:A)$ , we have $$A \ne 1$$ since we are in $\mathfrak{G}$ . Then we necessarily have derivations of $\Delta\vdash \gamma:\Gamma$ , $(\Gamma,x:A)\vdash$ and $\Delta\vdash t:A[\gamma]$ . By induction, those give derivations of the judgments $\big\uparrow{\Delta}\vdash\big\uparrow{\gamma}:\big\uparrow{\Gamma}$ , $\big\uparrow{\Gamma},x:\big\uparrow{A}\vdash$ and $\big\uparrow{\Delta}\vdash \big\uparrow{t}: \big\uparrow{A[\gamma]}$ . Lemma allows to rewrite the last of these judgments as $\big\uparrow{\Delta}\vdash \big\uparrow{t}:\big\uparrow{A}[\big\uparrow{\gamma}]$ . The rule se then provides a derivation of $\big\uparrow{\Delta}\vdash\big\uparrow{\langle{\gamma,x\mapsto t}\rangle}:\big\uparrow{(\Gamma,x:A)}$ .

Examples. We give a few examples of contexts in $\mathsf{MCaTT}$ along with their translations in $\mathsf{CaTT}$ to build intuition on this translation:

\begin{align*} \Gamma &= (x:\star) & \big\uparrow{\Gamma} &= (\bullet_{}:\star, x:{\bullet_{}}\underset{\star}{\xrightarrow{\phantom{\star}}} {\bullet_{}})\\ \Gamma &= (x:\star,f:{x}\underset{\star}{\xrightarrow{\phantom{\star}}}{x}, a:{1}) & \big\uparrow{\Gamma} &= (\bullet_{}:\star,x:{\bullet_{}}\underset{\star}{\xrightarrow{\phantom{\star}}}{\bullet_{}},f:{x}\underset{{\bullet_{}} \to {\bullet_{}}}{\xrightarrow{\phantom{{\bullet_{}} \to {\bullet_{}}}}}{x})\\ \Gamma &= (x:\star,y:\star;f:{x}\underset{\star}{\xrightarrow{\phantom{\star}}}{y}) & \big\uparrow{\Gamma} &= (\bullet_{}:\star,x: {\bullet_{}}\underset{\star}{\xrightarrow{\phantom{\star}}}{\bullet_{}},y:{\bullet_{}}\underset{\star}{\xrightarrow{\phantom{\star}}}{\bullet_{}},f: {x}\underset{{\bullet_{}} \to {\bullet_{}}}{\xrightarrow{\phantom{{\bullet_{}}\to{\bullet_{}}}}}{y})\end{align*}

These examples help understand why it is important to require that the translation is defined on normal forms. Indeed, in the second example, we have a derivation $\Gamma\vdash a:{1}$ but the term is not in normal form. Putting it in normal form before applying the reduced suspension yields to the term $\Gamma\vdash\bullet_{}:{1}$ which is indeed derivable. However, had we simply defined the reduced suspension of any variable to be itself, without consideration of whether it is in normal form, we would have gotten the judgment $\big\uparrow{\Gamma}\vdash a:\star$ which is not derivable.

Reduced suspension as a functor. Like for the desuspension, we can reformulate this result in a more categorical flavor. However the result that we prove here is weaker.

• For the empty context $\varnothing$ , we have $\operatorname{id}_{\varnothing} = \langle{}\rangle$ along with $\big\uparrow{\varnothing} = (\bullet_{}:\star)$ and $\big\uparrow{\langle{}\rangle}=\langle{\bullet_{}\mapsto \bullet_{}}\rangle$ , which is the identity of $\big\uparrow{\varnothing}$ .

• For a context of the form $(\Gamma, x:{1})$ , we have $\operatorname{id}_{(\Gamma,x:{1})} = \langle{\operatorname{id}_{\Gamma},\bullet_{}\mapsto\bullet_{}}\rangle$ . Hence $\big\uparrow{\operatorname{id}_{(\Gamma,x:{1})}} = \big\uparrow{\operatorname{id}_{\Gamma}}$ , and by induction $\big\uparrow{\operatorname{id}_{\Gamma}} = \operatorname{id}_{\big\uparrow{\Gamma}}$ . We conclude using the fact that $\big\uparrow{(\Gamma,x:{1})} = \big\uparrow{\Gamma}$ .

• For a context of the form $(\Gamma,x:A)$ with $$A \ne 1$$ , we have $\big\uparrow{\operatorname{id}_{(\Gamma,x:A)}} = \langle{\big\uparrow{\operatorname{id}_{\Gamma}},x\mapsto x}\rangle$ , and by induction, we have $\big\uparrow{\operatorname{id}_{\Gamma}} = \operatorname{id}_{\big\uparrow{\Gamma}}$ , which lets us conclude that $\big\uparrow{\operatorname{id}_{(\Gamma,x:A)}} = \operatorname{id}_{\big\uparrow{(\Gamma,x:A)}}$ .

Note that in fact Lemma 17 and Proposition 13 provide more structure than this. They show that this functor is almost a morphism of category with families. In fact it defines a morphism in $\operatorname{Cat}/\operatorname{Fam}$ , which respects the structures of categories with families of $\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}$ and $\operatorname{\mathcal{S}}_{\mathsf{CaTT}}$ . This functor however fails to be a morphism of categories with families as it does not preserve the terminal object, since the context $\varnothing$ is sent onto $(\bullet_{}:\star)$ which is not terminal. This result however is complicated to formulate cleanly in a categorical way.

4.3 Interaction between desuspension and reduced suspension

We have defined the theory $\mathsf{MCaTT}$ together with two translations, the desuspension and the reduced suspension, that define functors between their syntactic categories. We now study how these translations relate to each other syntactically and translate this result categorically as a relation between the two functors. In order to understand the interaction between the desuspension and the reduced suspension, we first show the following result, analogous to Lemma 8 for the theory $\mathsf{MCaTT}$ .

Desuspension of the reduced suspension. We can now express one of the relations that link the desuspension and the reduced suspension. We first express these relations on the type theory before leveraging the expressive power of the categorical semantics to provide a much more compact reformulation.

• For all context $\Gamma\vdash$ , there is an isomorphism $\eta_\Gamma : \Gamma \to \big\downarrow{\big\uparrow{\Gamma}}$ .

• For all type $\Gamma\vdash A$ , we have the equality $\Gamma\vdash A \equiv \big\downarrow{\big\uparrow{\Gamma}}[\eta_\Gamma]$ .

• For all term $\Gamma\vdash t:A$ , we have $\Gamma\vdash t \equiv \big\downarrow{\big\uparrow{t}}[\eta_\Gamma]:A$ .

• For all substitution $\Delta\vdash \gamma:\Gamma$ , the following square commutes

• (auxiliary induction case) for all context $\Gamma$ in the theory $\mathsf{CaTT}$ , we have $\big\downarrow{\bullet_{\Gamma}}\circ\eta_{\big\downarrow{\Gamma}} = \operatorname{id}_{\big\downarrow{\Gamma}}$ .

Induction for contexts:

• For the empty context $\varnothing\vdash$ , we have $\big\uparrow{\varnothing} = (\bullet {}:\star)$ , and thus $\big\downarrow{\big\uparrow{\varnothing}} = (\bullet_{}:{1})$ . Lemma 23 then provides the desired isomorphism $\eta_\varnothing=\langle{\bullet_{}\mapsto ()}\rangle : \varnothing \to \big\downarrow{\big\uparrow{\varnothing}}$ .

• For a context of the form $(\Gamma,x:{1})\vdash$ , we have $\big\uparrow{(\Gamma,x:{1})} = \big\uparrow{\Gamma}$ , hence $\big\downarrow{\big\uparrow{(\Gamma,x:{1})}} = \big\downarrow{\big\uparrow{\Gamma}}$ . By Lemma 23, the following weakening is an isomorphism $\pi : (\Gamma,x:{1})\overset{\sim}\to \Gamma$ , and the induction hypothesis on contexts provides the isomorphism $\eta_\Gamma : \Gamma \overset{\sim}\to \big\downarrow{\big\uparrow{\gamma}}$ . By composition, this provides the isomoprhism following (writing the weakening implicitly) $\eta_{(\Gamma,x:{1})} = \eta_\Gamma : (\Gamma,x:{1}) \to \big\downarrow{\big\uparrow{(\Gamma,x:{1})}}$ .

• For a context of the form $(\Gamma,x:A)\vdash$ with $$A \ne 1$$ , we have $\big\uparrow{(\Gamma,x:A)} = (\big\uparrow{\Gamma},x:\big\uparrow{A})$ . Since $\big\uparrow{A}$ is necessarily distinct from $\star$ , we have $\big\downarrow{\big\uparrow{(\Gamma,x:A)}} = (\big\downarrow{\big\uparrow {\Gamma}},x:\big\downarrow{\big\uparrow{A}})$ , and the induction case for contexts provides the isomoprhism $\eta_\Gamma : \Gamma\overset{\sim}\to\big\downarrow{\big\uparrow{\Gamma}}$ . Moreover, the induction case for types shows that $\Gamma\vdash A\equiv \big\downarrow{\big\uparrow{A}}[\eta_\Gamma]$ . Hence we define the isomoprhism $\eta_{(\Gamma,x:A)} = \langle{\eta_\Gamma,x\mapsto x}\rangle : (\Gamma,x:A)\overset\sim\to \big\downarrow{\big\uparrow{(\Gamma,x:A)}}$ , whose inverse is given by $\langle{\eta_\Gamma^{-1} , x\mapsto x}\rangle$ .

Induction for types:

• For the type $\Gamma\vdash {1}$ , we have $\big\downarrow{\big\uparrow{1}}[\eta_\Gamma] = {1}[\eta_\Gamma]$ . Since we have also by definition ${1}[\eta_\Gamma] = {1}$ , this shows that ${1} = \big\downarrow{\big\uparrow{1}}[\eta_\Gamma]$ .

• For the type $\star ={()}\underset{1}{\xrightarrow{\phantom{1}}}{()}$ , we have $\big\downarrow{\big\uparrow{\star}}[\eta_\Gamma] = {\bullet_{}[\eta_\Gamma]}\underset{1}{\xrightarrow{\phantom{1}}}{\bullet_{}[\eta_\Gamma]}$ . Note that by Proposition 21 along with the induction case for contexts, we have a derivation of $\Gamma\vdash \bullet_{}[\eta_\Gamma]:{1}$ . Hence, the rule $\eta_{1}$ applies and provides the equality $\Gamma\vdash \star\equiv \big\downarrow{\big\uparrow{\star}}[\eta_\Gamma]$ .

• For a type of the form $\Gamma\vdash {t}\underset{A}{\xrightarrow{\phantom{A}}}{u}$ with $$A \ne 1$$ , $\big\downarrow{\big\uparrow{{t}\underset{A}{\xrightarrow{\phantom{A}}}{u}}} ={\big\downarrow{\big\uparrow{t}}}\underset{\big\downarrow{\big\uparrow{A}}}{\xrightarrow{\phantom{\big\downarrow{\big\uparrow {A}}}}}{\big\downarrow{\big\uparrow{u}}}$ . The induction case for types then shows that $\Gamma\vdash A\equiv\big\downarrow{\big\uparrow{A}}[\eta_\Gamma]$ , and the induction case for terms shows $\Gamma\vdash t:A\equiv \big\downarrow{\big\uparrow{t}}[\eta_\Gamma]$ similarly for u, which lets us conclude.

Induction for terms:

• For the term $\Gamma\vdash ():{1}$ , we have $\Gamma\vdash \big\downarrow{\big\uparrow{()}}[\eta_\Gamma] : {1}$ , and the rule $\eta_{1}$ gives the desired definitional equality.

• For a variable $\Gamma\vdash x:A$ , we need to have $$A \ne 1$$ for the term to be in normal form, we have $\big\uparrow{x} = x$ and thus $\big\downarrow{\big\uparrow{x}} = x$ . Moreover, since the pair $x:A$ appears in $\Gamma$ with $$A \ne 1$$ , by definition of $\eta_\Gamma$ (induction case for contexts), the association $x\mapsto x$ appears in $\eta_\Gamma$ , and hence $\big\downarrow{\big\uparrow{x}}[\eta_\Gamma] = x$ .

• For a term of the form $\mathsf{mop}_{\Gamma,A}[\gamma]$ , we have $\big\uparrow{\mathsf{mop}_{\Gamma,A}[\gamma]} = \mathsf{op}_{\Gamma,A}[\bullet_{\Gamma\circ\big\uparrow{\gamma}}]$ , and thus we have the following equalities

  \begin{align*} (\big\downarrow{\big\uparrow{\mathsf{mop}_{\Gamma,A}[\gamma]}})[\eta_\Delta] &= \mathsf{mop}_{\Gamma,A}[\big\downarrow{(\bullet_{\Gamma\circ\big\uparrow{\gamma})}\circ \eta_\Delta}] \\ &= \mathsf{mop}_{\Gamma,A}[\big\downarrow{\bullet_{\Gamma}}\circ(\big\downarrow{\big\uparrow{\gamma}}\circ \eta_\Delta)] & \text{by Lemma} \, 12\\ &\equiv \mathsf{mop}_{\Gamma,A}[(\big\downarrow{\bullet_\Gamma}\circ \eta_{\big\downarrow{\Gamma}}) \circ \gamma] & \text{by the induction case for substitutions} \\ &\equiv \mathsf{mop}_{\Gamma,A}[\gamma] & \text{by the auxiliary induction case}\end{align*}
  Note that in the third step, the substitution $\eta_{\big\downarrow{\Gamma}}$ appears since we started with a definition $\Gamma$ whose target is $\big\downarrow{\Gamma}$ .

• The case for a term of the form $\mathsf{mcoh}_{\Gamma,A}[\gamma]$ follows the exact same steps.

Induction for substitutions:

• For the empty substitution $\Delta\vdash \langle{}\rangle:\varnothing$ , by the induction case for contexts, we have the following square of maps

Since by Lemma 23 both $\varnothing$ and $(x:{1})$ are terminal objects, this square has to commute.

• For a substitution of the form $\Delta\vdash \langle{\Gamma,x\mapsto t}\rangle:(\Gamma,x:{1})$ , after applying the induction case for contexts and computing the expressions, we are left with the following square.

Note that by definition, the map $\eta_{(\Gamma,x:{1})} = (\Gamma,x:{1}) \to \big\downarrow{\big\uparrow{\Gamma}}$ is the map $\eta_\Gamma$ weakened with respect to the variable x, hence we have $\eta_{(\Gamma,x:{1})} \circ \langle{\gamma,x\mapsto t}\rangle = \eta_\Gamma \circ \gamma$ . By the induction case for substitutions, this expression is equal to $\big\downarrow{\big\uparrow{\gamma}} \circ\eta_\Delta$ , which exactly provides the commutation of the above square.

• For a substitution of the form $\Delta\vdash\langle{\gamma,x\mapsto t}\rangle:(\Gamma,x:A)$ with $$A \ne 1$$ , we have the following equalities

  \begin{align*} \langle{\big\downarrow{\big\uparrow{\gamma}},x\mapsto \big\downarrow{\big\uparrow{t}}}\rangle\circ \eta_\Delta &= \langle{\big\downarrow{\big\uparrow{\gamma}}\circ\eta_\Delta, x\mapsto \big\downarrow{\big\uparrow{t}}[\eta_\Delta]}\rangle\\ &= \langle{\eta_\Gamma\circ \gamma, x\mapsto t}\rangle &\text{By induction on terms and substitutions}\\ &=\langle{\eta_\Gamma,x\mapsto x}\rangle \circ \langle{\gamma,x\mapsto t}\rangle &\text{Since $\eta_\Gamma$ is weakened with respect to} \, x \end{align*}
  which give exactly the commutation of desired naturality square.

Auxiliary induction case: We prove by induction on contexts that $\big\downarrow{\bullet_\Gamma}\circ\eta_{\big\downarrow{\Gamma}} = \operatorname{id}_{\big\downarrow{\Gamma}}$

• For the context $\varnothing$ in $\mathsf{CaTT}$ , the map $\big\downarrow{\bullet_\varnothing}\circ\eta_{\big\downarrow{\varnothing}}$ defines a map $\big\downarrow{\varnothing}\to\big\downarrow{\varnothing}$ . By definition, $\big\downarrow{\varnothing}$ is the terminal object in the category $\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}$ , the aforementioned map is thus necessarily the identity.

• For the context $(\Gamma,x:A)$ in $\mathsf{CaTT}$ , we have the following equalities

\begin{align*} \big\downarrow{\bullet_{(\Gamma,x:A)}}\circ\eta_{\big\downarrow{(\Gamma,x:A)}} &= \langle{\big\downarrow{\bullet_\Gamma},\big\downarrow{\big\uparrow{\big\downarrow{x}}}}\rangle \circ \eta_{\big\downarrow{\Gamma}} \\ &= \langle{\big\downarrow{\bullet_\Gamma}\circ\eta_\Gamma, \big\downarrow{\big\uparrow{x}}[\eta_{\big\downarrow{\Gamma}}]}\rangle &\text{Since $\big\downarrow{x} = x$}\\ &= \langle{\operatorname{id}_{\Gamma},x\mapsto x}\rangle &\text{By induction on terms} \end{align*}

A natural transformation. In order to study the reduced suspension, we have introduced the family of substitutions $\bullet_\Gamma$ for all contexts $\Gamma$ , and we have proved in Lemma 20, that it defines a family of morphisms $\bullet_\Gamma:\big\uparrow{\big\downarrow{\Gamma}}\to\Gamma$ . Moreover, the equality $\gamma\circ\bullet_\Delta =\bullet_\Gamma\circ\big\uparrow{\big\downarrow{\gamma}}$ that we proved in Lemma 19 for all substitution $\gamma$ can be expressed by the commutation of the following diagram

So we have in fact already proven the following proposition, which is simply a categorical reformulation of our previous fact

Adjunction between desuspension and reduced suspension. Combining Propositions 24 and 25, we have in fact proved the following categorical result about the functors induced by desuspension and the reduced suspension.

Theorem The functor $\big\uparrow{}$ is left adjoint to $\big\downarrow{}$ , the counit is given by the family $\bullet_\Gamma$ and the unit is the natural family of isomorphisms $\eta_\Gamma$ . This adjunction is thus coreflective.

• For the empty context $\varnothing$ , since $\bullet_{}$ is a variable, we have $\big\uparrow{\big\downarrow{\bullet_{}}} = \bullet_{}$ , and hence

  \begin{equation*} \bullet_{\big\uparrow{\varnothing}}\circ\big\uparrow{\eta_\varnothing} = \bullet_{(\bullet_{},\star)}\circ\big\uparrow{\langle{\bullet_{}\mapsto ()}\rangle} = \langle{\bullet_{}\mapsto \big\uparrow{\big\downarrow{\bullet_{}}}}\rangle\circ\langle{\bullet_{}\mapsto\bullet_{}}\rangle = \langle{\bullet_{}\mapsto\bullet_{}}\rangle = \operatorname{id}_{\big\uparrow{\varnothing}} \end{equation*}

• For the context $(\Gamma,x:{1})$ , we have by induction

  \begin{equation*} \bullet_{\big\uparrow{\Gamma,x:{1}}}\circ\big\uparrow{\eta_{(\Gamma,x:{1})}} = \bullet_{\big\uparrow{\Gamma}}\circ\big\uparrow{\eta_{\Gamma}} = \operatorname{id}_{\big\uparrow{\Gamma}} = \operatorname{id}_{\big\uparrow{\Gamma,x:{1}}} \end{equation*}

• For the context $(\Gamma,x:A)$ with $$A \ne 1$$ , we have

  \begin{align*} \bullet_{\big\uparrow{\Gamma,x:A}}\circ\big\uparrow{\eta_{(\Gamma,x:A)}} &= \bullet_{(\big\uparrow{\Gamma},x:\big\uparrow{A})}\circ\langle{\big\uparrow{\eta_{\Gamma}},x\mapsto x}\rangle \\ &=\langle{\bullet_{\big\uparrow{\Gamma}},x\mapsto \big\uparrow{\big\downarrow{x}}}\rangle \circ \langle{\big\uparrow{\eta_{\Gamma}},x\mapsto \big\uparrow{x}}\rangle\\ & = \langle{\bullet_{\big\uparrow{\Gamma}} \circ \big\uparrow{\eta_\Gamma}, x\mapsto \big\uparrow{\big\downarrow{x}} [\langle{\eta_\Gamma,x\mapsto \big\uparrow{x}}\rangle]}\rangle \end{align*}
  Using the induction hypothesis, and the fact that since x is a variable, we have $x = \big\downarrow{x} = \big\uparrow{\big\downarrow{x}}$ , it follows that $\bullet_{\big\uparrow{(\Gamma,x:A)}}\circ\big\uparrow{\eta_{(\Gamma,x:A)}} = \operatorname{id}_{(\big\uparrow{\Gamma},x:\big\uparrow{A})}$ .

This adjunction is to be understood as an analogue in the world of categories of the topological adjunction between the reduced suspension and the loop space. In our terminology, the desuspension corresponds to the loop space, and the reduced suspension corresponds to the reduced suspension.

5.1 Action of reduced suspension and desuspension on the models

Desuspension acting on the models of $\mathsf{MCaTT}$ . Consider a model $F : \operatorname{\mathcal{S}}_{\mathsf{MCaTT}}\to\operatorname{Set}$ and define the functor $\big\downarrow^*{F} : \operatorname{\mathcal{S}}_{\mathsf{CaTT}}\to\operatorname{Set}$ by precomposing with the functor $\big\downarrow{}$ , so we have $\big\downarrow^*{F}(\Gamma) = F(\big\downarrow{\Gamma})$ and $\big\downarrow^*{F} (\gamma) = F(\big\downarrow{\gamma})$ . By Corollary 14, $\big\downarrow{}$ is a morphism of categories with families, and those preserve display maps, the terminal object and pullbacks along display maps. Since F is a model, it also preserves the terminal and the pullback along display maps, hence so does the composite $\big\downarrow^*{F}$ . Thus $\big\downarrow^*{F}$ is a model of the theory $\mathsf{CaTT}$ , and the desuspension induces a functor $\big\downarrow^*{}:\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}})\to \mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ . Moreover, we have $\big\downarrow^*{F}(x:\star) = F(x:{1})$ and by Lemma 23, the context $(x:{1})$ is terminal and by definition, F preserves the terminal object, it follows that $\big\downarrow^*{F}(x:\star)$ is terminal in $\operatorname{Set}$ , hence $\big\downarrow^*{F}$ is an object of $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ . This shows that the desuspension induces a functor $\big\downarrow^*{}:\mathrm{Mod}({\mathsf{MCaTT}}) \to \mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ .

Reduced suspension acting on the models of $\mathsf{CaTT}$ . We define a similar construction for the reduced suspension. However, since the reduced suspension does not define an image for every term and does not preserve the terminal object, the construction is slightly more involved. We first consider start by showing the following result.

This shows that $\big\uparrow^*{F}$ is a model exactly when it preserves the initial object. Since we have by definition $\big\uparrow^*{F} (\varnothing) = F(\bullet_{}:\star)$ , this condition translates to $F (\bullet_{},\varnothing)$ being a singleton. Hence $\big\uparrow^*{F}$ is a model if and only if F is an object of $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ . This shows that $\big\uparrow^*{}$ defines a functor $ \big\uparrow^*{}:\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}}) \to \mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}})$ .

5.2 Models of the category $\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}$

Using the desuspension and the reduced suspension, we have defined a pair of functors $\big\downarrow^*{}$ and $\big\uparrow^*{}$ between the categories $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}})$ and $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ .

Theorem The functors $\big\downarrow^*{}$ and $\big\uparrow^*{}$ define an equivalence of categories between $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}})$ and $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$

• For the empty context $\varnothing$ , we necessarily have that $F(\varnothing) = \left\{{\bullet}\right\}$ , and since $\big\uparrow{\big\downarrow{\varnothing}} = D^0$ and $F\in\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ , we also have that $F(\big\uparrow{\big\downarrow{\varnothing}}) = \left\{{\bullet}\right\}$ . Hence, $F(\bullet_\varnothing)$ is the unique map between the singleton to itself, which is an isomorphism.

• For a context of the form $(\Gamma,x:\star)$ , it is obtained as a (trivial) pullback, and the map $\bullet_{(\Gamma,x:\star)}$ is obtained by universal property of the pullback, as follows

Taking the image by F on this pullback yields another pullback in $\operatorname{Set}$ (since F is a model of $\mathsf{CaTT}$ ), as follows

Since the square is a pullback, $F\pi$ is an isomorphism, and since by induction $F\bullet_\Gamma$ is also an isomorphism, necessarily $F\bullet_{\Gamma,x:\star}$ is an isomorphism.

• For a context of the form $(\Gamma,x:A)$ where A is a type distinct from $\star$ , the context is obtained as a pullback, the context $\big\uparrow{\big\downarrow{(\Gamma,x:A)}}$ is also a pullback and the substitution $\bullet_{(\Gamma,x:A)}$ is obtained by universal property as described in the following diagram which has the shape of a cube whose faces are commutative and whose front and back face are pullbacks

Taking the image by F of this diagram yields another cube whose faces are all commutative square, and whose front and back square are again pullback squares, since as a model, F preserves the pullbacks along the display maps (in the following figure, we have left implicit most of the arrows, they are simply the image by F of the ones of the previous figure).

By induction, the map $F(\bullet_\Gamma)$ is an isomorphism, making the span defining $F(\Gamma,x:A)$ and the span defining $F(\big\uparrow{\big\downarrow{(\Gamma,x:A)}})$ isomorphic. This proves that the map $F(\bullet_{(\Gamma,x:A)})$ is also an isomorphism, by uniqueness of the pullback up to isomorphism.

Reflective localization. We now give a reformulation of the construction we have presented. First note that the opposite of a category with families C embeds inside its category of models via a Yoneda embedding

\begin{equation*} \begin{array}{rcl} {C}^{\text{op}} & \hookrightarrow & \mathrm{Mod}({C})\\ \Gamma & \mapsto & C(\Gamma,\_) \end{array}\end{equation*}

Indeed, the functor $C(\Gamma,\_)$ preserves the pullbacks along display maps (and in fact all limits) by continuity of the Hom-functor. This lets us see the objects $\varnothing$ and $D^0$ as particular objects of $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ , with $\varnothing$ being the initial object. We then consider the unique map $s:\varnothing \to D^0$ in the category $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ . Then the category $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ is the category of all the s-local objects, i.e., all objects F such that the map

\begin{equation*} \mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})(s,F) : \mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})(\varnothing,F) \to \mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})(D^0,F)\end{equation*}

is a natural isomorphism. Indeed, since $\varnothing$ is an initial objects, s-local objects are exactly those such that $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})(D^0,F)$ is a singleton, which reformulates as $F(D^0)$ being a singleton by the Yoneda lemma. This exhibits $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ as a reflective localization of the category $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ at s. Theorem 5.2 then shows that $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}})$ is equivalent to $\mathrm{Mod}[_\bullet]({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ , and thus is also a reflective localization of $\mathrm{Mod}({\operatorname{\mathcal{S}}_{\mathsf{CaTT}}})$ at s. This localization lifts the coreflective adjunction between $\operatorname{\mathcal{S}}_{\mathsf{CaTT}}$ and $\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}$ realized by the desuspension and the reduced suspension, that we have stated in Theorem 4.3.

5.3 Interpretation

As we have proved independently (Benjamin et al. Reference Benjamin, Finster and Mimram2021), the models of the theory $\mathsf{CaTT}$ are equivalent to the Grothendieck–Maltsiniotis definition of weak $\omega$ -categories with the Batanin–Leinster coherator. In light of this fact, Theorem 5.2 can be reformulated as stating that the models of $\mathsf{MCaTT}$ are the weak $\omega$ -categories (in the sense of Grothendieck–Malstiniotis with the Batanin–Leinster coherator) with a single object. It is expected from higher category theory that such a result holds (Baez Reference Baez2006). Recall our interpretation of ${\operatorname{\mathcal{S}}_{\mathsf{CaTT}}}^{\text{op}}$ as finitely generated computads, and assume that similarly ${\operatorname{\mathcal{S}}_{\mathsf{MCaTT}}}^{\text{op}}$ is the category of finitely generated computads for an appropriate notion of computads for monoidal weak $\omega$ -categories. We can always view a computad for monoidal weak $\omega$ -category as a weak $\omega$ -category with a single object. In this case, it turns out that when adopting this view, the weak $\omega$ -category that we retrieve is again a freely generated computad, and this is why we were able to formulate the theory of monoidal weak $\omega$ -categories in terms of the theory of weak $\omega$ -category.

However, this fails for k-monoidal weak $\omega$ -categories, for $k>1$ . We illustrate this with $k=2$ , defining 2-monoidal $\omega$ -categories as 1-monoidal $\omega$ -categories with a single object, and we assume a suitable notion of computad for those. Then a computad for 2-monoidal $\omega$ -categories is naturally a 1-monoidal category with a single object. However, viewed as a 1-monoidal $\omega$ -category, it is not a computad. Indeed, any computad must contain at least the monoidal unit object e as well as all its iterated products $(e^{\otimes n})_{n \in\mathbb{N}}$ , so no computad may have a single object. As a result, it is impossible to transcribe the same ideas for 2-monoidal $\omega$ -categories literally. Still, we conjecture that there exists a dependent type theory for 2-monoidal weak $\omega$ -categories, along with a pair of translations back and forth to the theory $\mathsf{MCaTT}$ , and that those translation compensate the aforementioned obstruction by relying on a strictification procedure for 1-monoidal weak $\omega$ -categories, that strictifies the unit law of the monoidal product. We think that this construction should be related to the work of Finster et al. (Reference Finster, Reutter and Vicary2020) on strictly unital weak $\omega$ -categories, but we leave this conjecture and the connection between these theories for future work

We also speculate that weak $\omega$ -categories should be compared with an appropriate notion of weak equivalence, that can be described by a structure akin to a model structure, and similarly for the monoidal weak $\omega$ -categories. We have presented an equivalence between the categories with strict functors, but we expect this equivalence to lift and provide an equivalence between weak categories with weak functors. We conjecture that the relevant property in this weakened world is not having a single object (which is not expected to be invariant under weak equivalences), but having a 0-connected groupoidal core. Investigation in this direction to straighten and prove those claims are left for further work.