{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:13Z","timestamp":1740123313329,"version":"3.37.3"},"reference-count":7,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T00:00:00Z","timestamp":1529971200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005760","name":"University of Gothenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005760","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10817-018-9472-6","type":"journal-article","created":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T00:02:49Z","timestamp":1529971369000},"page":"159-171","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["The Univalence Axiom in Cubical Sets"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7320-1976","authenticated-orcid":false,"given":"Marc","family":"Bezem","sequence":"first","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2953-8894","authenticated-orcid":false,"given":"Simon","family":"Huber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,26]]},"reference":[{"issue":"1","key":"9472_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0305004108001783","volume":"146","author":"S Awodey","year":"2009","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Camb. Philos. Soc. 146(1), 45\u201355 (2009)","journal-title":"Math. Proc. Camb. Philos. Soc."},{"key":"9472_CR2","doi-asserted-by":"publisher","unstructured":"Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs (TYPES 2013), Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a026, pp. 107\u2013128. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2014). \n                    https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2013.107\n                    \n                  . \n                    http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2014\/4628","DOI":"10.4230\/LIPIcs.TYPES.2013.107"},{"key":"9472_CR3","unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2015). To appear in the proceedings of TYPES 2015"},{"key":"9472_CR4","unstructured":"Coquand, T.: A remark on contractible families of types (2013). Unpublished note available at \n                    http:\/\/www.cse.chalmers.se\/~coquand\/contr.pdf"},{"issue":"3","key":"9472_CR5","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10485-008-9137-4","volume":"17","author":"R Garner","year":"2009","unstructured":"Garner, R.: Understanding the small object argument. Appl. Categ. Struct. 17(3), 247\u2013285 (2009)","journal-title":"Appl. Categ. Struct."},{"key":"9472_CR6","unstructured":"Huber, S.: A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg (2015)"},{"key":"9472_CR7","unstructured":"Swan, A.: An algebraic weak factorisation system on 01-substitution sets: a constructive proof (2014). Preprint \n                    arXiv:1409.1829\n                    \n                   [math.LO]"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9472-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9472-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9472-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,9]],"date-time":"2019-07-09T09:20:18Z","timestamp":1562664018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9472-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,26]]},"references-count":7,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["9472"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9472-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,6,26]]},"assertion":[{"value":"20 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 June 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 June 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}