nucleation

LIT-095: Two-Level Type Theory and Applications

2 min read

Properties4
StatusActive — read in part on 2026-09-26, alongside the nLab page it supersedes (LIT-040) — §1–3, §4.7 and §5 in full, §4.3–4.6 at the level of statements; no NOTE yet, so a full reading is still owed
Tagsmathematics, logic
SupersedesLIT-040 — two-level type theory [descriptive title: nLab wiki entry "two-level type theory"]
Cited as “source” byTHEORY-642 — Basic two-level type theory, an inner homotopy type theory with an outer level of strict equality, is conservative over homotopy type theory, so an inner type it proves inhabited is already inhabited in HoTT, but a fibrant-replacement type former would force uniqueness of identity proofs on the inner level

Graph View

Danil Annenkov, Paolo Capriotti, Nicolai Kraus & Christian Sattler (2017; MSCS 2023) — ARXIV-1705.03307

Key takeaways

  • The reference presentation of two-level type theory: an inner, fibrant level where homotopy type theory holds and an outer level with strict equality, related by a fibrancy predicate.
  • Conservativity over HoTT (Props 2.18–2.19). Results about inner types proved in basic 2LTT hold in HoTT. This answers, for basic 2LTT, the “open question” the nLab page (LIT-040) still records. A stronger, bijective conservativity is conjectured (§5), with an argument credited to Kovács 2022.
  • A limit (Thm 2.20). Adding a fibrant-replacement type former forces uniqueness of identity proofs on the inner level.

Standing in the record

Filed on 2026-09-26 as the successor to the nLab page “two-level type theory” (LIT-040). That page’s close reading found it an accurate but thin gloss on this paper and its predecessor (arXiv 1604.03799), with no result, argument or citation not traceable to them. The same reading read this paper in part (above) to settle that. It is Active on that reading; a Read NOTE is still owed, and until one exists its results are cited from its statements, not from checked proofs. Riehl & Shulman’s synthetic ∞-categories (LIT-032) names this approach as the alternative way to make coherence towers internal to HoTT, and this paper names theirs.

Backlinks