Single-sorted presentation of higher-order categories

In the single-sorted presentation of higher-order categories, objects, morphisms, 2-morphisms, and all higher morphisms live in a single set, distinguished by source and target operations at each dimension. Also, composition at each dimension is defined as a partial operation that is only defined when appropriate source-target matching conditions are satisfied. In this chapter, we present the very basic definitions and axioms of single-sorted categories and single-sorted functors between them.

Notation .1

Throughout the text, if not otherwise specified, we will use \(\mathcal{I}\) to denote a set of indices equipped with a linear order relation \({\lt}\).

Single-sorted categories

We start by defining the necessary data for defining a single-sorted category.

Definition .2

HigherCategoryTheory.SingleSorted.CategoryStruct Let \(C\) be a set whose elements will be called morphisms. The required data for defining a single-sorted \(\mathcal{I}\)-category structure on \(C\) consists of:

A unary operation \(\Sc ^i \colon C \to C\) for each index \(i \in \mathcal{I}\), called the source at dimension \(i\).
A unary operation \(\Tg ^i \colon C \to C\) for each index \(i \in \mathcal{I}\), called the target at dimension \(i\).
A partial binary operation \(\Pcomp ^i \colon C \times C \rightharpoonup C\) for each index \(i \in \mathcal{I}\), called the composition at dimension \(i\).

The composition \(g \Pcomp ^i f\) is defined if and only if \(\Sc ^i (g) = \Tg ^i (f)\), in which case we say that \(g\) and \(f\) are composable at dimension \(i\).

We will represent the above data as a tuple \(\mathsf{C} = (C, (\Sc ^i, \Tg ^i, \Pcomp ^i)_{i \in \mathcal{I}})\).

We split the axioms of single-sorted categories into two parts: first, those concerning only one dimension at a time, and then those concerning the interaction between different dimensions. This division is made by first defining the notion of pre-single-sorted category:

Definition .3

def:SingleSortedCategoryStruct HigherCategoryTheory.SingleSorted.PreCategory A pre-single-sorted \(\mathcal{I}\)-category is a tuple \(\mathsf{C} = (C, (\Sc ^i, \Tg ^i, \Pcomp ^i)_{i \in \mathcal{I}})\) satisfying, for each index \(i \in \mathcal{I}\), the following axioms:

For all \(f \in C\),

^i (^i (f)) = ^i (f), ^i (^i (f)) = ^i (f),
^i (^i (f)) = ^i (f), ^i (^i (f)) = ^i (f).
For all \(f, g \in C\), if \(g\) and \(f\) are composable, then

^i (g ^i f) = ^i (f), ^i (g ^i f) = ^i (g).
For all \(f \in C\), the morphisms \(f\) and \(\Sc ^i (f)\) are composable and

\[ f \Pcomp ^i \Sc ^i (f) = f. \]
For all \(f \in C\), the morphisms \(\Tg ^i (f)\) and \(f\) are composable and

\[ \Tg ^i (f) \Pcomp ^i f = f. \]
For all \(f, g, h \in C\), if \(h\) and \(g\) are composable, and \(g\) and \(f\) are composable, then \(h \Pcomp ^i g\) and \(f\) and \(h\) and \(g \Pcomp ^i f\) are composable, and

\[ (h \Pcomp ^i g) \Pcomp ^i f = h \Pcomp ^i (g \Pcomp ^i f). \]

We finally define a single-sorted category structure by extending the above definition with the axioms concerning the interaction between different dimensions:

Definition .4 Single-sorted category

def:PreSingleSortedCategory HigherCategoryTheory.SingleSorted.Category A single-sorted \(\mathcal{I}\)-category is a pre-single-sorted \(\mathcal{I}\)-category \(\mathsf{C} = (C, (\Sc ^i, \Tg ^i, \Pcomp ^i)_{i \in \mathcal{I}})\) satisfying, in addition to the axioms of pre-single-sorted categories, the following cross-dimensional axioms:

For all \(f \in C\) and all indices \(j, k \in \mathcal{I}\) with \(j {\lt} k\),

^k (^j (f)) = ^j (f), ^j (^k (f)) = ^j (f),
^j (^k (f)) = ^j (f), ^k (^j (f)) = ^j (f),
^j (^k (f)) = ^j (f), ^j (^k (f)) = ^j (f).
For all \(f, g \in C\) and all indices \(j, k \in \mathcal{I}\) with \(j {\lt} k\), if \(g\) and \(f\) are composable at dimension \(j\), then \(\Sc ^k (g)\) and \(\Sc ^k (f)\) and \(\Tg ^k (g)\) and \(\Tg ^k (f)\) are also composable at dimension \(j\), and

