Author Archives: Nicolai Kraus

About Nicolai Kraus

At the University of Nottingham

Universal Properties of Truncations

Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation , and I want to write this blog post in case … Continue reading

Posted in Foundations, Homotopy Theory, Models, Paper, Talk | 3 Comments

The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible

Magic tricks are often entertaining, sometimes boring, and in some rarer cases astonishing. For me, the following trick belongs to the third type: the magician asks a volunteer in the audience to think of a natural number. The volunteer secretly … Continue reading

Posted in Code, Higher Inductive Types | 45 Comments

Universe n is not an n-Type

Joint work with Christian Sattler Some time ago, at the UF Program in Princeton, I presented a proof that Universe n is not an n-type. We have now formalized that proof in Agda and want to present it here. One … Continue reading

Posted in Code, Foundations, Talk, Univalence | Leave a comment

On h-Propositional Reflection and Hedberg’s Theorem

Thorsten Altenkirch, Thierry Coquand, Martin Escardo, Nicolai Kraus Overview Hedberg’s theorem states that decidable equality of a type implies that the type is an h-set, meaning that it has unique equality proofs. We describe how the assumption can be weakened. … Continue reading

Posted in Code, Foundations | 17 Comments

A direct proof of Hedberg’s theorem

In his article published 1998, Michael Hedberg has shown that a type with decidable equality also features the uniqueness of identity proofs property. Reading through Nils Anders Danielsson’s Agda formalization, I noticed that the statement “A has decidable equality”, i.e. … Continue reading

Posted in Code | 5 Comments