Univalence and completeness of Segal objects

DOI10.1016/J.JPAA.2022.107254zbMATH Open1502.18048arXiv1911.06640OpenAlexW4309138098MaRDI QIDQ2104885FDOQ2104885

Raffael Stenzel

Publication date: 8 December 2022

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

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 $(infty,1)$-categories. Completeness is a property of Segal spaces introduced by Rezk that characterizes those Segal spaces which are $(infty,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.

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

Recommendations

• Towards an axiomatization of the theory of higher categories
• Univalence in locally Cartesian closed categories
• A Cartesian presentation of weak \(n\)-categories
• Univalent categories and the Rezk completion
• Quasi-categories vs. Segal spaces: Cartesian edition
• Elements of \(\infty\)-category theory
• From fractions to complete Segal spaces
• A model for the homotopy theory of homotopy theory
• A model category structure on the category of simplicial categories
• A Survey of (∞, 1)-Categories

zbMATH Keywords

Segal objectsunivalent type theory

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Categorical logic and type theory
• Higher Topos Theory (AM-170)
• Generalized algebraic theories and contextual categories
• Homotopy Type Theory: Univalent Foundations of Mathematics
• A model for the homotopy theory of homotopy theory
• Comprehension categories and the semantics of type dependency
• Towards an axiomatization of the theory of higher categories
• Title not available (Why is that?)
• Function complexes in homotopical algebra
• Quasicategories of frames of cofibration categories
• Weighted limits in simplicial homotopy theory
• A model structure on internal categories in simplicial sets
• Homotopy theory of cocomplete quasicategories
• The Local Universes Model
• Homotopy-Theoretic Models of Type Theory
• Univalent categories and the Rezk completion
• Univalence for inverse diagrams and homotopy canonicity
• Higher Categories and Homotopical Algebra
• Univalent completion
• Internal languages of finitely complete \((\infty , 1)\)-categories
• Comparison of models for (∞,n)‐categories, II

Cited In (5)

• On existence of finite universal Korovkin sets in Segal algebras
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• The unambiguity of segmented morphisms
• Internal sums for synthetic fibered \((\infty,1)\)-categories
• Yoneda lemma for simplicial spaces

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)