English

Comparing semantic frameworks for dependently-sorted algebraic theories

Category Theory 2024-12-31 v1 Programming Languages Logic

Abstract

Algebraic theories with dependency between sorts form the structural core of Martin-L\"of 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.

Keywords

Cite

@article{arxiv.2412.19946,
  title  = {Comparing semantic frameworks for dependently-sorted algebraic theories},
  author = {Benedikt Ahrens and Peter LeFanu Lumsdaine and Paige Randall North},
  journal= {arXiv preprint arXiv:2412.19946},
  year   = {2024}
}

Comments

24 pages. Presented at APLAS 2024; this version lightly revised and expanded, numbering unchanged

R2 v1 2026-06-28T20:50:21.098Z