book
book copied to clipboard
HoTT
A textbook on informal homotopy type theory
Following the suggestions in #1111 and #1101, I wrote an initial draft for a code of conduct. Any suggestions for improvements are much appreciated.
I think it should be changed that first projection of coproduct type should be apparently parenthesized. `\sum_(x:A) P(x) \rightarrow A`
One of the cardinal multiplications is written with \times when it should be \cdot. ref: Lemma 10.2.4 Card is a commutative semiring
Would be great for those of us with e-book readers. Thanks!
I've tried to enable microtype and seems to work well (fewer overfull hboxes). The only problem was hyphenation of 2 section titles, but disabling tracking on those 2 pages seems...
I think there is a typo in page 133, theorem 4.2.3. "Proof. Suppose that (g, eta, epsilon) is a quasi-inverse for f ." In the definition of qinv, the first...
As per current layout, *page numbers* and *running heads* are both on top of the page, numbers on the *outside* (outside = away from the spine) and running heads on...
I am reading HoTT and I am finding quite well done. One think I disliked is that I had to clone and build the repository to get exercises solutions. Those...