Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Globular weak $ω$-categories as models of a type theory

Thibaut Benjamin, Eric Finster, Samuel Mimram

TL;DR

The paper establishes CaTT, a type-theoretic presentation of weak $oldsymbol{ ightharpoonup ext{ω}}$-categories, and proves that its models correspond precisely to Maltsiniotis’ weak $oldsymbol{ ightharpoonup ext{ω}}$-categories. It achieves this by developing a categorical semantics for type theories via categories with families and contextual categories, then introducing a type theory for globular sets (GSeTT) as a bridge to CaTT. The work connects the syntactic category of GSeTT to the Grothendieck–Maltsiniotis framework through finite globular sets and Kan extension machinery, and extends the syntax to CaTT with coherence operations that capture gluing and lifting needed for higher-cell coherence. A central result is an initiality theorem for CaTT, enabling a nerve-like correspondence between syntactic structures and weak $oldsymbol{ ightharpoonup ext{ω}}$-categories, and yielding an equivalence between Set-models of CaTT and Grothendieck–Maltsiniotis’ weak $oldsymbol{ ightharpoonup ext{ω}}$-categories. Overall, the paper provides a foundation for a nerve theorem in a class of dependent type theories and lays groundwork for further semantic correspondences among different higher-categorical definitions.

Abstract

We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $ω$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $ω$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories

Globular weak $ω$-categories as models of a type theory

TL;DR

The paper establishes CaTT, a type-theoretic presentation of weak -categories, and proves that its models correspond precisely to Maltsiniotis’ weak -categories. It achieves this by developing a categorical semantics for type theories via categories with families and contextual categories, then introducing a type theory for globular sets (GSeTT) as a bridge to CaTT. The work connects the syntactic category of GSeTT to the Grothendieck–Maltsiniotis framework through finite globular sets and Kan extension machinery, and extends the syntax to CaTT with coherence operations that capture gluing and lifting needed for higher-cell coherence. A central result is an initiality theorem for CaTT, enabling a nerve-like correspondence between syntactic structures and weak -categories, and yielding an equivalence between Set-models of CaTT and Grothendieck–Maltsiniotis’ weak -categories. Overall, the paper provides a foundation for a nerve theorem in a class of dependent type theories and lays groundwork for further semantic correspondences among different higher-categorical definitions.

Abstract

We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak -categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak -categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak -groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an -category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories

Paper Structure

This paper contains 16 sections, 4 theorems, 21 equations, 1 figure.

Table of Contents

  1. Categorical semantics of type theory
  2. Categories with families.
  3. Models of a category with families.
  4. Pullbacks in a category with families.
  5. Contextual categories.
  6. A type theory for globular sets
  7. The category of globular sets.
  8. The category of globes.
  9. The $n$-sphere globular set.
  10. Finite globular sets.
  11. The theory $\textnormal{GSeTT}$.
  12. Signature.
  13. Judgments.
  14. Syntactic properties.
  15. Action of substitutions, composition, identity.
  16. ...and 1 more sections

Key Result

Lemma 1

In a category with families $\mathcal{C}$, for every morphism $f:\Delta\to\Gamma$ in $\mathcal{C}$ and $A\in\operatorname{Ty}^\Gamma$, the square \begin{tikzcd} (\Delta,A[f])\ar[d,"\pi'"'] \ar[r,"\sub{f\circ\pi',p'}"]& (\Gamma,A)\ar[d,"\pi"]\\ \Delta \ar[r,"f"'] & \Gamma \end{tikzcd}

Theorems & Definitions (9)

  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • Definition 4
  • Lemma 5
  • proof