Category Archives: Talk

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

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

A seminar on HoTT Equivalences

I recorded our local Seminar on foundations in which I talked about the notion of equivalence in HoTT: Hopefully some people will find some use for it. It is pretty slowly going, and it might motivate some of the strange … Continue reading

Posted in Talk | 5 Comments