pith. sign in

arxiv: 2412.19946 · v2 · pith:W366J6DEnew · submitted 2024-12-27 · 🧮 math.CT · cs.PL· math.LO

Comparing semantic frameworks for dependently-sorted algebraic theories

classification 🧮 math.CT cs.PLmath.LO
keywords categoriesalgebraicbeencategoricalcomprehensionmanymodelmodels
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.