Many-sorted presentation of higher-order categories
In the many-sorted presentation of higher-order categories, morphisms at each dimension live in separate sets, connected by source, target, and identity maps between adjacent dimensions. Composition at each dimension is defined as a partial operation on morphisms of the same dimension, subject to appropriate source-target matching conditions. In this chapter, we present the basic definitions and axioms of many-sorted categories and many-sorted functors between them.
As in Chapter ??, we will use \(\mathcal{I}\) to denote a set of indices equipped with a linear order relation \({\lt}\).
Many-sorted categories
We start by defining the necessary data for defining a many-sorted category.
HigherCategoryTheory.ManySorted.CategoryStruct 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 \(j, k \in \mathcal{I}\):
A map \(\Sc ^{(k,j)} \colon C_k \to C_j\), called the \((k,j)\)-source.
A map \(\Tg ^{(k,j)} \colon C_k \to C_j\), called the \((k,j)\)-target.
A map \(\Idm ^{(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 \(\Sc ^{(k,j)} (g) = \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}}, (\Sc ^{(k,j)}, \Tg ^{(k,j)}, \Idm ^{(k,j)}, \circ ^{(k,j)})_{j, k \in \mathcal{I}})\).
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:
HigherCategoryTheory.ManySorted.PreCategory def:ManySortedCategoryStruct A pre-many-sorted \(\mathcal{I}\)-category is a tuple \(\mathsf{C} = ((C_k)_{k \in \mathcal{I}}, (\Sc ^{(k,j)}, \Tg ^{(k,j)}, \Idm ^{(k,j)}, \circ ^{(k,j)})_{j, k \in \mathcal{I}, \, j {\lt} k})\) satisfying, for each pair of indices \(j, k \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
^(k,j) (g ○^(k,j) f) = ^(k,j) (f), ^(k,j) (g ○^(k,j) f) = ^(k,j) (g).For all \(f \in C_j\),
\[ \Sc ^{(k,j)} (\Idm ^{(k,j)} (f)) = f, \qquad \Tg ^{(k,j)} (\Idm ^{(k,j)} (f)) = f. \]For all \(f \in C_k\), the morphisms \(f\) and \(\Idm ^{(k,j)} (\Sc ^{(k,j)} (f))\) are \((k,j)\)-composable and
\[ f \circ ^{(k,j)} \Idm ^{(k,j)} (\Sc ^{(k,j)} (f)) = f. \]Similarly, \(\Idm ^{(k,j)} (\Tg ^{(k,j)} (f))\) and \(f\) are \((k,j)\)-composable and
\[ \Idm ^{(k,j)} (\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). \]
That is, for each pair of indices \(j, k \in \mathcal{I}\) with \(j {\lt} k\), the data \((C_j, C_k, \Sc ^{(k,j)}, \Tg ^{(k,j)}, \Idm ^{(k,j)}, \circ ^{(k,j)})\) forms a category with objects \(C_j\) and morphisms \(C_k\).
An immediate consequence of the source/target axioms for identities is that the identity map at each pair of dimensions is injective:
HigherCategoryTheory.ManySorted.PreCategory.injetive_idm def:PreManySortedCategory Let \(\mathsf{C}\) be a pre-many-sorted \(\mathcal{I}\)-category and let \(j {\lt} k\) in \(\mathcal{I}\). Then the identity map \(\Idm ^{(k,j)} \colon C_j \to C_k\) is injective.
where both equalities use the axiom \(\Sc ^{(k,j)}(\Idm ^{(k,j)}(f)) = f\).
We now define a many-sorted category structure by extending the above definition with the axioms concerning the interaction between different pairs of indices:
HigherCategoryTheory.ManySorted.Category def:PreManySortedCategory A many-sorted \(\mathcal{I}\)-category is a pre-many-sorted \(\mathcal{I}\)-category \(\mathsf{C} = ((C_k)_{k \in \mathcal{I}}, (\Sc ^{(k,j)}, \Tg ^{(k,j)}, \Idm ^{(k,j)}, \circ ^{(k,j)})_{j, k \in \mathcal{I}, \, j {\lt} k})\) satisfying, in addition to the axioms of pre-many-sorted categories, the following cross-dimensional axioms:
For all \(f \in C_k\) and all indices \(i, j, k \in \mathcal{I}\) with \(i {\lt} j {\lt} k\),
^(j,i) (^(k,j) (f)) = ^(k,i) (f), ^(j,i) (^(k,j) (f)) = ^(k,i) (f),
^(j,i) (^(k,j) (f)) = ^(k,i) (f), ^(j,i) (^(k,j) (f)) = ^(k,i) (f).For all \(f, g \in C_k\) and all indices \(i, j, k \in \mathcal{I}\) with \(i {\lt} j {\lt} k\), if \(g\) and \(f\) are \((k,i)\)-composable, then \(\Sc ^{(k,j)} (g)\) and \(\Sc ^{(k,j)} (f)\) and \(\Tg ^{(k,j)} (g)\) and \(\Tg ^{(k,j)} (f)\) are also \((j,i)\)-composable, and
^(k,j) (g ○^(k,i) f) = ^(k,j) (g) ○^(j,i) ^(k,j) (f),
^(k,j) (g ○^(k,i) f) = ^(k,j) (g) ○^(j,i) ^(k,j) (f).For all \(f \in C_i\) and all indices \(i, j, k \in \mathcal{I}\) with \(i {\lt} j {\lt} k\),
\[ \Idm ^{(k,j)} (\Idm ^{(j,i)} (f)) = \Idm ^{(k,i)} (f). \]For all \(f, g \in C_j\) and all indices \(i, j, k \in \mathcal{I}\) with \(i {\lt} j {\lt} k\), if \(g\) and \(f\) are \((j,i)\)-composable, then \(\Idm ^{(k,j)} (g)\) and \(\Idm ^{(k,j)} (f)\) are \((k,i)\)-composable, and
\[ \Idm ^{(k,j)} (g \circ ^{(j,i)} f) = \Idm ^{(k,j)} (g) \circ ^{(k,i)} \Idm ^{(k,j)} (f). \]For all \(f_1, f_2, g_1, g_2 \in C_k\) and all indices \(i, j, k \in \mathcal{I}\) with \(i {\lt} j {\lt} 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\).
HigherCategoryTheory.ManySorted.NCategory def:ManySortedCategory 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\} \).
HigherCategoryTheory.ManySorted.OmegaCategory def:ManySortedCategory A many-sorted \(\omega \)-category is a many-sorted category indexed by the set of natural numbers \(\mathbb {N}\).
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.
def:ManySortedCategory HigherCategoryTheory.ManySorted.Functor Let \(\mathsf{C} = ((C_k)_{k \in \mathcal{I}}, (\Sc ^{(k,j)}, \Tg ^{(k,j)}, \Idm ^{(k,j)}, \circ ^{(k,j)})_{j, k \in \mathcal{I}, \, j {\lt} k})\) and \(\mathsf{D} = ((D_k)_{k \in \mathcal{I}}, (\Sc ^{(k,j)}, \Tg ^{(k,j)}, \Idm ^{(k,j)}, \circ ^{(k,j)})_{j, k \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_k \colon C_k \to D_k)_{k \in \mathcal{I}}\) satisfying, for each pair of indices \(j, k \in \mathcal{I}\) with \(j {\lt} k\), the following preservation properties:
For all \(f \in C_k\),
\[ F_j (\Sc ^{(k,j)} (f)) = \Sc ^{(k,j)} (F_k (f)), \qquad F_j (\Tg ^{(k,j)} (f)) = \Tg ^{(k,j)} (F_k (f)). \]For all \(f \in C_j\),
\[ F_k (\Idm ^{(k,j)} (f)) = \Idm ^{(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. The following results assert that these constructions yield valid many-sorted functors.
def:ManySortedFunctor HigherCategoryTheory.ManySorted.Functor.comp Let \(\mathsf{C}, \mathsf{D}, \mathsf{E}\) be many-sorted \(\mathcal{I}\)-categories, and let \((F_k)_{k \in \mathcal{I}} \colon \mathsf{C} \to \mathsf{D}\) and \((G_k)_{k \in \mathcal{I}} \colon \mathsf{D} \to \mathsf{E}\) be many-sorted \(\mathcal{I}\)-functors. Then, the family \((G_k \circ F_k)_{k \in \mathcal{I}} \colon \mathsf{C} \to \mathsf{E}\) is also a many-sorted \(\mathcal{I}\)-functor.
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)\).
def:ManySortedFunctor HigherCategoryTheory.ManySorted.Functor.id Let \(\mathsf{C}\) be a many-sorted \(\mathcal{I}\)-category. Then, the family of identity functions \((\id _{C_k})_{k \in \mathcal{I}}\) is a many-sorted \(\mathcal{I}\)-functor from \(\mathsf{C}\) to itself.
def:ManySortedNCategory, def:ManySortedFunctor HigherCategoryTheory.ManySorted.NFunctor Given a natural number \(n \in \mathbb {N}\), a many-sorted \(n\)-functor is a many-sorted functor between many-sorted \(n\)-categories.
def:ManySortedOmegaCategory, def:ManySortedFunctor HigherCategoryTheory.ManySorted.OmegaFunctor A many-sorted \(\omega \)-functor is a many-sorted functor between many-sorted \(\omega \)-categories.
The category of many-sorted categories
Lastly, we define the category whose objects are many-sorted categories and whose morphisms are many-sorted functors.
HigherCategoryTheory.ManySorted.Cat.category def:ManySortedCategory, def:ManySortedFunctor, thm:ManySortedFunctor_comp, thm:ManySortedFunctor_id, 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, which is well defined by Theorem .9.
The identity morphism for each object is given by the identity many-sorted functor, which is well defined by Theorem .10.
Since many-sorted \(n\)-categories are just many-sorted \(\mathcal{I}\)-categories where \(\mathcal{I}\) is the finite set \(n + 1 = \left\{ 0, 1, \ldots , n \right\} \), it follows that we can define the category of many-sorted \(n\)-categories and many-sorted \(n\)-functors between them, denoted by \(n\mathsf{Cat}_{\mathrm{ms}}\).
HigherCategoryTheory.ManySorted.OmegaCat.category def:ManySortedOmegaCategory, def:ManySortedOmegaFunctor, thm:ManySortedFunctor_comp, thm:ManySortedFunctor_id, The category of many-sorted \(\omega \)-categories, denoted by \(\omega \mathsf{Cat}_{\mathrm{ms}}\), is defined analogously to Definition .13, but using many-sorted \(\omega \)-categories and many-sorted \(\omega \)-functors instead.