Skip to content

Issues: HoTT/book

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

73 Open 561 Closed
73 Open 561 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt click/return to exclude labels
or ⇧ click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Dependent elimination of propositional truncation IS useful
#1028 opened May 21, 2019 by marcbezem
A minor suggesion on lemma 8.5.3
#1020 opened Mar 14, 2019 by u8633321
1
Omega and Prop in the Book
#1018 opened Feb 15, 2019 by martinescardo
3
Claimed need for definitional equality in the definition of [dependent] type theories
#1017 opened Feb 8, 2019 by martinescardo
1
Univalent cardinals
#1002 opened Sep 21, 2018 by VincentSe
10
HoTT Book Definition 10.3.19 (bounded simulation)
#994 opened Aug 8, 2018 by martinescardo
2
Introduce indexed-subset notation
#993 opened Jun 20, 2018 by mikeshulman
6
Clearer discussion of UA, qinv-UA, and FE Fix in 2nd edition
#990 opened May 21, 2018 by mikeshulman
Always write ap_f(p) instead of f(p)? Fix in 2nd edition
#989 opened Apr 25, 2018 by mikeshulman
10
"make labelcheck" is broken
#978 opened Mar 10, 2018 by mikeshulman
× binds stronger than →
#949 opened Oct 10, 2017 by AxelBoldt
3
Better explanation of constructivity example in introduction
#947 opened Oct 10, 2017 by AxelBoldt
1
11.3.40 incorrect proof Fix now math bug
#900 opened Jul 7, 2016 by SkySkimmer
6
11.3.15 (extension of Lipschitz functions) incorrect Fix now math bug
#899 opened Jul 5, 2016 by SkySkimmer
7
Lemma 7.2.4 already proved in Corollary 3.2.7 feature request Fix in 2nd edition
#864 opened Sep 5, 2015 by louisGarde
2
Coinductive types? feature request Fix in 2nd edition
#787 opened Apr 22, 2015 by spacekitteh
5
Terminology for Sigma and truncated-Sigma Fix in 2nd edition
#780 opened Mar 7, 2015 by mikeshulman Second edition
5
Replace 'mere proposition' with 'truth value' Fix in 2nd edition
#779 opened Mar 7, 2015 by mikeshulman Second edition
8
Summarize other parts of HoTT in intro feature request Fix in 2nd edition
#763 opened Feb 3, 2015 by mikeshulman
4
Proofs of Lems. 7.2.9 and 7.3.1 math question
#744 opened Dec 6, 2014 by kristinas
3
Think about the beginning of chapter 2 feature request Fix in 2nd edition
#740 opened Nov 5, 2014 by mikeshulman Second edition
3
Explain more category theory feature request Fix in 2nd edition
#733 opened Oct 21, 2014 by mikeshulman Second edition
1
Use and introduction of identity types feature request
#730 opened Oct 20, 2014 by mikeshulman
13
Definition of concatenation
#729 opened Oct 20, 2014 by mikeshulman
Tell readers that Introduction is not essential for book understanding.
#727 opened Oct 17, 2014 by andrejbauer
8
ProTip! Adding no:label will show everything without a label.