Make sure each chapter beginning is in accordance with "how to read this book"

[andrejbauer]

"How to read this book" in the introduction claims that "Each chapter in Part II begins with a brief overview of its subject, what univalent foundations has to contribute to it, and the necessary background from Part I". Make sure this is actually the case, or water down the claim.

[mikeshulman]

Yeah, this is something I discussed with Dan Licata yesterday. The introduction to the Homotopy Theory chapter was intended to do this, and at first it seemed weird to me, but after some discussion I started to feel that actually it might be a good idea for all the chapters in Part II to do it.

[dlicata335]

I think it's important to do this for the computer scientists in the audience, especially since some of them may be reading the book because they are interested in contributing to formalizations. Obviously we can't teach all of homotopy theory/category theory/set theory, but having a few pages to get people oriented seems useful.

[awodey]

in that case, it needs to say clearly (like in a section title) that it is "a sketch of homotopy theory for type theorists" -- or something of that sort.
Otherwise, I share Mike's impression that it's wierd.

But I don't think we need a few pages of "category theory for type theorists" or "set theory for type theorists" -- we can assume some prerequisites.

On Apr 17, 2013, at 9:51 AM, Dan Licata notifications@github.com wrote:

I think it's important to do this for the computer scientists in the audience, especially since some of them may be reading the book because they are interested in contributing to formalizations. Obviously we can't teach all of homotopy theory/category theory/set theory, but having a few pages to get people oriented seems useful.

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

[mikeshulman]

Not a few pages, no, but I think some short overview of each Part II
chapter "for those just joining us" could be helpful.

On Wed, Apr 17, 2013 at 10:06 AM, Steve Awodey notifications@github.comwrote:

in that case, it needs to say clearly (like in a section title) that it is
"a sketch of homotopy theory for type theorists" -- or something of that
sort.
Otherwise, I share Mike's impression that it's wierd.

But I don't think we need a few pages of "category theory for type
theorists" or "set theory for type theorists" -- we can assume some
prerequisites.

On Apr 17, 2013, at 9:51 AM, Dan Licata notifications@github.com wrote:

I think it's important to do this for the computer scientists in the
audience, especially since some of them may be reading the book because
they are interested in contributing to formalizations. Obviously we can't
teach all of homotopy theory/category theory/set theory, but having a few
pages to get people oriented seems useful.

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

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16507505
.

[andrejbauer]

So what would one say about the real numbers, for example? Do I need to explain what a field is?

[DanGrayson]

No, the book is addressed to mathematicians.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer notifications@github.comwrote:

So what would one say about the real numbers, for example? Do I need to
explain what a field is?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16520453
.

[awodey]

Sent from my iPhone

On Apr 17, 2013, at 1:47 PM, "Daniel R. Grayson" notifications@github.com wrote:

No, the book is addressed to mathematicians.

Which is why the intro to homotopy seems weird.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer notifications@github.comwrote:

So what would one say about the real numbers, for example? Do I need to
explain what a field is?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16520453
.

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

[dlicata335]

Here are the audiences that I think we could serve a little better by easing into the chapters in part 2 with a bit of an introduction:
(1) computer scientists who are interested in learning how we use HoTT to do math, e.g. because they are interested in contributing to formalizations. For this audience, it would be totally alienating to assume they know e.g. homotopy theory. But giving enough context that they can at least read and understand the material in that chapter seems doable, since it starts from fairly basic things (pi1(S1)). I don't know to what extent the same is true for the other chapters, but just giving a bit a of big picture sense of the field would be nice for context.
(2) mathematicians who flip to the chapter on a subject without reading part 1 and want to see if what we're doing is interesting. For this audience, it would be good to have some statement about what we think is good about our approach to this subject.

BTW, I totally disagree that the book is "addressed to mathematicians". We listed lots of possible audiences during the Tuesday meetings, and I don't remember a discussion in which we decided that this book was for mathematicians, and computer scientists can write their own book (maybe I was out of town? :) ). HoTT is an interdisciplinary project between mathematicians and computer scientists. There are lots of people in the dependent types community who are interested in this stuff. Why write off a big portion of the potential readership, when it would be so easy to make them feel included? A mathematician can easily skip ahead if a section feels familiar, just as a computer scientist can easily skip, say, the intro to type theory in chapter 1.

Anyway, I am in the middle of revising the intro to the homotopy chapter based on these thoughts and Mike's suggestion of moving some of it into chapter 2. So you can see what you think then.

[RobertHarper]

