Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algebraic Presentations of Type Dependency

Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke

TL;DR

The paper proves an equivalence between C-systems and B-systems by introducing unstratified CE- and E-systems and proving a modular chain of adjunctions that restrict to stratified rooted subcategories. It situates C-systems and B-systems within a broader semantic landscape of type-theory models and shows how initial semantics ideas underpin a constructive equivalence without choice. The main technical contributions are (i) the definitions and properties of CE- and E-systems, (ii) the stratification-based characterizations of C- and B-systems, and (iii) the two-step equivalence B-systems ≈ stratified E-systems and CE-systems ≈ stratified E-systems, culminating in an equivalence between C-systems and B-systems. The results provide a modular, constructive bridge between syntactic-like presentations of dependent type theories and their categorical models, with potential connections to categories with families and display-map frameworks. The framework advances the initiality program for type theories by enabling a rigorous, algebraic treatment of contexts and judgments through stratified, essentially algebraic structures.

Abstract

C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky. We construct this equivalence as the restriction of an equivalence between more general structures, called CE-systems and E-systems, respectively. To this end, we identify C-systems and B-systems as "stratified" CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.

Algebraic Presentations of Type Dependency

TL;DR

The paper proves an equivalence between C-systems and B-systems by introducing unstratified CE- and E-systems and proving a modular chain of adjunctions that restrict to stratified rooted subcategories. It situates C-systems and B-systems within a broader semantic landscape of type-theory models and shows how initial semantics ideas underpin a constructive equivalence without choice. The main technical contributions are (i) the definitions and properties of CE- and E-systems, (ii) the stratification-based characterizations of C- and B-systems, and (iii) the two-step equivalence B-systems ≈ stratified E-systems and CE-systems ≈ stratified E-systems, culminating in an equivalence between C-systems and B-systems. The results provide a modular, constructive bridge between syntactic-like presentations of dependent type theories and their categorical models, with potential connections to categories with families and display-map frameworks. The framework advances the initiality program for type theories by enabling a rigorous, algebraic treatment of contexts and judgments through stratified, essentially algebraic structures.

Abstract

C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky's construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky. We construct this equivalence as the restriction of an equivalence between more general structures, called CE-systems and E-systems, respectively. To this end, we identify C-systems and B-systems as "stratified" CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.
Paper Structure (42 sections, 51 theorems, 117 equations)

This paper contains 42 sections, 51 theorems, 117 equations.

Table of Contents

  1. Introduction
  2. Initial Semantics
  3. Voevodsky's approach towards a theory of type theories
  4. Setting the scene
  5. B-systems for the construction of C-systems
  6. Models of Type Theory
  7. Contextual categories and C-systems
  8. B-systems
  9. Other Notions of Model
  10. About the present work
  11. Foundations
  12. About our use of categories
  13. Version history
  14. Acknowledgements
  15. Preliminaries: stratification of categories
  16. ...and 27 more sections

Key Result

Lemma 2.6

Let $\mathcal{C}$ be a category with a terminal object $1$. A function $\ell \colon \mathrm{Ob} {\left(\mathcal{C}\right)} \to \mathbb{N}$ extends to a stratification $L \colon \mathcal{C} \to (\mathbb{N},\geq)$ of $\mathcal{C}$ if and only if the following three conditions hold:

Theorems & Definitions (191)

  • Example 1.1
  • Remark 1.2
  • Definition 2.1: Stratified strict categories, stratified functors
  • Remark 2.2
  • Remark 2.3
  • Definition 2.4
  • Lemma 2.6
  • proof
  • Remark 2.7
  • Proposition 2.8
  • ...and 181 more