Univalence and completeness of Segal objects (Q2104885)

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.