The biequivalence of path categories and axiomatic Martin-Löf type theories
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918361935380480 |
|---|---|
| author | Otten, Daniël Spadetto, Matteo |
| author_facet | Otten, Daniël Spadetto, Matteo |
| contents | The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categories, while adding Pi-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 1- and Sigma-types are biequivalent to certain path categories, while adding axiomatic Pi-types yields dependent homotopy exponents.
This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 1-, Sigma-, and Pi-types. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_15431 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The biequivalence of path categories and axiomatic Martin-Löf type theories Otten, Daniël Spadetto, Matteo Logic Logic in Computer Science Algebraic Topology Category Theory 03F50, 03G30, 18C10, 03B38, 03B70, 18N45, 18D30, 55U35, 55U40 F.4.1 The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categories, while adding Pi-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 1- and Sigma-types are biequivalent to certain path categories, while adding axiomatic Pi-types yields dependent homotopy exponents. This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 1-, Sigma-, and Pi-types. |
| title | The biequivalence of path categories and axiomatic Martin-Löf type theories |
| topic | Logic Logic in Computer Science Algebraic Topology Category Theory 03F50, 03G30, 18C10, 03B38, 03B70, 18N45, 18D30, 55U35, 55U40 F.4.1 |
| url | https://arxiv.org/abs/2503.15431 |