Outputs (3)

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.

Connecting Constructive Notions of Ordinals in Homotopy Type Theory (2021)
Presentation / Conference Contribution
Kraus, N., Nordvall Forsberg, F., & Xu, C. (2021, August). Connecting Constructive Notions of Ordinals in Homotopy Type Theory. Presented at 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), Tallinn, Estonia

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinal... Read More about Connecting Constructive Notions of Ordinals in Homotopy Type Theory.

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory (2020)
Presentation / Conference Contribution
Kraus, N., & Von Raumer, J. (2020, June). Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. Presented at ACM International Conference Proceeding Series, Saarbrücken Germany (held online)

Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of inducti... Read More about Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory.