{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T22:41:41Z","timestamp":1776724901518,"version":"3.51.2"},"reference-count":60,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2022,1,17]],"date-time":"2022-01-17T00:00:00Z","timestamp":1642377600000},"content-version":"unspecified","delay-in-days":291,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing \u03a0, \u03a3, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and M\u00f6rtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, \u03a0, \u03a3, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.<\/jats:p>","DOI":"10.1017\/s0960129521000347","type":"journal-article","created":{"date-parts":[[2022,1,17]],"date-time":"2022-01-17T05:40:17Z","timestamp":1642398017000},"page":"424-468","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":23,"title":["Syntax and models of Cartesian cubical type theory"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9590-3303","authenticated-orcid":false,"given":"Carlo","family":"Angiuli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Brunerie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-5153","authenticated-orcid":false,"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2310-3673","authenticated-orcid":false,"given":"Kuen-Bang","family":"Hou (Favonia)","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0697-7405","authenticated-orcid":false,"given":"Daniel R.","family":"Licata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,1,17]]},"reference":[{"key":"S0960129521000347_ref8","unstructured":"Awodey, S. (2016). Notes on cubical sets. Available from https:\/\/github.com\/awodey\/math\/blob\/master\/Cubical\/cubical.pdf."},{"key":"S0960129521000347_ref4","volume-title":"Computational higher type theory I: abstract cubical realizability","author":"Angiuli","year":"2016"},{"key":"S0960129521000347_ref22","doi-asserted-by":"crossref","unstructured":"Cavallo, E. and Harper, R. (2019). Higher inductive types in cubical computational type theory. Proceedings of the ACM on Programming Languages 3 (POPL) 1:1\u20131:27.","DOI":"10.1145\/3290314"},{"key":"S0960129521000347_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2017.02.013"},{"key":"S0960129521000347_ref36","unstructured":"Hofmann, M. (1995). Extensional Concepts in Intensional Type Theory. Phd thesis, University of Edinburgh."},{"key":"S0960129521000347_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009861"},{"key":"S0960129521000347_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9469-1"},{"key":"S0960129521000347_ref53","volume-title":"All (Y,1)-toposes have strict univalent universes","author":"Shulman","year":"2019"},{"key":"S0960129521000347_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009861"},{"key":"S0960129521000347_ref50","doi-asserted-by":"crossref","first-page":"147","DOI":"10.21136\/HS.2017.06","article-title":"A type theory for synthetic Y-categories","volume":"1","author":"Riehl","year":"2017","journal-title":"Higher Structures"},{"key":"S0960129521000347_ref52","unstructured":"Sattler, C. (2018). Do cubical models of type theory also model homotopy types? Talk at Workshop on Types, Homotopy Type theory, and Verification at Hausdorff Institute."},{"key":"S0960129521000347_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.08.002"},{"key":"S0960129521000347_ref11","first-page":"130","article-title":"Formalization of mathematics in type theory (Dagstuhl Seminar 18341)","volume":"8","author":"Bauer","year":"2019","journal-title":"Dagstuhl Reports"},{"key":"S0960129521000347_ref15","unstructured":"Bezem, M. , Coquand, T. and Huber, S. (2014). A model of type theory in cubical sets. In: Matthes, R. and Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs (TYPES 2013), 107\u2013128."},{"key":"S0960129521000347_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9472-6"},{"key":"S0960129521000347_ref17","unstructured":"Bickford, M. (2020). Formalization of cubical type theory in Nuprl. http:\/\/nuprl.org\/KB\/show.php?ID=774."},{"key":"S0960129521000347_ref19","unstructured":"Brunerie, G. and Licata, D. R. (2014). A cubical infinite-dimensional type theory. Talk at Oxford Workshop on Homotopy Type Theory."},{"key":"S0960129521000347_ref20","doi-asserted-by":"crossref","unstructured":"Buchholtz, U. and Morehouse, E. (2017). Varieties of cubical sets. In: Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15\u201318, 2017, Proceedings. Springer International Publishing.","DOI":"10.1007\/978-3-319-57418-9_5"},{"key":"S0960129521000347_ref21","unstructured":"Cavallo, E. (2021). Higher Inductive Types and Internal Parametricity for Cubical Type Theory. Phd thesis, Carnegie Mellon University. Technical Report CMU-CS-21-100. Available from http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2021\/CMU-CS-21-100.pdf."},{"key":"S0960129521000347_ref29","unstructured":"Coquand, T. (2015). Higher inductive types as cubical sets. Available from http:\/\/www.cse.chalmers.se\/coquand\/hit1.pdf."},{"key":"S0960129521000347_ref32","volume-title":"Constructive sheaf models of type theory","author":"Coquand","year":"2019"},{"key":"S0960129521000347_ref2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.1"},{"key":"S0960129521000347_ref3","volume-title":"Computational higher type theory II: dependent cubical realizability","author":"Angiuli","year":"2017"},{"key":"S0960129521000347_ref28","unstructured":"Coquand, T. (2014b). Variations on cubical sets (diagonals version). Available from http:\/\/www.cse.chalmers.se\/coquand\/diag.pdf."},{"key":"S0960129521000347_ref37","unstructured":"Hofmann, M. and Streicher, T. (1997). Lifting Grothendieck universes. Available from http:\/\/www.mathematik.tu-darmstadt.de\/streicher\/NOTES\/lift.pdf."},{"key":"S0960129521000347_ref39","unstructured":"Isaev, V. (2014). Homotopy type theory with an interval type. Available from https:\/\/valis.github.io\/doc.pdf."},{"key":"S0960129521000347_ref1","unstructured":"Angiuli, C. (2019). Computational Semantics of Cartesian Cubical Type Theory. Phd thesis, Carnegie Mellon University. Technical Report CMU-CS-19-127. Available from http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2019\/abstracts\/19-127.html."},{"key":"S0960129521000347_ref35","doi-asserted-by":"crossref","unstructured":"Harper, R. and Angiuli, C. (2018). Computational (higher) type theory. Tutorial at POPL 2018.","DOI":"10.1145\/3009837.3009861"},{"key":"S0960129521000347_ref44","unstructured":"Orton, I. and Pitts, A. M. (2016). Axioms for modelling cubical type theory in a topos. In: Talbot, J.-M. and Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 24:1\u201324:19."},{"key":"S0960129521000347_ref26","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"Constable","year":"1986"},{"key":"S0960129521000347_ref45","unstructured":"Orton, I. and Pitts, A. M. (2018). Axioms for modelling cubical type theory in a topos (extended version). Logical Methods in Computer Science 14 (4:23) 1\u201333."},{"key":"S0960129521000347_ref54","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"S0960129521000347_ref55","unstructured":"Sterling, J. , Angiuli, C. and Gratzer, D. (2019). Cubical syntax for reflection-free extensional equality. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Leibniz International Proceedings in Informatics (LIPIcs), vol. 131, Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 31:1\u201331:25."},{"key":"S0960129521000347_ref56","first-page":"1","article-title":"An algebraic weak factorization system on 01-substitution sets: a constructive proof","volume":"8","author":"Swan","year":"2016","journal-title":"Journal of Logic and Analysis"},{"key":"S0960129521000347_ref59","volume-title":"A very short note on homotopy l-calculus","author":"Voevodsky","year":"2006"},{"key":"S0960129521000347_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394794"},{"key":"S0960129521000347_ref40","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.41.12.1092"},{"key":"S0960129521000347_ref46","doi-asserted-by":"publisher","DOI":"10.17863\/CAM.35681"},{"key":"S0960129521000347_ref57","unstructured":"The Univalent Foundations Program, Institute for Advanced Study (2013). Homotopy Type Theory: Univalent Foundations Of Mathematics. Available from homotopytypetheory.org\/book."},{"key":"S0960129521000347_ref27","unstructured":"Coquand, T. (2014a). Variations on cubical sets. Talk at Oxford Workshop on Homotopy Type Theory. Available from http:\/\/www.cse.chalmers.se\/coquand\/comp.pdf."},{"key":"S0960129521000347_ref42","unstructured":"Licata, D. (2016). Weak univalence with \u201cbeta\u201d implies full univalence. Email to Homotopy Type Theory mailing list. https:\/\/groups.google.com\/d\/msg\/homotopytypetheory\/j2KBIvDw53s\/YTDK4D0NFQAJ."},{"key":"S0960129521000347_ref12","volume-title":"Naive cubical type theory","author":"Bentzen","year":"2019"},{"key":"S0960129521000347_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9471-7"},{"key":"S0960129521000347_ref24","article-title":"Les pr\u00c9faisceaux comme mod\u00c8les des types d\u2019homotopie","volume":"308","author":"Cisinski","year":"2006","journal-title":"Ast\u00c9risque, Soc. Math. France"},{"key":"S0960129521000347_ref13","doi-asserted-by":"crossref","unstructured":"Bernardy, J.-P. , Coquand, T. and Moulin, G. (2015). A presheaf model of parametric type theory. In: Mathematical Foundations of Programming Semantics.","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"S0960129521000347_ref43","unstructured":"Licata, D. R. , Orton, I. , Pitts, A. M. and Spitters, B. (2018). Internal universes in models of homotopy type theory. In: Formal Structures for Computation and Deduction (FSCD). arXiv:1801.07664."},{"key":"S0960129521000347_ref48","unstructured":"Pitts, A. M. (2015). Nominal presentation of cubical sets models of type theory. In: 20th International Conference on Types for Proofs and Programs (TYPES 2014). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik."},{"key":"S0960129521000347_ref49","unstructured":"Riehl, E. (2019). The equivariant uniform Kan fibration model of cubical homotopy type theory. Talk at the International Conference on Homotopy Type Theory (HoTT 2019)."},{"key":"S0960129521000347_ref58","doi-asserted-by":"crossref","unstructured":"Vezzosi, A. , M\u00d6rtberg, A. and Abel, A. (2019). Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Proceedings of the ACM on Programming Languages 3 (ICFP) 87:1\u201387:29.","DOI":"10.1145\/3341691"},{"key":"S0960129521000347_ref25","unstructured":"Cohen, C. , Coquand, T. , Huber, S. and M\u00d6rtberg, A. (2018). Cubical type theory: a constructive interpretation of the univalence axiom. In: Uustalu, T. (ed.) 21st International Conference on Types for Proofs and Programs (TYPES 2015), 5:1\u20135:34."},{"key":"S0960129521000347_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"S0960129521000347_ref31","unstructured":"Coquand, T. , Huber, S. and Sattler, C. (2019a). Homotopy canonicity for cubical type theory. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Leibniz International Proceedings in Informatics (LIPIcs), vol. 131, Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 11:1\u201311:23."},{"key":"S0960129521000347_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.01.035"},{"key":"S0960129521000347_ref7","unstructured":"Angiuli, C. , Hou (Favonia), K.-B. and Harper, R. (2018b). Cartesian cubical computational type theory: constructive reasoning with paths and equalities. In: Computer Science Logic."},{"key":"S0960129521000347_ref51","volume-title":"The equivalence extension property and model structures","author":"Sattler","year":"2017"},{"key":"S0960129521000347_ref9","unstructured":"Awodey, S. (2018a). An algebraic fibrant replacement for cubical sets. Talk at Category Theory OctoberFest."},{"key":"S0960129521000347_ref23","unstructured":"Cavallo, E. , M\u00d6rtberg, A. and Swan, A. W. (2020). Unifying cubical models of univalent type theory. In: Fern\u00c1ndez, M. and Muscholl, A. (eds.) 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), Leibniz International Proceedings in Informatics (LIPIcs), vol. 152, Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 14:1\u201314:17."},{"key":"S0960129521000347_ref41","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"},{"key":"S0960129521000347_ref34","unstructured":"Harper, R. (2018). Computational type theory. Lectures at Oregon Programming Languages Summer School 2018."},{"key":"S0960129521000347_ref47","doi-asserted-by":"publisher","DOI":"10.17863\/CAM.36690"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000347","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T04:39:58Z","timestamp":1674448798000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000347\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["S0960129521000347"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000347","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}