Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

Benedikt Ahrens; Peter Le Fanu Lumsdaine; Paige Randall North

doi:10.1007/978-981-97-8943-6_1

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

Benedikt Ahrens^*
, Peter Le Fanu Lumsdaine
, Paige Randall North

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

Original language	English
Title of host publication	Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings
Editors	Oleg Kiselyov
Publisher	Springer
Pages	3-22
Number of pages	20
ISBN (Electronic)	978-981-97-8943-6
ISBN (Print)	978-981-97-8942-9
DOIs	https://doi.org/10.1007/978-981-97-8943-6_1
Publication status	Published - 2025
Event	22nd Asian Symposium on Programming Languages and Systems, APLAS 2024 - Kyoto, Japan Duration: 22 Oct 2024 → 24 Oct 2024

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	15194 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd Asian Symposium on Programming Languages and Systems, APLAS 2024
Country/Territory	Japan
City	Kyoto
Period	22/10/24 → 24/10/24

Bibliographical note

Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.

Keywords

categorical semantics
dependent types

Access to Document

10.1007/978-981-97-8943-6_1

Cite this

Ahrens, B., Lumsdaine, P. L. F., & North, P. R. (2025). Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. In O. Kiselyov (Ed.), Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings (pp. 3-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15194 LNCS). Springer. https://doi.org/10.1007/978-981-97-8943-6_1

Ahrens, Benedikt ; Lumsdaine, Peter Le Fanu ; North, Paige Randall. / Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings. editor / Oleg Kiselyov. Springer, 2025. pp. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5a47269a189840c185ee5f2a27c1dfbb,

title = "Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories",

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

keywords = "categorical semantics, dependent types",

author = "Benedikt Ahrens and Lumsdaine, \{Peter Le Fanu\} and North, \{Paige Randall\}",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.; 22nd Asian Symposium on Programming Languages and Systems, APLAS 2024 ; Conference date: 22-10-2024 Through 24-10-2024",

year = "2025",

doi = "10.1007/978-981-97-8943-6\_1",

language = "English",

isbn = "978-981-97-8942-9",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--22",

editor = "Oleg Kiselyov",

booktitle = "Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings",

}

Ahrens, B, Lumsdaine, PLF & North, PR 2025, Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. in O Kiselyov (ed.), Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 15194 LNCS, Springer, pp. 3-22, 22nd Asian Symposium on Programming Languages and Systems, APLAS 2024, Kyoto, Japan, 22/10/24. https://doi.org/10.1007/978-981-97-8943-6_1

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. / Ahrens, Benedikt; Lumsdaine, Peter Le Fanu; North, Paige Randall.
Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings. ed. / Oleg Kiselyov. Springer, 2025. p. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15194 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 - 2025

Y1 - 2025

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 - https://www.scopus.com/pages/publications/85209784333

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 -

Ahrens B, Lumsdaine PLF, North PR. Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories. In Kiselyov O, editor, Programming Languages and Systems - 22nd Asian Symposium, APLAS 2024, Proceedings. Springer. 2025. p. 3-22. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2024 Oct 28. doi: 10.1007/978-981-97-8943-6_1