Author Archives: Mike Shulman
Submissions of talks are now open for the International Homotopy Type Theory conference (HoTT 2019), to be held from August 12th to 17th, 2019, at Carnegie Mellon University in Pittsburgh, USA. Contributions are welcome in all areas related to homotopy type … Continue reading
In this post I will argue that, improving on previous work of Awodey-Frey-Speight, (higher) inductive types can be defined using impredicative encodings with their full dependent induction principles — in particular, eliminating into all type families without any truncation hypotheses … Continue reading
The wiki used for the 2012-2013 Univalent Foundations program at the Institute for Advanced Study was hosted at a provider called Wikispaces. After the program was over, the wiki was no longer used, but was kept around for historical and … Continue reading
At the 2018 U.S. Joint Mathematics Meetings in San Diego, there will be an AMS special session about homotopy type theory. It’s a continuation of the HoTT MRC that took place this summer, organized by some of the participants to … Continue reading
From June 4 — 10, 2017, there will be a workshop on homotopy type theory as one of the AMS’s Mathematical Research Communities (MRCs).
Two new papers have recently appeared online: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory by me, and Adjoint logic with a 2-category of modes, by Dan Licata with a bit of help from me. Both of them have fairly … Continue reading
First of all, in case anyone missed it, Chris Kapulkin recently wrote a guest post at the n-category cafe summarizing the current state of the art regarding “homotopy type theory as the internal language of higher categories”. I’ve just posted … Continue reading