PUBLICATIONS MATHÉMATIQUES DE L'IHES

Online first
Article
Martin-Löf identity types in C-systems
Publications Mathématiques de l'IHÉS, Volume 138 (2023), pp. 1-67
PDF

This paper continues a series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Löf type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper play a crucial role in the construction of the univalent model of type theory in simplicial sets.

Published online:
DOI: 10.1007/s10240-023-00138-2 
@article{PMIHES_2023__138__1_0,
     author = {Vladimir Voevodsky},
     title = {Martin-L\"of identity types in {C-systems}},
     journal = {Publications Math\'ematiques de l'IH\'ES},
     pages = {1--67},
     year = {2023},
     publisher = {Springer International Publishing},
     address = {Cham},
     volume = {138},
     doi = {10.1007/s10240-023-00138-2},
     mrnumber = {4666930},
     zbl = {07780365},
     language = {en},
     url = {https://pmihes.centre-mersenne.org/articles/10.1007/s10240-023-00138-2/}
}
TY  - JOUR
AU  - Vladimir Voevodsky
TI  - Martin-Löf identity types in C-systems
JO  - Publications Mathématiques de l'IHÉS
PY  - 2023
SP  - 1
EP  - 67
VL  - 138
PB  - Springer International Publishing
PP  - Cham
UR  - https://pmihes.centre-mersenne.org/articles/10.1007/s10240-023-00138-2/
DO  - 10.1007/s10240-023-00138-2
LA  - en
ID  - PMIHES_2023__138__1_0
ER  - 
%0 Journal Article
%A Vladimir Voevodsky
%T Martin-Löf identity types in C-systems
%J Publications Mathématiques de l'IHÉS
%D 2023
%P 1-67
%V 138
%I Springer International Publishing
%C Cham
%U https://pmihes.centre-mersenne.org/articles/10.1007/s10240-023-00138-2/
%R 10.1007/s10240-023-00138-2
%G en
%F PMIHES_2023__138__1_0
Vladimir Voevodsky. Martin-Löf identity types in C-systems. Publications Mathématiques de l'IHÉS, Volume 138 (2023), pp. 1-67. doi: 10.1007/s10240-023-00138-2

[1.] S. Awodey; M. A. Warren Homotopy theoretic models of identity types, Math. Proc. Camb. Philos. Soc., Volume 146 (2009), pp. 45-55 | MR | DOI | Zbl

[2.] M. Bezem; T. Coquand; S. Huber A model of type theory in cubical sets, 19th International Conference on Types for Proofs and Programs, Volume 26 (2013), pp. 107-128 (Schloss Dagstuhl – Leibniz-Zentrum für Informatik) | MR | Zbl

[3.] J. Cartmell, Generalised algebraic theories and contextual categories, Ph.D. Thesis, Oxford University, 1978. See http://www.cs.ru.nl/~spitters/Cartmell.pdf.

[4.] J. Cartmell Generalised algebraic theories and contextual categories, Ann. Pure Appl. Log., Volume 32 (1986), pp. 209-243 | MR | DOI | Zbl

[5.] P. Dybjer Internal type theory, Types for Proofs and Programs, Volume 1158 (1996), pp. 120-134 | DOI | MR | Zbl

[6.] N. Gambino; R. Garner The identity type weak factorisation system, Theor. Comput. Sci., Volume 409 (2008), pp. 94-109 | MR | DOI | Zbl

[7.] M. Hofmann; T. Streicher The groupoid interpretation of type theory, Twenty-Five Years of Constructive Type Theory, Volume 36 (1998), pp. 83-111 | Zbl | MR

[8.] B. Jacobs Categorical Logic and Type Theory, 141, North-Holland, Amsterdam, 1999 | Zbl | MR

[9.] P. Martin-Löf An intuitionistic theory of types: predicative part, Logic Colloquium ’73, Volume 80 (1975), pp. 73-118 | MR | Zbl

[10.] P. Martin-Löf Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science, VI, Volume 104 (1982), pp. 153-175 | MR | Zbl

[11.] T. Streicher Semantics of Type Theory, Birkhäuser, Boston, 1991 (Correctness, completeness and independence results, with a foreword by Martin Wirsing) | Zbl | MR | DOI

[12.] B. van den Berg; R. Garner Types are weak ω-groupoids, Proc. Lond. Math. Soc. (3), Volume 102 (2011), pp. 370-394 | MR | DOI | Zbl

[13.] B. van den Berg; R. Garner Topological and simplicial models of identity types, ACM Trans. Comput. Log., Volume 13 (2012) | MR | Zbl | DOI

[14.] V. Voevodsky, The equivalence axiom and univalent models of type theory, February 4, 2010. See | arXiv

[15.] V. Voevodsky Simplicial radditive functors, J. K-Theory, Volume 5 (2010), pp. 201-244 | MR | DOI | Zbl

[16.] V. Voevodsky, C -system of a module over a monad on sets, pp. 1–20, 2014. See https://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#1407.3394. | arXiv

[17.] V. Voevodsky A C-system defined by a universe category, Theory Appl. Categ., Volume 30 (2015), pp. 1181-1215 (http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf) | MR | Zbl

[18.] V. Voevodsky, Products of families of types in the C-systems defined by a universe category, pp. 1–30, 2015. https://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#1503.07072. | arXiv | MR

[19.] V. Voevodsky Products of families of types and (Π,λ)-structures on C-systems, Theory Appl. Categ., Volume 31 (2016), pp. 1044-1094 (See http://www.tac.mta.ca/tac/volumes/31/36/31-36.pdf. Preprint: http://arxiv.org/abs/1503.07072) | MR | Zbl

[20.] V. Voevodsky Subsystems and regular quotients of C-systems, A Panorama of Mathematics: Pure and Applied, 658, Am. Math. Soc., Providence, 2016, pp. 127-137 (Preprint: http://arxiv.org/abs/1406.7413) | Zbl | MR

[21.] V. Voevodsky C-systems defined by universe categories: presheaves, Theory Appl. Categ., Volume 32 (2017), pp. 53-112 (See http://www.tac.mta.ca/tac/volumes/32/3/32-03.pdf) | MR | Zbl

[22.] V. Voevodsky The (Π,λ)-structures on the C-systems defined by universe categories, Theory Appl. Categ., Volume 32 (2017), pp. 113-121 (http://www.tac.mta.ca/tac/volumes/32/4/32-04.pdf) | MR | Zbl

[23.] M. Warren, Homotopy models of intensional type theory, 2006. See http://mawarren.net/papers/prospectus.pdf.

[24.] M. Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis, Carnegie Mellon University, 2008. See http://mawarren.net/papers/phd.pdf.

[25.] M. A. Warren The strict ω-groupoid interpretation of type theory, Models, Logics, and Higher-Dimensional Categories, 53, Am. Math. Soc., Providence, 2011, pp. 291-340 | DOI | MR | Zbl

Cited by Sources: