Issues

Inconsistent notation for the type of pointed types
HoTT/book#1197 · opened on Jul 11, 2026
Nightly build can't find package gh
HoTT/book#1195 · opened on May 13, 2026
Clarification about judgmental unequality
HoTT/book#1194 · opened on Feb 14, 2026
6
Explanation of “fundamental group” is confusing
HoTT/book#1190 · opened on Aug 27, 2025
2
Simplifications for Theorem 11.2.12 {RD-cauchy-complete}
HoTT/book#1167 · opened on Mar 27, 2025
2
Incorrect diagram for Example 8.7.16
HoTT/book#1163 · opened on Sep 2, 2024
1
Exercise 11.6 seems to need WLPO not LPO
HoTT/book#1162 · opened on Aug 4, 2024
3
max and sup
HoTT/book#1161 · opened on Jul 13, 2024
9
Switch to using truncated logic as default in the book
HoTT/book#1160 · opened on Jun 19, 2024
2
real numbers in the introduction
HoTT/book#1158 · opened on Jun 15, 2024
7
cardinal numbers in the introduction
HoTT/book#1157 · opened on Jun 14, 2024
5
proof-theoretic consistency in the introduction
HoTT/book#1156 · opened on Jun 14, 2024
6
Exercise 7.3 could be made stronger
HoTT/book#1151 · opened on Dec 29, 2023
Lemma 8.5.9 is missing a label
HoTT/book#1149 · opened on Oct 3, 2023
Corollary 8.8.5
HoTT/book#1148 · opened on Sep 22, 2023
4
Typos in proof of Lemma 10.3.12
HoTT/book#1134 · opened on Feb 3, 2023
5
identity type usage
HoTT/book#1128 · opened on Oct 13, 2022
19
Assumption that A // R is a set
HoTT/book#1126 · opened on Sep 21, 2022
4
Deducing propositional uniqueness for product types
HoTT/book#1122 · opened on Jun 11, 2022
1
Corollary 2.4.4. (use of naturality and whiskering)
HoTT/book#1121 · opened on Jun 9, 2022
9
"term" vs "element"
HoTT/book#1120 · opened on May 24, 2022
2
Lemma 2.1.2. Concatenation of paths
HoTT/book#1119 · opened on May 16, 2022
4
The initial σ-frame in Section 11.2
HoTT/book#1116 · opened on May 8, 2022
1
Code of conduct
HoTT/book#1111 · opened on Apr 12, 2022
23
Mismached functions in page 133 theorem 4.2.3
HoTT/book#1087 · opened on Aug 5, 2021
1