{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:36Z","timestamp":1780994676932,"version":"3.54.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"VR","award":["2014-04864"],"award-info":[{"award-number":["2014-04864"]}]},{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"crossref","award":["2016-06828"],"award-info":[{"award-number":["2016-06828"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.<\/jats:p>","DOI":"10.1145\/3341691","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":50,"title":["Cubical agda: a dependently typed programming language with univalence and higher inductive types"],"prefix":"10.1145","volume":"3","author":[{"given":"Andrea","family":"Vezzosi","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[{"name":"Stockholm University, Sweden \/ Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Abel","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden \/ University of Gothenburg, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"e_1_2_2_3_1","unstructured":"Agda development team. 2018. Agda 2.5.4.2 documentation. http:\/\/agda.readthedocs.io\/en\/v2.5.4.2\/  Agda development team. 2018. Agda 2.5.4.2 documentation. http:\/\/agda.readthedocs.io\/en\/v2.5.4.2\/"},{"key":"e_1_2_2_4_1","volume-title":"Non-wellfounded trees in Homotopy Type Theory. CoRR abs\/1504.02949","author":"Ahrens Benedikt","year":"2015"},{"key":"e_1_2_2_5_1","unstructured":"Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. (2006). Unpublished draft.  Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. (2006). Unpublished draft."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_2_2_7_1","volume-title":"Licata","author":"Angiuli Carlo","year":"2019"},{"key":"e_1_2_2_8_1","unstructured":"Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. (2017). Preprint arXiv:1712.01800v1.  Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2017. Computational Higher Type Theory III: Univalent Universes and Exact Equality. (2017). Preprint arXiv:1712.01800v1."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209153"},{"key":"e_1_2_2_10_1","volume-title":"Homotopical patch theory. Journal of Functional Programming 26","author":"Angiuli Carlo","year":"2016"},{"key":"e_1_2_2_11_1","unstructured":"Danil Annenkov Paolo Capriotti and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. (2017). https:\/\/arxiv. org\/abs\/1705.03307  Danil Annenkov Paolo Capriotti and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. (2017). https:\/\/arxiv. org\/abs\/1705.03307"},{"key":"e_1_2_2_12_1","volume-title":"Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. CoRR abs\/1806.06114","author":"Bickford Mark","year":"2018"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290314"},{"key":"e_1_2_2_16_1","first-page":"6","article-title":"HoTTSQL","volume":"52","author":"Chu Shumo","year":"2017","journal-title":"Proving Query Rewrites with Univalent SQL Semantics. SIGPLAN Not."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236770"},{"key":"e_1_2_2_18_1","volume-title":"https:\/\/github.com\/mortberg\/ cubicaltt","author":"Cohen Cyril","year":"2015"},{"key":"e_1_2_2_19_1","volume-title":"Types for Proofs and Programs (TYPES 2015)","volume":"69","author":"Cohen Cyril","year":"2018"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.indag.2013.09.002"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_2_23_1","unstructured":"Thierry Coquand Simon Huber and Christian Sattler. 2019. Homotopy canonicity for cubical type theory. (2019). Preprint available at http:\/\/www.cse.chalmers.se\/ simonhu\/papers\/can.pdf.  Thierry Coquand Simon Huber and Christian Sattler. 2019. Homotopy canonicity for cubical type theory. (2019). Preprint available at http:\/\/www.cse.chalmers.se\/ simonhu\/papers\/can.pdf."},{"key":"e_1_2_2_24_1","volume-title":"25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings.","author":"de Moura Leonardo","year":"2015"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9469-1"},{"key":"e_1_2_2_26_1","unstructured":"Simon Huber. 2017. A Cubical Type Theory for Higher Inductive Types. (2017). http:\/\/www.cse.chalmers.se\/~simonhu\/ misc\/hcomp.pdf  Simon Huber. 2017. A Cubical Type Theory for Higher Inductive Types. (2017). http:\/\/www.cse.chalmers.se\/~simonhu\/ misc\/hcomp.pdf"},{"key":"e_1_2_2_27_1","volume-title":"The Simplicial Model of Univalent Foundations (after Voevodsky). (Nov","author":"Kapulkin Chris","year":"2012"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.19"},{"key":"e_1_2_2_29_1","volume-title":"Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","volume":"108","author":"Licata Daniel R.","year":"2018"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_2_2_31_1","volume-title":"Semantics of higher inductive types. (May","author":"LeFanu Lumsdaine Peter","year":"2017"},{"key":"e_1_2_2_32_1","volume-title":"Logic Colloquium \u201973","author":"Martin-L\u00f6f Per"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1812941.1812953"},{"key":"e_1_2_2_34_1","volume-title":"25th EACSL Annual Conference on Computer Science Logic (CSL 2016)","volume":"62","author":"Orton Ian"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2992783"},{"key":"e_1_2_2_37_1","volume-title":"Carlo Angiuli, and Daniel Gratzer","author":"Sterling Jonathan","year":"2019"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"e_1_2_2_39_1","unstructured":"The Coq Development Team. 2019. The Coq Proof Assistant version 8.9.0.  The Coq Development Team. 2019. The Coq Proof Assistant version 8.9.0."},{"key":"e_1_2_2_40_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\/"},{"key":"e_1_2_2_41_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent"},{"key":"e_1_2_2_42_1","unstructured":"Andrea Vezzosi. 2017. Streams for Cubical Type Theory. (2017). http:\/\/saizan.github.io\/streams-ctt.pdf .  Andrea Vezzosi. 2017. Streams for Cubical Type Theory. (2017). http:\/\/saizan.github.io\/streams-ctt.pdf ."},{"key":"e_1_2_2_43_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https:\/\/www.math.ias.edu\/vladimir\/sites\/ math.ias.edu.vladimir\/files\/HTS.pdf  Vladimir Voevodsky. 2013. A simple type system with two identity types. (2013). https:\/\/www.math.ias.edu\/vladimir\/sites\/ math.ias.edu.vladimir\/files\/HTS.pdf"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000577"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341691","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":43,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341691"],"URL":"https:\/\/doi.org\/10.1145\/3341691","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}