Two-Level Type Theory

Definition

A type theory with two distinct universes (layers):

1. Fibrant Layer (${\mathcal{U}}_f$): univalence holds; equality is path equality. This represents the “homotopical” world of HoTT.
2. Strict Layer (${\mathcal{U}}_s$): Axiom K (UIP) holds; no Univalence. This represents the “pre-homotopical” or strict metatheory.

Application

2LTT is used to solve coherence problems, such as defining semi-simplicial types. One defines the structures in ${\mathcal{U}}_s$, where composition is strictly associative and equations hold definitionally, and then interprets them into ${\mathcal{U}}_f$.

References

• Annenkov, D., Capriotti, P., Kraus, N., Sattler, C. (2019). “Two-Level Type Theory and Applications”. arXiv:1705.03307.