ok, fools wade in where sane people dare not tread. my main complaint is precisely that the book is addressed to mathematicians. for me computer scientists ought also to be the audience for this book, but they are not. consequently, it's perfectly ok to speak about presheaves and fibrations, but we dare not use a turnstile, or utter the word "judgement" for fear of offending the mathematicians. but i would say that the situation is precisely dual for computer scientists, and i regret that we are not treating both audiences with equanimity.

bob

On Apr 17, 2013, at 1:47 PM, Daniel R. Grayson wrote:

No, the book is addressed to mathematicians.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer notifications@github.comwrote:

So what would one say about the real numbers, for example? Do I need to
explain what a field is?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16520453
.

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

[cangiuli]

I agree with Dan L. I don't think it's unreasonable to give a short overview of each chapter in Part II. That does not mean we have to include a complete undergraduate math program.

While the book should not be "for mathematicians", it is a book of math (in type theory), not a book of computer science. This is the justification for using mathematical language; the audience is not the justification.

[spitters]

I agree. It would be nice to serve both audiences.
Moreover, I believe we are building a community of people that fit both
descriptions.

On Wed, Apr 17, 2013 at 8:27 PM, Robert Harper notifications@github.comwrote:

ok, fools wade in where sane people dare not tread. my main complaint is
precisely that the book is addressed to mathematicians. for me computer
scientists ought also to be the audience for this book, but they are not.
consequently, it's perfectly ok to speak about presheaves and fibrations,
but we dare not use a turnstile, or utter the word "judgement" for fear of
offending the mathematicians. but i would say that the situation is
precisely dual for computer scientists, and i regret that we are not
treating both audiences with equanimity.

bob

On Apr 17, 2013, at 1:47 PM, Daniel R. Grayson wrote:

No, the book is addressed to mathematicians.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer notifications@github.comwrote:

So what would one say about the real numbers, for example? Do I need
to
explain what a field is?

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16520453>
.

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

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16524144
.

[DanGrayson]

I am swayed by the recent cogent statements by everybody -- maybe we should
say what a field is.

On Wed, Apr 17, 2013 at 2:50 PM, spitters notifications@github.com wrote:

I agree. It would be nice to serve both audiences.
Moreover, I believe we are building a community of people that fit both
descriptions.

On Wed, Apr 17, 2013 at 8:27 PM, Robert Harper notifications@github.comwrote:

ok, fools wade in where sane people dare not tread. my main complaint is
precisely that the book is addressed to mathematicians. for me computer
scientists ought also to be the audience for this book, but they are
not.
consequently, it's perfectly ok to speak about presheaves and
fibrations,
but we dare not use a turnstile, or utter the word "judgement" for fear
of
offending the mathematicians. but i would say that the situation is
precisely dual for computer scientists, and i regret that we are not
treating both audiences with equanimity.

bob

On Apr 17, 2013, at 1:47 PM, Daniel R. Grayson wrote:

No, the book is addressed to mathematicians.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer <
notifications@github.com>wrote:

So what would one say about the real numbers, for example? Do I need
to
explain what a field is?

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16520453>
.

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

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16524144>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16531616
.

[mikeshulman]

Actually, the chapter does already say what a field is!
On Apr 17, 2013 4:04 PM, "Daniel R. Grayson" notifications@github.com
wrote:

I am swayed by the recent cogent statements by everybody -- maybe we
should
say what a field is.

On Wed, Apr 17, 2013 at 2:50 PM, spitters notifications@github.com
wrote:

I agree. It would be nice to serve both audiences.
Moreover, I believe we are building a community of people that fit both
descriptions.

On Wed, Apr 17, 2013 at 8:27 PM, Robert Harper notifications@github.comwrote:

ok, fools wade in where sane people dare not tread. my main complaint
is
precisely that the book is addressed to mathematicians. for me
computer
scientists ought also to be the audience for this book, but they are
not.
consequently, it's perfectly ok to speak about presheaves and
fibrations,
but we dare not use a turnstile, or utter the word "judgement" for
fear
of
offending the mathematicians. but i would say that the situation is
precisely dual for computer scientists, and i regret that we are not
treating both audiences with equanimity.

bob

On Apr 17, 2013, at 1:47 PM, Daniel R. Grayson wrote:

No, the book is addressed to mathematicians.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer <
notifications@github.com>wrote:

So what would one say about the real numbers, for example? Do I
need
to
explain what a field is?

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16520453>
.

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

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16524144>
.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16531616>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16532270
.

[awodey]

