{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:44:23Z","timestamp":1752230663173,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373825","type":"proceedings-article","created":{"date-parts":[[2020,2,4]],"date-time":"2020-02-04T14:20:45Z","timestamp":1580826045000},"page":"158-171","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Cubical synthetic homotopy theory"],"prefix":"10.1145","author":[{"given":"Anders","family":"M\u00f6rtberg","sequence":"first","affiliation":[{"name":"Stockholm University, Sweden"}]},{"given":"Lo\u00efc","family":"Pujet","sequence":"additional","affiliation":[{"name":"Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Agda development team. 2019. Agda 2.6.0.1 documentation. https: \/\/agda.readthedocs.io\/en\/v2.6.0.1\/  Agda development team. 2019. Agda 2.6.0.1 documentation. https: \/\/agda.readthedocs.io\/en\/v2.6.0.1\/"},{"key":"e_1_3_2_1_2_1","volume-title":"Licata","author":"Angiuli Carlo","year":"2019","unstructured":"Carlo Angiuli , Guillaume Brunerie , Thierry Coquand , Kuen-Bang Hou (Favonia), Robert Harper , and Daniel R . Licata . 2019 . Syntax and Models of Cartesian Cubical Type Theory. (February 2019). https: \/\/github.com\/dlicata335\/cart-cube Preprint . Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. 2019. Syntax and Models of Cartesian Cubical Type Theory. (February 2019). https: \/\/github.com\/dlicata335\/cart-cube Preprint."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.6"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_3_2_1_6_1","volume-title":"Computer-generated proofs for the monoidal structure of the smash product. (Nov","author":"Brunerie Guillaume","year":"2018","unstructured":"Guillaume Brunerie . 2018. Computer-generated proofs for the monoidal structure of the smash product. (Nov . 2018 ). https:\/\/ www.uwo.ca\/math\/faculty\/kapulkin\/seminars\/hottest.html Homotopy Type Theory Electronic Seminar Talks . Guillaume Brunerie. 2018. Computer-generated proofs for the monoidal structure of the smash product. (Nov. 2018). https:\/\/ www.uwo.ca\/math\/faculty\/kapulkin\/seminars\/hottest.html Homotopy Type Theory Electronic Seminar Talks."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209188"},{"volume-title":"Synthetic cohomology in homotopy type theory. Master\u2019s thesis","author":"Cavallo Evan","key":"e_1_3_2_1_8_1","unstructured":"Evan Cavallo . 2015. Synthetic cohomology in homotopy type theory. Master\u2019s thesis . Carnegie Mellon University . Evan Cavallo. 2015. Synthetic cohomology in homotopy type theory. Master\u2019s thesis. Carnegie Mellon University."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290314"},{"key":"e_1_3_2_1_10_1","volume-title":"https:\/\/github.com\/mortberg\/cubicaltt","author":"Cohen Cyril","year":"2015","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2015. Cubicaltt. ( 2015 ). https:\/\/github.com\/mortberg\/cubicaltt . Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2015. Cubicaltt. (2015). https:\/\/github.com\/mortberg\/cubicaltt ."},{"key":"e_1_3_2_1_11_1","volume-title":"Types for Proofs and Programs (TYPES 2015)","volume":"69","author":"Cohen Cyril","year":"2018","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2018 . Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom . In Types for Proofs and Programs (TYPES 2015) (LIPIcs), Vol. 69 . 5:1\u20135:34. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Types for Proofs and Programs (TYPES 2015) (LIPIcs), Vol. 69. 5:1\u20135:34."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_3_2_1_13_1","volume-title":"31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916","author":"Kuen-Bang","year":"2016","unstructured":"Kuen-Bang Hou (Favonia), Eric Finster , Daniel R. Licata , and Peter LeFanu Lumsdaine . 2016 . A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory . In 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916 . ACM, 565\u2013574. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. 2016. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916. ACM, 565\u2013574."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.22"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9469-1"},{"key":"e_1_3_2_1_16_1","volume-title":"The Simplicial Model of Univalent Foundations (after Voevodsky). (Nov","author":"Kapulkin Chris","year":"2012","unstructured":"Chris Kapulkin and Peter LeFanu Lumsdaine . 2012. The Simplicial Model of Univalent Foundations (after Voevodsky). (Nov . 2012 ). Preprint arXiv:1211.2851v4. Chris Kapulkin and Peter LeFanu Lumsdaine. 2012. The Simplicial Model of Univalent Foundations (after Voevodsky). (Nov. 2012). Preprint arXiv:1211.2851v4."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_18_1","volume-title":"Licata and Guillaume Brunerie","author":"Daniel","year":"2013","unstructured":"Daniel R. Licata and Guillaume Brunerie . 2013 . \u03c0\u03b7 (\u0405\u03b7?) in Homotopy Type Theory. In Certified Programs and Proofs, Georges Gonthier and Michael Norrish (Eds.). Springer International Publishing , 1?16. Daniel R. Licata and Guillaume Brunerie. 2013. \u03c0\u03b7 (\u0405\u03b7?) in Homotopy Type Theory. In Certified Programs and Proofs, Georges Gonthier and Michael Norrish (Eds.). Springer International Publishing, 1?16."},{"volume-title":"30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201915","author":"Daniel","key":"e_1_3_2_1_19_1","unstructured":"Daniel R. Licata and Guillaume Brunerie. 2015. A Cubical Approach to Synthetic Homotopy Theory . In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201915 . ACM, 92\u2013103. Daniel R. Licata and Guillaume Brunerie. 2015. A Cubical Approach to Synthetic Homotopy Theory. In 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201915. ACM, 92\u2013103."},{"volume-title":"Logic Colloquium \u201973","author":"Martin-L\u00f6f Per","key":"e_1_3_2_1_20_1","unstructured":"Per Martin-L\u00f6f . 1975. An Intiutionistic Theory of Types: Predicative Part . In Logic Colloquium \u201973 , H. E. Rose and J. Shepherdson (Eds.). North\u2013Holland , Amsterdam , 73\u2013118. Per Martin-L\u00f6f. 1975. An Intiutionistic Theory of Types: Predicative Part. In Logic Colloquium \u201973, H. E. Rose and J. Shepherdson (Eds.). North\u2013Holland, Amsterdam, 73\u2013118."},{"key":"e_1_3_2_1_21_1","volume-title":"The equivariant uniform Kan fibration model of cubical homotopy type theory. (Aug","author":"Riehl Emily","year":"2019","unstructured":"Emily Riehl . 2019. The equivariant uniform Kan fibration model of cubical homotopy type theory. (Aug . 2019 ). https:\/\/hott.github.io\/ HoTT-2019\/\/programme\/#riehl Talk given at The International Conference on Homotopy Type Theory (HoTT 2019) at Carnegie Mellon University . Emily Riehl. 2019. The equivariant uniform Kan fibration model of cubical homotopy type theory. (Aug. 2019). https:\/\/hott.github.io\/ HoTT-2019\/\/programme\/#riehl Talk given at The International Conference on Homotopy Type Theory (HoTT 2019) at Carnegie Mellon University."},{"key":"e_1_3_2_1_22_1","unstructured":"Egbert Rijke. 2017. The join construction. (2017). Preprint arXiv:1701.07538v1.  Egbert Rijke. 2017. The join construction. (2017). Preprint arXiv:1701.07538v1."},{"key":"e_1_3_2_1_23_1","volume-title":"Do cubical models of type theory also model homotopy types?","author":"Sattler Christian","year":"2018","unstructured":"Christian Sattler . 2018. Do cubical models of type theory also model homotopy types? ( 2018 ). https:\/\/www.him.unibonn.de\/programs\/past-programs\/past-trimester-programs\/typessets-constructions\/workshop-types-homotopy-type-theory-andverification\/schedule\/#c13292 Talk given at Types, Homotopy Type theory, and Verification at the Hausdorff Center for Mathematics in Bonn. Christian Sattler. 2018. Do cubical models of type theory also model homotopy types? (2018). https:\/\/www.him.unibonn.de\/programs\/past-programs\/past-trimester-programs\/typessets-constructions\/workshop-types-homotopy-type-theory-andverification\/schedule\/#c13292 Talk given at Types, Homotopy Type theory, and Verification at the Hausdorff Center for Mathematics in Bonn."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2992783"},{"key":"e_1_3_2_1_25_1","unstructured":"The RedPRL Development Team. 2018. The red tt Proof Assistant. https:\/\/github.com\/RedPRL\/redtt\/  The RedPRL Development Team. 2018. The red tt Proof Assistant. https:\/\/github.com\/RedPRL\/redtt\/"},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","key":"e_1_3_2_1_26_1","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics . Institute for Advanced Study . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_30"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_2_1_30_1","volume-title":"The equivalence axiom and univalent models of type theory. (Talk at CMU on","author":"Voevodsky Vladimir","year":"2010","unstructured":"Vladimir Voevodsky . 2014. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010 ). (2014). Preprint arXiv:1402.5556. Vladimir Voevodsky. 2014. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010). (2014). Preprint arXiv:1402.5556."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000577"}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"New Orleans LA USA","acronym":"POPL '20"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373825","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373825","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373825"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":29,"alternative-id":["10.1145\/3372885.3373825","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373825","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}