Monthly Archives: June 2014

Fibrations with fiber an Eilenberg-MacLane space

One of the fundamental constructions of classical homotopy theory is the Postnikov tower of a space X. In homotopy type theory, this is just its tower of truncations: One thing that’s special about this tower is that each map has … Continue reading

Posted in Homotopy Theory | 2 Comments

Higher inductive-recursive univalence and type-directed definitions

In chapter 2 of the HoTT book, we prove theorems (or, in a couple of cases, assert axioms) characterizing the equality types of all the standard type formers. For instance, we have and (that’s function extensionality) and (that’s univalence). However, … Continue reading

Posted in Code, Foundations, Higher Inductive Types, Univalence | 7 Comments