I don't think we should explain every old basic concept from math grad school -- people can use google.
besides, providing definitions of basic stuff everywhere only dumbs things down and will put the knowledgable reader off -- unless it's clearly marked as a "sketch of X for Y", and isolated from the rest of the text, so it can be skipped by someone who doesn't need it.

On Apr 17, 2013, at 4:15 PM, Mike Shulman notifications@github.com wrote:

Actually, the chapter does already say what a field is!
On Apr 17, 2013 4:04 PM, "Daniel R. Grayson" notifications@github.com
wrote:

I am swayed by the recent cogent statements by everybody -- maybe we
should
say what a field is.

On Wed, Apr 17, 2013 at 2:50 PM, spitters notifications@github.com
wrote:

I agree. It would be nice to serve both audiences.
Moreover, I believe we are building a community of people that fit both
descriptions.

On Wed, Apr 17, 2013 at 8:27 PM, Robert Harper notifications@github.comwrote:

ok, fools wade in where sane people dare not tread. my main complaint
is
precisely that the book is addressed to mathematicians. for me
computer
scientists ought also to be the audience for this book, but they are
not.
consequently, it's perfectly ok to speak about presheaves and
fibrations,
but we dare not use a turnstile, or utter the word "judgement" for
fear
of
offending the mathematicians. but i would say that the situation is
precisely dual for computer scientists, and i regret that we are not
treating both audiences with equanimity.

bob

On Apr 17, 2013, at 1:47 PM, Daniel R. Grayson wrote:

No, the book is addressed to mathematicians.

On Wed, Apr 17, 2013 at 12:33 PM, Andrej Bauer <
notifications@github.com>wrote:

So what would one say about the real numbers, for example? Do I
need
to
explain what a field is?

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16520453>
.

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

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16524144>
.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-16531616>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16532270
.

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

[andrejbauer]

After some thought (while lying in bed next to my daughter so she could fall asleep despite a chocolate-induced tummy ache), I concluded we shouldn't be writing any introductions because:

1. We have had a feature freeze whose purpose is exactly to avoid this sort of situation.
2. Of the four chapters (homotopy, categories, sets, reals) only homotopy can reasonably be "introduced" to a typical theoretical computer scientists, and we already have an introduction.
3. I have absolutely no idea what an introduction to real numbers might say.

So let's just clean up the introduction to homotopy, and remove the claim from "how to read this book".

[mikeshulman]

My understanding was that 'features' referred to mathematics, not
necessarily expositional choices.
On Apr 17, 2013 5:02 PM, "Andrej Bauer" notifications@github.com wrote:

After some thought (while lying in bed next to my daughter so she could
fall asleep despite a chocolate-induced tummy ache), I concluded we
shouldn't be writing any introductions because:

1. We have had a feature freeze whose purpose is exactly to avoid
   this sort of situation.
2. Of the four chapters (homotopy, categories, sets, reals) only
   homotopy can reasonably be "introduced" to a typical theoretical computer
   scientists, and we already have an introduction.
3. I have absolutely no idea what an introduction to real numbers
   might say.

So let's just clean up the introduction to homotopy, and remove the claim
from "how to read this book".

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16535518
.

[awodey]

I agree with Andrej.
we're not writing an encyclopedia or even a textbook.
let's just fix up that intro to homotopy

On Apr 17, 2013, at 5:02 PM, Andrej Bauer notifications@github.com wrote:

After some thought (while lying in bed next to my daughter so she could fall asleep despite a chocolate-induced tummy ache), I concluded we shouldn't be writing any introductions because:

We have had a feature freeze whose purpose is exactly to avoid this sort of situation.
Of the four chapters (homotopy, categories, sets, reals) only homotopy can reasonably be "introduced" to a typical theoretical computer scientists, and we already have an introduction.
I have absolutely no idea what an introduction to real numbers might say.
So let's just clean up the introduction to homotopy, and remove the claim from "how to read this book".

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

[andrejbauer]

"Feature freeze" means to me "don't add new stuff unless absolutely necessary".

[mikeshulman]

Rather than getting into an argument based on all the different ways
concepts from software engineering like "feature" and "bug" could be
applied to mathematics, let me say instead that in my experience, even
when writing short mathematics papers, it is essential to spend
some time after all the mathematics is in place thinking about the
exposition -- not only at a local level, but at a global level across
the entire paper: what order in which to introduce things, what paths
through the paper might be taken by different groups of readers, how
much to advertise theorems in advance, how much background is
necessary to give and where, etc. etc. Sometimes this step can
necessitate radical restructuring of the material or extensive new
explanatory writing. We have been doing some of this all the way
through, but until all the mathematics was in place we could not do it
comprehensively. I think the book will suffer greatly if we don't
allow ourselves this step of thinking carefully about exposition and
presentation at a global level, with a willingness to change things.

