All Outputs (26)

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.

Set-Theoretic and Type-Theoretic Ordinals Coincide (2023)
Presentation / Conference Contribution
KRAUS, N., de Jong, T., Nordvall Forsberg, F., & Xu, C. (2023, June). Set-Theoretic and Type-Theoretic Ordinals Coincide. Paper presented at Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, USA

In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (... Read More about Set-Theoretic and Type-Theoretic Ordinals Coincide.

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.

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 (2023)
Journal Article
Kraus, N. (2023). 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.

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.

Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT (2021)
Presentation / Conference Contribution
Kraus, N. (2021, June). Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT. Presented at ACM/IEEE LICS 2021: 36th Annual Symposium on Logic in Computer Science, Online

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer'... Read More about Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT.

Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT (2021)
Presentation / Conference Contribution
Kraus, N. (2021, June). Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT. Presented at LICS'21 - ACM/IEEE Symposium on Logic in Computer Science, Rome, Italy

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer'... Read More about Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT.

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.

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

© 2019, Springer Nature Switzerland AG. 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 exampl... 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.

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory (2019)
Presentation / Conference Contribution
Pinyo, G., & Kraus, N. (2019, June). From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. Paper presented at TYPES 2019, Oslo, Norway

Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent foundations, where types carry the structure of such higher groupoids... Read More about From Cubes to Twisted Cubes via Graph Morphisms in 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)
Book Chapter
Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., & Nordvall Forsberg, F. (2018). Quotient inductive-inductive types. In C. Baier, & U. Dal Lago (Eds.), FoSSaCS 2018: Foundations of Software Science and Computation Structures (293-310). Springer Publishing Company. https://doi.org/10.1007/978-3-319-89366-2_16

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.

Univalent higher categories via complete semi-segal types (2017)
Journal Article
Capriotti, P., & Kraus, N. (2018). Univalent higher categories via complete semi-segal types. Proceedings of the ACM on Programming Languages, 2(POPL), https://doi.org/10.1145/3158132

Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.)solves this by considering only... Read More about Univalent higher categories via complete semi-segal types.

Notions of anonymous existence in Martin-Löf type theory (2017)
Journal Article
Kraus, N., Escardo, M., Coquand, T., & Altenkirch, T. (in press). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 13(1),

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have uniqu... Read More about Notions of anonymous existence in Martin-Löf type theory.

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2017)
Presentation / Conference Contribution
Altenkirch, T., Danielson, N. A., & Kraus, N. (2017, April). Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. Presented at 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, Uppsala, Sweden

Capretta’s delay monad can be used to model partial computations, but it has the “wrong” notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the “right” notion of equality, weak bisimilarity. However, re... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.

Extending Homotopy Type Theory with Strict Equality (2016)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., & Kraus, N. (2016, August). Extending Homotopy Type Theory with Strict Equality. Presented at 25th EACSL Annual Conference on Computer Science Logic, CSL 2016., Marseille, France

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult a... Read More about Extending Homotopy Type Theory with Strict Equality.