Dear all,
This is very sad news indeed.
My memory of Erik is as a quiet but thoughtful and warm person,
candid and principled, and vastly knowledgeable.
Erik was my entry-point into the world of type theory, when, in 2016, he let me, then an impressionable masters student, into his cavernous setoid libraries, where I spent six happy months messing with E-categories---'"Erik"-categories'---and ECwAs, lost in the heady lure of checking coherences in a proof assistant.
-Chaitanya.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-k00GTNS4jm3vgvJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com.