^k (g ^j f) = ^k (g) ^j ^k (f),
^k (g ^j f) = ^k (g) ^j ^k (f).
For all \(f_1, f_2, g_1, g_2 \in C\) and all indices \(j, k \in \mathcal{I}\) with \(j {\lt} k\), suppose that:
- \(g_2\) and \(f_2\) are composable at dimension \(j\),
- \(g_1\) and \(f_1\) are composable at dimension \(j\),
- \(g_2\) and \(g_1\) are composable at dimension \(k\), and
- \(f_2\) and \(f_1\) are composable at dimension \(k\).
Then, the morphisms \((g_2 \Pcomp ^j f_2)\) and \((g_1 \Pcomp ^j f_1)\) are composable at dimension \(k\), and the morphisms \((g_2 \Pcomp ^k g_1)\) and \((f_2 \Pcomp ^k f_1)\) are composable at dimension \(j\), and

\[ (g_2 \Pcomp ^j f_2) \Pcomp ^k (g_1 \Pcomp ^j f_1) = (g_2 \Pcomp ^k g_1) \Pcomp ^j (f_2 \Pcomp ^k f_1). \]

That is, composing first at dimension \(j\) and then at dimension \(k\) yields the same result as composing first at dimension \(k\) and then at dimension \(j\).

Definition .5 Single-sorted finite category

def:SingleSortedCategory HigherCategoryTheory.SingleSorted.NCategory Given a natural number \(n \in \mathbb {N}\), a single-sorted \(n\)-category is a single-sorted category indexed by the finite set \(n = \left\{ 0, 1, \ldots , n-1 \right\} \).

We now define the notion of cell or identity morphism at a given dimension in a single-sorted category.

Definition .6 Cell

def:SingleSortedCategory HigherCategoryTheory.SingleSorted.cell, HigherCategoryTheory.SingleSorted.cell_sc, HigherCategoryTheory.SingleSorted.cells, HigherCategoryTheory.SingleSorted.cells_sc Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(k \in \mathcal{I}\). We say that a morphism \(f \in C\) is a \(k\)-cell or identity morphism at dimension \(k\) if and only if

\[ \Sc ^k (f) = f. \]

We will denote the set of \(k\)-cells of \(\mathsf{C}\) by \(C_k\).

The above definition defines \(k\)-cells using the source operation, however, it is also possible to define them using the targer operation and, using the axioms of single-sorted categories, one can prove that both definitions are equivalent.

Definition .7 Target-based cell

def:SingleSortedCategory HigherCategoryTheory.SingleSorted.cell_tg, HigherCategoryTheory.SingleSorted.cells_tg Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(k \in \mathcal{I}\). A morphism \(f \in C\) is a target-based \(k\)-cell if and only if

\[ \Tg ^k (f) = f. \]

Theorem .8 Equivalence of cell definitions

def:cell, def:cell_tg HigherCategoryTheory.SingleSorted.cell_sc_iff_cell_tg, HigherCategoryTheory.SingleSorted.cells_sc_eq_cells_tg Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(k \in \mathcal{I}\). A morphism \(f \in C\) is a \(k\)-cell if and only if it is a target-based \(k\)-cell.

It follows that the set of \(k\)-cells \(C_k\) is equal to the set of target-based \(k\)-cells.

▼

Let \(f \in C\). Suppose first that \(f\) is a \(k\)-cell, i.e., \(\Sc ^k (f) = f\). By the axioms of single-sorted categories, we have that

\[ \Tg ^k (f) = \Tg ^k (\Sc ^k (f)) = \Sc ^k (f) = f, \]

so \(f\) is a target-based \(k\)-cell.

Conversely, suppose that \(f\) is a target-based \(k\)-cell, i.e., \(\Tg ^k (f) = f\). By the axioms of single-sorted categories, we have that

\[ \Sc ^k (f) = \Sc ^k (\Tg ^k (f)) = \Tg ^k (f) = f, \]

so \(f\) is a \(k\)-cell.

▼

Definition .9 Single-sorted omega category

def:cell HigherCategoryTheory.SingleSorted.OmegaCategory A single-sorted \(\omega \)-category is a single-sorted category indexed by the set of natural numbers \(\mathbb {N}\), satisfying and additional axiom: for all \(f \in C\), there exists a dimension \(k \in \mathbb {N}\) such that \(f\) is a \(k\)-cell.

Single-sorted functors

Unlike traditional category theory where functors act separately on objects and morphisms, here a single-sorted functor is simply a function on the set of morphisms that preserves sources, targets, and composition at each dimension.

Definition .10 Single-sorted functor

def:SingleSortedCategory HigherCategoryTheory.SingleSorted.Functor Let \(\mathsf{C} = (C, (\Sc ^i, \Tg ^i, \Pcomp ^i)_{i \in \mathcal{I}})\) and \(\mathsf{D} = (D, (\Sc ^i, \Tg ^i, \Pcomp ^i)_{i \in \mathcal{I}})\) be single-sorted \(\mathcal{I}\)-categories. A single-sorted \(\mathcal{I}\)-functor from \(\mathsf{C}\) to \(\mathsf{D}\) is a map \(F \colon C \to D\) satisfying, for each index \(k \in \mathcal{I}\), the following preservation properties:

For all \(f \in C\),

\[ F (\Sc ^k (f)) = \Sc ^k (F (f)), \qquad F (\Tg ^k (f)) = \Tg ^k (F (f)). \]
For all \(f, g \in C\), if \(g\) and \(f\) are composable at dimension \(k\), then \(F (g)\) and \(F (f)\) are also composable at dimension \(k\), and

