The simplicial model of univalent foundations (after Voevodsky). (English) Zbl 1471.18025

Kapulkin, Krzysztof; Lumsdaine, Peter Lefanu

J. Eur. Math. Soc. (JEMS) 23, No. 6, 2071-2126 (2021).

The Univalent Foundations program is a new proposed approach to foundations of mathematics, originally suggested in [https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf], building on the systems of dependent type theory developed by P. Martin-Löf [Intuitionistic type theory. Notes by Giovanni Sambin of a Series of Lectures given in Padua, June 1980. Napoli: Bibliopolis (1984; Zbl 0571.03030)] and others. In dependent type theory, equality can carry information. One can not ask whether elements of a type are equal on the nose in the classical sense. The Univalent Axiom introduced by Voevodsky strengthens this characteristics. The Univalent Axiom claims that equality between types, as elements of a universe, is the same as equivalence between them, as types, formalizing the practice of treating equivalent structures as completely interchangeable. It soiidifies the idea of types as some kind of spaces in the homotopy-theoretic sense.
The principal objective in this paper is to justify the idea of types as spaces, constructing a model of type theory in the Quillen model category of simplicial sets in which the Univalent Axiom obtains. The fibrations called Kan fibrations serve as an interpretation of type dependency, Kan complexes standing for closed types.
A synopsis of the paper goes as follows.

●

§1 is concerned with general techniques for constructing models of type theory. §1.1 sets out the specific type theory that this paper considers, while §1.2 reviews some fundamental facts concerning its intended semantics in contextual categories after [T. Streicher, Semantics of type theory. Correctness, completeness and independence results. With a foreword by Martin Wirsing. Basel: Birkhäuser Verlag (1991; Zbl 0790.68068)]. §1.3 makes use of universes to construct contextual categories representing the structural core of type theory, while §1.4 exploits categorical constructions on the universe to model the logical constructions of type theory, which presents a new solution to the coherence problem for modeling type theory [M. Hofmann, Lect. Notes Comput. Sci. 933, 427–441 (1995; Zbl 1044.03544)].

●

§2 aims at constructing a model in the category of simplicial sets. §2.1 and §2.2 are dedicated to the construction and investigation of a weakly universal Kan fibration (a universe of Kan complexes), which is exploited to apply the techniques in §1, giving a model of the full type theory in simplicial sets.

●

§3 is concerned wtih the univalence axiom. §3.1 formulates univalence in type theory, while it is formulated in terms of homotopy theory in §3.2. It is shown in §3.3 that these definitions correspond under the simplicial model. §3.4 demonstrates that the universal Kan fibration is univalent, the univalence axiom holding in the simplicial model. §3.5 discusses an alternative formulation of univalence, shedding further light on the universal property of the universe.

●

The paper contains two appendices, setting out in full the type theory under consideration. Appendix A is devoted to a conventional syntactic presentation, while Appendix B deals with its translation into algebraic structure on contextual categories.

Reviewer: Hirokazu Nishimura (Tsukuba)

MSC:

18N45	Categories of fibrations, relations to \(K\)-theory, relations to type theory
18C50	Categorical semantics of formal languages
55U10	Simplicial sets and complexes in algebraic topology
55U35	Abstract and axiomatic homotopy theory in algebraic topology

Keywords:

univalent foundations; simplicial sets; dependent type theory; contextual categories; univalence

Citations:

Zbl 0571.03030; Zbl 0790.68068; Zbl 1044.03544

References:

