Annenkov, D., Capriotti, P., Kraus, N., & Sattler, C. (2023). Two-level type theory and applications. Mathematical Structures in Computer Science, 33(8), 688-743. https://doi.org/10.1017/s0960129523000130