{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T12:15:07Z","timestamp":1683893707642},"reference-count":28,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2019,7,15]],"date-time":"2019-07-15T00:00:00Z","timestamp":1563148800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Univalence axiom, due to Vladimir Voevodsky, is often taken to be one of the most important discoveries arising from the Homotopy Type Theory (HoTT) research programme. It is said by Steve Awodey that Univalence embodies mathematical structuralism, and that Univalence may be regarded as \u2018expanding the notion of identity to that of equivalence\u2019. This article explores the conceptual, foundational and philosophical status of Univalence in Homotopy Type Theory. It extends our Types-as-Concepts interpretation of HoTT to Universes, and offers an account of the Univalence axiom in such terms. We consider Awodey\u2019s informal argument that Univalence is motivated by the principle that reasoning should be invariant under isomorphism, and we examine whether an autonomous and rigorous justification along these lines can be given. We consider two problems facing such a justification. First, there is a difference between <jats:italic>equivalence<\/jats:italic> and <jats:italic>isomorphism<\/jats:italic> and Univalence must be formulated in terms of the former. Second, the argument as presented cannot establish Univalence itself but only a weaker version of it, and must be supplemented by an additional principle. The article argues that the prospects for an autonomous justification of Univalence are promising.<\/jats:p>","DOI":"10.1017\/s1755020316000460","type":"journal-article","created":{"date-parts":[[2019,7,15]],"date-time":"2019-07-15T07:38:46Z","timestamp":1563176326000},"page":"426-455","source":"Crossref","is-referenced-by-count":3,"title":["UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY"],"prefix":"10.1017","volume":"12","author":[{"given":"JAMES","family":"LADYMAN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"STUART","family":"PRESNELL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,7,15]]},"reference":[{"key":"S1755020316000460_ref25","volume-title":"Philosophy of Mathematics: Structure and Ontology","author":"Shapiro","year":"1997"},{"key":"S1755020316000460_ref23","first-page":"191","volume-title":"Twenty-five Years of Constructive Type Theory (Venice, 1995)","volume":"36","author":"Palmgren","year":"1998"},{"key":"S1755020316000460_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(79)90018-5"},{"key":"S1755020316000460_ref21","unstructured":"Luo Z. (2012). Notes on universes in type theory. Available at: www.cs.rhul.ac.uk\/home\/zhaohui\/universes.pdf."},{"key":"S1755020316000460_ref13","unstructured":"Gambino N. , Kapulkin C. , & Lumsdaine P. L. (2011). The univalence axiom and functional extensionality. Notes prepared by Kapulkin and Lumsdaine from Gambino\u2019s lecture during the Oberwolfach Mini-Workshop on the Homotopy Interpretation of Constructive Type Theory (2011). Available at: http:\/\/www-home.math.uwo.ca\/ \u223c kkapulki\/notes\/UA_implies_FE.pdf."},{"key":"S1755020316000460_ref1","volume-title":"Univalence as a New Principle of Logic","author":"Awodey","year":"2014a"},{"key":"S1755020316000460_ref22","unstructured":"nLab (2015). Grothendieck universe. Available at: http:\/\/ncatlab.org\/nlab\/show\/Grothendieck+universe."},{"key":"S1755020316000460_ref17","doi-asserted-by":"publisher","DOI":"10.1093\/philmat\/nkv014"},{"key":"S1755020316000460_ref28","unstructured":"Voevodsky V. (2009). Notes on type systems. Unpublished notes. Available at: http:\/\/www.math.ias.edu\/\u223cvladimir\/Site3\/Univalent_Foundations.html."},{"key":"S1755020316000460_ref18","doi-asserted-by":"publisher","DOI":"10.1093\/bjps\/axw006"},{"key":"S1755020316000460_ref10","unstructured":"Dorais F. (2014a). On the structure of universes in HoTT. Available at: http:\/\/logic.dorais.org\/archives\/1532."},{"key":"S1755020316000460_ref11","unstructured":"Dorais F. (2014b). Super HoTT. Available at: http:\/\/logic.dorais.org\/archives\/1543."},{"key":"S1755020316000460_ref19","first-page":"210","article-title":"Identity in homotopy type theory: Part II, the conceptual and philosophical status of identity in HoTT","volume":"25","author":"Ladyman","year":"2016b","journal-title":"Philosophia Mathematica"},{"key":"S1755020316000460_ref24","unstructured":"Rijke E. & Escard\u00f3 M. (2014). Generalize 7.2.2 and simplify encode-decode. Available at: https:\/\/github.com\/HoTT\/book\/issues\/718."},{"key":"S1755020316000460_ref20","unstructured":"Licata D. (2016). Weak univalence with \u201cbeta\u201d implies full univalence. Available at: https:\/\/groups.google.com\/d\/msg\/homotopytypetheory\/j2KBIvDw53s\/YTDK4D0NFQAJ."},{"key":"S1755020316000460_ref7","first-page":"107","volume-title":"19th International Conference on Types for Proofs and Programs (TYPES 2013)","author":"Bezem","year":"2014"},{"key":"S1755020316000460_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/philmat\/nkt030"},{"key":"S1755020316000460_ref6","unstructured":"Bezem M. & Shulman M. (2013). Why isprop (isequiv(f ) ) important? Available at: https:\/\/github.com\/HoTT\/book\/issues\/553."},{"key":"S1755020316000460_ref16","unstructured":"Ladyman J. & Presnell S. (2014). A primer on homotopy type theory. Available at: http:\/\/www.bristol.ac.uk\/homotopy-type-theory\/."},{"key":"S1755020316000460_ref14","volume-title":"Interpretation fonctionelle et eleimination des coupures dans l\u2019arithmetique d\u2019ordre superieure","volume":"7","author":"Girard","year":"1972"},{"key":"S1755020316000460_ref9","first-page":"227","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science","author":"Coquand","year":"1986"},{"key":"S1755020316000460_ref26","unstructured":"Shulman M. (2012). Universe polymorphism and typical ambiguity. Article at The n-Category Caf\u00e9. Available at: https:\/\/golem.ph.utexas.edu\/category\/2012\/12\/universe_polymorphism_and_typi.html."},{"key":"S1755020316000460_ref12","unstructured":"Gaillard P.-Y. (2016). HoTT Reading Notes. \u201cAn informal set of comments on the HoTT Book\u201d. Available at: http:\/\/iecl.univ-lorraine.fr\/\u223cPierre-Yves.Gaillard\/HoTT\/ReadingNotes\/HoTT_Reading_Notes_a.pdf."},{"key":"S1755020316000460_ref4","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/230\/03336"},{"key":"S1755020316000460_ref8","volume-title":"Platonism, Naturalism, and Mathematical Knowledge","author":"Brown","year":"2011"},{"key":"S1755020316000460_ref27","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S1755020316000460_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2183530"},{"key":"S1755020316000460_ref3","doi-asserted-by":"publisher","DOI":"10.1090\/noti1043"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020316000460","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T09:05:23Z","timestamp":1567069523000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020316000460\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,15]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S1755020316000460"],"URL":"https:\/\/doi.org\/10.1017\/s1755020316000460","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,15]]}}}