Issues

• Inconsistent notation for the type of pointed types

  HoTT/book#1197 · Filter by author Yosuke-Ito-345 opened on Jul 11, 2026

• Nightly build can't find package gh

  HoTT/book#1195 · Filter by author mikeshulman opened on May 13, 2026

• Clarification about judgmental unequality

  HoTT/book#1194 · Filter by author Yosuke-Ito-345 opened on Feb 14, 2026
  6

• Explanation of “fundamental group” is confusing

  HoTT/book#1190 · Filter by author Bolpat opened on Aug 27, 2025
  2

• Simplifications for Theorem 11.2.12 {RD-cauchy-complete}

  HoTT/book#1167 · Filter by author lowasser opened on Mar 27, 2025
  2

• Incorrect diagram for Example 8.7.16

  HoTT/book#1163 · Filter by author roconnor opened on Sep 2, 2024
  1

• Exercise 11.6 seems to need WLPO not LPO

  HoTT/book#1162 · Filter by author jkingdon opened on Aug 4, 2024
  3

• max and sup

  HoTT/book#1161 · Filter by author ncfavier opened on Jul 13, 2024
  9

• Switch to using truncated logic as default in the book

  HoTT/book#1160 · Filter by author ghost opened on Jun 19, 2024
  2

• real numbers in the introduction

  HoTT/book#1158 · Filter by author mikeshulman opened on Jun 15, 2024
  7

• cardinal numbers in the introduction

  HoTT/book#1157 · Filter by author mikeshulman opened on Jun 14, 2024
  5

• proof-theoretic consistency in the introduction

  HoTT/book#1156 · Filter by author mikeshulman opened on Jun 14, 2024
  6

• Exercise 7.3 could be made stronger

  HoTT/book#1151 · Filter by author ncfavier opened on Dec 29, 2023

• Lemma 8.5.9 is missing a label

  HoTT/book#1149 · Filter by author Alizter opened on Oct 3, 2023

• Corollary 8.8.5

  HoTT/book#1148 · Filter by author blindFS opened on Sep 22, 2023
  4

• Typos in proof of Lemma 10.3.12

  HoTT/book#1134 · Filter by author LuuBluum opened on Feb 3, 2023
  5

• identity type usage

  HoTT/book#1128 · Filter by author DanGrayson opened on Oct 13, 2022
  19

• Assumption that A // R is a set

  HoTT/book#1126 · Filter by author FernandoChu opened on Sep 21, 2022
  4

• Deducing propositional uniqueness for product types

  HoTT/book#1122 · Filter by author tbrs2 opened on Jun 11, 2022
  1

• Corollary 2.4.4. (use of naturality and whiskering)

  HoTT/book#1121 · Filter by author IanRay11 opened on Jun 9, 2022
  9

• "term" vs "element"

  HoTT/book#1120 · Filter by author ghost opened on May 24, 2022
  2

• Lemma 2.1.2. Concatenation of paths

  HoTT/book#1119 · Filter by author IanRay11 opened on May 16, 2022
  4

• The initial σ-frame in Section 11.2

  HoTT/book#1116 · Filter by author ghost opened on May 8, 2022
  1

• Code of conduct

  HoTT/book#1111 · Filter by author andrejbauer opened on Apr 12, 2022
  23

• Mismached functions in page 133 theorem 4.2.3

  HoTT/book#1087 · Filter by author wgbusch opened on Aug 5, 2021
  1