Mike Shulman
Mike Shulman
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...
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...
I propose that in the second edition, we state the result of exercise 2.17(i) in section 2.6, and similarly for the analogous statements in sections 2.7, 2.9, and 2.12. We...
The script "make labelcheck" is not be robust to different versions of latex or something. On my work computer, it fails because there are extra numbers in all the section...
We try to introduce technical words from topology, category theory, and type theory where we use them, but it might be helpful to people without any background in one or...
ISBN
I've received a comment from someone who wanted to request that their library order a copy of the book, but wasn't sure how to due to the lack of an...
From Dan Piponi on G+: > So pretty please can we have a table of operator precedence near the index of symbols in the HoTT book? I know I'm not...
I've had two questions so far about the prerequisites / expected background to read the book. Do we address this anywhere _in_ the book?
I did a much better job minimizing this one! ```agda {-# OPTIONS --rewriting #-} postulate _≡_ : {A : Set₁} (a : A) → A → Set {-# BUILTIN REWRITE...