On Wed, Apr 17, 2013 at 5:22 PM, Andrej Bauer notifications@github.com wrote:

"Feature freeze" means to me "don't add new stuff unless absolutely necessary".

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

[andrejbauer]

Sure, I am not against that. It's just that in this particular case I really don't see what, for example, I would write at the begining of chapter on the reals.

[mikeshulman]

What about something like

"We shall see that the construction of Dedekind reals proceeds in
essentially the same way as in any other foundational system: one must be
careful if being constructive, but the issues are the same as in
constructive set theory. However, for the Cauchy reals, we can improve on
the usual situation in constructive mathematics. Traditionally, excluded
middle or countable choice is required in order for the Cauchy reals to be
Cauchy complete, but by using a higher inductive type (or more precisely, a
higher inductive-inductive type), we can Cauchy complete the rationals
without invoking either of these principles. At the end of the chapter, we
discuss a presentation of Conway's surreal numbers as a similar higher
inductive type.

In this chapter we work mainly with sets and mere propositions, making
heavy use of propositional truncation and the traditional logical notation
introduced in Chapter 3. The higher inductive-inductive definition of the
Cauchy reals will be easier to understand after having seen other examples
of higher inductive types in Chapter 6, but we will describe its induction
principle explicitly and work from that alone. We also use some basic
facts about sets from Chapter 10, but they are all well-known in set theory
and should be easy to believe."

?

On Thu, Apr 18, 2013 at 12:59 AM, Andrej Bauer notifications@github.comwrote:

Sure, I am not against that. It's just that in this particular case I
really don't see what, for example, I would write at the begining of
chapter on the reals.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16557908
.

[andrejbauer]

That is fine, it serves well as an introduction to the chapter, but it only partially fulfills the promise "Each chapter in Part II begins with a brief overview of its subject, what univalent foundations has to contribute to it, and the necessary background from Part I"

Let's just write these, and then see if the claim in the "How to read this book" needs to be changed.

[dlicata335]

I moved some of the background on homotopy and oo-groupoids into the beginning of chapter 2. Many of these concepts are also brought up in the intro, but not quite in as much detail as I'd like, so I think a little bit of an iterative deepening of them is helpful for understanding chapter 2. There are many references to these concepts in Chapter 2, and I think it's important to at least have a spot in the main text where they are "defined" (at least informally), because otherwise when we start mentioning things like "higher groupoids" it sends the message that we expect the reader to know what these are, which I don't think is fair, or even really true. See what you think. I haven't revised the intro to the homotopy chapter 7, but it will get compacted a bunch because it duplicates what's here.

[awodey]

OK, this can work here.
It will need to be revised a bit to be integrated with the following text, but this seems like a reasonable place for this background -- the reader who already knows these concepts can skip ahead if there is some signage.
For example, it could begin with:
The central new idea in homotopy type theory is that types can be regarded as spaces in homotopy theory, or higher-dimensional groupoids in category theory.

Recall that in classical homotopy theory, a space X is a set of points ...

then further down, say after a \bigskip, it could say:

Now, in homotopy type theory, each type in type theory bears the structure of an ∞-groupoid ...

On Apr 18, 2013, at 10:19 AM, Dan Licata notifications@github.com wrote:

I moved some of the background on homotopy and oo-groupoids into the beginning of chapter 2. Many of these concepts are also brought up in the intro, but not quite in as much detail as I'd like, so I think a little bit of an iterative deepening of them is helpful for understanding chapter 2. There are many references to these concepts in Chapter 2, and I think it's important to at least have a spot in the main text where they are "defined" (at least informally), because otherwise when we start mentioning things like "higher groupoids" it sends the message that we expect the reader to know what these are, which I don't think is fair, or even really true. See what you think. I haven't revised the intro to the homotopy chapter 7, but it will get compacted a bunch because it duplicates what's here.

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

[dlicata335]

I did rewrite it to fit in here, but if anyone has particular suggestions to make it fit better, let me know.

[andrejbauer]

Please no big, small or medium skips. There is \mentalpause macro, that you should use. In general, insert semantic macros, not hardwired formatting, if possible.

[mikeshulman]

This is good. I agree it could use a bit of stitching up, but I think it
will fit and be helpful.

