Univalence in Higher Category Theory

TL;DR

This paper generalizes the concept of univalence to finitely complete $ abla$-categories, characterizes it via representability and Segal objects, and explores its implications in various $ abla$-categories and topos theory.

Contribution

It introduces a new definition of univalent morphisms in finitely complete $ abla$-categories focusing on $ abla$-categorical aspects and characterizes univalence through internal $ abla$-categories.

Findings

Univalence in a locally Cartesian closed $ abla$-category is equivalent to the completeness of a Segal object.

Univalence can be characterized via representability of certain functors.

Connections between univalence and elementary topos theory are established.

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.