Category Archives: Uncategorized
This post is to announce a new article that I recently uploaded to the arxiv: https://arxiv.org/abs/1701.07538 The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in … Continue reading
From June 4 — 10, 2017, there will be a workshop on homotopy type theory as one of the AMS’s Mathematical Research Communities (MRCs).
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
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
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
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
Many of us working on homotopy type theory believe that it will be a better framework for doing math, and in particular computer-checked math, than set theory or classical higher-order logic or non-univalent type theory. One reason we believe this … Continue reading