Andrej Bauer

In addition to a statement of welcoming and inclusivity, it might be a good idea to state that the issue and the pull requests are dedicated to improvements, questions, and...

Being an administrator is predominantly a technical role, not a leadership role. The administrators are the people who currently maintain the book, or have done so actively in the past....

I think the problem is that the Introduction is very useful for some people, but there are others who seem to be discouraged by the fact that they don't understand...

I like Egbert's thinking. We could also add a whole section to the introduction "Background knowledge" or "Prerequisites", and possibly even "What is in the book".

Without a doubt we should follow the open source community here. Which means that we would branch, what Vladimir proposes would make sense if we did not have Github. But...

There are various settings which default to `master` unless otherwise specified. I'll try to figure out whether the open source community has good reasons for their scheme (and whether I...

Have a look at issue #287. @loopspace (Andrew Stacey) made some progress in converting the book to HTML.

Wow, we're practically there.

As in "add coinductive types" to the HoTT book? That would be something for 2nd edition.

Do we need the identity types for any purpose other than to have a non-trivial dependent type?