book
book copied to clipboard
HoTT
A textbook on informal homotopy type theory
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...
On [page 372 of the HoTT ebook](http://hottheory.files.wordpress.com/2013/03/hott-ebook-611-ga1a258c.pdf#page=386), `The quotient is generated by the following equalities (see Remark 8.7.3)` is slightly cut off.
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...
Supposing we want to add new mathematics, let's discuss how to do it in a new thread. Some possibilities: - Create a branch for the second edition and make all...
The [Planetmath version](http://planetmath.org/node/87534) adds a lot of hyperlinks (automatically). Although many of their links are wrong (particularly because they go to elsewhere in planetmath rather than to appropriate places in...
The empty pages which make sure that chapters start on odd pages, etc., don't make sense in the ebook format, and quite possibly also in the online version.
I propose that in the second edition, we improve the presentation of metatheoretic facts about funext and univalence. I think we originally tried to minimize metatheoretic discussion out of an...