State explicitly that the HoTT book is not the definitive work on the subject.

[andrejbauer]

The statement by@mikeshulman in his blog post The HoTT Book does not define HoTT should be reflected somewhere in the book.

The best place for it would be very early on. One possibility is to put it at the beginning of "How to read this book" in the introduction. Another is to create new section of the introduction "Hot not to read this book". We could explain that historically the book originated from Peter Aczel's group at IAS, and generally summarize all the things that Mike said in the blog post.

On the other hand, we do say that the book is an experiment, that the subject is young etc. So, this is an issue.

[vladimirias]

On Jan 29, 2015, at 3:00 AM, Andrej Bauer notifications@github.com wrote:

We could explain that historically the book originated from Peter Aczel's group at IAS,

I think saying this explicitly would be very helpful.

Vladimir.

[andrejbauer]

In Preface we read:

We did not set out to write a book. The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine.

Is this enough?

Historical notes with people's names are usually in the Chapter notes of each chapter, not in the main text. Generally, we did not tally up the pieces of the book and we purposely kept it all very homogeneous. What do others think? I have no problem mentioning Peter, he of course deserves it, but I want to stick to the style of the book, which is not to disclose too much information on who did what.

[awodey]

I think we should not change the preface. We can add something to the introduction. I don't mind mentioning Peter's WG as the origin, as long as it's clear that the book goes far beyond that. The main point should be Mike's that there is more to HoTT than is in the book

Sent from my iPhone

On Jan 30, 2015, at 2:30 AM, Andrej Bauer notifications@github.com wrote:

In Preface we read:

We did not set out to write a book. The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine.

Is this enough?

Historical notes with people's names are usually in the Chapter notes of each chapter, not in the main text. Generally, we did not tally up the pieces of the book and we purposely kept it all very homogeneous. What do others think? I have not problem mentioning Peter, he of course deserves it, but I want to stick to the style of the book, which is not to disclose too much information on who did what.

— Reply to this email directly or view it on GitHub.

[vladimirias]

The book does not reflect my views. It is because of this that I want it to state clearly how it appeared.

Vladimir.

On Jan 30, 2015, at 2:30 AM, Andrej Bauer notifications@github.com wrote:

In Preface we read:

We did not set out to write a book. The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine.

Is this enough?

Historical notes with people's names are usually in the Chapter notes of each chapter, not in the main text. Generally, we did not tally up the pieces of the book and we purposely kept it all very homogeneous. What do others think? I have not problem mentioning Peter, he of course deserves it, but I want to stick to the style of the book, which is not to disclose too much information on who did what.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/760#issuecomment-72164294.

[awodey]

the first section of the Introduction concludes with this:

We emphasize that homotopy type theory is a young field, and univalent foundations is very much a work in progress. This book should be regarded as a “snapshot” of the state of the field at the time it was written, rather than a polished exposition of an established edifice. As we will discuss briefly later, there are many aspects of homotopy type theory that are not yet fully understood — but as of this writing, its broad outlines seem clear enough. The ultimate theory will probably not look exactly like the one described in this book, but it will surely be at least as capable and powerful; we therefore believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.

this could be expanded a bit to also emphasize that there are many topics that are not even touched on in the book.

On Jan 30, 2015, at 11:15 AM, Vladimir Voevodsky notifications@github.com wrote:

The book does not reflect my views. It is because of this that I want it to state clearly how it appeared.

Vladimir.

On Jan 30, 2015, at 2:30 AM, Andrej Bauer notifications@github.com wrote:

In Preface we read:

We did not set out to write a book. The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine.

Is this enough?

Historical notes with people's names are usually in the Chapter notes of each chapter, not in the main text. Generally, we did not tally up the pieces of the book and we purposely kept it all very homogeneous. What do others think? I have not problem mentioning Peter, he of course deserves it, but I want to stick to the style of the book, which is not to disclose too much information on who did what.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/760#issuecomment-72164294.

— Reply to this email directly or view it on GitHub.

[mikeshulman]

@awodey that does seem like a natural place for it. In particular, we probably ought to change the phrase "snapshot of the state of the field" as it can easily be read to imply that the book is a snapshot of the entire state of the field.

[awodey]

We emphasize that homotopy type theory is a young field, and univalent foundations is very much a work in progress. This book should be regarded as a “snapshot” of just one portion of the field, taken at the time it was written, rather than a polished exposition of an completed edifice. As we will discuss briefly later, there are many aspects of homotopy type theory that are not yet fully understood — and some that are not even touched upon here. The ultimate theory will almost certainly not look exactly like the one described in this book, but it will surely be at least as capable and powerful; we therefore believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.

On Jan 30, 2015, at 1:35 PM, Mike Shulman notifications@github.com wrote:

@awodey https://github.com/awodey that does seem like a natural place for it. In particular, we probably ought to change the phrase "snapshot of the state of the field" as it can easily be read to imply that the book is a snapshot of the entire state of the field.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/760#issuecomment-72247887.

[andrejbauer]

Will you make a pull request? It addresses well what Mike said.

[awodey]

Will do.

Sent from my iPhone

On Jan 31, 2015, at 4:07 AM, Andrej Bauer notifications@github.com wrote:

Will you make a pull request? It addresses well what Mike said.

— Reply to this email directly or view it on GitHub.

[andrejbauer]

I think #761 closes this issue.

[mikeshulman]

Steve's fix is good, but reading over the introduction again I think there is something else missing: a brief summary of the other aspects of the field that the book is not about. The "Open problems" section makes some reference to these, but I think it may be more confusing than helpful to discuss open problems without having at least a very vague idea of the outlines of current knowledge.

[andrejbauer]

Reopen or new issue?