Category Archives: Univalence
First of all, in case anyone missed it, Chris Kapulkin recently wrote a guest post at the n-category cafe summarizing the current state of the art regarding “homotopy type theory as the internal language of higher categories”. I’ve just posted … Continue reading
As discussed at length on the mailing list some time ago, there are several different things that one might mean by saying that a function is “constant”. Here is my preferred terminology: is constant if we have such that for … Continue reading
A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.
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
For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment: Eilenberg-MacLane Spaces in Homotopy Type Theory Dan … Continue reading
The fact, due to Voevodsky, that univalence implies function extensionality, has always been a bit mysterious to me—the proofs that I have seen have all seemed a bit non-obvious, and I have trouble re-inventing or explaining them. Moreover, there are … Continue reading
This posting is the official announcement of The HoTT Book, or more formally: Homotopy Type Theory: Univalent Foundations of Mathematics The Univalent Foundations Program, Institute for Advanced Study The book is the result of an amazing collaboration between virtually everyone involved … Continue reading