7 Many-sorted underlying transformations
Every many-sorted \(n\)-category contains a lower-dimensional \(m\)-category obtained by restricting the family to its first \(m + 1\) sets: one simply discards the sets and operations at dimensions above \(m\), keeping only those at pairs \((k, j)\) with \(j {\lt} k \leq m\). This construction extends naturally to the \(\omega \)-categorical setting. Moreover, any many-sorted \(n\)-functor restricts to a functor between the resulting lower-dimensional categories by keeping only the maps at dimensions up to \(m\). We call this process the underlying transformation, and we show that it is functorial.
7.1 Underlying many-sorted categories
Unlike the single-sorted case, where the underlying construction requires showing that the operations preserve the subset of \(m\)-cells, the many-sorted construction is straightforward: we simply restrict the index set.
Let \(\mathsf{C}\) be a many-sorted \(n\)-category on a family \((C_k)_{k \leq n}\), and let \(m \in \mathbb {N}\) with \(m {\lt} n\). The underlying \(m\)-category of \(\mathsf{C}\) is the many-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) on the restricted family \((C_k)_{k \leq m}\), with the source, target, identity, and composition operations at each pair \((k, j)\) with \(j {\lt} k \leq m\) being those of \(\mathsf{C}\).
Every axiom of \(\mathsf{C}^{{\lt}m}\) is an axiom of \(\mathsf{C}\) restricted to lower dimensions.
Let \(\mathsf{C}\) be a many-sorted \(\omega \)-category on a family \((C_k)_{k \in \mathbb {N}}\), and let \(m \in \mathbb {N}\). The underlying \(m\)-category of \(\mathsf{C}\) is the many-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) on the restricted family \((C_k)_{k \leq m}\), defined by the same construction as in Definition 7.1.
The many-sorted category axioms follow by the same argument as in Definition 7.1.
7.2 Underlying many-sorted functors
Let \(\mathsf{C}\) and \(\mathsf{D}\) be many-sorted \(n\)-categories, and let \(F = (F_k)_{k \leq n} \colon \mathsf{C} \to \mathsf{D}\) be a many-sorted \(n\)-functor. For any \(m \in \mathbb {N}\) with \(m {\lt} n\), the restricted family \((F_k)_{k \leq m}\) is a many-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\).
Every preservation axiom of \(F^{{\lt}m}\) is a preservation axiom of \(F\) restricted to lower dimensions.
Let \(\mathsf{C}\) and \(\mathsf{D}\) be many-sorted \(\omega \)-categories, and let \(F = (F_k)_{k \in \mathbb {N}} \colon \mathsf{C} \to \mathsf{D}\) be a many-sorted \(\omega \)-functor. For any \(m \in \mathbb {N}\), the restricted family \((F_k)_{k \leq m}\) is a many-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\).
The argument is identical to that of Definition 7.3.
7.3 Many-sorted underlying functors
The underlying constructions of the previous sections are in fact functorial, as the following definition makes precise.
Let \(n, m \in \overline{\mathbb {N}}\) with \(m \leq n\). The many-sorted underlying functor \(\operatorname{\mathcal{U}}_{\mathrm{ms}}^{(n, m)}\) from \(n\mathsf{Cat}_{\mathrm{ms}}\) to \(m\mathsf{Cat}_{\mathrm{ms}}\) is the functor that maps every many-sorted \(n\)-category \(\mathsf{C}\) to its underlying \(m\)-category \(\mathsf{C}^{{\lt}m}\) and every many-sorted \(n\)-functor \(F \colon \mathsf{C} \to \mathsf{D}\) to its underlying \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\). If \(n = m\), then \(\operatorname{\mathcal{U}}_{\mathrm{ms}}^{(n, n)}\) stands for the identity functor on \(n\mathsf{Cat}_{\mathrm{ms}}\).
Functoriality follows from the fact that restricting the family preserves identities and compositions: the identity functor on \(\mathsf{C}\) restricts to the identity functor on \(\mathsf{C}^{{\lt}m}\), and the composition of two \(n\)-functors restricts to the composition of their underlying \(m\)-functors.