Monthly Archives: January 2015

The torus is the product of two circles, cubically

Back in the summer of 2012, emboldened by how nicely the calculation π₁(S¹) had gone, I asked a summer research intern, Joseph Lee, to work on formalizing a proof that the higher-inductive definition of the torus (see Section 6.6 of the HoTT book) … Continue reading

Posted in Higher Inductive Types, Homotopy Theory | 31 Comments

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