Tell readers that Introduction is not essential for book understanding.

[andrejbauer]

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 piece of it, may be safely skipped. Where would be the best place to do so?

[vladimirias]

Why not to create a special section or sections where these issues will be discussed and move them from the introduction to these sections?

Having something in the narrative and then saying that this is better skipped on the first read is, I think, a very unpleasant practice.

Vladimir.

On Oct 17, 2014, at 7:46 PM, Andrej Bauer notifications@github.com wrote:

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 piece of it, may be safely skipped. Where would be the best place to do so?

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

[andrejbauer]

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 parts of the introduction (because they lack a piece of background knowledge). They mistakenly think that they won't be able to read the rest of the book.

I wouldn't scale down the introduction, because it is the right place to explain "the big picture" and to give an overview of things. We just need to put in a short remark somewhere that say "you can move on".

[awodey]

I agree.

Sent from my iPhone

On Oct 17, 2014, at 5:16 PM, Andrej Bauer notifications@github.com wrote:

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 parts of the introduction (because they lack a piece of background knowledge). They mistakenly think that they won't be able to read the rest of the book.

I wouldn't scale down the introduction, because it is the right place to explain "the big picture" and to give an overview of things. We just need to put in a short remark somewhere that say "you can move on".

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

[EgbertRijke]

The problem Gershom brought to attention exists for two reasons:

• we didn't tell anywhere what sort of background knowledge we require of the reader.
• we didn't tell the purpose of the story we tell in the introduction.

So somebody who is reading this for the first time might think (1) he needs to have knowledge of the subjects we mention there and (2, this is pointed out by Martin) that we will delve deeper into the connections with the subjects we mention in the introduction.

Saying that "you can safely skip the introduction" doesn't accurately solve this problem (and understandably some people might be annoyed when reading such a sentence). Before we move to the section "Type theory" we need what we're doing in the introduction and that main body of the book is self-contained so that we do not require knowledge of any specific field of mathematics or computer science. With this information, the reader can judge for himself whether he's willing to skip the introduction or not.

I suggest that to the end of the third paragraph we add: "In this introduction, we will sketch a broad overview of what homotopy type theory is and how it is related to other fields of mathematics and computer science, but in fact no knowledge of any of these related fields is required in the rest of the book." To the sentence "This book is intended as a first systematic [ast] exposition..." we might add "and accessible" at the [ast].

[andrejbauer]

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".

[mikeshulman]

336

[louisGarde]

I suggest that you use the Hott amateurs group to ask for a feedback from beginners: what are the concepts that were the more difficult to understand with no/poor background in homotopy theory and/or category theory ?

With my experience as a beginner, I have not found the introduction intimidating. It was clear to me that the book would not teach me the concepts of Logic, Set theory, Homotopy theory or Category theory that I am missing but "only" how to do the mathematics I already know in a new way. The introduction makes it very clear what are the concepts that you need to understand; everything else is optional and just depends on your knowledge and motivations.

[jkingdon]

I'm a beginner who hasn't gotten very far into the book yet. EgbertRijke's suggestion is on the right track, and I'll also note that the most reassuring part of the introduction is "How to read this book". Perhaps the section of the introduction on type theory could say something like "in chapter 1, or more formally in appendix A, we give the rules of type theory" (and likewise for the other sections). Writing this sort of introduction will never be easy. For me, the mentions of univalence, spaces, paths, and category theory were intimidating and I picked up the book hoping to learn type theory from essentially no type theory, but constructive logic was a piece of cake. Other people might be very much hung up on the constructive aspects of the logic (either in terms of understanding how it functions, or whether they think it is practical), so reassuring words are called for there.

Even univalence, which is a bit of a mind stretch, seems worth mentioning early. I certainly got it at the level of 'isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the “official” doctrines of conventional foundations', even if the more technical discussion of Kan simplicial sets and the like fell into the category of "I hope this isn't a prerequisite".