Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The elementary theory of the 2-category of small categories

Calum Hughes, Adrian Miranda

TL;DR

The paper develops ET2CSC, an elementary theory describing the $2$-category of small categories by axiomatising internal categories, functors, and natural transformations within a setting modeling ETCS. It extends Bourke's internal-category framework to capture the two-dimensional structure, introducing notions such as $2$-well-pointedness, full-subobject classifiers, and a categorified axiom of choice, and showing how generating families and orthogonal factorisations transfer to $ extbf{Cat}( extbf{E})$. The central result is a biequivalence between the 2-category of ETCS models and the 2-category of ET2CSC models, realized via the nerve/discretisation adjunctions and the correspondence between properties in $ extbf{E}$ and in $ extbf{Cat}( extbf{E})$. The work also characterises when $ extbf{Cat}( extbf{E})$ models ET2CSC in terms of ETCS-models for $ extbf{E}$ and establishes a Morita biequivalence between ETCS and ET2CSC, with an eye toward future extensions such as the axiom of replacement and higher categorical generalisations. This provides a purely 2-categorical, first-order framing of the foundational structure of categories and their morphisms, paralleling ETCS for sets.

Abstract

We give an elementary description of $2$-categories $\mathbf{Cat}\left(\mathcal{E}\right)$ of internal categories, functors and natural transformations, where $\mathcal{E}$ is a category modelling Lawvere's elementary theory of the category of sets (ETCS). This extends Bourke's characterisation of $2$-categories $\mathbf{Cat}\left(\mathcal{E}\right)$ where $\mathcal{E}$ has pullbacks to take account for the extra properties in ETCS, and Lawvere's characterisation of the (one dimensional) category of small categories to take account of the two-dimensional structure. Important two-dimensional concepts which we introduce include $2$-well-pointedness, full-subobject classifiers, and the categorified axiom of choice. Along the way, we show how generating families (resp. orthogonal factorisation systems) on $\mathcal{E}$ give rise to generating families (resp. orthogonal factorisation systems) on $\mathbf{Cat}\left(\mathcal{E}\right)_{1}$, results which we believe are of independent interest.

The elementary theory of the 2-category of small categories

TL;DR

The paper develops ET2CSC, an elementary theory describing the -category of small categories by axiomatising internal categories, functors, and natural transformations within a setting modeling ETCS. It extends Bourke's internal-category framework to capture the two-dimensional structure, introducing notions such as -well-pointedness, full-subobject classifiers, and a categorified axiom of choice, and showing how generating families and orthogonal factorisations transfer to . The central result is a biequivalence between the 2-category of ETCS models and the 2-category of ET2CSC models, realized via the nerve/discretisation adjunctions and the correspondence between properties in and in . The work also characterises when models ET2CSC in terms of ETCS-models for and establishes a Morita biequivalence between ETCS and ET2CSC, with an eye toward future extensions such as the axiom of replacement and higher categorical generalisations. This provides a purely 2-categorical, first-order framing of the foundational structure of categories and their morphisms, paralleling ETCS for sets.

Abstract

We give an elementary description of -categories of internal categories, functors and natural transformations, where is a category modelling Lawvere's elementary theory of the category of sets (ETCS). This extends Bourke's characterisation of -categories where has pullbacks to take account for the extra properties in ETCS, and Lawvere's characterisation of the (one dimensional) category of small categories to take account of the two-dimensional structure. Important two-dimensional concepts which we introduce include -well-pointedness, full-subobject classifiers, and the categorified axiom of choice. Along the way, we show how generating families (resp. orthogonal factorisation systems) on give rise to generating families (resp. orthogonal factorisation systems) on , results which we believe are of independent interest.
Paper Structure (23 sections, 33 theorems, 45 equations)

This paper contains 23 sections, 33 theorems, 45 equations.

Table of Contents

  1. Introduction
  2. Outline of main results
  3. Key ideas and techniques
  4. Internal Category Theory and Bourke's characterisation of $\mathbf{Cat(\mathcal{E})}$
  5. Generating families
  6. Adjunctions and full subobject classifiers
  7. Orthogonal factorisations and the categorified axiom of choice
  8. Notation, conventions and background on internal category theory
  9. Internal categories and the $2$-category $\mathbf{Cat(\mathcal{E})}$
  10. Adjunctions between $\mathcal{E}$ and $\mathbf{\mathbf{Cat(\mathcal{E})}}_{1}$
  11. Finite limits and Bourke's characterisation of $\mathbf{Cat(\mathcal{E})}$
  12. Cartesian closedness
  13. Well-pointedness
  14. Natural numbers objects
  15. Subobject classifiers
  16. ...and 8 more sections

Key Result

Proposition 2.8

Consider the functors $(-)_{0}, (-)_{1}: \mathbf{Cat(\mathcal{E})}_{1} \to \mathcal{E}$, which send an internal category to its object of objects and object of arrows respectively.

Theorems & Definitions (108)

  • Definition 1.1
  • Remark 2.2
  • Definition 2.3
  • Remark 2.4
  • Definition 2.5
  • Remark 2.6
  • Remark 2.7
  • Proposition 2.8
  • proof
  • Definition 2.9
  • ...and 98 more