Homotopy Type Theory
Univalent categories and the Rezk completion


Univalent categories and the Rezk completion. Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Math. Structures Comput. Sci. 25 (2015), no. 5, 1010?1039.


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 January 19, 2019 at 13:11:40. See the history of this page for a list of all contributions to it.