Monthly Archives: September 2014

The cumulative hierarchy of sets (guest post by Jeremy Ledent)

In section 10.5 of the HoTT book, the cumulative hierarchy V is defined as a rather non-standard higher inductive type. We can then define a membership relation ∈ on this type, such that (V, ∈) satisfies most of the axioms … Continue reading

Posted in Uncategorized | 2 Comments

Homotopical Patch Theory

This week at ICFP, Carlo will talk about our paper: Homotopical Patch Theory Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper Homotopy type theory is an extension of Martin-Loef type theory, based on a correspondence with homotopy theory and higher category … Continue reading

Posted in Uncategorized | 4 Comments