2021/03/23 by Nima Rasekh, Rasekh, Nima · 3 citations
Mathematics · #Advanced Topics in Algebra #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology
paper · pdf · doi:10.48550/arxiv.2103.12762
openalex publication_date 2021/03/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently generalized to locally Cartesian closed presentable ∞-categories by Gepner and Kock. These definitions were used to characterize various ∞-categories as models of type theories. We give a definition for univalent morphisms in finitely complete ∞-categories that generalizes the aforementioned definitions and completely focuses on the ∞-categorical aspects, characterizing it via representability of certain functors, which should remind the reader of concepts such as adjunctions or limits. We then prove that in a locally Cartesian closed ∞-category (that is not necessarily presentable) univalence of a morphism is equivalent to the completeness of a certain Segal object we construct out of the morphism, characterizing univalence via internal ∞-categories, which had been considered in a strict setting by Stenzel. We use these results to study the connection between univalence and elementary topos theory. We also study univalent morphisms in the category of groups, the ∞-category of ∞-categories, and pointed ∞-categories.