Outputs (19)

Ordinal Exponentiation in Homotopy Type Theory (2025)
Presentation / Conference Contribution
de Jong, T., Kraus, N., Nordvall Forsberg, F., & Xu, C. (2025, June). Ordinal Exponentiation in Homotopy Type Theory. Presented at Fortieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2025), Singapore

We present two seemingly different definitions of constructive ordinal exponentiation, where an ordinal is taken to be a transitive, extensional, and wellfounded order on a set. The first definition is abstract, uses suprema of ordinals, and is solel... Read More about Ordinal Exponentiation in Homotopy Type Theory.

On symmetries of spheres in univalent foundations (2024)
Presentation / Conference Contribution
Cagne, P., Buchholtz, U. T., Kraus, N., & Bezem, M. (2024, July). On symmetries of spheres in univalent foundations. Presented at LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Tallinn

Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form Sn = Sn. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, th... Read More about On symmetries of spheres in univalent foundations.

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.

Type-theoretic approaches to ordinals (2023)
Journal Article
Kraus, N., Nordvall Forsberg, F., & Xu, C. (2023). Type-theoretic approaches to ordinals. Theoretical Computer Science, 957, Article 113843. https://doi.org/10.1016/j.tcs.2023.113843

In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensi... Read More about Type-theoretic approaches to ordinals.

A Rewriting Coherence Theorem with Applications in Homotopy Type Theory (2022)
Journal Article
Kraus, N. (2022). A Rewriting Coherence Theorem with Applications in Homotopy Type Theory. Mathematical Structures in Computer Science, 32(7), 982-1014. https://doi.org/10.1017/S0960129523000026

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a... Read More about A Rewriting Coherence Theorem with Applications in Homotopy Type Theory.

A rewriting coherence theorem with applications in homotopy type theory (2022)
Journal Article
Kraus, N., & von Raumer, J. (2022). A rewriting coherence theorem with applications in homotopy type theory. Mathematical Structures in Computer Science, 32(7), 982-1014. https://doi.org/10.1017/s0960129523000026

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a... Read More about A rewriting coherence theorem with applications in homotopy type theory.

Shallow Embedding of Type Theory is Morally Correct (2019)
Presentation / Conference Contribution
Kaposi, A., Kovács, A., & Kraus, N. (2019, October). Shallow Embedding of Type Theory is Morally Correct. Presented at Mathematics of Program Construction, Porto, Portugal

There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to refer to the syntax, for example in proofs of canonicity and normalisat... Read More about Shallow Embedding of Type Theory is Morally Correct.

Path Spaces of Higher Inductive Types in Homotopy Type Theory (2019)
Presentation / Conference Contribution
Kraus, N., & von Raumer, J. (2019, June). Path Spaces of Higher Inductive Types in Homotopy Type Theory. Presented at 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, BC, Canada

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pus... Read More about Path Spaces of Higher Inductive Types in Homotopy Type Theory.

Free Higher Groups in Homotopy Type Theory (2018)
Presentation / Conference Contribution
Kraus, N., & Altenkirch, T. (2018, July). Free Higher Groups in Homotopy Type Theory. Presented at LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford United Kingdom

© 2018 ACM. Given a type A in homotopy type theory (HoTT), we can define the free∞-group onA as the loop space of the suspension ofA+1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit : F(A),... Read More about Free Higher Groups in Homotopy Type Theory.

Quotient inductive-inductive types (2018)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2018, April). Quotient inductive-inductive types. Presented at 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of H... Read More about Quotient inductive-inductive types.