On Thu, Apr 18, 2013 at 10:49 AM, Steve Awodey notifications@github.comwrote:

OK, this can work here.
It will need to be revised a bit to be integrated with the following text,
but this seems like a reasonable place for this background -- the reader
who already knows these concepts can skip ahead if there is some signage.
For example, it could begin with:
The central new idea in homotopy type theory is that types can be regarded
as spaces in homotopy theory, or higher-dimensional groupoids in category
theory.

Recall that in classical homotopy theory, a space X is a set of points ...

then further down, say after a \bigskip, it could say:

Now, in homotopy type theory, each type in type theory bears the structure
of an ∞-groupoid ...

On Apr 18, 2013, at 10:19 AM, Dan Licata notifications@github.com
wrote:

I moved some of the background on homotopy and oo-groupoids into the
beginning of chapter 2. Many of these concepts are also brought up in the
intro, but not quite in as much detail as I'd like, so I think a little bit
of an iterative deepening of them is helpful for understanding chapter 2.
There are many references to these concepts in Chapter 2, and I think it's
important to at least have a spot in the main text where they are "defined"
(at least informally), because otherwise when we start mentioning things
like "higher groupoids" it sends the message that we expect the reader to
know what these are, which I don't think is fair, or even really true. See
what you think. I haven't revised the intro to the homotopy chapter 7, but
it will get compacted a bunch because it duplicates what's here.

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

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16580986
.

[awodey]

now stitching …

On Apr 18, 2013, at 11:15 AM, Mike Shulman notifications@github.com wrote:

This is good. I agree it could use a bit of stitching up, but I think it
will fit and be helpful.

On Thu, Apr 18, 2013 at 10:49 AM, Steve Awodey notifications@github.comwrote:

OK, this can work here.
It will need to be revised a bit to be integrated with the following text,
but this seems like a reasonable place for this background -- the reader
who already knows these concepts can skip ahead if there is some signage.
For example, it could begin with:
The central new idea in homotopy type theory is that types can be regarded
as spaces in homotopy theory, or higher-dimensional groupoids in category
theory.

Recall that in classical homotopy theory, a space X is a set of points ...

then further down, say after a \bigskip, it could say:

Now, in homotopy type theory, each type in type theory bears the structure
of an ∞-groupoid ...

On Apr 18, 2013, at 10:19 AM, Dan Licata notifications@github.com
wrote:

I moved some of the background on homotopy and oo-groupoids into the
beginning of chapter 2. Many of these concepts are also brought up in the
intro, but not quite in as much detail as I'd like, so I think a little bit
of an iterative deepening of them is helpful for understanding chapter 2.
There are many references to these concepts in Chapter 2, and I think it's
important to at least have a spot in the main text where they are "defined"
(at least informally), because otherwise when we start mentioning things
like "higher groupoids" it sends the message that we expect the reader to
know what these are, which I don't think is fair, or even really true. See
what you think. I haven't revised the intro to the homotopy chapter 7, but
it will get compacted a bunch because it duplicates what's here.

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

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16580986
.

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

[awodey]

done.

On Apr 18, 2013, at 11:26 AM, steve awodey steveawodey@icloud.com wrote:

now stitching …

On Apr 18, 2013, at 11:15 AM, Mike Shulman notifications@github.com wrote:

This is good. I agree it could use a bit of stitching up, but I think it
will fit and be helpful.

On Thu, Apr 18, 2013 at 10:49 AM, Steve Awodey notifications@github.comwrote:

OK, this can work here.
It will need to be revised a bit to be integrated with the following text,
but this seems like a reasonable place for this background -- the reader
who already knows these concepts can skip ahead if there is some signage.
For example, it could begin with:
The central new idea in homotopy type theory is that types can be regarded
as spaces in homotopy theory, or higher-dimensional groupoids in category
theory.

Recall that in classical homotopy theory, a space X is a set of points ...

then further down, say after a \bigskip, it could say:

Now, in homotopy type theory, each type in type theory bears the structure
of an ∞-groupoid ...

On Apr 18, 2013, at 10:19 AM, Dan Licata notifications@github.com
wrote:

I moved some of the background on homotopy and oo-groupoids into the
beginning of chapter 2. Many of these concepts are also brought up in the
intro, but not quite in as much detail as I'd like, so I think a little bit
of an iterative deepening of them is helpful for understanding chapter 2.
There are many references to these concepts in Chapter 2, and I think it's
important to at least have a spot in the main text where they are "defined"
(at least informally), because otherwise when we start mentioning things
like "higher groupoids" it sends the message that we expect the reader to
know what these are, which I don't think is fair, or even really true. See
what you think. I haven't revised the intro to the homotopy chapter 7, but
it will get compacted a bunch because it duplicates what's here.

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

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-16580986
.

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

