Comparing semantic frameworks for dependently-sorted algebraic theories

Autor:	Ahrens, Benedikt, Lumsdaine, Peter LeFanu, North, Paige Randall
Rok vydání:	2024
Předmět:	Mathematics - Category Theory Computer Science - Programming Languages Mathematics - Logic 18C50 Categorical semantics of formal languages (primary) 03G30 Categorical logic and topoi 03B15 Higher-order logic and type theory
Zdroj:	Programming Languages and Systems (Proc. APLAS 2024), Oleg Kiselyov (ed.), 2025, Springer Nature Singapore, pp. 3-22
Druh dokumentu:	Working Paper
DOI:	10.1007/978-981-97-8943-6_1
Popis:	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. Comment: 24 pages. Presented at APLAS 2024; this version lightly revised and expanded, numbering unchanged
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2412.19946 Zobrazit plný text záznamu View this record from Arxiv