A Formalization of Higher-Order Categories in Lean 4

2 Underlying transformations

In this chapter, for any two naturals \(n\) and \(m\) with \(m {\lt} n\), we provide a way to transform single-sorted \(n\)-categories (or \(\omega \)-categories) into single-sorted \(m\)-categories by forgetting morphisms that are not \(m\)-cells in the original category.

Similarly, we provide a way to transform single-sorted \(n\)-functors (or \(\omega \)-functors) into single-sorted \(m\)-functors by forgetting the action on morphisms that are not \(m\)-cells in the original category.

We conclude the chapter by showing that these transformations are functorial, i.e., they define a functor from \(n\mathsf{Cat}\) (or \(\omega \mathsf{Cat}\)) to \(m\mathsf{Cat}\).

2.1 Underlying single-sorted categories

Lemma 2.1

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f \in \mathsf{C}\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), we have that \(\operatorname{sc}^k (f)\) is a \(m\)-cell in \(\mathsf{C}\).

Proof

Applying one of the axioms of single-sorted categories, we have that

\[ \operatorname{sc}^m (\operatorname{sc}^k f) = \operatorname{sc}^k (f). \]
Lemma 2.2

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f \in \mathsf{C}\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), we have that \(\operatorname{tg}^k (f)\) is a \(m\)-cell in \(\mathsf{C}\).

Proof

Applying one of the axioms of single-sorted categories, we have that

\[ \operatorname{tg}^m (\operatorname{tg}^k f) = \operatorname{tg}^k (f). \]

That is, \(\operatorname{tg}^k (f)\) is a target-based \(m\)-cell in \(\mathsf{C}\). However, we know that every target-based \(m\)-cell is also a \(m\)-cell.

Lemma 2.3

Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f, g \in C_m\) (i.e., \(f\) and \(g\) are \(m\)-cells in \(\mathsf{C}\)) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), if the comoposition \(g \operatorname{\# }^k f\) is defined, then \(g \operatorname{\# }^k f\) is a \(m\)-cell in \(\mathsf{C}\).

Proof

Applying one of the axioms of single-sorted categories and the fact that \(f\) and \(g\) are \(m\)-cells, we have that

\[ \operatorname{sc}^m (g \operatorname{\# }^k f) = \operatorname{sc}^m (g) \operatorname{\# }^k \operatorname{sc}^m (f) = g \operatorname{\# }^k f. \]
Definition 2.4 Underlying single-sorted category

Let \(\mathsf{C}\) be a single-sorted \(n\)-category (or \(\omega \)-category) and \(m\) be a natural number such that \(m {\lt} n\) 1 . We define the underlying single-sorted \(m\)-category of \(\mathsf{C}\) as the single-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) defined on the set of \(m\)-cells of \(\mathsf{C}\), \(C_m\), with the source, target, and composition operations of \(\mathsf{C}\) restricted to \(C_m\).

Note that, by Lemmas 2.1, 2.2, and 2.3, these operations are well-defined. Also, the axioms of single-sorted categories for \(\mathsf{C}_m\) follow directly from the corresponding axioms for \(\mathsf{C}\).

2.2 Underlying single-sorted functors

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(\mathcal{I}\)-categories, \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted functor, and \(m \in \mathcal{I}\). Then, for every \(f \in C_m\) we have that \(F(f) \in D_m\), i.e., the image of \(m\)-cells under a single-sorted functor are \(m\)-cells.

Proof

Applying one of the axioms of single-sorted functors and the fact that \(f\) is a \(m\)-cell, we have that

\[ \operatorname{sc}^m (F(f)) = F(\operatorname{sc}^m (f)) = F(f). \]
Definition 2.6 Underlying single-sorted functor

Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(n\)-categories (or \(\omega \)-categories), \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted \(n\)-functor (or \(\omega \)-functor), and \(m {\lt} n\) 2 . We define the underlying single-sorted \(m\)-functor of \(F\) as the single-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\) defined as the restriction of \(F\) to the sets of \(m\)-cells \(C_m\) and \(D_m\).

Note that, by Lemma 2.5, this function is well-defined. Also, the axioms of single-sorted functors for \(F_m\) follow directly from the corresponding axioms for \(F\).

2.3 Functoriality of the underlying transformations

For any two naturals \(n\) and \(m\) with \(m \leq n\), we first note that the underlying transformations defined in Definitions 2.4 and 2.6 are in fact functorial transformations from \(n\mathsf{Cat}\) to \(m\mathsf{Cat}\).

Definition 2.7 Underlying functor

Let \(n\) and \(m\) be naturals such that \(m \le n\). We define the underlying functor \(\operatorname{\mathcal{U}}^{(n, m)} \colon n\mathsf{Cat}\to m\mathsf{Cat}\) as the functor that maps every single-sorted \(n\)-category \(\mathsf{C}\) to its underlying single-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) (as defined in Definition 2.4) and every single-sorted \(n\)-functor \(F \colon \mathsf{C} \to \mathsf{D}\) to its underlying single-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\) (as defined in Definition 2.6).

  1. If \(\mathsf{C}\) is an \(\omega \)-category, then \(m\) can be any natural number.
  2. If \(F\) is an \(\omega \)-functor, then \(m\) can be any natural number.