TY - GEN
T1 - Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories
AU - Ahrens, Benedikt
AU - Lumsdaine, Peter Le Fanu
AU - North, Paige Randall
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.
PY - 2024/10/28
Y1 - 2024/10/28
N2 - 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.
AB - 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.
KW - categorical semantics
KW - dependent types
UR - http://www.scopus.com/inward/record.url?scp=85209784333&partnerID=8YFLogxK
U2 - 10.1007/978-981-97-8943-6_1
DO - 10.1007/978-981-97-8943-6_1
M3 - Conference contribution
AN - SCOPUS:85209784333
SN - 978-981-97-8942-9
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 22
BT - Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings
A2 - Kiselyov, Oleg
PB - Springer
T2 - 22nd Asian Symposium on Programming Languages and Systems, APLAS 2024
Y2 - 22 October 2024 through 24 October 2024
ER -