Two-Level Type Theory and Applications
Citation
Danil Annenkov and Paolo Capriotti and Nicolai Kraus and Christian Sattler. (2023). Two-Level Type Theory and Applications. Mathematical Structures in Computer Science. 33(8). pp. 688–743.
Why this reference is included
Annenkov et al.’s 2023 Two-Level Type Theory and Applications, published in Mathematical Structures in Computer Science, is one of the program’s working technical references. Cited across Book I (Categorical Foundations), Part 18, Chapter The Self-Hosting Landscape; Book I (Categorical Foundations), Part 18, Chapter Star-Autonomous Categories and the Diagonal Barrier — the central framing is “Two-level type theory separates an inner type theory (typically HoTT, with univalence and higher inductive types) from an outer strict type theory (with uniqueness of identity…”.
Cited in
-
Book I — Categorical Foundations Part 18Chapter The Self-Hosting Landscape
Two-level type theory separates an inner type theory (typically HoTT, with univalence and higher inductive types) from an outer strict type theory (with uniqueness of identity proofs and strict computation rules)
-
Book I — Categorical Foundations Part 18Chapter Star-Autonomous Categories and the Diagonal Barrier
Two-level type theory (2LTT) : an inner homotopy type theory supplemented by an outer strict type theory that serves as internalized metatheory