[dlicata335]

I think the Homotopy chapter is compliant.

[andrejbauer]

I'll do something about the reals.

[mikeshulman]

I've expanded the Categories chapter with some stuff from my paper with Benedikt and Chris, and I think it is now compliant.

[mikeshulman]

Looks like the reals is the only chapter remaining. Andrej, are you still planning to do that?

[andrejbauer]

Done by fa681e5, reopen if needs fixed.

[mikeshulman]

Looks good! I added a bit in 406ae5e, including the "necessary background from Part I". I'm a little unsatisfied with the placement of the "not the reals we're looking for" comment -- I'd rather not put so much emphasis on it by putting it in the first paragraph. It used to be at the very end of the introduction, which was fine with me, but maybe a footnote would also work.

[andrejbauer]

I agree the "these are not the reals you are looking for" is badly placed. I moved it around until I got tired. Maybe beginning of the Cauchy reals section?

[mikeshulman]

I like having it in the intro to the chapter, just not at the very beginning of the intro. What's wrong with the end? 5aef0ec

[andrejbauer]

It is fine there. I am closing.

[spitters]

I would be inclined to say "axiom of (dependent) countable choice" instead
of AC.
" By assuming excluded middle and the axiom of choice we get the classical
picture "

On Fri, May 10, 2013 at 10:31 PM, Andrej Bauer notifications@github.comwrote:

It is fine there. I am closing.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-17742845
.

[andrejbauer]

The point of this sentence is to reassure the rest of the world we are just weirdos, not heretics. So it is not supposed to be a technical observation, but rather a political statement. Maybe we should even say "By assuming excluded middle and the axiom of choice we get standard classical analysis". Certainly standard classical analysis uses more than dependent choice here and there?

[spitters]

Certainly standard classical analysis uses more than dependent choice
here and there?

Yes, typically for non-separable spaces, but we have not reached that point
yet in the book.

On Mon, May 13, 2013 at 2:52 PM, Andrej Bauer notifications@github.comwrote:

The point of this sentence is to reassure the rest of the world we are
just weirdos, not heretics. So it is not supposed to be a technical
observation, but rather a political statement. Maybe we should even say "By
assuming excluded middle and the axiom of choice we get standard classical
analysis". Certainly standard classical analysis uses more than dependent
choice here and there?

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-17809472
.

[andrejbauer]

As I said, this is not supposed to be a technical statement, it's in the introduction to the chapter. It cannot hinge on a little detail such as "these people here never consider non-separable spaces".

[awodey]

yes, keep it simple -- the remark is aimed at classically-minded readers who don't know or care about the subtleties of constructive analysis.

On May 13, 2013, at 9:02 AM, Andrej Bauer notifications@github.com wrote:

As I said, this is not supposed to be a technical statement, it's in the introduction to the chapter. It cannot hinge on a little detail such as "these people here never consider non-separable spaces".

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

[guillaumebrunerie]

yes, keep it simple -- the remark is aimed at classically-minded readers who don't know or care about the subtleties of constructive analysis.

And who probably don’t care about the subtleties of choice vs dependent choice vs countable choice either.

[mikeshulman]

Agreed: distinguishing between different kinds of choice is too much of a
subtlety for this sentence.
On May 13, 2013 7:44 AM, "Guillaume Brunerie" notifications@github.com
wrote:

yes, keep it simple -- the remark is aimed at classically-minded readers
who don't know or care about the subtleties of constructive analysis.

And who probably don’t care about the subtleties of choice vs dependent
choice vs countable choice either.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-17816160
.

[spitters]

I think we all agree.

On Mon, May 13, 2013 at 5:36 PM, Mike Shulman notifications@github.comwrote:

Agreed: distinguishing between different kinds of choice is too much of a
subtlety for this sentence.
On May 13, 2013 7:44 AM, "Guillaume Brunerie" notifications@github.com
wrote:

yes, keep it simple -- the remark is aimed at classically-minded readers
who don't know or care about the subtleties of constructive analysis.

And who probably don’t care about the subtleties of choice vs dependent
choice vs countable choice either.

—
Reply to this email directly or view it on GitHub<
https://github.com/HoTT/book/issues/137#issuecomment-17816160>
.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/137#issuecomment-17819714
.