{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T18:17:43Z","timestamp":1648923463286},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2015,3,10]],"date-time":"2015-03-10T00:00:00Z","timestamp":1425945600000},"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 give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.<\/jats:p>","DOI":"10.1017\/s0960129514000474","type":"journal-article","created":{"date-parts":[[2015,3,10]],"date-time":"2015-03-10T07:22:13Z","timestamp":1425972133000},"page":"1005-1009","source":"Crossref","is-referenced-by-count":0,"title":["Introduction \u2013 from type theory and homotopy theory to univalent foundations"],"prefix":"10.1017","volume":"25","author":[{"given":"STEVE","family":"AWODEY","sequence":"first","affiliation":[]},{"given":"NICOLA","family":"GAMBINO","sequence":"additional","affiliation":[]},{"given":"ERIK","family":"PALMGREN","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,3,10]]},"reference":[{"key":"S0960129514000474_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S0960129514000474_ref18","unstructured":"Voevodsky V. (2009) Notes on Type Systems. Preprint. Available from the author's web page http:\/\/www.math.ias.edu\/\u223cvladimir\/Site3\/Univalent_Foundations.html"},{"key":"S0960129514000474_ref16","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"S0960129514000474_ref13","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-00-02653-2"},{"key":"S0960129514000474_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"S0960129514000474_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071371"},{"key":"S0960129514000474_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0960129514000474_ref5","unstructured":"Harper R. and Licata D. R. (2012) Canonicity for 2-dimensional type theory. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 337\u2013348."},{"key":"S0960129514000474_ref19","unstructured":"Warren M. A. (2008) Homotopy Theoretic Aspects of Constructive Type Theory, Ph.D. thesis, Carnegie Mellon University."},{"key":"S0960129514000474_ref7","unstructured":"Joyal A. (2008) The Theory of Quasi-Categories and its Applications. Quaderns 45 (II) Centre de Recerca Matem\u00e0tica."},{"key":"S0960129514000474_ref10","unstructured":"Lurie J. (2004) Derived Algebraic Geometry, Ph.D. thesis, M. I. T."},{"key":"S0960129514000474_ref6","first-page":"83","volume-title":"Twenty-Five Years of Constructive Type Theory","author":"Hofmann","year":"1998"},{"key":"S0960129514000474_ref14","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0960129514000474_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097438"},{"key":"S0960129514000474_ref11","doi-asserted-by":"crossref","unstructured":"Lurie J. (2009) Higher Topos Theory, Princeton University Press.","DOI":"10.1515\/9781400830558"},{"key":"S0960129514000474_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2004.05.004"},{"key":"S0960129514000474_ref2","unstructured":"Bezem M. , Coquand T. and Huber S. (2014) A model of type theory in cubical sets. Preprint available from the second-named author's web page http:\/\/www.cse.chalmers.se\/\u223ccoquand\/mod1.pdf"},{"key":"S0960129514000474_ref4","first-page":"163","article-title":"A machine-checked proof of the odd order theorem","volume":"7998","author":"Gonthier","year":"2013","journal-title":"Springer Lecture Notes in Mathematics"},{"key":"S0960129514000474_ref8","first-page":"1","article-title":"Weak \u03c9-categories from intensional type theory","volume":"6","author":"LeFanu Lumsdaine","year":"2010","journal-title":"Logical Methods in Computer Science"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000474","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T20:34:51Z","timestamp":1566419691000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000474\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,10]]},"references-count":19,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000474"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000474","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,10]]}}}