{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:24Z","timestamp":1747173444631,"version":"3.40.5"},"reference-count":21,"publisher":"Cambridge University Press (CUP)","issue":"10","license":[{"start":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T00:00:00Z","timestamp":1647302400000},"content-version":"unspecified","delay-in-days":134,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman\u2013Hilton duality.<\/jats:p>","DOI":"10.1017\/s096012952200007x","type":"journal-article","created":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T11:58:47Z","timestamp":1647345527000},"page":"1205-1231","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Naive cubical type theory"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5987-7806","authenticated-orcid":false,"given":"Bruno","family":"Bentzen","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,3,15]]},"reference":[{"year":"2002","author":"Constable","key":"S096012952200007X_ref12"},{"key":"S096012952200007X_ref1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T. (2019). Na\u00efve type theory. In: Reflections on the Foundations of Mathematics, Springer, 101\u2013136. https:\/\/doi.org\/10.1007\/978-3-030-15655-8_5.","DOI":"10.1007\/978-3-030-15655-8_5"},{"key":"S096012952200007X_ref15","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1017\/S1755020316000460","article-title":"Universes and univalence in homotopy type theory","volume":"3","author":"Ladyman","year":"2019","journal-title":"The Review of Symbolic Logic"},{"key":"S096012952200007X_ref14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-1645-0","volume-title":"Naive Set Theory","author":"Halmos","year":"1974"},{"key":"S096012952200007X_ref8","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), Leibniz International Proceedings in Informatics (LIPIcs), vol. 26, Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 107\u2013128."},{"key":"S096012952200007X_ref6","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S0305004108001783","article-title":"Homotopy theoretic models of identity types","volume":"146","author":"Awodey","year":"2009","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"S096012952200007X_ref5","doi-asserted-by":"crossref","first-page":"1270","DOI":"10.1016\/j.apal.2018.08.002","article-title":"A cubical model of homotopy type theory","volume":"169","author":"Awodey","year":"2018","journal-title":"Annals of Pure and Applied Logic"},{"key":"S096012952200007X_ref2","unstructured":"Angiuli, C. (2019). Computational Semantics of Cartesian Cubical Type Theory. Phd thesis, Carnegie Mellon University. https:\/\/www.cs.cmu.edu\/cangiuli\/thesis\/thesis.pdf."},{"key":"S096012952200007X_ref18","unstructured":"The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics. https:\/\/homotopytypetheory.org\/book\/."},{"key":"S096012952200007X_ref11","unstructured":"Cohen, C. , Coquand, T. , Huber, S. and M\u00f6rtberg, 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), Leibniz International Proceedings in Informatics (LIPIcs), vol. 69, Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 5:1\u20135:34."},{"key":"S096012952200007X_ref20","unstructured":"Voevodsky, V. (2006). A very short note on the homotopy $\\lambda$ -calculus. http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda.pdf. Unpublished note."},{"key":"S096012952200007X_ref10","unstructured":"Cavallo, E. and Harper, R. (2018). Computational Higher Type Theory IV: Inductive Types. https:\/\/arxiv.org\/pdf\/1801.01568.pdf. Preprint."},{"key":"S096012952200007X_ref21","unstructured":"Voevodsky, V. (2009). Notes on type systems. https:\/\/www.math.ias.edu~\/vladimir\/Site3\/Univalent_Foundations_files\/expressions_current.pdf. Unpublished note."},{"key":"S096012952200007X_ref9","unstructured":"Brunerie, G. , Ljungstr\u00f6m, A. and M\u00f6rtberg, A. (2021). Synthetic cohomology theory in cubical agda. https:\/\/staff.math.su.se\/anders.mortberg\/papers\/zcohomology.pdf."},{"key":"S096012952200007X_ref4","unstructured":"Angiuli, C. , Hou (Favonia), K.-B. and Harper, R. (2018). Computational higher type theory iii: Univalent universes and exact equality. https:\/\/arxiv.org\/abs\/1712.01800. Preprint."},{"key":"S096012952200007X_ref17","unstructured":"The RedPRL Development Team. (2018). The redtt Proof Assistant. https:\/\/github.com\/RedPRL\/redtt\/."},{"key":"S096012952200007X_ref16","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-6(3:24)2010","article-title":"Weak omega-categories from intensional type theory","volume":"6","author":"Lumsdaine","year":"2010","journal-title":"Logical Methods in Computer Science"},{"key":"S096012952200007X_ref7","doi-asserted-by":"crossref","unstructured":"Bentzen, B. (2020). On different ways of being equal. Erkenntnis. https:\/\/doi.org\/10.1007\/s10670-020-00275-8.","DOI":"10.1007\/s10670-020-00275-8"},{"key":"S096012952200007X_ref3","unstructured":"Angiuli, C. , Brunerie, G. , Coquand, T. , Hou (Favonia), K.-B. , Harper, R. and Licata, D. (2019). Syntax and models of cartesian cubical type theory. https:\/\/github.com\/dlicata335\/cart-cube. Preprint."},{"key":"S096012952200007X_ref13","doi-asserted-by":"crossref","unstructured":"Coquand, T. , Huber, S. and M\u00f6rtberg, A. (2018). On higher inductive types in cubical type theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS\u201918, New York, NY, USA. ACM, 255\u2013264.","DOI":"10.1145\/3209108.3209197"},{"key":"S096012952200007X_ref19","doi-asserted-by":"crossref","unstructured":"Vezzosi, A. , M\u00f6rtberg, 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) 1\u201329. https:\/\/dl.acm.org\/doi\/10.1145\/3341691.","DOI":"10.1145\/3341691"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012952200007X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,28]],"date-time":"2022-09-28T10:13:38Z","timestamp":1664360018000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012952200007X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11]]},"references-count":21,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["S096012952200007X"],"URL":"https:\/\/doi.org\/10.1017\/s096012952200007x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,11]]},"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"}}]}}