Univalence and completeness of Segal objects. (English) Zbl 1502.18048
On the one hand, univalence, originally a type-theoretical notion at the heart of Voevodsky’s Univalent Foundation Program [The Univalent Foundations Program, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)], has found general importance as a higher categorical property characterizing descent and hence classifying maps in \((\infty,1)\)-categories. On the other hand, completeness is a property of Segal spaces introduced by C. Rezk [Trans. Am. Math. Soc. 353, No. 3, 973–1007 (2001; Zbl 0961.18008)] characterising those Segal spaces which are \((\infty,1)\)-categories. The principal objective in this paper is first to make rigorous a ostensible analogy between univalence and completeness that has found various informal expressions in the higher categorical research community to date, and second to study its ramifications.
The basic strategy is to understand its quintessence as a translation between internal and external notions, motivated by model categorical considerations of A. Joyal and M. Tierney [Contemp. Math. 431, 277–326 (2007; Zbl 1138.55016)]. Consequently, the author characterizes the internal notion of univalence in logical model categories by the external notion of completeness defined as the right Quillen conditions of suitably indexed Set-weighted limit functors.
Furthermore, the author extends the analogy, showing that univalent completion in the sense of B. van den Berg and I. Moerdijk [Math. Ann. 371, No. 3–4, 1337–1350 (2018; Zbl 1400.55007)] translates to Rezk-completion of associated Segal objects as well. Depending on these correspondence, the author exhibits univalence as a homotopical locality condition whenever univalent completion exists.
A connection of Rezk-completeness and univalence via a nerve correspondence \(p\mapsto N(p)\)has been investigated by N. Rasekh [“Complete Segal objects”, Preprint, arXiv:1805.03561, §6], where a theory of complete Segal objects in \((\infty,1)\)-categories was developed and univalence of a map \(p\)in a locally cartesian closed \((\infty,1)\)-category \(\mathcal{C} \)was defined as completeness of its associated Segal object \(N(p)\). B. Ahrens et al. [Math. Struct. Comput. Sci. 25, No. 5, 1010–1039 (2015; Zbl 1362.18003)] introduced a notion of Rezk-completeness of precategories to categories in the syntax of Homotopy Type Theory, proposing a definition of ‘category’ for which equality and equivalence of categories agree. They gave a construction corresponding to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.
The basic strategy is to understand its quintessence as a translation between internal and external notions, motivated by model categorical considerations of A. Joyal and M. Tierney [Contemp. Math. 431, 277–326 (2007; Zbl 1138.55016)]. Consequently, the author characterizes the internal notion of univalence in logical model categories by the external notion of completeness defined as the right Quillen conditions of suitably indexed Set-weighted limit functors.
Furthermore, the author extends the analogy, showing that univalent completion in the sense of B. van den Berg and I. Moerdijk [Math. Ann. 371, No. 3–4, 1337–1350 (2018; Zbl 1400.55007)] translates to Rezk-completion of associated Segal objects as well. Depending on these correspondence, the author exhibits univalence as a homotopical locality condition whenever univalent completion exists.
A connection of Rezk-completeness and univalence via a nerve correspondence \(p\mapsto N(p)\)has been investigated by N. Rasekh [“Complete Segal objects”, Preprint, arXiv:1805.03561, §6], where a theory of complete Segal objects in \((\infty,1)\)-categories was developed and univalence of a map \(p\)in a locally cartesian closed \((\infty,1)\)-category \(\mathcal{C} \)was defined as completeness of its associated Segal object \(N(p)\). B. Ahrens et al. [Math. Struct. Comput. Sci. 25, No. 5, 1010–1039 (2015; Zbl 1362.18003)] introduced a notion of Rezk-completeness of precategories to categories in the syntax of Homotopy Type Theory, proposing a definition of ‘category’ for which equality and equivalence of categories agree. They gave a construction corresponding to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.
Reviewer: Hirokazu Nishimura (Tsukuba)
MSC:
| 18N45 | Categories of fibrations, relations to \(K\)-theory, relations to type theory |
| 18N50 | Simplicial sets, simplicial objects |
| 18N60 | \((\infty,1)\)-categories (quasi-categories, Segal spaces, etc.); \(\infty\)-topoi, stable \(\infty\)-categories |
| 18C50 | Categorical semantics of formal languages |
| 55U35 | Abstract and axiomatic homotopy theory in algebraic topology |
References:
| [1] | Ahrens, B.; Kapulkin, K.; Shulman, M., Univalent categories and the Rezk completion, Math. Struct. Comput. Sci., 25, 5, 1010-1039 (2015) · Zbl 1362.18003 |
| [2] | Arndt, P.; Kapulkin, K., Homotopy-theoretic models of type theory, (Typed Lambda Calculi and Applications. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 6690 (2011), Springer: Springer Berlin, Heidelberg), 45-60 · Zbl 1331.03044 |
| [3] | Barwick, C., \((\infty, n)\)-cat as a closed model category (2005), University of Pennsylvania: University of Pennsylvania Philadelphia, PA 19104, United States, Ph.D. thesis |
| [4] | Bergner, J. E.; Rezk, C., Comparison of models for \((\infty, n)\)-categories, II, J. Topol., 13, 4, 1554-1581 (2020) · Zbl 1461.18017 |
| [5] | van den Berg, B.; Moerdijk, I., Univalent completion, Math. Ann., 371, 3-4, 1337-1350 (2018) · Zbl 1400.55007 |
| [6] | Capriotti, P., Models of type theory with strict equality (2016), University of Nottingham: University of Nottingham Nottingham NG7 2RD, United Kingdom, Ph.D. thesis |
| [7] | Cartmell, J., Generalized algebraic theories and contextual categories, Ann. Pure Appl. Log., 32, 209-243 (1986) · Zbl 0634.18003 |
| [8] | Cisinski, D. C., Higher Categories and Homotopical Algebra, Cambridge Studies in Advanced Mathematics, vol. 180 (2019), Cambridge University Press · Zbl 1430.18001 |
| [9] | Dwyer, W. G.; Kan, D. M., Function complexes in homotopical algebra, Topology, 19, 427-440 (1980) · Zbl 0438.55011 |
| [10] | Gambino, N., Weighted limits in simplicial homotopy theory, J. Pure Appl. Algebra, 214, 7, 1193-1199 (2010) · Zbl 1228.18013 |
| [11] | Gepner, D.; Kock, J., Univalence in locally Cartesian closed infinity-categories, Forum Math., 29, 3 (2012) |
| [12] | Horel, G., A model structure on internal categories in simplicial sets, Theory Appl. Categ., 30, 20, 704-750 (2015) · Zbl 1317.18018 |
| [13] | Hovey, M., Model Categories, Mathematical Surveys and Monographs, vol. 63 (1999), American Mathematical Society · Zbl 0909.55001 |
| [14] | Jacobs, B., Comprehension categories and the semantics of type dependency, Theor. Comput. Sci., 107, 169-207 (1993) · Zbl 0804.18007 |
| [15] | Jacobs, B., Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141 (1999), Elsevier Science B.V. · Zbl 0911.03001 |
| [16] | Joyal, A., Notes on clans and tribes (2017), [Online, v1] |
| [17] | Joyal, A.; Tierney, M., Quasi-categories vs Segal spaces, (Categories in Algebra, Geometry and Mathematical Physics (2006), American Mathematical Society), 277-326 · Zbl 1138.55016 |
| [18] | Kapulkin, C., Locally Cartesian closed quasicategories from type theory, J. Topol., 10, 4 (2015) |
| [19] | Kapulkin, C.; Lumsdaine, P. L.; Voevodsky, V., The simplicial model of univalent foundations (2012), [Online] |
| [20] | Kapulkin, C.; Szumiło, K., Quasicategories of frames of cofibration categories, Appl. Categ. Struct., 25, 3, 323-347 (2017) · Zbl 1372.55014 |
| [21] | Kapulkin, C.; Szumiło, K., Internal languages of finitely complete \((\infty, 1)\)-categories, Sel. Math. New Ser., 25, 33 (2019) · Zbl 1462.18007 |
| [22] | Lumsdaine, P. L.; Warren, M., The local universes model: an overlooked coherence construction for dependent type theories, ACM Trans. Comput. Log., 16, 3, 1-31 (2015) · Zbl 1354.03101 |
| [23] | Lurie, J., Higher Topos Theory, Annals of Mathematics Studies, vol. 170 (2009), Princeton University Press · Zbl 1175.18001 |
| [24] | The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics (2013) · Zbl 1298.03002 |
| [25] | Rasekh, N., Complete Segal objects (2018), [Online, v1] |
| [26] | Rezk, C., A model for the homotopy theory of homotopy theories, Trans. Am. Math. Soc., 973-1007 (1999) · Zbl 0961.18008 |
| [27] | Rezk, C., Toposes and homotopy toposes (version 0.15) (2010) |
| [28] | Shulman, M., Univalence for inverse diagrams and homotopy canonicity, Math. Struct. Comput. Sci., 25, 5, 1203-1277 (2015) · Zbl 1362.03008 |
| [29] | Stenzel, R., On univalence, Rezk completeness and presentable quasi-categories (2019), University of Leeds: University of Leeds Leeds LS2 9JT, Ph.D. thesis |
| [30] | Szumiło, K., Homotopy theory of cocomplete quasicategories, Algebraic Geom. Topol., 17, 2, 765-791 (2017) · Zbl 1364.55019 |
| [31] | Toën, B., Vers une axiomatisation de la théorie des catégories supérieures, K-Theory, 34, 3, 233-263 (2005) · Zbl 1083.18003 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
