Hostname: page-component-74656f9884-j7cmm Total loading time: 0 Render date: 2026-11-09T08:56:29.645Z Has data issue: false hasContentIssue false
  • English
  • Français

Univalent categories and the Rezk completion

Published online by Cambridge University Press:  19 January 2015

BENEDIKT AHRENS ,
KRZYSZTOF KAPULKIN  and
MICHAEL SHULMAN
BENEDIKT AHRENS
Affiliation:
Institut de Recherche en Informatique de Toulouse, Université Paul Sabatier, France E-mail: benedikt.ahrens@irit.fr
KRZYSZTOF KAPULKIN
Affiliation:
University of Pittsburgh, Pittsburgh, PA, U.S.A. E-mail: k.kapulkin@gmail.com
MICHAEL SHULMAN
Affiliation:
University of San Diego, San Diego, CA, U.S.A. E-mail: shulman@sandiego.edu
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

References

Ahrens, B., Kapulkin, K. and Shulman, M. (2013) Univalent categories and the Rezk completion in Coq. Git repository of Coq files. Available at: https://github.com/benediktahrens/rezk_completion.Google Scholar
Arndt, P. and Kapulkin, K. (2011) Homotopy-theoretic models of type theory. In: Typed Lambda Calculi and Applications. Springer Lecture Notes in Computer Science 6690 45–60. Doi: 10.1007/978-3-642-21691-6_7.Google Scholar
Awodey, S. and Warren, M. A. (2009) Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society 146.1 45–55. ISSN: . Doi: 10.1017/S0305004108001783. ArXiv: 0709.0248.Google Scholar
Barwick, C. and Schommer-Pries, C. (2011) On the unicity of the homotopy theory of higher categories. ArXiv: 1112.0040.Google Scholar
Bergner, J. E. (2009) A survey of (1; 1)-categories. In: Baez, J. C. C. and May, J. P. (eds.) Towards Higher Categories, The IMA Volumes in Mathematics and its Applications volume 152, Springer 69–83. ArXiv: math.CT/0610239.Google Scholar
Bunge, M. (1979) Stack completions and Morita equivalence for categories in a topos. Cahiers Topologie Géométrie Différentielle 20.4 401–436. ISSN: .Google Scholar
Coquand, T. and Danielsson, N. A. (2013) Isomorphism is equality. Indagationes Mathematicae 24 (4) 1105–1120.Google Scholar
Gonthier, G. (2013) A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C. and Pichardie, D. (eds.) Interactive Theorem Proving. Springer Lecture Notes in Computer Science 7998 163–179.CrossRefGoogle Scholar
Hofmann, M. and Streicher, T. (1998) The groupoid interpretation of type theory. In: Oxford Logic Guides, Twenty-five years of constructive type theory (Venice, 1995). volume 36, New York: Oxford University Press 83–111.Google Scholar
Joyal, A. and Tierney, M. (1991) Strong stacks and classifying spaces. In: Category theory (Como, 1990). Springer Lecture Notes in Mathematics 1488, Berlin 213–236.Google Scholar
Kapulkin, K., Lumsdaine, P. L. and Voevodsky, V. (2012) The simplicial model of univalent foundations. ArXiv: 1211.2851.Google Scholar
Lumsdaine, P. L. and Shulman, M. (2014) Higher inductive types. In preparation.Google Scholar
Martin-Löf, P. (1984) Intuitionistic Type Theory: Notes by Giovanni Sambin, Studies in Proof Theory. Lecture Notes volume 1, Naples: Bibliopolis. ISBN: 88-7088-105-9.Google Scholar
Pelayo, Á. and Warren, M. A. (2012) Homotopy type theory and Voevodsky's univalent foundations. ArXiv: 1210.5658.Google Scholar
Rezk, C. (2001) A model for the homotopy theory of homotopy theory. Transactions of the American Mathematical Society 353.3 973–1007 (electronic). ISSN: . ArXiv: math.AT 9811037.CrossRefGoogle Scholar
Univalent Foundations Program, T. (2013) Homotopy type theory: Univalent foundations of mathematics. Available at: http://homotopytypetheory.org/book.Google Scholar
van den Berg, B. and Garner, R. (2012). Topological and simplicial models of identity types. ACM Transactions on Computer Systems 13.1 Art. 3, 44. ISSN: . doi: 10.1145/2071368.2071371.Google Scholar
Voevodsky, V. (2010) Univalent Foundations Project. Available at: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.pdf.Google Scholar
Voevodsky, V. (2013) Experimental library of univalent formalization of mathematics. ArXiv: 1401.0053.Google Scholar
Warren, M. A. (2008) Homotopy Theoretic Aspects of Constructive Type Theory, Ph.D. thesis, Carnegie Mellon University.Google Scholar
Werner, B. (1994) Une Théorie des Constructions Inductives, Ph.D. thesis, Université Paris 7 (Denis Diderot).Google Scholar
Supplementary material: File

Ahrens et al. supplementary material

Supplementary material

Download Ahrens et al. supplementary material(File)
File 193 KB