HoTT/book

Issues

• typos in proof of 7.3.12, and other comments about that proof

  #940 opened 7 years ago
  2

• Update Lulu paperback version

  #939 opened 8 years ago
  7

• typo in 8.10

  #937 opened 8 years ago
  2

• The definition of disc is out of border in ebook version (68th page).

  #930 opened 8 years ago
  0

• Formal type theory : Dependent function types

  #929 opened 7 years ago
  11

• How to cite bibliography entries from errata list?

  #928 opened 7 years ago
  8

• Section numbers missing

  #923 opened 8 years ago
  1

• Suggestion of an exercise about connectedness

  #920 opened 7 years ago
  5

• \choice{\infty,\infty} in Exercise 7.8

  #915 opened 8 years ago
  2

• Lemma 2.9.6 Ambiguous / confusing language

  #913 opened 8 years ago
  6

• Notation `v ∈ V` in Section 10.5

  #912 opened 8 years ago
  8

• Ambiguous variable bindings in Exercise 10.13

  #910 opened 8 years ago
  3

• what does the book mean by "making the latter more explicit" in section '6.5 Suspensions' ?

  #905 opened 8 years ago
  8

• Different arrows: confusion

  #903 opened 8 years ago
  5

• Missing proof obligation in Corollary 7.7.3 (Reflective subuniverse preserves products)

  #901 opened 7 years ago
  1

• 11.3.40 incorrect proof

  #900 opened 8 years ago
  6

• 11.3.15 (extension of Lipschitz functions) incorrect

  #899 opened 8 years ago
  7

• The book bugs on TeX Live 2016

  #898 opened 9 years ago
  6

• "R_c-induction" can *only* show mere propositions

  #897 opened 8 years ago
  4

• Link to pdf for on screen viewing (and the other hott book links on website) down

  #896 opened 9 years ago
  2

• Topological example in 1.12.1 goes into the margin.

  #892 opened 7 years ago
  6

• Potential problem with Definition 7.4.7

  #887 opened 7 years ago
  0

• axioms, rules, canonicity

  #885 opened 7 years ago
  2

• inconsistent use of hyphen in "path-constructor"

  #882 opened 9 years ago
  16

• correction to reference

  #881 opened 8 years ago
  3

• New release?

  #872 opened 9 years ago
  14

• Path induction, possible typo

  #870 opened 9 years ago
  4

• Make it more clear that univalence axiom is not "(A=B) ~ (A~B)"

  #869 opened 9 years ago
  2

• A theorem proves contractibility by showing ∑a, Π x (x = a) instead of the other direction.

  #868 opened 9 years ago
  4

• Extra path ?

  #867 opened 9 years ago
  2

• A remark by Thomas Streicher

  #866 opened 9 years ago
  1

• Lemma 7.2.4 already proved in Corollary 3.2.7

  #864 opened 9 years ago
  2

• yoneda lemma inverse proof functor misalignment?

  #862 opened 9 years ago
  7

• Proposal for an alternative description of the cumulative hierarchy of sets V

  #861 opened 9 years ago
  16

• Link to PDF output from the GitHub project description or README.md

  #857 opened 9 years ago
  1

• Proof of Lemma 6.12.4

  #854 opened 9 years ago
  1

• exponential category missing in Index of Symbols

  #851 opened 9 years ago
  31

• Unclear abuse of notation in the definition of the free group as a set-quotient.

  #850 opened 9 years ago
  2

• Equivalence between retractions and split surjections

  #849 opened 9 years ago
  1

• Adjunctions question

  #847 opened 9 years ago
  7

• keep old nightly builds around for a day

  #846 opened 8 years ago
  5

• missing definition of named equivalence

  #841 opened 9 years ago
  5

• ZFC with urelements

  #836 opened 9 years ago
  3

• abuse of language: "f : A \equiv B" vs "f: A -> B"

  #819 opened 10 years ago
  1

• Why brackets in $\Prod_{(x:A)} ...$?

  #805 opened 10 years ago
  2

• The Second Presentation and induction from functions

  #804 opened 9 years ago
  1

• Configure travis to automatically post nightly builds

  #799 opened 9 years ago
  44

• Theorem 10.4.4

  #796 opened 10 years ago
  1

• Theorem 10.5.8(vi) proof

  #794 opened 10 years ago
  12

• Theorem 10.2.10

  #793 opened 9 years ago
  5