[1]	Ad´amek, J., Rosick´y, J.: Locally Presentable and Accessible Categories. London Math. Soc. Lecture Note Ser. 189, Cambridge Univ. Press, Cambridge (1994) Zbl 0795.18007 MR 1294136
[2]	Arndt, P., Kapulkin, K.: Homotopy-theoretic models of type theory. In: Typed Lambda Calculi and Applications, Lecture Notes in Computer Sci. 6690, Springer, Heidelberg, 45-60 (2011)Zbl 1331.03044 MR 2830786 · Zbl 1331.03044
[3]	Awodey, S., Warren, M. A.: Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc.146, 45-55 (2009)Zbl 1205.03065 MR 2461866 · Zbl 1205.03065
[4]	Barras, B.: Semantical investigations in intuitionistic set theory and type theories with inductive families. Habilitation, Univ. Paris 7 (Denis Diderot) (2012)
[5]	Barratt, M. G., Gugenheim, V. K. A. M., Moore, J. C.: On semisimplicial fibrebundles. Amer. J. Math.81, 639-657 (1959)Zbl 0127.39002 MR 0111028 · Zbl 0127.39002
[6]	Cartmell, J.: Generalised algebraic theories and contextual categories. Ph.D. thesis, Oxford (1978) · Zbl 0634.18003
[7]	Dybjer, P.: Internal type theory. In: Types for Proofs and Programs (Torino, 1995), Lecture Notes in Computer Sci. 1158, Springer, Berlin, 120-134 (1996) Zbl 1434.03149 MR 1474535 · Zbl 1434.03149
[8]	Gambino, N., Garner, R.: The identity type weak factorisation system. Theoret. Computer Sci.409, 94-109 (2008)Zbl 1157.68022 MR 2469279 · Zbl 1157.68022
[9]	Gambino, N., Hyland, M.: Wellfounded trees and dependent polynomial functors. In: Types for Proofs and Programs, Lecture Notes in Computer Sci. 3085, Springer, Berlin, 210-225 (2004)Zbl 1100.03055 MR 2151336 · Zbl 1100.03055
[10]	Garner, R.: On the strength of dependent products in the type theory of Martin-L¨of. Ann. Pure Appl. Logic160, 1-12 (2009)Zbl 1171.03004 MR 2525970 · Zbl 1171.03004
[11]	Garner, R., van den Berg, B.: Types are weakω-groupoids. Proc. London Math. Soc. (3)102, 370-394 (2011)Zbl 1229.18007 MR 2769118 · Zbl 1229.18007
[12]	Gepner, D., Kock, J.: Univalence in locally cartesian closed∞-categories. Forum Math.29, 617-652 (2017)Zbl 1376.55018 MR 3641669 · Zbl 1376.55018
[13]	Goerss, P. G., Jardine, J. F.: Simplicial Homotopy Theory. Modern Birkh¨auser Classics, Birkh¨auser (2009)Zbl 1195.55001 MR 2840650
[14]	Gonthier, G.: Formal proof—the four-color theorem. Notices Amer. Math. Soc.55, 1382-1393 (2008)Zbl 1195.05026 MR 2463991 · Zbl 1195.05026
[15]	Grayson, D. R.: An introduction to univalent foundations for mathematicians. Bull. Amer. Math. Soc.55, 427-450 (2018)Zbl 06945518 MR 3854072 · Zbl 1461.03012
[16]	Hofmann, M.: Extensional concepts in intensional type theory. Ph.D. thesis, Univ. of Edinburgh (1995)
[17]	Hofmann, M.: On the interpretation of type theory in locally Cartesian closed categories. In: Computer Science Logic (Kazimierz, 1994), Lecture Notes in Computer Sci. 933, Springer, Berlin, 427-441 (1995)Zbl 1044.03544 MR 1471244 · Zbl 1044.03544
[18]	Hofmann, M.: Syntax and semantics of dependent types. In: Semantics and Logics of Computation (Cambridge, 1995), Publ. Newton Inst. 14, Cambridge Univ. Press, Cambridge, 79-130 (1997)Zbl 0919.68083 MR 1629519 · Zbl 0919.68083
[19]	Hofmann, M., Streicher, T.: Lifting Grothendieck universes. Unpublished note (199?);http://www.mathematik.tu-darmstadt.de/∼streicher/
[20]	Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: TwentyFive Years of Constructive Type Theory (Venice, 1995), Oxford Logic Guides 36, Oxford Univ. Press, New York, 83-111 (1998)Zbl 0930.03089 MR 1686862 · Zbl 0930.03089
[21]	Hovey, M.: Model Categories. Math. Surveys Monogr. 63, Amer. Math. Soc., Providence, RI (1999)Zbl 0909.55001 MR 1650134 · Zbl 0909.55001
[22]	Jacobs, B.: Comprehension categories and the semantics of type dependency. Theoret. Computer Sci.107, 169-207 (1993)Zbl 0804.18007 MR 1201808 · Zbl 0804.18007
[23]	Johnstone, P. T.: Sketches of an Elephant: a Topos Theory Compendium. Vol. 1. Oxford Logic Guides 43, Clarendon Press, Oxford Univ. Press, New York (2002) Zbl 1071.18001 MR 1953060 · Zbl 1071.18001
[24]	Joyal, A.: A result on Kan fibrations. Unpublished note (2011)
[25]	Lumsdaine, P. L., Warren, M. A.: The local universes model: an overlooked coherence construction for dependent type theories. ACM Trans. Comput. Log.16, no. 3, art. 23, 31 pp. (2015)Zbl 1354.03101 MR 3372323 · Zbl 1354.03101
[26]	Mac Lane, S.: Categories for the Working Mathematician. 2nd ed., Grad. Texts in Math. 5, Springer, New York (1998)Zbl 0906.18001 MR 1712872 · Zbl 0906.18001
[27]	Martin-L¨of,P.:IntuitionisticTypeTheory.Bibliopolis,Naples(1984) Zbl 0571.03030
[28]	May, J. P.: Simplicial Objects in Algebraic Topology. Math. Stud. 11, Van Nostrand (1967)Zbl 0165.26004 MR 0222892 Zbl 0906.18001 · Zbl 0769.55001
[29]	Moerdijk, I., Palmgren, E.: Wellfounded trees in categories. In: Proc. Workshop on Proof Theory and Complexity, PTAC’98 (Aarhus), Ann. Pure Appl. Logic104, 189- 218 (2000)Zbl 1010.03056 MR 1778939 · Zbl 1010.03056
[30]	Moggi, E.: A category-theoretic account of program modules. Math. Structures Computer Sci.1, 103-139 (1991)Zbl 0747.18009 MR 1108806 · Zbl 0747.18009
[31]	Nordstr¨om, B., Petersson, K., Smith, J. M.: Programming in Martin-L¨of’s Type Theory. Int. Ser. Monographs on Computer Sci. 7, Clarendon Press, Oxford Univ. Press, New York (1990)Zbl 0744.03029 MR 1243882
[32]	Paulin-Mohring, C.: Inductive definitions in higher-order type theory. Habilitation, Univ. Claude Bernard (Lyon I) (1996) · Zbl 1407.68439
[33]	Pelayo, ´A., Warren, M. A.: Homotopy type theory and Voevodsky’s univalent foundations. Bull. Amer. Math. Soc.51, 597-648 (2014)Zbl 1432.03019 MR 3237761 · Zbl 1432.03019
[34]	Pitts, A. M.: Categorical logic. In: Handbook of Logic in Computer Science, Vol. 5, Oxford Univ. Press, New York, 39-128 (2000)
[35]	Quillen, D. G.: The geometric realization of a Kan fibration is a Serre fibration. Proc. Amer. Math. Soc.19, 1499-1500 (1968)Zbl 0181.26503 MR 0238322 · Zbl 0181.26503
[36]	Scott, D.: Definitions by abstraction in axiomatic set theory. Bull. Amer. Math. Soc. 61, 442 (1955) (abstract only)
[37]	Seely, R. A. G.: Locally Cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc.95, 33-48 (1984)Zbl 0539.03048 MR 0727078 · Zbl 0539.03048
[38]	Selinger, P.: A survey of graphical languages for monoidal categories. In: New Structures for Physics, Lecture Notes in Phys. 813, Springer, Heidelberg, 289-355 (2011) Zbl 1217.18002 MR 2767048 · Zbl 1217.18002
[39]	Shulman, M.: Univalence for inverse diagrams and homotopy canonicity. Math. Structures Computer Sci.25, 1203-1277 (2015)Zbl 1362.03008 MR 3340541 · Zbl 1362.03008
[40]	Streicher, T.: Semantics of Type Theory. Progr. Theoret. Computer Sci., Birkh¨auser Boston, Boston, MA (1991)Zbl 0790.68068 MR 1134134 · Zbl 0790.68068
[41]	The Univalent Foundations Program, Homotopy type theory: Univalent foundations of mathematics.http://homotopytypetheory.org/book, Institute for Advanced Study (2013)Zbl 1298.03002 MR 3204653 · Zbl 1298.03002
[42]	van den Berg, B., Moerdijk, I.: W-types in homotopy type theory. Math. Structures Computer Sci.25, 1100-1115 (2015)Zbl 1362.03009 MR 3340536 · Zbl 1362.03009
[43]	van den Berg, B.: Moerdijk, I.: W-types in homotopy-type theory—corrigendum. Math. Structures Computer Sci.28, 140 (2018)Zbl 1376.03012 MR 3737240
[44]	Voevodsky, V.: A very short note on homotopyλ-calculus. Notes from seminars given at Stanford Univ. (2006);http://math.ucr.edu/home/baez/Voevodsky note.ps
[45]	Voevodsky, V.: Notes on type systems. Unpublished notes (2012);http://www.math. ias.edu/∼vladimir/Site3/Univalent Foundations files/expressions current.pdf
[46]	Voevodsky, V.: C-system of a module over a monad on sets. Submitted (2014) arXiv:1407.3394
[47]	Voevodsky, V.: A C-system defined by a universe category. Theory Appl. Categ.30, 1181-1215 (2015)Zbl 1436.03311 MR 3402489 · Zbl 1436.03311
[48]	Voevodsky, V.: An experimental library of formalized mathematics based on the univalent foundations. Math. Structures Computer Sci.25, 1278-1294 (2015) Zbl 1361.68192 MR 3340542 · Zbl 1361.68192
[49]	Voevodsky, V.: Martin-L¨of identity types in the C-systems defined by a universe category.arXiv:1505.06446(2015) · Zbl 1436.03311
[50]	Voevodsky, V.: Products of families of types and(5, λ)-structures on C-systems. Theory Appl. Categ.31, 1044-1094 (2016)Zbl 1380.03072 MR 3584698 · Zbl 1380.03072
[51]	Voevodsky, V.: Subsystems and regular quotients of C-systems. In: A Panorama of Mathematics: Pure and Applied (Kuwait City, 2014), Contemp. Math. 658, Amer. Math. Soc., 127-137 (2016)Zbl 06607949 MR 3475277 · Zbl 1452.03040
[52]	Voevodsky, V.: The(5, λ)-structures on the C-systems defined by universe categories. Theory Appl. Categ.32, 113-121 (2017)Zbl 1383.03056 MR 3607210 · Zbl 1383.03056
[53]	Warren, M. A.: Homotopy theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon Univ. (2008)
[54]	Warren, M. A.: The strictω-groupoid interpretation of type theory. In: Models, Logics, and Higher-Dimensional Categories, CRM Proc. Lecture Notes 53, Amer. Math. Soc., 291-340 (2011)Zbl 1243.03012 MR 2867977 · Zbl 1243.03012
[55]	Werner, B.: Une th´eorie des constructions inductives. Ph.D. thesis, Univ