\[ F (g \Pcomp ^k f) = F (g) \Pcomp ^k F (f). \]

We can define composition of single-sorted functors as the usual composition of functions, and the identity single-sorted functor as the identity function on the set of morphisms. The following results assert that these constructions yield valid single-sorted functors.

Theorem .11 Composition of single-sorted functors

def:SingleSortedFunctor HigherCategoryTheory.SingleSorted.Functor.comp Let \(\mathsf{C}, \mathsf{D}, \mathsf{E}\) be single-sorted \(\mathcal{I}\)-categories, and let \(F \colon \mathsf{C} \to \mathsf{D}\) and \(G \colon \mathsf{D} \to \mathsf{E}\) be single-sorted \(\mathcal{I}\)-functors. Then, the composition \(G \circ F \colon \mathsf{C} \to \mathsf{E}\) is also a single-sorted \(\mathcal{I}\)-functor.

▼

Let \(k \in \mathcal{I}\). For all \(f \in C\), since \(F\) and \(G\) are single-sorted functors, we have that

\[ (G \circ F) (\Sc ^k (f)) = G (F (\Sc ^k (f))) = G (\Sc ^k (F (f))) = \Sc ^k (G (F (f))) = \Sc ^k ((G \circ F) (f)), \]

and similarly,

\[ (G \circ F) (\Tg ^k (f)) = G (F (\Tg ^k (f))) = G (\Tg ^k (F (f))) = \Tg ^k (G (F (f))) = \Tg ^k ((G \circ F) (f)), \]

that is, \(G \circ F\) preserves sources and targets at dimension \(k\).

Now, let \(f, g \in C\) be composable at dimension \(k\). We have that

\[ \begin{split} \end{split} (G \circ F) (g \Pcomp ^k f) & = G (F (g \Pcomp ^k f)) \\ & = G (F (g) \Pcomp ^k F (f)) \\ & = G (F (g)) \Pcomp ^k G (F (f)) \\ & = (G \circ F) (g) \Pcomp ^k (G \circ F) (f), \end{split} \]

so \(G \circ F\) preserves composition at dimension \(k\).

▼

Theorem .12 Identity single-sorted functor

def:SingleSortedFunctor HigherCategoryTheory.SingleSorted.Functor.id Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category. Then, the identity function \(\id _C \colon C \to C\) is a single-sorted \(\mathcal{I}\)-functor from \(\mathsf{C}\) to itself.

▼

It trivially follows from reflexivity.

▼

Definition .13 Single-sorted finite functor

def:SingleSortedNCategory, def:SingleSortedFunctor HigherCategoryTheory.SingleSorted.NFunctor Given a natural number \(n \in \mathbb {N}\), a single-sorted \(n\)-functor is a single-sorted functor between single-sorted \(n\)-categories.

Definition .14 Single-sorted omega functor

def:SingleSortedOmegaCategory, def:SingleSortedFunctor HigherCategoryTheory.SingleSorted.OmegaFunctor A single-sorted \(\omega \)-functor is a single-sorted functor between single-sorted \(\omega \)-categories.

The category of single-sorted categories

Lastly, we define the category whose objects are single-sorted categories and whose morphisms are single-sorted functors.

Definition .15 Category of single-sorted categories

def:SingleSortedCategory, def:SingleSortedFunctor, thm:SingleSortedFunctor_comp, thm:SingleSortedFunctor_id, HigherCategoryTheory.SingleSorted.Cat.category The category of single-sorted \(\mathcal{I}\)-categories, denoted by \(\mathcal{I}\mathsf{Cat}\), is defined as follows:

Its objects are single-sorted \(\mathcal{I}\)-categories.
Its morphisms are single-sorted \(\mathcal{I}\)-functors between single-sorted \(\mathcal{I}\)-categories.
Composition of morphisms is given by composition of single-sorted functors, which is well defined by Theorem .11.
The identity morphism for each object is given by the identity single-sorted functor, which is well defined by Theorem .12.

▼

The required category laws trivially follow from the corresponding properties of function composition.

▼

Notation .16

Since single-sorted \(n\)-categories are just single-sorted \(\mathcal{I}\)-categories where \(\mathcal{I}\) is the finite set \(n\), it follows that we can define the category of single-sorted \(n\)-categories and single-sorted \(n\)-functors between them, denoted by \(n\mathsf{Cat}\).

Definition .17 Category of single-sorted omega categories

def:SingleSortedOmegaCategory, def:SingleSortedOmegaFunctor, thm:SingleSortedFunctor_comp, thm:SingleSortedFunctor_id, HigherCategoryTheory.SingleSorted.OmegaCat.category The category of single-sorted \(\omega \)-categories, denoted by \(\omega \mathsf{Cat}\), is defined analogously to Definition .15, but using single-sorted \(\omega \)-categories and single-sorted \(\omega \)-functors instead.

▼

As in Definition .15, the required category laws trivially follow from the corresponding properties of function composition.

▼