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.
@article{PMIHES_2023__138__1_0,
author = {Voevodsky, Vladimir},
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://www.numdam.org/articles/10.1007/s10240-023-00138-2/}
}
TY - JOUR AU - Voevodsky, Vladimir 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://www.numdam.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 Voevodsky, Vladimir %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://www.numdam.org/articles/10.1007/s10240-023-00138-2/ %R 10.1007/s10240-023-00138-2 %G en %F PMIHES_2023__138__1_0
Voevodsky, Vladimir. Martin-Löf identity types in C-systems. Publications Mathématiques de l'IHÉS, Tome 138 (2023), pp. 1-67. doi: 10.1007/s10240-023-00138-2
[1.] Homotopy theoretic models of identity types, Math. Proc. Camb. Philos. Soc., Volume 146 (2009), pp. 45-55 | MR | DOI | Zbl
[2.] 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.] Generalised algebraic theories and contextual categories, Ann. Pure Appl. Log., Volume 32 (1986), pp. 209-243 | MR | DOI | Zbl
[5.] Internal type theory, Types for Proofs and Programs, Volume 1158 (1996), pp. 120-134 | DOI | MR | Zbl
[6.] The identity type weak factorisation system, Theor. Comput. Sci., Volume 409 (2008), pp. 94-109 | MR | DOI | Zbl
[7.] The groupoid interpretation of type theory, Twenty-Five Years of Constructive Type Theory, Volume 36 (1998), pp. 83-111 | Zbl | MR
[8.] Categorical Logic and Type Theory, 141, North-Holland, Amsterdam, 1999 | Zbl | MR
[9.] An intuitionistic theory of types: predicative part, Logic Colloquium ’73, Volume 80 (1975), pp. 73-118 | MR | Zbl
[10.] Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science, VI, Volume 104 (1982), pp. 153-175 | MR | Zbl
[11.] Semantics of Type Theory, Birkhäuser, Boston, 1991 (Correctness, completeness and independence results, with a foreword by Martin Wirsing) | Zbl | MR | DOI
[12.] Types are weak -groupoids, Proc. Lond. Math. Soc. (3), Volume 102 (2011), pp. 370-394 | MR | DOI | Zbl
[13.] 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.] Simplicial radditive functors, J. K-Theory, Volume 5 (2010), pp. 201-244 | MR | DOI | Zbl
[16.] V. Voevodsky, -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.] 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.] 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.] 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.] 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.] 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.] 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
Cité par Sources :
