Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: deprecated: history of ideas

Topic: HOTT Book


view this post on Zulip Aleks Kissinger (Aug 28 2020 at 10:30):

Hi @Mike Shulman and @Steve Awodey, I'm curious about your experience in writing (or rather leading the writing of) a massive open-source math textbook https://github.com/HoTT/book.

Did you or some of the other authors write anything about this? And anyway, would you be willing to answer some general big-picture questions here?

view this post on Zulip Mike Shulman (Aug 28 2020 at 13:02):

There were some blog posts when the book first came out: https://homotopytypetheory.org/2013/06/20/the-hott-book/, https://golem.ph.utexas.edu/category/2013/06/the_hott_book.html, http://math.andrej.com/2013/06/20/the-hott-book/. And here are some slides from a talk I gave once that might be relevant: http://home.sandiego.edu/~shulman/papers/nlabhott.pdf. I'd be happy to answer questions too.

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 13:24):

Great. I'll have a read through those, and see what's left to say. :)

view this post on Zulip Jules Hedges (Aug 28 2020 at 13:49):

Is this a secret hint that there could be an open source CQM book in the future?

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 14:22):

@Mike Shulman I guess the thing that interested me the most, which you already touched on in your blog and talk, was how you and the other core writers kept the whole thing from falling into chaos. You mentioned in your slides a "unity of vision" of the core contributors, which really helped. Is that something you more or less had from the start, or was it (perhaps painstakingly) established during writing?

view this post on Zulip Steve Awodey (Aug 28 2020 at 14:54):

Andrej Bauer wrote a nice article for the Institute Letter, which is here:
https://www.ias.edu/ideas/2013/bauer-hott-book
don't miss the neat video linked there depicting the authorship of the book.
Andrej was also interviewed about it for an article in Wired magazine - maybe someone has the link.

view this post on Zulip Steve Awodey (Aug 28 2020 at 15:14):

One thing that should be remembered is that we were basically living together on a space ship for nearly a year, meeting daily for seminars, working groups, tea, meals, walks, etc. GitHub allowed us to do the actual writing and that was necessarily online, but there was a lot face to face interaction and discussion that wasn't online - even sometimes sitting around a big table with laptops open and writing text together while discussing it. I think it would be very different trying to do everything online.

view this post on Zulip Mike Shulman (Aug 28 2020 at 15:17):

Maybe this one? https://www.wired.com/2013/06/cades-witty-headline-here/

view this post on Zulip Steve Awodey (Aug 28 2020 at 15:19):

yup

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 15:23):

Steve Awodey said:

One thing that should be remembered is that we were basically living together on a space ship for nearly a year, meeting daily for seminars, working groups, tea, meals, walks, etc.

Sounds like fun. :) Also very intense.

view this post on Zulip Mike Shulman (Aug 28 2020 at 15:24):

Steve is right that being all together at IAS for a year was very helpful. Also, the long list of participants in the preface may be a bit misleading as the number of people actively writing large amounts of text for the book was significantly smaller (roughly enough to fit around a large table, as Steve says). However, I don't think it would be impossible to manage online, even with a larger number of contributors, as long as there were one or a few "dictators" who had a coherent vision and were enabled to freely edit everything. Wikipedia manages to have a surprisingly consistent style despite having orders of magnitude more editors.

view this post on Zulip Steve Awodey (Aug 28 2020 at 17:08):

I suppose that zoom meetings could also replace some of the face-to-face interaction.

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 17:43):

Steve Awodey said:

I suppose that zoom meetings could also replace some of the face-to-face interaction.

Yeah. Though probably pretty hard to recreate that "hackathon" atmosphere of a lot of people around a table tex'ing/coq'ing away.

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 17:44):

How did you decide who to call an author (vs someone who did a couple of pull req's)? Was there some particular threshold, or just kindof common sense?

view this post on Zulip Mike Shulman (Aug 28 2020 at 17:54):

Technically no person is explicitly designated as an "author" of the HoTT Book. The people listed in the preface are all the participants of the special year, all of whom we regard as having contributed something to the book, whether by writing some of the text or by development of the ideas expressed therein. So we didn't have to set any threshold or make any judgment calls.

view this post on Zulip Mike Shulman (Aug 28 2020 at 17:56):

Post-publication, various fixes have been contributed on github by others who were not at the special year, but we tried to be clear in advance that although we invite such contributions (subject to our policies about what sorts of changes will be made to the first edition), they will not be given any sort of coauthor credit.

view this post on Zulip Steve Awodey (Aug 28 2020 at 18:27):

except the fame that comes with an accepted pull request!

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 19:37):

Mike Shulman said:

Technically no person is explicitly designated as an "author" of the HoTT Book.

That's pretty radical, maybe more so that than doing the whole thing "open source" in the first place. But it also makes sense. No need to make awkward decisions about who's in the "in crowd" and who's not.

view this post on Zulip Aleks Kissinger (Aug 28 2020 at 19:47):

What sorts of procedures / roles / documents / etc did you set up to help keep things uniform and going in the right direction? Was there anything you didn't do from the start that you wish you had?

view this post on Zulip Mike Shulman (Aug 28 2020 at 21:29):

Unfortunately my memory is kind of spotty. If I'd known at the time people would be so interested in the process of writing the book, I would have paid better attention and maybe taken notes!

view this post on Zulip Mike Shulman (Aug 28 2020 at 21:32):

One thing I do remember that I think was helpful was to enforce the use of semantic LaTeX macros. That allowed us to sidestep many arguments about notation by saying "just use the macro; later on we can change the macro definition." I believe we had a "technical dictator" whose job was to uniformize everyone's LaTeX code to use the semantic macros.

view this post on Zulip Mike Shulman (Aug 28 2020 at 21:34):

I believe we did assign specific chapters to specific people at the beginning, although the particular assignments didn't always persist. I have a vague memory of there being someone designated as a dictator of another sort too, but I can't remember what it was.

view this post on Zulip Mike Shulman (Aug 28 2020 at 21:37):

Oh, I see from https://ncatlab.org/ufias2012/published/The+book (archived from the wiki we used during the special year) that it was a "logical dictator". But I don't remember what that meant.

view this post on Zulip Aleks Kissinger (Aug 30 2020 at 11:34):

would be interesting to know what the "logical dictator" did. maybe making sure you used the same exact version/formulation of axioms and rules throughout?

view this post on Zulip Nikolaj Kuntner (Aug 30 2020 at 16:10):

Crazy to think the book was released over 7 years ago.