{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:21:56Z","timestamp":1770290516799,"version":"3.49.0"},"reference-count":55,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2017,8,17]],"date-time":"2017-08-17T00:00:00Z","timestamp":1502928000000},"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":[[2018,6]]},"abstract":"<jats:p>We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of \u2018adjoint logic\u2019 in which the discretization and codiscretization modalities are characterized using a judgemental formalism of \u2018crisp variables.\u2019 This yields type theories that we call \u2018spatial\u2019 and \u2018cohesive,\u2019 in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the \u2018fundamental \u221e-groupoid\u2019 or \u2018shape\u2019), disentangling the \u2018identifications\u2019 of homotopy type theory from the \u2018continuous paths\u2019 of topology. In a further refinement called \u2018real-cohesion,\u2019 the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.<\/jats:p>","DOI":"10.1017\/s0960129517000147","type":"journal-article","created":{"date-parts":[[2017,8,17]],"date-time":"2017-08-17T04:09:26Z","timestamp":1502942966000},"page":"856-941","source":"Crossref","is-referenced-by-count":31,"title":["Brouwer's fixed-point theorem in real-cohesive homotopy type theory"],"prefix":"10.1017","volume":"28","author":[{"given":"MICHAEL","family":"SHULMAN","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2017,8,17]]},"reference":[{"key":"S0960129517000147_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S144678870002718X"},{"key":"S0960129517000147_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.06.017"},{"key":"S0960129517000147_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00101-X"},{"key":"S0960129517000147_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(02)00283-9"},{"key":"S0960129517000147_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.topol.2007.01.018"},{"key":"S0960129517000147_ref16","doi-asserted-by":"publisher","DOI":"10.2140\/gt.2003.7.645"},{"key":"S0960129517000147_ref10","doi-asserted-by":"publisher","DOI":"10.1006\/aima.2001.2014"},{"key":"S0960129517000147_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)05135-7"},{"key":"S0960129517000147_ref41","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"S0960129517000147_ref43","unstructured":"Rezk C. (2014). Global homotopy theory and cohesion. Available at http:\/\/www.math.uiuc.edu\/~rezk\/global-cohesion.pdf."},{"key":"S0960129517000147_ref13","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1016\/j.apal.2016.04.010","article-title":"The intrinsic topology of Martin-L\u00f6f universes","volume":"167","author":"Escard\u00f3","year":"2016","journal-title":"Annals of Pure and Applied Logic"},{"key":"S0960129517000147_ref31","unstructured":"Lin Z. (2014). Answer to MathOverflow question \u2018The real numbers object in Sh(Top).\u2019 Available at http:\/\/mathoverflow.net\/a\/186165\/49."},{"key":"S0960129517000147_ref24","first-page":"1","volume-title":"Applications of Categorical Algebra","author":"Lawvere","year":"1970"},{"key":"S0960129517000147_ref21","unstructured":"Joyal A. (2008). Notes on logoi. Available at http:\/\/www.math.uchicago.edu\/~may\/IMA\/JOYAL\/Joyal.pdf."},{"key":"S0960129517000147_ref40","unstructured":"Penon J. (1985). De l'infinit\u00e9simal au local (Th\u00e9se de Doctorat d'\u00c9tat). In: Diagrammes S13. Available at http:\/\/www.numdam.org\/item?id=DIA_1985_S13_1_0, pp. 1\u2013191."},{"key":"S0960129517000147_ref15","unstructured":"Gepner D. and Kock J. (2012). Univalence in locally cartesian closed (\u221e, 1)-categories. arXiv:1208.1749."},{"key":"S0960129517000147_ref28","unstructured":"Licata D.R. and Shulman M. (2013). Calculating the fundamental group of the circle in homotopy type theory. In: LICS'13. eprint: arXiv:1301.3443."},{"key":"S0960129517000147_ref52","volume-title":"Constructivism in Mathematics. Vol. I","author":"Troelstra","year":"1988"},{"key":"S0960129517000147_ref35","unstructured":"Lurie J. (2014). Higher algebra. Available at http:\/\/www.math.harvard.edu\/~lurie\/."},{"key":"S0960129517000147_ref30","unstructured":"Licata D.R. , Shulman M. and Riley M. (2017). A fibrational framework for substructural and modal logics. To appear in FSCD '17."},{"key":"S0960129517000147_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0960129517000147_ref14","unstructured":"Frank M. (2017). Interpolating between choices for the approximate intermediate value theorem. arXiv:1701.02227."},{"key":"S0960129517000147_ref4","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-2011-05107-X"},{"key":"S0960129517000147_ref45","unstructured":"Rijke E. , Shulman M. and Spitters B. (2017). Modalities in homotopy type theory. arXiv:1706.07526."},{"key":"S0960129517000147_ref17","unstructured":"HoTT Project (2015). The homotopy type theory coq library. Available at http:\/\/github.com\/HoTT\/HoTT\/."},{"key":"S0960129517000147_ref34","doi-asserted-by":"crossref","DOI":"10.1515\/9781400830558","volume-title":"Higher Topos Theory","author":"Lurie","year":"2009"},{"key":"S0960129517000147_ref42","unstructured":"Reed J. (2009). A judgmental deconstruction of modal logic. Available at http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf."},{"key":"S0960129517000147_ref18","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-38.2.237"},{"key":"S0960129517000147_ref22","unstructured":"Kapulkin C. and Lumsdaine P.L. (2012). The simplicial model of univalent foundations (after Voevodsky). arXiv:1211.2851."},{"key":"S0960129517000147_ref19","volume-title":"Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2","author":"Johnstone","year":"2002"},{"key":"S0960129517000147_ref25","first-page":"41","article-title":"Axiomatic cohesion","volume":"19","author":"Lawvere","year":"2007","journal-title":"Theory and Applications of Categories"},{"key":"S0960129517000147_ref26","first-page":"909","article-title":"Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness","volume":"30","author":"Lawvere","year":"2015","journal-title":"Theory Applications of Categories"},{"key":"S0960129517000147_ref27","unstructured":"Licata D. and Finster E. (2014). Eilenberg\u2013MacLane spaces in homotopy type theory. In: LICS. Available at http:\/\/dlicata.web.wesleyan.edu\/pubs\/lf14em\/lf14em.pdf."},{"key":"S0960129517000147_ref32","unstructured":"Lumsdaine P.L. and Shulman M. (2017). Semantics of higher inductive types. arXiv:1705.07088."},{"key":"S0960129517000147_ref12","unstructured":"Escard\u00f3 M. (2004b). Topology via higher-order intuitionistic logic. Unfinished draft. Available at http:\/\/www.cs.bham.ac.uk\/~mhe\/papers\/index.html."},{"key":"S0960129517000147_ref23","doi-asserted-by":"crossref","unstructured":"Kraus N. (2016). Constructions with non-recursive higher inductive types. In: LICS'16.","DOI":"10.1145\/2933575.2933586"},{"key":"S0960129517000147_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2754931"},{"key":"S0960129517000147_ref36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0927-0","volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"Mac Lane","year":"1994"},{"key":"S0960129517000147_ref37","first-page":"542","volume":"29","author":"Menni","year":"2014","journal-title":"Theory and Applications of Categories"},{"key":"S0960129517000147_ref39","volume-title":"Resolution of the Uniform Lower Bound Problem in Constructive Analysis","author":"Palmgren","year":"2007"},{"key":"S0960129517000147_ref44","unstructured":"Rijke E. (2017). The join construction. arXiv:1701.07538."},{"key":"S0960129517000147_ref46","unstructured":"Schreiber U. (2013). Differential cohomology in a cohesive (\u221e, 1)-topos. Available at http:\/\/ncatlab.org\/schreiber\/show\/differential+cohomology+in+a+cohesive+topos; arXiv:1310.7930."},{"key":"S0960129517000147_ref47","unstructured":"Schreiber U. and Shulman M. (2012). Quantum gauge field theory in cohesive homotopy type theory. In: QPL'12. Available at http:\/\/ncatlab.org\/schreiber\/files\/QFTinCohesiveHoTT.pdf."},{"key":"S0960129517000147_ref48","unstructured":"Shulman M. (2011a). Internalizing the external, or the joys of codiscreteness. Available at https:\/\/golem.ph.utexas.edu\/category\/2011\/11\/internalizing_the_external_or.html."},{"key":"S0960129517000147_ref49","unstructured":"Shulman M. (2011b). Reflective subfibrations, factorization systems, and stable units. Available at https:\/\/golem.ph.utexas.edu\/category\/2011\/12\/reflective_subfibrations_facto.html."},{"key":"S0960129517000147_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"S0960129517000147_ref51","first-page":"1","article-title":"A lambda calculus for real analysis","volume":"2","author":"Taylor","year":"2010","journal-title":"Journal of Logic and Analysis"},{"key":"S0960129517000147_ref54","unstructured":"van Doorn F. (2016). Constructing the propositional truncation using non-recursive HITs. In: Certified Programs and Proofs '16. arXiv:1512.02274."},{"key":"S0960129517000147_ref55","doi-asserted-by":"crossref","DOI":"10.1142\/1047","volume-title":"Lecture Notes on Topoi and Quasitopoi","author":"Wyler","year":"1991"},{"key":"S0960129517000147_ref53","unstructured":"Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. first edition. Available at http:\/\/homotopytypetheory.org\/book\/"},{"key":"S0960129517000147_ref6","doi-asserted-by":"crossref","first-page":"756","DOI":"10.1016\/j.aim.2016.03.007","article-title":"On the homotopy type of higher orbifolds and Haefliger classifying spaces","volume":"294","author":"Carchedi","year":"2016","journal-title":"Advances in Mathematics"},{"key":"S0960129517000147_ref8","unstructured":"Dubuc E.J. and Espa\u00f1ol L. (2006). Quasitopoi over a base category. arXiv:math\/0612727."},{"key":"S0960129517000147_ref20","first-page":"51","volume":"25","author":"Johnstone","year":"2011","journal-title":"Theory and Applications of Categories"},{"key":"S0960129517000147_ref29","unstructured":"Licata D. and Shulman M. (2016). Adjoint logic with a 2-category of modes. In: LFCS '16. Available at http:\/\/dlicata.web.wesleyan.edu\/pubs\/ls15adjoint\/ls15adjoint.pdf."},{"key":"S0960129517000147_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061821"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129517000147","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T13:44:21Z","timestamp":1570023861000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129517000147\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,17]]},"references-count":55,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["S0960129517000147"],"URL":"https:\/\/doi.org\/10.1017\/s0960129517000147","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,17]]}}}