Monthly Archives: May 2013
Homotopy Theory in Type Theory: Progress Report
A little while ago, we gave an overview of the kinds of results in homotopy theory that we might try to prove in homotopy type theory (such as calculating homotopy groups of spheres), and the basic tools used in our synthetic approach … Continue reading
Posted in Higher Inductive Types, Homotopy Theory
13 Comments
Universe n is not an n-Type
Joint work with Christian Sattler Some time ago, at the UF Program in Princeton, I presented a proof that Universe n is not an n-type. We have now formalized that proof in Agda and want to present it here. One … Continue reading
Posted in Code, Foundations, Talk, Univalence
Leave a comment
Homotopy Type Theory 