Univalence and completeness of Segal objects

DOI10.1016/J.JPAA.2022.107254MaRDI QIDQ2104885zbMATH OpenOpenAlexFDO

Publication date 8 December 2022

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1911.06640

Categorical semantics of formal languages (18C50) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Simplicial sets, simplicial objects (18N50) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Abstract: Univalence, originally a type theoretical notion at the heart of Voevodsky's Univalent Foundations Program, has found general importance as a higher categorical property that characterizes descent and hence classifying maps in

(i n f t y, 1)

-categories. Completeness is a property of Segal spaces introduced by Rezk that characterizes those Segal spaces which are

(i n f t y, 1)

-categories. In this paper, first, we make rigorous an analogy between univalence and completeness that has found various informal expressions in the higher categorical research community to date, and second, study its ramifications. The core aspect of this analogy can be understood as a translation between internal and external notions, motivated by model categorical considerations of Joyal and Tierney. As a result, we characterize the internal notion of univalence in logical model categories by the external notion of completeness defined as the right Quillen condition of suitably indexed Set-weighted limit functors. Furthermore, we extend the analogy and show that univalent completion in the sense of van den Berg and Moerdijk translates to Rezk-completion of associated Segal objects as well. Motivated by these correspondences, we exhibit univalence as a homotopical locality condition whenever univalent completion exists.

Review text

On the one hand, \textit{univalence}, originally a type-theoretical notion at the heart of Voevodsky's Univalent Foundation Program [\textit{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, \textit{completeness} is a property of Segal spaces introduced by \textit{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 \textit{A. Joyal} and \textit{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 \textit{B. van den Berg} and \textit{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 \textit{N. Rasekh} [``Complete Segal objects, Preprint, \url{arXiv:1805.03561}, \S 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)\). \textit{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.

Recommendations

Cites work

Cited in

(9)

This page was built for publication: Univalence and completeness of Segal objects

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104885)