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