Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Comparing semantic frameworks for dependently-sorted algebraic theories

Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North

TL;DR

The paper addresses the problem of comparing semantic frameworks for dependently-sorted algebraic theories by using comprehension categories as a unifying 2-categorical language. It systematically embeds existing frameworks where types are either maps (display maps) or primitive (CwA, CwF, contextual categories) into the 2-category $\mathbf{CompCat}$, and establishes a network of adjunctions and equivalences that relate these models. Key contributions include precise 2-categorical embeddings of display-map based structures (including structured and rooted variants) as well as a suite of equivalences between primitive-type frameworks and discrete/comprehension-category formulations. The resulting picture provides a cohesive, high-level map of how diverse models interrelate, enabling cross-transfer of results and a unified viewpoint on the semantics of dependent type theories.

Abstract

Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take *comprehension categories* as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.

Comparing semantic frameworks for dependently-sorted algebraic theories

TL;DR

The paper addresses the problem of comparing semantic frameworks for dependently-sorted algebraic theories by using comprehension categories as a unifying 2-categorical language. It systematically embeds existing frameworks where types are either maps (display maps) or primitive (CwA, CwF, contextual categories) into the 2-category , and establishes a network of adjunctions and equivalences that relate these models. Key contributions include precise 2-categorical embeddings of display-map based structures (including structured and rooted variants) as well as a suite of equivalences between primitive-type frameworks and discrete/comprehension-category formulations. The resulting picture provides a cohesive, high-level map of how diverse models interrelate, enabling cross-transfer of results and a unified viewpoint on the semantics of dependent type theories.

Abstract

Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take *comprehension categories* as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.
Paper Structure (13 sections, 18 theorems, 9 equations, 5 figures)

This paper contains 13 sections, 18 theorems, 9 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Comprehension categories: a broad church
  3. 2-categories of comprehension categories
  4. Frameworks with types as certain maps
  5. Display map categories
  6. Structured display map categories
  7. Rooted display map categories
  8. Clans
  9. Finite-limit categories
  10. Frameworks with types as primitive
  11. Categories with families, and equivalents
  12. Contextual categories, and equivalents
  13. Conclusion

Key Result

Lemma 14

Any display map category $(\mathcal{C}, \mathcal{D})$ gives a comprehension category $(\mathcal{C},\mathcal{D},\operatorname{cod} \circ \iota,\iota)$ where $\iota : \mathcal{D} \mathrel{\mkern-1mu \begin{tikzpicture}[baseline={([yshift=-0.55ex]a.south)}]{ \node[minimum width=1.5em,align=center,

Figures (5)

  • Figure 1: Models with types as display maps (\ref{['sec:types-as-maps']})
  • Figure 2: Models with types as primitive (\ref{['sec:types-as-primitive']})
  • Figure 3: Notions with types as maps, unrooted
  • Figure 4: Notions with types as maps, rooted
  • Figure 5: Notions with types primitive

Theorems & Definitions (62)

  • Definition 1
  • Definition 2
  • Remark 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Remark
  • Remark \ref{def:conditions-on-compcats}a
  • Definition 8
  • ...and 52 more