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}_m\) defined on the set of \(m\)-cells of \(\mathsf{C}\), \(C_m\), with the corestriction of the source, target, identity, and composition operations of \(\mathsf{C}\) 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 \(\mathcal{I}\)-categories, \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted functor, and \(m \in \mathcal{I}\). We define the underlying single-sorted \(m\)-functor of \(F\) as the single-sorted \(m\)-functor \(F_m \colon \mathsf{C}_m \to \mathsf{D}_m\) defined as the corestriction 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

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