HoTT/book

Issues

• Possible Typo in Section 5.3

  #1064 opened 4 years ago
  3

• Missing substitution rule?

  #1061 opened 4 years ago
  3

• Definition and notation of dependent functions?

  #1060 opened 4 years ago
  6

• swap parameters for swap function

  #1059 opened 4 years ago
  3

• HoTT Book

  #1057 opened 5 years ago
  0

• Dangling sentence at the end of Sec. 11.1

  #1053 opened 5 years ago
  0

• Slight contradiction between sections A.2.1 and A.2.2

  #1051 opened 4 years ago
  30

• Links on https://homotopytypetheory.org/book/ are broken

  #1049 opened 5 years ago
  1

• Error in A.1.2

  #1046 opened 5 years ago
  0

• Relate exercises to relevant sections

  #1045 opened 5 years ago
  0

• Inconsistent notations regarding composition

  #1043 opened 5 years ago
  31

• Exercise 11.2 refers to a term "boundedness" which is not defined

  #1041 opened 5 years ago
  1

• Simpler multiplication on circle Lemma 8.5.8

  #1039 opened 5 years ago
  4

• §2.12 maybe wrong prove step when showing decode ( x, encode ( x, p )) = p

  #1033 opened 5 years ago
  2

• are there plans for a real-cohesive homotopy type theory book?

  #1030 opened 5 years ago
  2

• Help finding an image

  #1029 opened 6 years ago
  2

• Dependent elimination of propositional truncation IS useful

  #1028 opened 6 years ago
  0

• Maybe a typo on page 300

  #1022 opened 5 years ago
  3

• Same letter $P$ is used for different propose in the proof of a lemma

  #1021 opened 6 years ago
  1

• A minor suggesion on lemma 8.5.3

  #1020 opened 6 years ago
  1

• Omega and Prop in the Book

  #1018 opened 6 years ago
  3

• Claimed need for definitional equality in the definition of [dependent] type theories

  #1017 opened 6 years ago
  1

• Broken link in voe12 reference

  #1015 opened 5 years ago
  1

• Switches for changing notation

  #1011 opened 5 years ago
  2

• Lebesgue measure in HOTT

  #1007 opened 6 years ago
  2

• Suggestion: use different example for binding rule of dependent pair types

  #1004 opened 6 years ago
  1

• Univalent cardinals

  #1002 opened 6 years ago
  10

• A suggestion of an exercise about split monomorphisms

  #999 opened 6 years ago
  1

• Elimination of products

  #997 opened 6 years ago
  1

• Include eta-conversion in A.1

  #995 opened 5 years ago
  25

• HoTT Book Definition 10.3.19 (bounded simulation)

  #994 opened 6 years ago
  2

• Introduce indexed-subset notation

  #993 opened 7 years ago
  6

• Clearer discussion of UA, qinv-UA, and FE

  #990 opened 7 years ago
  0

• Always write ap_f(p) instead of f(p)?

  #989 opened 7 years ago
  10

• keep old nightly builds around

  #986 opened 4 years ago
  8

• Missing inverse

  #980 opened 7 years ago
  1

• "make labelcheck" is broken

  #978 opened 7 years ago
  0

• Tagalog Localization/Translation

  #976 opened 5 years ago
  2

• Cebuano Localization

  #974 opened 5 years ago
  1

• Translation to Spanish

  #969 opened 7 years ago
  8

• Wrong definition for the return type at paragraph 5.3

  #965 opened 2 years ago
  2

• Gap in proof of Lemma 3.8.2

  #964 opened 7 years ago
  3

• Update "in preparation" references?

  #957 opened 7 years ago
  1

• Travis is broken?

  #950 opened 7 years ago
  6

• × binds stronger than →

  #949 opened 7 years ago
  3

• Syntax rule for dependent function types

  #948 opened 7 years ago
  2

• Better explanation of constructivity example in introduction

  #947 opened 7 years ago
  1

• Technical error in first sentence of section 1.9

  #946 opened 7 years ago
  1

• Confusing Notation in Section 1.6

  #943 opened 7 years ago
  13

• Ill-typed equality in 6.7, last bullet point

  #942 opened 7 years ago
  3