Andrej Bauer
Andrej Bauer
Bibtex?
It would probably be useful to have a Bibtex version of each paper. An easy solution would be to just add it to each entry.
Following the events of #1101, I am opening an issue to discuss the adoption of a code of conduct. Please note that we already are bound by the [GitHub Community...
As Gershom points out on the HoTT mailing list, parts of the Introduction are fairly advanced and they intimidate beginners. We should explicitly state somewhere that the Introduction, or some...
The incremental improvements to the book are working very nicely, I think. But the fact that we decided not to change numbering is making it hard to iterate towards a...
The empty pages which make sure that chapters start on odd pages, etc., don't make sense in the ebook format, and quite possibly also in the online version.
Where do I report bugs? ```agda open import Relation.Binary.PropositionalEquality module Error where data N : Set where Z : N S : N → N infixr 5 _+_ _+_ :...
Coq is asking me why the left and the right side of the equation at the bottom of page 3 (the one that says 'apD Hrec (p_i a) = q_i...
Somewhere in the proof we presumably rely on the fact that there is a bound on how deeply the point constructors are nested in the path constructors. Where? (I do...
In Section 3, it is not explained anywhere what the purpose of all the data for the construction is. For instance, what are `Q` and `R` and `j_Q` about? These...
There is currently quite a lot of confusion in the paper. I am going to list the problems I see, but it's probably a bad idea to try to fix...