All Outputs (9)

Connecting Constructive Notions of Ordinals in Homotopy Type Theory (2021)
Conference Proceeding
Kraus, N., Nordvall Forsberg, F., & Xu, C. (2021). Connecting Constructive Notions of Ordinals in Homotopy Type Theory.

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)
Conference Proceeding
Kraus, N. (2021). Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (1-14). https://doi.org/10.1109/LICS52264.2021.9470667

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)
Conference Proceeding
Kraus, N., & Von Raumer, J. (2020). Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. In LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (662-675). https://doi.org/10.1145/3373718.3394800

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.

Path Spaces of Higher Inductive Types in Homotopy Type Theory (2019)
Conference Proceeding
Kraus, N., & von Raumer, J. (2019). Path Spaces of Higher Inductive Types in Homotopy Type Theory. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). https://doi.org/10.1109/LICS.2019.8785661

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)
Conference Proceeding
Kraus, N., & Altenkirch, T. (2018). Free Higher Groups in Homotopy Type Theory. In LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (599-608). https://doi.org/10.1145/3209108.3209183

© 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.

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2017)
Conference Proceeding
Altenkirch, T., Danielson, N. A., & Kraus, N. (2017). Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. In Foundations of Software Science and Computation Structures: FoSSaCS 2017 (534-549). https://doi.org/10.1007/978-3-662-54458-7_31

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,... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.

Extending Homotopy Type Theory with Strict Equality (2016)
Conference Proceeding
Altenkirch, T., Capriotti, P., & Kraus, N. (2016). Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (21:1-21:17). https://doi.org/10.4230/LIPIcs.CSL.2016.21

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.

Constructions with Non-Recursive Higher Inductive Types (2016)
Conference Proceeding
Kraus, N. (2016). Constructions with Non-Recursive Higher Inductive Types. In LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (595-604). https://doi.org/10.1145/2933575.2933586

© 2016 ACM. Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say tha... Read More about Constructions with Non-Recursive Higher Inductive Types.

Generalizations of Hedberg’s Theorem (2013)
Conference Proceeding
Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2013). Generalizations of Hedberg’s Theorem. In Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June (173-188). https://doi.org/10.1007/978-3-642-38946-7_14

As the groupoid interpretation by Hofmann and Streicher shows, uniqueness of identity proofs (UIP) is not provable. Generalizing a theorem by Hedberg, we give new characterizations of types that satisfy UIP. It turns out to be natural in this context... Read More about Generalizations of Hedberg’s Theorem.