Univalent categories and the Rezk completion

DOI10.1017/S0960129514000486MaRDI QIDQ5740648zbMATH OpenDBLPWikidataFDO

Authors Benedikt Ahrens, Krzysztof Kapulkin, Michael Shulman

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1303.0584

Mathematics Subject Classification ID

Foundations, relations to logic and deductive systems (18A15)

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.

Recommendations

• Univalence and completeness of Segal objects
• A type theory for synthetic -categories
• Categorical structures for type theory in univalent foundations
• The simplicial model of univalent foundations (after Voevodsky)
• Bicategories in univalent foundations

Cites work

• A machine-checked proof of the odd order theorem
• A model for the homotopy theory of homotopy theory
• Isomorphism is equality

Cited in

(41)

• Homotopy type theory in Lean
• Univalent foundations as structuralist foundations
• Iterated extensions and uniserial length categories
• Axiomatizations of arithmetic and the first-order/second-order divide
• Univalence and completeness of Segal objects
• The construction of set-truncated higher inductive types
• From signatures to monads in \textsf{UniMath}
• Some Wellfounded Trees in UniMath
• A type theory for synthetic -categories
• Displayed categories
• A C-system defined by a universe category
• Heterogeneous substitution systems revisited
• Categorical structures for type theory in univalent foundations
• An introduction to univalent foundations for mathematicians
• Constructing higher inductive types as groupoid quotients
• scientific article; zbMATH DE number 7379288 (Why is no real title available?)
• Bicategories in univalent foundations
• Bicategories in univalent foundations
• Displayed Categories
• The fullness axiom and exact completion of homotopy categories
• Signatures and induction principles for higher inductive-inductive types
• Univalence in locally Cartesian closed categories
• The Univalence Axiom in posetal model categories
• Foundations of Software Science and Computation Structures
• On equality of objects in categories in constructive type theory
• Univalent Foundations and the Equivalence Principle
• Higher Structures in Homotopy Type Theory
• Bicategorical type theory: semantics and syntax
• An unsuspended description of the E-theory category
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Semantics for two-dimensional type theory
• Formalizing the algebraic small object argument in UniMath
• A direct-categorical approach to opetopic sets and opetopes
• Univalent enriched categories and the enriched rezk completion
• Exponentiable functors between synthetic -categories
• Continuous and algebraic domains in univalent foundations
• The formal theory of monads, univalently
• The category of iterative sets in homotopy type theory and univalent foundations
• The univalence principle
• Insights from univalent foundations: a case study using double categories
• Isomorphism is equality

This page was built for publication: Univalent categories and the Rezk completion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740648)