5 Many-sorted presentation of higher-order categories
In the many-sorted presentation of higher-order categories, morphisms at each dimension live in separate sets, related by source, target, and identity maps across different dimensions. Composition at each pair of indices is defined as a partial operation on morphisms of the higher dimension, only when appropriate source-target matching conditions are satisfied. In this chapter, we present the basic definitions and axioms of many-sorted categories and many-sorted functors between them, concluding with the definition of the category of many-sorted categories itself.
5.1 Many-sorted categories
We start by defining the necessary data for defining a many-sorted category.
Let \((C_k)_{k \in \mathcal{I}}\) be a family of sets whose elements will be called \(k\)-morphisms. The required data for defining a many-sorted \(\mathcal{I}\)-category structure on \((C_k)_{k \in \mathcal{I}}\) consists of, for each pair of indices \(k, j \in \mathcal{I}\) with \(j {\lt} k\):
A map \(\operatorname{sc}^{(k,j)} \colon C_k \to C_j\), called the \((k,j)\)-source.
A map \(\operatorname{tg}^{(k,j)} \colon C_k \to C_j\), called the \((k,j)\)-target.
A map \(\operatorname{i}^{(k,j)} \colon C_j \to C_k\), called the \((k,j)\)-identity.
A partial binary operation \(\circ ^{(k,j)} \colon C_k \times C_k \rightharpoonup C_k\), called the \((k,j)\)-composition.
The composition \(g \circ ^{(k,j)} f\) is defined if and only if \(\operatorname{sc}^{(k,j)} (g) = \operatorname{tg}^{(k,j)} (f)\), in which case we say that \(g\) and \(f\) are \((k,j)\)-composable.
We will represent the above data as a tuple \(\mathsf{C} = ((C_k)_{k \in \mathcal{I}}, (\operatorname{sc}^{(k,j)}, \operatorname{tg}^{(k,j)}, \operatorname{i}^{(k,j)}, \circ ^{(k,j)})_{k, j \in \mathcal{I}, \, j {\lt} k})\).
We split the axioms of many-sorted categories into two parts: first, those concerning only one pair of indices at a time, and then those concerning the interaction between different pairs. This division is made by first defining the notion of pre-many-sorted category:
A pre-many-sorted \(\mathcal{I}\)-category is a tuple
satisfying, for each pair of indices \(k, j \in \mathcal{I}\) with \(j {\lt} k\), the following axioms:
For all \(f, g \in C_k\), if \(g\) and \(f\) are \((k,j)\)-composable, then
\begin{align*} \operatorname{sc}^{(k,j)} (g \circ ^{(k,j)} f) = \operatorname{sc}^{(k,j)} (f), \qquad & \operatorname{tg}^{(k,j)} (g \circ ^{(k,j)} f) = \operatorname{tg}^{(k,j)} (g). \end{align*}For all \(f \in C_j\),
\[ \operatorname{sc}^{(k,j)} (\operatorname{i}^{(k,j)} (f)) = f, \qquad \operatorname{tg}^{(k,j)} (\operatorname{i}^{(k,j)} (f)) = f. \]For all \(f \in C_k\), the morphisms \(f\) and \(\operatorname{i}^{(k,j)} (\operatorname{sc}^{(k,j)} (f))\) are \((k,j)\)-composable and
\[ f \circ ^{(k,j)} \operatorname{i}^{(k,j)} (\operatorname{sc}^{(k,j)} (f)) = f. \]Similarly, \(\operatorname{i}^{(k,j)} (\operatorname{tg}^{(k,j)} (f))\) and \(f\) are \((k,j)\)-composable and
\[ \operatorname{i}^{(k,j)} (\operatorname{tg}^{(k,j)} (f)) \circ ^{(k,j)} f = f. \]For all \(f, g, h \in C_k\), if \(h\) and \(g\) are \((k,j)\)-composable, and \(g\) and \(f\) are \((k,j)\)-composable, then \(h \circ ^{(k,j)} g\) and \(f\) and \(h\) and \(g \circ ^{(k,j)} f\) are \((k,j)\)-composable, and
\[ (h \circ ^{(k,j)} g) \circ ^{(k,j)} f = h \circ ^{(k,j)} (g \circ ^{(k,j)} f). \]
An immediate consequence of the source/target axioms for identities is that the identity map at each pair of dimensions is injective:
Let \(\mathsf{C}\) be a pre-many-sorted \(\mathcal{I}\)-category and let \(j {\lt} k\) in \(\mathcal{I}\). Then the identity map \(\operatorname{i}^{(k,j)} \colon C_j \to C_k\) is injective.
Let \(f, g \in C_j\) with \(\operatorname{i}^{(k,j)}(f) = \operatorname{i}^{(k,j)}(g)\). Then
where both equalities use Axiom 5.2.2.
We now define a many-sorted category structure by extending the above definition with the axioms concerning the interaction between different pairs of indices:
A many-sorted \(\mathcal{I}\)-category is a pre-many-sorted \(\mathcal{I}\)-category \(\mathsf{C} = ((C_k)_{k \in \mathcal{I}}, (\operatorname{sc}^{(k,j)}, \operatorname{tg}^{(k,j)}, \operatorname{i}^{(k,j)}, \circ ^{(k,j)})_{k, j \in \mathcal{I}, \, j {\lt} k})\) satisfying, in addition to the axioms of pre-many-sorted categories, the following cross-dimensional axioms, for all indices \(k, j, i \in \mathcal{I}\) with \(i {\lt} j {\lt} k\):
For all \(f \in C_k\),
\begin{align*} \operatorname{sc}^{(j,i)} (\operatorname{sc}^{(k,j)} (f)) = \operatorname{sc}^{(k,i)} (f), \qquad & \operatorname{sc}^{(j,i)} (\operatorname{tg}^{(k,j)} (f)) = \operatorname{sc}^{(k,i)} (f), \\ \operatorname{tg}^{(j,i)} (\operatorname{tg}^{(k,j)} (f)) = \operatorname{tg}^{(k,i)} (f), \qquad & \operatorname{tg}^{(j,i)} (\operatorname{sc}^{(k,j)} (f)) = \operatorname{tg}^{(k,i)} (f). \end{align*}For all \(f, g \in C_k\), if \(g\) and \(f\) are \((k,i)\)-composable, then \(\operatorname{sc}^{(k,j)} (g)\) and \(\operatorname{sc}^{(k,j)} (f)\) and \(\operatorname{tg}^{(k,j)} (g)\) and \(\operatorname{tg}^{(k,j)} (f)\) are also \((j,i)\)-composable, and
\begin{align*} \operatorname{sc}^{(k,j)} (g \circ ^{(k,i)} f) = \operatorname{sc}^{(k,j)} (g) \circ ^{(j,i)} \operatorname{sc}^{(k,j)} (f), \\ \operatorname{tg}^{(k,j)} (g \circ ^{(k,i)} f) = \operatorname{tg}^{(k,j)} (g) \circ ^{(j,i)} \operatorname{tg}^{(k,j)} (f). \end{align*}For all \(f \in C_i\),
\[ \operatorname{i}^{(k,j)} (\operatorname{i}^{(j,i)} (f)) = \operatorname{i}^{(k,i)} (f). \]For all \(f, g \in C_j\), if \(g\) and \(f\) are \((j,i)\)-composable, then \(\operatorname{i}^{(k,j)} (g)\) and \(\operatorname{i}^{(k,j)} (f)\) are \((k,i)\)-composable, and
\[ \operatorname{i}^{(k,j)} (g \circ ^{(j,i)} f) = \operatorname{i}^{(k,j)} (g) \circ ^{(k,i)} \operatorname{i}^{(k,j)} (f). \]For all \(f_1, f_2, g_1, g_2 \in C_k\), suppose that:
\(g_2\) and \(g_1\) are \((k,j)\)-composable,
\(f_2\) and \(f_1\) are \((k,j)\)-composable,
\(g_2\) and \(f_2\) are \((k,i)\)-composable, and
\(g_1\) and \(f_1\) are \((k,i)\)-composable.
Then, the morphisms \((g_2 \circ ^{(k,i)} f_2)\) and \((g_1 \circ ^{(k,i)} f_1)\) are \((k,j)\)-composable, and the morphisms \((g_2 \circ ^{(k,j)} g_1)\) and \((f_2 \circ ^{(k,j)} f_1)\) are \((k,i)\)-composable, and
\[ (g_2 \circ ^{(k,i)} f_2) \circ ^{(k,j)} (g_1 \circ ^{(k,i)} f_1) = (g_2 \circ ^{(k,j)} g_1) \circ ^{(k,i)} (f_2 \circ ^{(k,j)} f_1). \]That is, composing first at dimension \(j\) and then at dimension \(i\) yields the same result as composing first at dimension \(i\) and then at dimension \(j\).
Given a natural number \(n \in \mathbb {N}\), a many-sorted \(n\)-category is a many-sorted category indexed by the finite set \(n + 1 = \left\{ 0, 1, \ldots , n \right\} \).
Any pre-many-sorted \(1\)-category is, in fact, a many-sorted \(1\)-category. Since the index set \(1 + 1 = \left\{ 0, 1 \right\} \) has exactly two elements, there are no triples of distinct indices \(i {\lt} j {\lt} k\), so all cross-dimensional axioms are vacuously satisfied.
A many-sorted \(\omega \)-category is a many-sorted category indexed by the set of natural numbers \(\mathbb {N}\).
5.2 Many-sorted functors
In the many-sorted setting, a functor is a family of maps, one for each dimension, that collectively preserve sources, targets, identities, and composition at each pair of dimensions.
Let \(\mathsf{C} = ((C_k)_{k \in \mathcal{I}}, (\operatorname{sc}^{(k,j)}, \operatorname{tg}^{(k,j)}, \operatorname{i}^{(k,j)}, \circ ^{(k,j)})_{k, j \in \mathcal{I}, \, j {\lt} k})\) and \(\mathsf{D} = ((D_k)_{k \in \mathcal{I}}, (\operatorname{sc}^{(k,j)}, \operatorname{tg}^{(k,j)}, \operatorname{i}^{(k,j)}, \circ ^{(k,j)})_{k, j \in \mathcal{I}, \, j {\lt} k})\) be many-sorted \(\mathcal{I}\)-categories. A many-sorted \(\mathcal{I}\)-functor from \(\mathsf{C}\) to \(\mathsf{D}\) is a family of maps \(F = (F_k \colon C_k \to D_k)_{k \in \mathcal{I}}\), written \(F \colon \mathsf{C} \to \mathsf{D}\), satisfying, for each pair of indices \(k, j \in \mathcal{I}\) with \(j {\lt} k\), the following preservation properties:
For all \(f \in C_k\),
\[ F_j (\operatorname{sc}^{(k,j)} (f)) = \operatorname{sc}^{(k,j)} (F_k (f)), \qquad F_j (\operatorname{tg}^{(k,j)} (f)) = \operatorname{tg}^{(k,j)} (F_k (f)). \]For all \(f \in C_j\),
\[ F_k (\operatorname{i}^{(k,j)} (f)) = \operatorname{i}^{(k,j)} (F_j (f)). \]For all \(f, g \in C_k\), if \(g\) and \(f\) are \((k,j)\)-composable, then \(F_k (g)\) and \(F_k (f)\) are also \((k,j)\)-composable, and
\[ F_k (g \circ ^{(k,j)} f) = F_k (g) \circ ^{(k,j)} F_k (f). \]
We can define composition of many-sorted functors componentwise, and the identity many-sorted functor as the family of identity functions.
Let \(\mathsf{C}, \mathsf{D}, \mathsf{E}\) be many-sorted \(\mathcal{I}\)-categories, and let \(F = (F_k)_{k \in \mathcal{I}} \colon \mathsf{C} \to \mathsf{D}\) and \(G = (G_k)_{k \in \mathcal{I}} \colon \mathsf{D} \to \mathsf{E}\) be many-sorted \(\mathcal{I}\)-functors. Then, the family \(G \circ F = (G_k \circ F_k)_{k \in \mathcal{I}} \colon \mathsf{C} \to \mathsf{E}\) is also a many-sorted \(\mathcal{I}\)-functor.
Let \(k, j \in \mathcal{I}\) with \(j {\lt} k\). For all \(f \in C_k\), since \(F\) and \(G\) are many-sorted functors, we have that
and similarly,
that is, \(G \circ F\) preserves sources and targets at pair \((k,j)\).
For all \(f \in C_j\), we have that
so \(G \circ F\) preserves identities at pair \((k,j)\).
Now, let \(f, g \in C_k\) be \((k,j)\)-composable. We have that
so \(G \circ F\) preserves composition at pair \((k,j)\).
Let \(\mathsf{C}\) be a many-sorted \(\mathcal{I}\)-category. Then, the family of identity functions \(\operatorname{id}_{\mathsf{C}} = (\operatorname{id}_{C_k})_{k \in \mathcal{I}}\), written \(\operatorname{id}_{\mathsf{C}} \colon \mathsf{C} \to \mathsf{C}\), is a many-sorted \(\mathcal{I}\)-functor from \(\mathsf{C}\) to itself.
It trivially follows from reflexivity.
Given a natural number \(n \in \mathbb {N}\), a many-sorted \(n\)-functor is a many-sorted functor between many-sorted \(n\)-categories.
A many-sorted \(\omega \)-functor is a many-sorted functor between many-sorted \(\omega \)-categories.
5.3 The category of many-sorted categories
Lastly, we define the category whose objects are many-sorted categories and whose morphisms are many-sorted functors.
The category of many-sorted \(\mathcal{I}\)-categories, denoted by \(\mathcal{I}\mathsf{Cat}_{\mathrm{ms}}\), is defined as follows:
Its objects are many-sorted \(\mathcal{I}\)-categories.
Its morphisms are many-sorted \(\mathcal{I}\)-functors between many-sorted \(\mathcal{I}\)-categories.
Composition of morphisms is given by composition of many-sorted functors.
The identity morphism for each object is given by the identity many-sorted functor.
Given a natural number \(n \in \mathbb {N}\), the category of many-sorted \(n\)-categories, denoted by \(n\mathsf{Cat}_{\mathrm{ms}}\), is the particular case of Definition 5.13 where \(\mathcal{I}\) is the finite set \(n + 1 = \left\{ 0, 1, \ldots , n \right\} \). Its objects are many-sorted \(n\)-categories and its morphisms are many-sorted \(n\)-functors.
This is a particular case of Definition 5.13, so the result follows immediately.
The category of many-sorted \(\omega \)-categories, denoted by \(\omega \mathsf{Cat}_{\mathrm{ms}}\), is the particular case of Definition 5.13 where \(\mathcal{I}\) is the set of natural numbers \(\mathbb {N}\). Its objects are many-sorted \(\omega \)-categories and its morphisms are many-sorted \(\omega \)-functors.
This is a particular case of Definition 5.13, so the result follows immediately.
We extend the notation \(n\mathsf{Cat}_{\mathrm{ms}}\) to all \(n \in \overline{\mathbb {N}}\), understanding that,