Introduction to Homotopy Type Theory](https://arxiv.org/abs/2212.11082) (Egbert Rijke)

Typos:

  • p. 9: “It also provides the identity function on the type 𝐴 in context Γ.” - unclear; reference Definition 2.2.3?
  • p. 11: “term” - same as “element”? Define at first occurrence: “what is on the left of the : in the typing judgement”…
  • p. ?: “extensional”….
  • p. ?: := - introduce the symbol before its use
  • p. ?: “generic element”
  • p. 14: “domain” is defined - but it was used before (p. 12)
  • p. 15: “In the special case where …, then we often write” - spurious “then”
  • p. 16: 𝑔 ◦ 𝑓 - notation was already introduced on p. 15
  • p. 16: “generic functions of 𝐴 → 𝐵 and 𝐵 → 𝐶 can also be evaluated” - unclear
  • p. 18: “𝑓 and 𝑔 take equal values” - is “take values” now accepted terminology?
  • p. 22: “for each step in the induction principle, covering the base case and the inductive step” - first occurrence of “step” should be changed to something else
  • p. 28: “if we assume the empty type has a term, then we can prove anything” - Curry-Howard correspondence was not yet introduced (see p. 31)
  • p. 28: “…because ex falso quodlibet” - because?!
  • p. 32: “0” should have the N subscript (Natural 0)
  • p. ??, p. 38: - propositions as types (types as proof-relevant propositions) referenced but not introduxed
  • p. 38: “how should we think of the elements of 𝑥 = 𝑦.” - maybe question mark?
  • p. 39: “all functions preserve equality” - maybe, preserve identification?