{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T03:12:47Z","timestamp":1767150767109,"version":"build-2238731810"},"update-to":[{"DOI":"10.1017\/s0960129523000130","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T00:00:00Z","timestamp":1685404800000}}],"reference-count":1,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T00:00:00Z","timestamp":1688947200000},"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":[[2024,1]]},"abstract":"Abstract<\/jats:title>\n \n We define and develop\n 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 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 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 n<\/jats:italic>\n can be constructed in HoTT for any externally fixed natural number\n n<\/jats:italic>\n . Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where\n 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 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 \n \n \n $(\\infty,1)$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -\n category<\/jats:italic>\n and give some examples.\n <\/jats:p>","DOI":"10.1017\/s096012952300021x","type":"journal-article","created":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T05:06:11Z","timestamp":1688965571000},"page":"80-80","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Two-level type theory and applications - ERRATUM"],"prefix":"10.1017","volume":"34","author":[{"given":"Danil","family":"Annenkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Capriotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolai","family":"Kraus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Sattler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,7,10]]},"reference":[{"key":"S096012952300021X_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000130"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012952300021X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T04:27:15Z","timestamp":1706070435000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012952300021X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,10]]},"references-count":1,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1]]}},"alternative-id":["S096012952300021X"],"URL":"https:\/\/doi.org\/10.1017\/s096012952300021x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,10]]},"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"}]}}