Mike Shulman
Mike Shulman
I think we did a fairly good job of not assuming too much background in topology and in type theory, but we did use a fair number of category-theoretic concepts...
It's annoying that we use the identity type for some examples in chapter 1 before we actually introduce it. I still do think that we should wait until the end...
Currently the book defines concatenation by path induction on both arguments, the way we do it in the Coq library. (The Agda library defines two different concatenations, one by induction...
In the second edition, I think we should add as a fifth condition to 5.8.2 that the function transport^R(-,r_0) in (iii) is a retraction. The equivalence of this with the...
In order to prove that V as defined in Exercise 10.11 admits the constructor (ii) of Definition 10.5.1 (which in the Coq formalization is called `setext'`), we let `R :...
It was suggested some time ago that it would be good to mention somewhere in chapter 10 that unlike the ordinary axiom of choice, the axiom of _global_ choice, at...
Chapter 2 has no exercises that make use of univalence. Can we come up with any good ones?
@martinescardo has pointed out that the proof of 4.6.3 essentially uses the equivalence of embeddings with (-1)-truncated maps (i.e. those whose fibers are hprops), which is not mentioned until section...
Currently the exercises are thrown together in a bit of an ad hoc way and are just sort of "everything we could think of", including some stuff that we just...