{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T10:52:24Z","timestamp":1763635944884,"version":"3.45.0"},"reference-count":24,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T00:00:00Z","timestamp":1763596800000},"content-version":"unspecified","delay-in-days":323,"URL":"https:\/\/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":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory, such as Agda. The difference from prior works is that these proofs do not assume any abuse of notation, providing more direct formalization. Also, some new notions, such as function extensionality for cofibrant exo-types, are introduced. The necessity of such notions arises during the task of formalization. In addition, we provide some novel results about inductive types using cofibrant exo-nat, the natural number type at the non-fibrant level. While emphasizing the necessity of this axiom by citing new applications as justifications, we also touch upon the semantic aspect of the theory by presenting various models that satisfy this axiom.<\/jats:p>","DOI":"10.1017\/s0960129525100297","type":"journal-article","created":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T10:47:32Z","timestamp":1763635652000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing two-level type theory with cofibrant exo-nat"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3836-7193","authenticated-orcid":false,"given":"Elif","family":"Uskuplu","sequence":"first","affiliation":[{"name":"Indiana University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,11,20]]},"reference":[{"key":"S0960129525100297_ref9","unstructured":"Boulier, S. and Tabareau, N. (2020). Two-level type theory in coq. Available at https:\/\/github.com\/CoqHott\/coq-2ltt."},{"key":"S0960129525100297_ref23","unstructured":"Uskuplu, E. (2023). Formalizing two-level type theory with cofibrant exo-nat. arXiv preprint arXiv:2309.09395."},{"key":"S0960129525100297_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"S0960129525100297_ref22","unstructured":"Norell, U. (2007). Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology, https:\/\/www.cse.chalmers.se\/."},{"key":"S0960129525100297_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"S0960129525100297_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139015165"},{"key":"S0960129525100297_ref8","unstructured":"Boulier, S. and Tabareau, N. (2017). Model structure on the universe in a two level type theory. Available at https:\/\/hal.science\/hal-01579822."},{"key":"S0960129525100297_ref11","unstructured":"Capriotti, P. (2016). Models of type theory with strict equality. Ph.D. thesis, University of Nottingham."},{"key":"S0960129525100297_ref4","first-page":"1","volume-title":"Mathematical Structures in Computer Science","author":"Annenkov","year":"2023"},{"key":"S0960129525100297_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0001-5"},{"key":"S0960129525100297_ref18","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0960129525100297_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"S0960129525100297_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0960129525100297_ref17","volume-title":"Model Categories. Mathematical Surveys and Monographs","author":"Hovey","year":"1999"},{"key":"S0960129525100297_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2754931"},{"key":"S0960129525100297_ref24","unstructured":"Uskuplu, E. (2025). 2LTT-Agda: Formalization of Two-Level Type Theory in Agda. GitHub repository, commit 073a255. https:\/\/github.com\/ElifUskuplu\/2LTT-Agda."},{"key":"S0960129525100297_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S0960129525100297_ref2","doi-asserted-by":"publisher","DOI":"10.1090\/memo\/1541"},{"key":"S0960129525100297_ref25","unstructured":"Voevodsky, V. (2013). A simple type system with two identity types. Available at Unpublished note. https:\/\/www.math.ias.edu\/vladimir\/sites\/math.ias.edu.vladimir\/files\/HTS.pdf."},{"key":"S0960129525100297_ref19","doi-asserted-by":"publisher","DOI":"10.4171\/jems\/1050"},{"key":"S0960129525100297_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"S0960129525100297_ref3","unstructured":"Annenkov, D. , Capriotti, P. and Kraus, N. (2019). Lean Formalisation of two-level type theory. Available at https:\/\/github.com\/annenkov\/two-level."},{"key":"S0960129525100297_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"S0960129525100297_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9440-6"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525100297","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T10:47:35Z","timestamp":1763635655000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525100297\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":24,"alternative-id":["S0960129525100297"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525100297","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. 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 (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article 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"}],"article-number":"e30"}}