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
3 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
Homotopy Type Theory 