Univalence in Higher Category Theory

Abstract

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 $\infty$-categories by Gepner and Kock. These definitions were used to characterize various $\infty$-categories as models of type theories. We give a definition for univalent morphisms in finitely complete $\infty$-categories that generalizes the aforementioned definitions and completely focuses on the $\infty$-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 $\infty$-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 $\infty$-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 $\infty$-category of $\infty$-categories, and pointed $\infty$-categories.

arXiv comment40 Pages, originally part of arXiv:1805.03561, fixed a mistake in section 3, corrected some typos and added some references. Comments welcome!

References in corpus (15)

• The identity type weak factorisation system
• Universality of multiplicative infinite loop space machines
• Univalent categories and the Rezk completion
• The $\infty$-Categorical Eckmann-Hilton Argument
• Weak omega-categories from intensional type theory
• Internal categories, anafunctors and localisations
• All $(\infty ,1)$-toposes have strict univalent universes
• A Theory of Elementary Higher Toposes
• A Type Theory for Strictly Unital $\infty$-Categories
• Univalence and completeness of Segal objects
• Quasi-Categories vs. Segal Spaces: Cartesian Edition
• An Elementary Approach to Truncations
• $(\infty ,1)$-Categorical Comprehension Schemes
• Every Elementary Higher Topos has a Natural Number Object
• Filter Quotients and Non-Presentable $(\infty ,1)$-Toposes

Cited by in corpus (1)

• Yoneda Lemma for $\mathcal{D}$-Simplicial Spaces