{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:01:28Z","timestamp":1767927688286,"version":"3.49.0"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2015,1,19]],"date-time":"2015-01-19T00:00:00Z","timestamp":1421625600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,6]]},"abstract":"<jats:p>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 \u2018category\u2019 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 \u2018saturated\u2019 or \u2018univalent\u2019 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.<\/jats:p>","DOI":"10.1017\/s0960129514000486","type":"journal-article","created":{"date-parts":[[2015,1,19]],"date-time":"2015-01-19T01:30:54Z","timestamp":1421631054000},"page":"1010-1039","source":"Crossref","is-referenced-by-count":33,"title":["Univalent categories and the Rezk completion"],"prefix":"10.1017","volume":"25","author":[{"given":"BENEDIKT","family":"AHRENS","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"KRZYSZTOF","family":"KAPULKIN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MICHAEL","family":"SHULMAN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,1,19]]},"reference":[{"key":"S0960129514000486_ref17","article-title":"Topological and simplicial models of identity types","volume":"13","author":"van den Berg","year":"2012","journal-title":"ACM Transactions on Computer Systems"},{"key":"S0960129514000486_ref16","unstructured":"Univalent Foundations Program, T. (2013) Homotopy type theory: Univalent foundations of mathematics. Available at: http:\/\/homotopytypetheory.org\/book."},{"key":"S0960129514000486_ref6","first-page":"401","article-title":"Stack completions and Morita equivalence for categories in a topos","volume":"20","author":"Bunge","year":"1979","journal-title":"Cahiers Topologie G\u00e9om\u00e9trie Diff\u00e9rentielle"},{"key":"S0960129514000486_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_7"},{"key":"S0960129514000486_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"S0960129514000486_ref15","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-00-02653-2"},{"key":"S0960129514000486_ref18","doi-asserted-by":"crossref","unstructured":"Voevodsky V. (2010) Univalent Foundations Project. Available at: http:\/\/www.math.ias.edu\/~vladimir\/Site3\/Univalent_Foundations_files\/univalent_foundations_project.pdf.","DOI":"10.1007\/978-3-642-20920-8_4"},{"key":"S0960129514000486_ref11","unstructured":"Kapulkin K. , Lumsdaine P. L. and Voevodsky V. (2012) The simplicial model of univalent foundations. ArXiv: 1211.2851."},{"key":"S0960129514000486_ref12","unstructured":"Lumsdaine P. L. and Shulman M. (2014) Higher inductive types. In preparation."},{"key":"S0960129514000486_ref21","unstructured":"Werner B. (1994) Une Th\u00e9orie des Constructions Inductives, Ph.D. thesis, Universit\u00e9 Paris 7 (Denis Diderot)."},{"key":"S0960129514000486_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0960129514000486_ref20","unstructured":"Warren M. A. (2008) Homotopy Theoretic Aspects of Constructive Type Theory, Ph.D. thesis, Carnegie Mellon University."},{"key":"S0960129514000486_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084222"},{"key":"S0960129514000486_ref5","first-page":"69","volume-title":"Towards Higher Categories","author":"Bergner","year":"2009"},{"key":"S0960129514000486_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.indag.2013.09.002"},{"key":"S0960129514000486_ref13","unstructured":"Martin-L\u00f6f P. (1984) Intuitionistic Type Theory: Notes by Giovanni Sambin, Studies in Proof Theory. Lecture Notes volume 1, Naples: Bibliopolis. ISBN: 88-7088-105-9."},{"key":"S0960129514000486_ref1","unstructured":"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."},{"key":"S0960129514000486_ref14","unstructured":"Pelayo \u00c1. and Warren M. A. (2012) Homotopy type theory and Voevodsky's univalent foundations. ArXiv: 1210.5658."},{"key":"S0960129514000486_ref4","unstructured":"Barwick C. and Schommer-Pries C. (2011) On the unicity of the homotopy theory of higher categories. ArXiv: 1112.0040."},{"key":"S0960129514000486_ref9","first-page":"83","volume-title":"Oxford Logic Guides","author":"Hofmann","year":"1998"},{"key":"S0960129514000486_ref19","unstructured":"Voevodsky V. (2013) Experimental library of univalent formalization of mathematics. ArXiv: 1401.0053."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000486","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T16:38:23Z","timestamp":1566232703000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000486\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,19]]},"references-count":21,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000486"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000486","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,19]]}}}