nLab Univalent categories and the Rezk completion

on internal categories in homotopy type theory and their Rezk completion to univalent categories.

Abstract. We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of “category” for which equality and equivalence of categories agree. Such categories satisfy a version of the Univalence Axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them “saturated” or "univalent" categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

category: reference

Last revised on June 9, 2022 at 17:25:59. See the history of this page for a list of all contributions to it.