{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:21Z","timestamp":1763468241850},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,24]],"date-time":"2014-11-24T00:00:00Z","timestamp":1416787200000},"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 will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.<\/jats:p>","DOI":"10.1017\/s0960129514000516","type":"journal-article","created":{"date-parts":[[2014,11,24]],"date-time":"2014-11-24T08:00:26Z","timestamp":1416816026000},"page":"1100-1115","source":"Crossref","is-referenced-by-count":7,"title":["W-types in homotopy type theory"],"prefix":"10.1017","volume":"25","author":[{"given":"BENNO","family":"VAN DEN BERG","sequence":"first","affiliation":[]},{"given":"IEKE","family":"MOERDIJK","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,24]]},"reference":[{"key":"S0960129514000516_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0348-8707-6"},{"key":"S0960129514000516_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"S0960129514000516_ref3","volume-title":"Non-Well-Founded Sets","author":"Aczel","year":"1988"},{"key":"S0960129514000516_ref26","doi-asserted-by":"crossref","unstructured":"Shulman M. (2013b) Univalence for inverse diagrams and homotopy canonicity. arXiv:103.3253.","DOI":"10.1017\/S0960129514000565"},{"key":"S0960129514000516_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.12.001"},{"key":"S0960129514000516_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-012-1082-0"},{"key":"S0960129514000516_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0018349"},{"key":"S0960129514000516_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S0960129514000516_ref23","doi-asserted-by":"publisher","DOI":"10.2307\/1970725"},{"key":"S0960129514000516_ref14","unstructured":"Kapulkin C. , Lumsdaine P. L. and Voevodsky V. (2012) The simplicial model of univalent foundations. arXiv:1211.2851."},{"key":"S0960129514000516_ref15","doi-asserted-by":"publisher","DOI":"10.2307\/2275015"},{"key":"S0960129514000516_ref19","first-page":"1","volume-title":"Indexed Categories and their Applications","author":"Par\u00e9","year":"1978"},{"key":"S0960129514000516_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s00209-010-0770-x"},{"key":"S0960129514000516_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S1446788700018735"},{"key":"S0960129514000516_ref4","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1191333841"},{"key":"S0960129514000516_ref16","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0960129514000516_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00079-3"},{"key":"S0960129514000516_ref8","doi-asserted-by":"crossref","first-page":"117","DOI":"10.4064\/fm-117-2-117-160","article-title":"Words, free algebras, and coequalizers","volume":"117","author":"Blass","year":"1983","journal-title":"Fundamenta Mathematicae"},{"key":"S0960129514000516_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)00103-P"},{"key":"S0960129514000516_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00012-9"},{"key":"S0960129514000516_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097438"},{"key":"S0960129514000516_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"S0960129514000516_ref22","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1968-0238322-1"},{"key":"S0960129514000516_ref25","unstructured":"Shulman M. (2013a) The univalence axiom for elegant Reedy presheaves. arXiv:1307.6248."},{"key":"S0960129514000516_ref27","unstructured":"Voevodsky V. (2011) Notes on type systems. Available at http:\/\/www.math.ias.edu\/~vladimir\/Site3\/Univalent_Foundations.html."},{"key":"S0960129514000516_ref11","doi-asserted-by":"publisher","DOI":"10.1112\/jtopol\/jtt004"},{"key":"S0960129514000516_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0040-9383(74)90022-6"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T19:12:59Z","timestamp":1566069179000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000516\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,24]]},"references-count":27,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000516"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000516","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,24]]}}}