{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T20:46:10Z","timestamp":1786999570283,"version":"build-2736575974"},"reference-count":64,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T00:00:00Z","timestamp":1685404800000},"content-version":"unspecified","delay-in-days":0,"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":[[2023,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We define and develop\n                    <jats:italic>two-level type theory<\/jats:italic>\n                    (2LTT), a version of Martin-L\u00f6f type theory which combines two different type theories. We refer to them as the \u2018inner\u2019 and the \u2018outer\u2019 type theory. In our case of interest, the inner theory is\n                    <jats:italic>homotopy type theory<\/jats:italic>\n                    (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating\n                    <jats:italic>uniqueness of identity proofs<\/jats:italic>\n                    (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level\n                    <jats:italic>n<\/jats:italic>\n                    can be constructed in HoTT for any externally fixed natural number\n                    <jats:italic>n<\/jats:italic>\n                    . Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where\n                    <jats:italic>n<\/jats:italic>\n                    will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky\u2019s\n                    <jats:italic>Homotopy Type System<\/jats:italic>\n                    (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be assumed by postulating that the inner and outer natural numbers types are isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000130_inline1.png\"\/>\n                        <jats:tex-math>$(\\infty,1)$<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -\n                    <jats:italic>category<\/jats:italic>\n                    and give some examples.\n                  <\/jats:p>","DOI":"10.1017\/s0960129523000130","type":"journal-article","created":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T02:21:48Z","timestamp":1685413308000},"page":"688-743","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":16,"title":["Two-level type theory and applications"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8278-3069","authenticated-orcid":false,"given":"Danil","family":"Annenkov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4836-1804","authenticated-orcid":false,"given":"Paolo","family":"Capriotti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8729-4077","authenticated-orcid":false,"given":"Nicolai","family":"Kraus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6374-4427","authenticated-orcid":false,"given":"Christian","family":"Sattler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2023,5,30]]},"reference":[{"key":"S0960129523000130_ref36","unstructured":"Kapulkin, C. and Lumsdaine, P. L. (2018). The simplicial model of Univalent Foundations (after Voevodsky). ArXiv e-prints."},{"key":"S0960129523000130_ref41","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470667"},{"key":"S0960129523000130_ref50","article-title":"Axioms for modelling cubical type theory in a topos","volume":"14","author":"Pitts","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000130_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"S0960129523000130_ref10","unstructured":"Barras, B. and Maestracci, V. (2020). Implementation of two layers type theory in dedukti and application to cubical type theory. In: LFMPT 2020 - Logical Frameworks and Meta-Languages: Theory and Practice 2020, Paris, France."},{"key":"S0960129523000130_ref39","unstructured":"Kraus, N. (2015b). Truncation Levels in Homotopy Type Theory. Phd thesis, School of Computer Science, University of Nottingham, Nottingham, UK."},{"key":"S0960129523000130_ref19","unstructured":"Brunerie, G. , de Boer, M. , Lumsdaine, P. L. and M\u00f6rtberg, A. (2019). A formalization of the initiality conjecture in agda. Talk given by Brunerie at the HoTT 2019 conference, slides available at https:\/\/guillaumebrunerie.github.io\/pdf\/initiality.pdf."},{"key":"S0960129523000130_ref49","unstructured":"Norell, U. (2007). Towards a Practical Programming Language Based on Dependent Type Theory. Phd thesis, Department of Computer Science and Engineering, Chalmers University of Technology and G\u00f6teborg University."},{"key":"S0960129523000130_ref51","unstructured":"Radulescu-Banu, A. (2006). Cofibrations in homotopy theory. arXiv preprint math\/0610009."},{"key":"S0960129523000130_ref8","unstructured":"Angiuli, C. , Hou (Favonia), K.-B. and Harper, R. (2018). Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In: Ghica, D. and Jung, A. (eds.) 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 119, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 6:1\u20136:17."},{"key":"S0960129523000130_ref56","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2015.v17.n2.a6"},{"key":"S0960129523000130_ref29","doi-asserted-by":"crossref","unstructured":"Dybjer, P. (1995). Internal type theory. In: Berardi, S. and Coppo, M. (eds.) Types for Proofs and Programs (TYPES), Lecture Notes in Computer Science, vol. 1158, Springer-Verlag, 120\u2013134.","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0960129523000130_ref23","doi-asserted-by":"crossref","unstructured":"Capriotti, P. and Kraus, N. (2017). Univalent higher categories via complete semi-segal types. Proceedings of the ACM on Programming Languages 2 (POPL\u201918) 44:1\u201344:29. Full version available at https:\/\/arxiv.org\/abs\/1707.03693.","DOI":"10.1145\/3158132"},{"key":"S0960129523000130_ref12","unstructured":"Bertot, Y. (2013). Private inductive types: Proposing a language extension. http:\/\/coq.inria.fr\/files\/coq5_submission_3.pdf."},{"key":"S0960129523000130_ref45","author":"Lumsdaine","year":"2013"},{"key":"S0960129523000130_ref58","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"S0960129523000130_ref57","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"S0960129523000130_ref33","unstructured":"Hofmann, M. and Streicher, T. (1997). Lifting grothendieck universes. Unpublished note. Available at https:\/\/www2.mathematik.tu-darmstadt.de\/streicher\/NOTES\/lift.pdf."},{"key":"S0960129523000130_ref16","unstructured":"Bonacina, R. and Ahrens, B. (2021). Syntax for two-level type theory. Abstract, presented at TYPES\u201921."},{"key":"S0960129523000130_ref61","unstructured":"The Univalent Foundations Program. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book\/."},{"key":"S0960129523000130_ref17","unstructured":"Bonacina, R. , Ahrens, B. and Kraus, N. (2021). Syntax for two-level type theory. Abstract, presented at HoTT\/UF\u201921."},{"key":"S0960129523000130_ref13","volume-title":"EATCS Texts in Theoretical Computer Science","author":"Bertot","year":"2010"},{"key":"S0960129523000130_ref43","unstructured":"Licata, D. R. , Orton, I. , Pitts, A. M. and Spitters, B. (2018). Internal universes in models of homotopy type theory. In: Kirchner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 108, Dagstuhl, Germany, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 22:1\u201322:17."},{"key":"S0960129523000130_ref5","unstructured":"Altenkirch, T. , Capriotti, P. and Kraus, N. (2016). Extending homotopy type theory with strict equality. In: Talbot, J.-M. and Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), vol. 62, 21:1\u201321:17."},{"key":"S0960129523000130_ref9","unstructured":"Assaf, A. , Burel, G. , Cauderlier, R. , Delahaye, D. , Dowek, G. , Dubois, C. , Gilbert, F. , Halmagrand, P. , Hermant, O. and Saillard, R. (2016). Dedukti: a logical framework based on the \u03bb\u03c0-calculus modulo theory. Manuscript http:\/\/www.lsv.fr\/dowek\/Publi\/expressing.pdf."},{"key":"S0960129523000130_ref28","unstructured":"de Moura, L. , Kong, S. , Avigad, J. , van Doorn, F. and von Raumer, J. (2015). The lean theorem prover. In: Automated Deduction - CADE-25, 25th International Conference on Automated Deduction."},{"key":"S0960129523000130_ref38","unstructured":"Kraus, N. (2015a). The general universal property of the propositional truncation. In: Herbelin, H. , Letouzey, P. and Sozeau, M. (eds.) 20th International Conference on Types for Proofs and Programs (TYPES 2014), Leibniz International Proceedings in Informatics (LIPIcs), vol. 39, Dagstuhl, Germany, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 111\u2013145."},{"key":"S0960129523000130_ref44","unstructured":"Lumsdaine, P. L. and M\u00f6rtberg, A. (2018). Formalising the initiality conjecture in coq. Talk given by Lumsdaine at the G\u00f6teborg-Stockholm Joint Type Theory Seminar, slides available at http:\/\/peterlefanulumsdaine.com\/research\/Lumsdaine-2018-Goteborg-Initiality.pdf."},{"key":"S0960129523000130_ref30","doi-asserted-by":"crossref","unstructured":"Gilbert, G. , Cockx, J. , Sozeau, M. and Tabareau, N. (2019). Definitional proof-irrelevance without K. Proceedings of the ACM on Programming Languages 3 (POPL) 3:1\u20133:28.","DOI":"10.1145\/3290316"},{"key":"S0960129523000130_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_31"},{"key":"S0960129523000130_ref48","unstructured":"Makkai, M. (1995). First order logic with dependent sorts, with applications to category theory. preprint, available at http:\/\/www.math.mcgill.ca\/makkai."},{"key":"S0960129523000130_ref63","unstructured":"Uskuplu, E. (2022). An implementation of 2LTT in Agda. Abstract, presented at HoTT\/UF\u201922."},{"key":"S0960129523000130_ref42","unstructured":"Kraus, N. and Sattler, C. (2017). Space-valued diagrams, type-theoretically (extended abstract). ArXiv e-prints."},{"key":"S0960129523000130_ref60","unstructured":"Streicher, T. (1993). Investigations into intensional type theory. Habilitationsschrift, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"S0960129523000130_ref64","unstructured":"Voevodsky, V. (2013). A simple type system with two identity types. Unpublished note."},{"key":"S0960129523000130_ref59","unstructured":"Shulman, M. (2019). All (\u221e, 1)-toposes have strict univalent universes. arXiv preprint arXiv:1904.07004."},{"key":"S0960129523000130_ref52","unstructured":"Reedy, C. L. (1974). Homotopy theory of model categories. Unpublished manuscript. Available at http:\/\/www-math.mit.edu\/psh\/reedy.pdf."},{"key":"S0960129523000130_ref22","unstructured":"Capriotti, P. (2016). Models of Type Theory with Strict Equality. Phd thesis, School of Computer Science, University of Nottingham."},{"key":"S0960129523000130_ref18","unstructured":"Boulier, S. and Tabareau, N. (2017). Model structure on the universe in a two level type theory. HAL e-prints. <hal-01579822>."},{"key":"S0960129523000130_ref40","unstructured":"Kraus, N. (2018). On the role of semisimplicial types. Abstract, presented at TYPES\u201918."},{"key":"S0960129523000130_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"S0960129523000130_ref14","unstructured":"Bezem, M. , Coquand, T. and Huber, S. (2014). A model of type theory in cubical sets. In: Matthes, R. and Schubert, A. (eds.) Types for Proofs and Programs (TYPES), Leibniz International Proceedings in Informatics (LIPIcs), vol. 26, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 107\u2013128."},{"key":"S0960129523000130_ref21","unstructured":"Brunerie, G. and Lumsdaine, P. L. (2020). Initiality for martin-l\u00f6f type theory. Talk at the Homotopy Type Theory Electronic Seminar Talks (HOTTEST)."},{"key":"S0960129523000130_ref26","unstructured":"Coquand, T. , Huber, S. and Sattler, C. (2019). Homotopy canonicity for cubical type theory. In: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"S0960129523000130_ref54","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"S0960129523000130_ref62","unstructured":"Uemura, T. (2019). A general framework for the semantics of type theory. arXiv preprint arXiv:1904.04097."},{"key":"S0960129523000130_ref27","unstructured":"de Boer, M. (2020). A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory. Phd thesis, Stockholm University, Faculty of Science, Department of Mathematics, Stockholm, Sweden. Available online at https:\/\/su.diva-portal.org\/smash\/record.jsf?pid=diva2%3A1431287"},{"key":"S0960129523000130_ref47","volume-title":"From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics","author":"Maietti","year":"2005"},{"key":"S0960129523000130_ref46","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.01.006"},{"key":"S0960129523000130_ref32","doi-asserted-by":"crossref","unstructured":"Hofmann, M. (1997). Syntax and semantics of dependent types. In: Semantics and Logics of Computation, Cambridge University Press, 79\u2013130.","DOI":"10.1017\/CBO9780511526619.004"},{"key":"S0960129523000130_ref1","first-page":"1","article-title":"Univalent categories and the Rezk completion","author":"Ahrens","year":"2015","journal-title":"Mathematical Structures in Computer Science (MSCS)"},{"key":"S0960129523000130_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"S0960129523000130_ref35","article-title":"Signatures and induction principles for higher inductive-inductive types","volume":"16","author":"Kaposi","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000130_ref53","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-00-02653-2"},{"key":"S0960129523000130_ref15","volume-title":"Lecture Notes in Mathematics","volume":"347","author":"Boardman","year":"1973"},{"key":"S0960129523000130_ref31","doi-asserted-by":"publisher","DOI":"10.2140\/agt.2015.15.2303"},{"key":"S0960129523000130_ref24","first-page":"3127","article-title":"Cubical type theory: A constructive interpretation of the univalence axiom","volume":"4","author":"Cohen","year":"2017","journal-title":"IfCoLog Journal of Logics and their Applications"},{"key":"S0960129523000130_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394755"},{"key":"S0960129523000130_ref20","unstructured":"Brunerie, G. and Lumsdaine, P. L. (2018). Formalising the initiality conjecture in coq and agda. Talk at the Stockholm-G\u00f6teborg Type Theory Serminar."},{"key":"S0960129523000130_ref11","unstructured":"Bauer, A. , Gilbert, G. , Haselwarter, P. , Pretnar, M. and Stone, C. Andromeda . Implementation of a type theory with equality reflection. http:\/\/andromedans.github.io\/andromeda\/."},{"key":"S0960129523000130_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(02)00135-4"},{"key":"S0960129523000130_ref3","unstructured":"Ahrens, B. , North, P. R. , Shulman, M. and Tsementzis, D. (2021). The univalence principle. ArXiv e-prints."},{"key":"S0960129523000130_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"S0960129523000130_ref55","first-page":"256","article-title":"The theory and practice of Reedy categories","volume":"29","author":"Riehl","year":"2014","journal-title":"Theory and Applications of Categories"}],"updated-by":[{"DOI":"10.1017\/s096012952300021x","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T00:00:00Z","timestamp":1685404800000}}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000130","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,3]],"date-time":"2023-10-03T07:41:17Z","timestamp":1696318877000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000130\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,30]]},"references-count":64,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["S0960129523000130"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000130","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,30]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. 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, 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"}]}}