Univalent categories and the Rezk completion

By Benedikt Ahrens, Krzysztof Kapulkin, Michael Shulman. 2013

123 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Geometry and Topology, Mathematical Physics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Geometry and Topology

In Mathematical Physics

Citations in the corpus

Heterogeneous substitution systems revisited (2016, neutral): “The equivalence principle for univalent categories, proved in [7], then says that any two equivalent such categories cannot be distinguished either, that is, the postulated invariance on objects (univalence) lifts to the categories themselves.”
Isomorphism is equality (2013, unknown): “Is-proposition (x 6 y)) × (∀ x . x 6 x ) × (∀ x y z . x 6 y → y 6 z → x 6 z ) × (∀ x y . x 6 y → y 6 x → x ≡ y) For posets P1 = (C1, 61 , laws1) and P2 = (C2, 62 , laws2) we get that Isomorphic poset P1 P2 is definitionally equal to Σ eq : C1 ' C2.”
A type theory for synthetic ∞-categories (2017, background): “Note that the need for a “completeness” condition, or equivalently the fact that flagged categories must be defined before unflagged ones, also arises when defining categories and higher categories inside homotopy type theory; see [29, Chapter 9] or [1].”