Dr NICOLAI KRAUS's Outputs (26)

Constructions with Non-Recursive Higher Inductive Types (2016)
Presentation / Conference Contribution
Kraus, N. (2016, July). Constructions with Non-Recursive Higher Inductive Types. Presented at LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York NY USA

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

The General Universal Property of the Propositional Truncation (2015)
Journal Article
Kraus, N. (2015). The General Universal Property of the Propositional Truncation. LIPIcs, 39, 111-145. https://doi.org/10.4230/LIPIcs.TYPES.2014.111

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant functions from A to B. This involves an infinite tower of coherence c... Read More about The General Universal Property of the Propositional Truncation.

Functions out of Higher Truncations (2015)
Journal Article
Capriotti, P., Kraus, N., & Vezzosi, A. (2015). Functions out of Higher Truncations. LIPIcs, 41, https://doi.org/10.4230/LIPIcs.CSL.2015.359

In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate... Read More about Functions out of Higher Truncations.

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), Article 18. 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.

Generalizations of Hedberg’s Theorem (2013)
Presentation / Conference Contribution
Kraus, N., Escardó, M., Coquand, T., & Altenkirch, T. (2013, June). Generalizations of Hedberg’s Theorem. Presented at TLCA: International Conference on Typed Lambda Calculi and Applications, Eindhoven, The Netherlands

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.

A Lambda Term Representation Inspired by Linear Ordered Logic (2011)
Journal Article
Abel, A., & Kraus, N. (2011). A Lambda Term Representation Inspired by Linear Ordered Logic. Electronic Proceedings in Theoretical Computer Science, 71, 1-13. https://doi.org/10.4204/EPTCS.71.1

We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional information where... Read More about A Lambda Term Representation Inspired by Linear Ordered Logic.