{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:56Z","timestamp":1779836756342,"version":"3.53.1"},"reference-count":57,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T00:00:00Z","timestamp":1617667200000},"content-version":"unspecified","delay-in-days":95,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <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 (HITs). 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 HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.<\/jats:p>","DOI":"10.1017\/s0956796821000034","type":"journal-article","created":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T00:02:12Z","timestamp":1617667332000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":24,"title":["Cubical Agda: A dependently typed programming language with univalence and higher inductive types"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9570-9407","authenticated-orcid":false,"given":"ANDREA","family":"VEZZOSI","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDERS","family":"M\u00d6RTBERG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDREAS","family":"ABEL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,4,6]]},"reference":[{"key":"S0956796821000034_ref46","unstructured":"Sterling, J. , Angiuli, C. & Gratzer, D. (2019) Cubical syntax for reflection-free extensional equality. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019. Leibniz International Proceedings in Informatics, LIPIcs, Geuvers, H. (ed). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing."},{"key":"S0956796821000034_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"S0956796821000034_ref55","unstructured":"Voevodsky, V. (2013) A Simple Type System with Two Identity Types. https:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/HTS.pdf."},{"key":"S0956796821000034_ref41","unstructured":"Orton, I. & Pitts, A. M. (2016) Axioms for modelling cubical type theory in a topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). LIPIcs 62, pp. 24:1\u201324:19."},{"key":"S0956796821000034_ref57","unstructured":"Wood, J. (2019) Vectors and Matrices in Agda. Blog post at https:\/\/personal.cis.strath.ac.uk\/james.wood.100\/blog\/html\/VecMat.html."},{"key":"S0956796821000034_ref53","unstructured":"Vezzosi, A. (2017) Streams for Cubical Type Theory. http:\/\/saizan.github.io\/streams-ctt.pdf."},{"key":"S0956796821000034_ref50","unstructured":"The RedPRL Development Team. (2018) The redtt Proof Assistant."},{"key":"S0956796821000034_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394760"},{"key":"S0956796821000034_ref28","unstructured":"de Moura, L. , Kong, S. , Avigad, J. , van Doorn, F. & von Raumer, J. (2015) The lean theorem prover. In Automated Deduction - CADE-25, 25th International Conference on Automated Deduction, Berlin, Germany, August 1\u20137, 2015, Proceedings."},{"key":"S0956796821000034_ref38","unstructured":"Martin-L\u00f6f, P. (1975) An intiutionistic theory of types: Predicative part. In Logic Colloquium\u201973, Rose, H. E. & Shepherdson, J. (eds). Amsterdam: North\u2013Holland, pp. 73\u2013118."},{"key":"S0956796821000034_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"S0956796821000034_ref29","unstructured":"Escard\u00f3, M. H. (2019) Introduction to Univalent Foundations of Mathematics with Agda."},{"key":"S0956796821000034_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"S0956796821000034_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3236770"},{"key":"S0956796821000034_ref8","unstructured":"Angiuli, C. , Cavallo, E. , M\u00c3\u00b6rtberg, A. & Zeuner, M. (2020) Internalizing Representation Independence with Univalence. Preprint arXiv:2009.05547v2 [cs.PL]."},{"key":"S0956796821000034_ref36","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"S0956796821000034_ref4","unstructured":"Ahrens, B. , Capriotti, P. & Spadotti, R. (2015) Non-wellfounded trees in homotopy type theory. CoRR abs\/1504.02949."},{"key":"S0956796821000034_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000198"},{"key":"S0956796821000034_ref13","unstructured":"Bickford, M. (2018) Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. CoRR abs\/1806.06114."},{"key":"S0956796821000034_ref23","unstructured":"Cohen, C. , D\u00e9n\u00e8s, M. & M\u00f6rtberg, A. (2013) Refinements for free! In Certified Programs and Proofs, Gonthier, G. & Norrish, M. (eds). Lecture Notes in Computer Science, vol. 8307. Springer International Publishing, pp. 147\u2013162."},{"key":"S0956796821000034_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3236787"},{"key":"S0956796821000034_ref3","unstructured":"Agda Development Team. (2018) Agda 2.5.4.2 Documentation."},{"key":"S0956796821000034_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373814"},{"key":"S0956796821000034_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_9"},{"key":"S0956796821000034_ref7","unstructured":"Angiuli, C. , Brunerie, G. , Coquand, T. , Hou (Favonia), K.-B., Harper, R. & Licata, D. R. (2019) Syntax and Models of Cartesian Cubical Type Theory. Preprint."},{"key":"S0956796821000034_ref22","unstructured":"Cohen, C. , Coquand, T. , Huber, S. & M\u00f6rtberg, A. (2018) Cubical type theory: A constructive interpretation of the univalence axiom. In Types for Proofs and Programs (TYPES 2015). LIPIcs, vol. 69, pp. 5:1\u20135:34."},{"key":"S0956796821000034_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373825"},{"key":"S0956796821000034_ref44","unstructured":"Sattler, C. (2018) Do cubical models of type theory also model homotopy types? Talk given at Types, Homotopy Type Theory, and Verification at the Hausdorff Center for Mathematics in Bonn."},{"key":"S0956796821000034_ref42","unstructured":"Riehl, E. (2019) The equivariant uniform Kan fibration model of cubical homotopy type theory. Talk given at The International Conference on Homotopy Type Theory (HoTT 2019) at Carnegie Mellon University."},{"key":"S0956796821000034_ref16","unstructured":"Brunerie, G. (2016) On the Homotopy Groups of Spheres in Homotopy Type Theory. PhD thesis, Universit\u00e9 de Nice."},{"key":"S0956796821000034_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"S0956796821000034_ref10","unstructured":"Angiuli, C. , Hou (Favonia), K.-B. & Harper, R. (2018) Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Ghica, D. & Jung, A. (eds), Leibniz International Proceedings in Informatics (LIPIcs), vol. 119. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, pp. 6:1\u20136:17."},{"key":"S0956796821000034_ref33","unstructured":"Kapulkin, C. & Lumsdaine, P. L. (2012) The Simplicial Model of Univalent Foundations (after Voevodsky). Preprint arXiv:1211.2851v4."},{"key":"S0956796821000034_ref32","unstructured":"Huber, S. (2017) A Cubical Type Theory for Higher Inductive Types."},{"key":"S0956796821000034_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681800014X"},{"key":"S0956796821000034_ref5","unstructured":"Altenkirch, T. , McBride, C. & Swierstra, W. (2007) Observational equality, now! In PLPV\u201907: Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification. ACM, pp. 57\u201368."},{"key":"S0956796821000034_ref34","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.19"},{"key":"S0956796821000034_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S0956796821000034_ref1","unstructured":"Abel, A. , \u00d6hman, J. & Vezzosi, A. (2017) Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. 2(POPL), 23:1\u201323:29."},{"key":"S0956796821000034_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062348"},{"key":"S0956796821000034_ref37","unstructured":"Lumsdaine, P. L. & Shulman, M. (2017) Semantics of Higher Inductive Types. Preprint arXiv:1705.07088."},{"key":"S0956796821000034_ref27","unstructured":"Danielsson, N. A. (2020) Higher Inductive Type Eliminators Without Paths. http:\/\/www.cse.chalmers.se\/nad\/publications\/danielsson-hits-without-paths.html."},{"key":"S0956796821000034_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3290314"},{"key":"S0956796821000034_ref26","unstructured":"Coquand, T. , Huber, S. & Sattler, C. (2019) Homotopy Canonicity for Cubical Type Theory. Preprint available at http:\/\/www.cse.chalmers.se\/ simonhu\/papers\/can.pdf."},{"key":"S0956796821000034_ref12","unstructured":"Annenkov, D. , Capriotti, P. & Kraus, N. (2017) Two-Level Type Theory and Applications."},{"key":"S0956796821000034_ref43","doi-asserted-by":"crossref","first-page":"147","DOI":"10.21136\/HS.2017.06","article-title":"A type theory for synthetic \u00a5-categories","volume":"1","author":"Riehl","year":"2017","journal-title":"Higher Struct."},{"key":"S0956796821000034_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009861"},{"key":"S0956796821000034_ref31","unstructured":"Huber, S. (2016) Canonicity for Cubical Type Theory. Preprint arXiv:1607.04156."},{"key":"S0956796821000034_ref49","unstructured":"Team, T. C. D. (2019) The Coq Proof Assistant, version 8.9.0."},{"key":"S0956796821000034_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.indag.2013.09.002"},{"key":"S0956796821000034_ref51","unstructured":"Univalent Foundations Program, T. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics."},{"key":"S0956796821000034_ref35","unstructured":"Licata, D. R. , Orton, I. , Pitts, A. M. & Spitters, B. (2018) Internal universes in models of homotopy type theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9\u201312, 2018, Oxford, UK, Kirchner, H. (ed). LIPIcs, vol. 108. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 22:1\u201322:17."},{"key":"S0956796821000034_ref21","unstructured":"Cohen, C. , Coquand, T. , Huber, S. & M\u00f6rtberg, A. (2015) Cubicaltt. https:\/\/github.com\/mortberg\/cubicaltt."},{"key":"S0956796821000034_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2992783"},{"key":"S0956796821000034_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373835"},{"key":"S0956796821000034_ref56","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000577"},{"key":"S0956796821000034_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9471-7"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796821000034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:54Z","timestamp":1779835014000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796821000034\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":57,"alternative-id":["S0956796821000034"],"URL":"https:\/\/doi.org\/10.1017\/s0956796821000034","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e8"}}