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
Homotopy Type Theory 