1: \begin{abstract}

2:  {\it Univalence} was first defined in the setting of homotopy type theory by Voevodsky \cite{hottbook2013}, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting \cite{kapulkinlumsdaine2012kanunivalent}, which was subsequently generalized to locally Cartesian closed presentable $\infty$-categories by Gepner and Kock \cite{gepnerkock2017univalence}. 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.

3:  

4:  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 \cite{stenzel2019univalence}. 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.

5: \end{abstract}