{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:29:24Z","timestamp":1761611364047},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T00:00:00Z","timestamp":1422576000000},"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>Homotopy type theory may be seen as an internal language for the \u221e-category of weak \u221e-groupoids. Moreover, weak \u221e-groupoids model the univalence axiom. Voevodsky proposes this (language for) weak \u221e-groupoids as a new foundation for Mathematics called the univalent foundations. It includes the sets as weak \u221e-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those \u2018discrete\u2019 groupoids do in fact form a (predicative) topos. More generally, homotopy type theory is conjectured to be the internal language of \u2018elementary\u2019 of \u221e-toposes. We prove that sets in homotopy type theory form a \u03a0W-pretopos. This is similar to the fact that the 0-truncation of an \u221e-topos is a topos. We show that both a subobject classifier and a 0-object classifier are available for the type theoretical universe of sets. However, both of these are large and moreover the 0-object classifier for sets is a function between 1-types (i.e. groupoids) rather than between sets. Assuming an impredicative propositional resizing rule we may render the subobject classifier small and then we actually obtain a topos of sets.<\/jats:p>","DOI":"10.1017\/s0960129514000553","type":"journal-article","created":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T04:14:15Z","timestamp":1422591255000},"page":"1172-1202","source":"Crossref","is-referenced-by-count":11,"title":["Sets in homotopy type theory"],"prefix":"10.1017","volume":"25","author":[{"given":"EGBERT","family":"RIJKE","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BAS","family":"SPITTERS","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2015,1,30]]},"reference":[{"key":"S0960129514000553_ref45","unstructured":"van den Berg B. (2012) Predicative toposes. arXiv:1207.0959."},{"key":"S0960129514000553_ref44","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S0960129509007440","article-title":"Three extensional models of type theory","volume":"19","author":"Van","year":"2009","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0960129514000553_ref38","unstructured":"Rijke E. and Spitters B. (2013b) Orthogonal factorization systems in homotopy type theory. Technical report. Available at: http:\/\/uf-ias-2012.wikispaces.com\/file\/view\/images.pdf\/401765624\/images.pdf."},{"key":"S0960129514000553_ref35","unstructured":"Pelayo \u00c1. and Warren M. (2012) Homotopy type theory and Voevodsky's univalent foundations. arXiv:1210.5658."},{"key":"S0960129514000553_ref39","unstructured":"Shulman M. (2013) The univalence axiom for inverse diagrams and homotopy canonicity. MSCS. arXiv:1203.3253."},{"key":"S0960129514000553_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8640-5"},{"key":"S0960129514000553_ref14","unstructured":"Danielsson N. A. (2013) Closure properties for h-levels. Technical report, Available at: http:\/\/www.cse.chalmers.se\/~nad\/listings\/equality\/H-level.Closure.html."},{"key":"S0960129514000553_ref29","unstructured":"Maietti M. E. and Rosolini G. (2012) Elementary quotient completion. ArXiv:1206.0162."},{"key":"S0960129514000553_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511752483"},{"key":"S0960129514000553_ref16","unstructured":"Hofmann M. (1995) Extensional Concepts in Intensional Type Theory, Ph.D. thesis, University of Edinburgh."},{"key":"S0960129514000553_ref4","doi-asserted-by":"crossref","unstructured":"Altenkirch T. (1999) Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science 412\u2013420. doi:10.1109\/LICS.1999.782636.","DOI":"10.1109\/LICS.1999.782636"},{"key":"S0960129514000553_ref21","unstructured":"Kapulkin K. , Lumsdaine P. and Voevodsky V. (2012) The simplicial model of univalent foundations. arXiv:1211.2851."},{"key":"S0960129514000553_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014566"},{"key":"S0960129514000553_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2013.04.001"},{"key":"S0960129514000553_ref36","unstructured":"Rezk C. (2010) Toposes and homotopy toposes (version 0.15). Available at: http:\/\/www.math.uiuc.edu\/~rezk\/homotopy-topos-sketch.pdf."},{"key":"S0960129514000553_ref3","unstructured":"Ahrens B. , Kapulkin K. and Shulman M. (2013) Univalent categories and the Rezk completion. MSCS. arXiv:1303.0584."},{"key":"S0960129514000553_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-4435-6_9"},{"key":"S0960129514000553_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_13"},{"key":"S0960129514000553_ref1","first-page":"1","volume-title":"Types for Proofs and Programs","author":"Aczel","year":"2002"},{"key":"S0960129514000553_ref37","unstructured":"Rijke E. and Spitters B. (2013a) Limits and colimits in homotopy type theory. In preparation."},{"key":"S0960129514000553_ref32","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory, Chalmers University of Technology. Ph.D. thesis, Chalmers University of Technology."},{"key":"S0960129514000553_ref24","unstructured":"Lumsdaine P. and Shulman M. (2015) Higher inductive types. In preparation."},{"key":"S0960129514000553_ref13","unstructured":"Coq Development Team. (2012) The Coq Proof Assistant Reference Manual, INRIA-Rocquencourt."},{"key":"S0960129514000553_ref7","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"S0960129514000553_ref8","doi-asserted-by":"crossref","unstructured":"Awodey S. , Gambino N. and Sojakova K. (2012) Inductive types in homotopy type theory. In: Logic in Computer Science, IEEE 95\u2013104.","DOI":"10.1109\/LICS.2012.21"},{"key":"S0960129514000553_ref5","unstructured":"Avigad J. , Kapulkin K. and Lumsdaine P. (2013) Homotopy limits in Coq. arXiv:1304.0680."},{"key":"S0960129514000553_ref43","unstructured":"The Univalent Foundations Program. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study. arXiv:1308.0729."},{"key":"S0960129514000553_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004962"},{"key":"S0960129514000553_ref49","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000071"},{"key":"S0960129514000553_ref11","first-page":"107","article-title":"A model of type theory in cubical sets","volume":"26","author":"Bezem","year":"2014","journal-title":"19th International Conference on Types for Proofs and Programs (TYPES 2013)"},{"key":"S0960129514000553_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90021-7"},{"key":"S0960129514000553_ref12","volume-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"S0960129514000553_ref9","unstructured":"Barras B. (2013) Native implementation of higher inductive types (HITs) in Coq. Technical report. Available at: http:\/\/www.crm.cat\/en\/Activities\/Documents\/barras-crm-2013.pdf."},{"key":"S0960129514000553_ref19","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"Johnstone","year":"2002"},{"key":"S0960129514000553_ref2","unstructured":"Aczel P. and Rathjen M. (2001) Notes on constructive set theory."},{"key":"S0960129514000553_ref25","doi-asserted-by":"crossref","DOI":"10.1515\/9781400830558","volume-title":"Higher Topos Theory","author":"Lurie","year":"2009"},{"key":"S0960129514000553_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00079-3"},{"key":"S0960129514000553_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511755460"},{"key":"S0960129514000553_ref18","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"S0960129514000553_ref34","unstructured":"Pelayo \u00c1. , Voevodsky V. and Warren M. (2013) A preliminary univalent formalization of the p-adic numbers. arXiv:1302.1207."},{"key":"S0960129514000553_ref26","first-page":"501","volume-title":"Handbook of Algebra","author":"Mac"},{"key":"S0960129514000553_ref17","first-page":"83","article-title":"The groupoid interpretation of type theory","volume":"36","author":"Hofmann","year":"1998","journal-title":"Twenty-Five Years of Constructive Type Theory (Venice, 1995)"},{"key":"S0960129514000553_ref27","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"S0960129514000553_ref10","unstructured":"Barras B. , Coquand T. and Huber S. (2013) A generalization of Takeuti-Gandy interpretation. Available at: http:\/\/uf-ias-2012.wikispaces.com\/file\/view\/semi.pdf."},{"key":"S0960129514000553_ref46","unstructured":"Voevodsky V. (2012) A universe polymorphic type system. Available at: http:\/\/uf-ias-2012.wikispaces.com\/file\/view\/Universe+polymorphic+type+sytem.pdf."},{"key":"S0960129514000553_ref22","volume-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek","year":"1988"},{"key":"S0960129514000553_ref40","unstructured":"Spiwack A. (2011) A Journey Exploring the Power and Limits of Dependent Type Theory, Ph.D. thesis, \u00c9cole Polytechnique, Palaiseau, France."},{"key":"S0960129514000553_ref33","doi-asserted-by":"crossref","unstructured":"Palmgren E. (2012) Constructivist and structuralist foundations: Bishops and Lawveres theories of sets. Annals of Pure and Applied Logic. doi:10.1016\/j.apal.2012.01.011.","DOI":"10.1016\/j.apal.2012.01.011"},{"key":"S0960129514000553_ref47","unstructured":"Voevodsky V. (2014) Experimental library of univalent formalization of mathematics. Technical report. 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\/S0960129514000553","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T05:58:30Z","timestamp":1566280710000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000553\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,30]]},"references-count":49,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000553"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000553","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,30]]}}}