Univalent categories and the Rezk completion

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.

27 pages, ancillary files contain formalized proofs in the proof assistant Coq; v2: version for publication in Math. Struct. in Comp. Sci., incorporating suggestions by referees and Voevodsky

References in corpus (4)

• Homotopy theoretic models of identity types
• Univalent categories and the Rezk completion
• Homotopy Theoretic Models of Type Theory
• Experimental library of univalent formalization of mathematics

Cited by in corpus (34)

• Univalent categories and the Rezk completion
• Experience Implementing a Performant Category-Theory Library in Coq
• An introduction to univalent foundations for mathematicians
• Homotopy limits in type theory
• Homotopy Type Theory in Lean
• Sets in homotopy type theory
• The join construction
• Impredicative Encodings of (Higher) Inductive Types
• Formalizing of Category Theory in Agda
• Non-wellfounded trees in Homotopy Type Theory
• Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
• Experimental library of univalent formalization of mathematics
• Reedy categories and their generalizations
• A Higher Structure Identity Principle
• Univalence and completeness of Segal objects
• Signatures and Induction Principles for Higher Inductive-Inductive Types
• From signatures to monads in UniMath
• Displayed Categories
• Implementing a Category-Theoretic Framework for Typed Abstract Syntax
• The General Universal Property of the Propositional Truncation
• A type theory for synthetic $\infty$-categories
• Constructing Higher Inductive Types as Groupoid Quotients
• Bicategories in Univalent Foundations
• Bicategorical type theory: semantics and syntax
• The HoTT Library: A formalization of homotopy type theory in Coq
• Presentable signatures and initial semantics
• Univalence in Higher Category Theory
• The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
• Heterogeneous substitution systems revisited
• Continuous and algebraic domains in univalent foundations
• Exponentiable functors between synthetic $\infty$-categories
• Types are Internal $\infty$-Groupoids
• Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT
• The derivator of setoids