Author Archives: Steve Awodey
HoTT 2023
The 2nd International Conference on Homotopy Type Theory (HoTT 2023) will be held Monday 22nd May – Thursday 25th May 2023 at Carnegie Mellon University, Pittsburgh (USA). Abstracts of no more than 2 pages should be submitted via Easychair, see the submissions … Continue reading
Erik Palmgren Memorial Conference
Erik Palmgren, professor of Mathematical Logic at Stockholm University, passed away unexpectedly in November 2019. This conference will be an online workshop to remember and celebrate Erik’s life and work. There will be talks by Erik’s friends and colleagues, as … Continue reading
HoTT Dissertation Fellowship
Update (Nov. 13): Application deadline extended to December 1, 2020. PhD students close to finishing their thesis are invited to apply for a Dissertation Fellowship in Homotopy Type Theory. This fellowship, generously funded by Cambridge Quantum Computing and Ilyas Khan, will provide … Continue reading
HoTT 2019 Last Call
Last call for submissions INTERNATIONAL CONFERENCE AND SUMMER SCHOOL ON HOMOTOPY TYPE THEORY 12-17 August 2019 Carnegie Mellon University, Pittsburgh USA https://hott.github.io/HoTT-2019 Submission of talks and registration are open for the International Homotopy Type Theory conference (HoTT 2019), to be … Continue reading
HoTT 2019
Save the date! Next summer will be the first: International Conference on Homotopy Type Theory (HoTT 2019) Carnegie Mellon University 12 – 17 August 2019 There will also be an associated: HoTT Summer School 7 – 10 August 2019 More … Continue reading
HoTT awarded a MURI
We are pleased to announce that a research team based at Carnegie Mellon University has received a $7.5 million, five-year grant from the US Air Force Office of Scientific Research, as part of the highly competitive, DoD Multidisciplinary University Research Initiative … Continue reading
The HoTT Book
This posting is the official announcement of The HoTT Book, or more formally: Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program, Institute for Advanced Study The book is the result of an amazing collaboration between virtually everyone involved … Continue reading
HoTT Updates
Many updates have been made to the various other pages on the site: Code, Events, Links, People, References. For example, there are several new items on models of the Univalence Axiom on the References page.
Inductive Types in HoTT
With all the excitement about higher inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report … Continue reading
Constructive Validity
(This is intended to complement Mike Shulman’s nCat Cafe posting HoTT, II.) The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with respect to the statements that hold … Continue reading
Homotopy Type Theory, II | The n-Category Café
Mike Shulman has another great posting on HoTT over at the n-Cat Cafe’. It starts out like this: Homotopy Type Theory, II — Posted by Mike Shulman … Last time we talked about the correspondence between the syntax of intensional … Continue reading
Function Extensionality from Univalence
Andrej Bauer and Peter Lumsdaine have worked out a proof of Function Extensionality from Univalence that is somewhat different from Vladimir Voevodsky’s original. In it, they identify and employ a very useful consequence of Univalence: induction along weak-equivalences. Andrej has … Continue reading
Homotopy Type Theory 