Mike Shulman

Introduce indexed-subset notation

6

Do we formally introduce the notation `{ f(x) | x:A }` anywhere, for a function `f : A -> B` between sets? It doesn't seem to be in section 3.7,...

I suggest that in the second edition, sections 4.1 and 4.9 and exercise 4.6 be refactored into something like the following sequence: - Naive non-dependent funext implies full dependent funext,...

Always write ap_f(p) instead of f(p)?

10

For the second edition, perhaps we should reconsider the decision to write `f(p)` for `ap_f(p)`. It confuses some readers, especially those trying to formalize the arguments in a proof assistant,...

This is mainly because the format of .aux files seems to have changed; cleveref lines now *end* the label with `@cref` instead of starting with `cref@`, and some entries have...

Replace 'mere proposition' with 'truth value'

8

To be clear, I'm not saying that we _will_ or even necessarily that we _should_ do this. We should think carefully about the implications before making a decision, and probably...

Terminology for Sigma and truncated-Sigma

5

@vladimirias has suggested to use the following terminology: - Σ (x : A) P(x) is "there is given x in A such that P(x)" - ∃ (x : A) P(x)...

Summarize other parts of HoTT in intro

4

Reading over the introduction again, I think there is something else missing: a brief summary of the other aspects of the field that the book is not about. The "Open...

Think about the beginning of chapter 2

3

We seem to get a fair number of people who hit the beginning of chapter 2 and think "oh no, I don't know what an ∞-groupoid is" and get stuck...