Skip to main content

Research Repository

Advanced Search

All Outputs (2)

Two-level type theory and applications (2023)
Journal Article
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

We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the ‘inner’ and the ‘outer’ type theory. In our case of interest, the inner theory is homotopy typ... Read More about Two-level type theory and applications.

Higher Homotopies in a Hierarchy of Univalent Universes (2015)
Journal Article
Kraus, N., & Sattler, C. (2015). Higher Homotopies in a Hierarchy of Univalent Universes. ACM Transactions on Computational Logic, 16(2), https://doi.org/10.1145/2729979

For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher... Read More about Higher Homotopies in a Hierarchy of Univalent Universes.