Category Archives: Uncategorized

Impredicative Encodings of Inductive Types in HoTT

I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading

Posted in Applications, Foundations, Uncategorized | 4 Comments

In memoriam: Vladimir Voevodsky

Posted in Uncategorized | 1 Comment

A hands-on introduction to cubicaltt

Some months ago I gave a series of hands-on lectures on cubicaltt at Inria Sophia Antipolis that can be found at: The lectures cover the main features of the system and don’t assume any prior knowledge of Homotopy Type … Continue reading

Posted in Uncategorized | 56 Comments

Type theoretic replacement & the n-truncation

This post is to announce a new article that I recently uploaded to the arxiv: The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in … Continue reading

Posted in Uncategorized | Leave a comment


From June 4 — 10, 2017, there will be a workshop on homotopy type theory as one of the AMS’s Mathematical Research Communities (MRCs).

Posted in News, Publicity, Uncategorized | Leave a comment

HoTT is not an interpretation of MLTT into abstract homotopy theory

Almost at the top of the HoTT website are the words: “Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  ” I think it is time to change these words … Continue reading

Posted in Uncategorized | 30 Comments

The HoTT Book does not define HoTT

The intent of this post is to address certain misconceptions that I’ve noticed regarding the HoTT Book and its role in relation to HoTT. (At least, I consider them misconceptions.) Overall, I think the HoTT Book project has been successful … Continue reading

Posted in Uncategorized | 6 Comments