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

Posted in Uncategorized | 2 Comments

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

Posted in Uncategorized | 1 Comment

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

Posted in News, Support | 1 Comment

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 Submission of talks and registration are open for the International Homotopy Type Theory conference (HoTT 2019), to be … Continue reading

Posted in Meeting, Uncategorized | 1 Comment

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

Posted in News | 6 Comments

In memoriam: Vladimir Voevodsky

Posted in Uncategorized | Leave a comment

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

Posted in News | 2 Comments

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

Posted in Foundations, Higher Inductive Types, Homotopy Theory, Paper, Univalence | 3 Comments

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.

Posted in Uncategorized | Leave a comment

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

Posted in Code, Foundations, Paper | 9 Comments

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

Posted in Foundations | 17 Comments

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

Posted in Foundations | Leave a comment

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

Posted in Univalence | 6 Comments