search

HoTT / book

A textbook on informal homotopy type theory
2.04k stars 360 forks source link

Write a reasonable intro to Chapter 7 #124

Closed andrejbauer closed 11 years ago

andrejbauer commented 11 years ago

Chapter 7 introduction is just a stub.

andrejbauer commented 11 years ago

Furthermore, the beginning of the chapter could use some work. We probably don't need all those subsubsubsubsections, etc.

mikeshulman commented 11 years ago

I feel like the sections "Classical homotopy theory" and "Homotopy theory of oo-groupoids" in this chapter are misplaced: the people who need to read them are probably not going to get this far in the book without having read them already. Concepts like paths, homotopy, and homotopy equivalence have been ubiquitous since chapter 2. Maybe a version of these sections could go into the early sections of chapter 2 instead?

awodey commented 11 years ago

yes, these sections are a bit awkward. maybe they should be retitled something like: A quick review of homotopy theory, or Homotopy for type theorists, or A thumbnail sketch of homotopy theory… ? I wouldn't want to insert them further up, since that text is now so polished and this would disrupt it.
But we could have a forward reference in Ch. 2 to this section "for those readers who want a quick review of homotopy theory", or something.

On Apr 16, 2013, at 12:13 PM, Mike Shulman notifications@github.com wrote:

I feel like the sections "Classical homotopy theory" and "Homotopy theory of oo-groupoids" in this chapter are misplaced: the people who need to read them are probably not going to get this far in the book without having read them already. Concepts like paths, homotopy, and homotopy equivalence have been ubiquitous since chapter 2. Maybe a version of these sections could go into the early sections of chapter 2 instead?

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

mikeshulman commented 11 years ago

I don't think we're really put a lot of effort into polishing the initial sections of chapter 2. I was reading it over last night and I thought it could actually benefit from a mention of the idea of "synthetic homotopy theory", e.g. to emphasize that the "paths" we are talking about are basic objects rather than things made up of points. Chapter 2 is kind of light on touchy-feely stuff, actually -- at the moment it's mostly just all the lemmas we need everywhere else, stuck together in a vaguely reasonable order.

On Tue, Apr 16, 2013 at 1:19 PM, Steve Awodey notifications@github.comwrote:

yes, these sections are a bit awkward. maybe they should be retitled something like: A quick review of homotopy theory, or Homotopy for type theorists, or A thumbnail sketch of homotopy theory… ? I wouldn't want to insert them further up, since that text is now so polished and this would disrupt it. But we could have a forward reference in Ch. 2 to this section "for those readers who want a quick review of homotopy theory", or something.

On Apr 16, 2013, at 12:13 PM, Mike Shulman notifications@github.com wrote:

I feel like the sections "Classical homotopy theory" and "Homotopy theory of oo-groupoids" in this chapter are misplaced: the people who need to read them are probably not going to get this far in the book without having read them already. Concepts like paths, homotopy, and homotopy equivalence have been ubiquitous since chapter 2. Maybe a version of these sections could go into the early sections of chapter 2 instead?

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

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/124#issuecomment-16458393 .

dlicata335 commented 11 years ago

I revised the intro to the homotopy chapter; have a look. I'm happy with it, and think it solves these issues, so let me know if you have suggestions, or else close.

andrejbauer commented 11 years ago

Excellent, thanks Dan. I am closing this because you fulfilled what the issue asks for: we now have a (more than) reasonable intro to Chapter 7. If anyone has anything else to say about the intro to Chapter 7, please open a new issue about that specific thing. (One little detail: You like to capitalize the word after the colon---is this one of those anti-German things where in English capitalization and commas aren't 100% fixed by rules? The German in me wants to make all those upper case letters lower case.)

dlicata335 commented 11 years ago

I believe both are correct. I use "Sentence 1: Sentence 2. Sentence 3." when both Sentence 1 and Sentence 2 are an iterative deepening of Sentence 1, which is often the case here I think. Otherwise, "Sentence 1: sentence 2. Sentence 3." gets the associativity wrong, because it binds 1 and 2 together more tightly than 2 and 3.

guillaumebrunerie commented 11 years ago

(One little detail: You like to capitalize the word after the colon---is this one of those anti-German things where in English capitalization and commas aren't 100% fixed by rules? The German in me wants to make all those upper case letters lower case.)

According to Wikipedia, that’s indeed something American people do.

awodey commented 11 years ago

It' up to the author. I use lowercase.

Sent from my iPhone

On Apr 20, 2013, at 12:38 PM, Guillaume Brunerie notifications@github.com wrote:

(One little detail: You like to capitalize the word after the colon---is this one of those anti-German things where in English capitalization and commas aren't 100% fixed by rules? The German in me wants to make all those upper case letters lower case.)

According to Wikipedia, that’s indeed something American people do.

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

andrejbauer commented 11 years ago

Such "rules" would never fly in the old world.

awodey commented 11 years ago

*very& nicely done, Dan -- thanks! I made just a few minor tweaks here and there.

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

I revised the intro to the homotopy chapter; have a look. I'm happy with it, and think it solves these issues, so let me know if you have suggestions, or else close.

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

DanGrayson commented 11 years ago

Does anyone really regard something like

"Foo bar foo bar: foo bar foo bar."

as being two sentences? It's one sentence.

On Sat, Apr 20, 2013 at 5:23 AM, Dan Licata notifications@github.comwrote:

I believe both are correct. I use "Sentence 1: Sentence 2. Sentence 3." when both Sentence 1 and Sentence 2 are an iterative deepening of Sentence 1, which is often the case here I think. Otherwise, "Sentence 1: sentence

  1. Sentence 3." gets the associativity wrong, because it binds 1 and 2 together more tightly than 2 and 3.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/124#issuecomment-16701861 .

dlicata335 commented 11 years ago

I regard X : Y. as two sentences, and X : y. as one sentence. I.e. I believe that colon can separate sentences as well as clauses.

mikeshulman commented 11 years ago

On Apr 22, 2013 1:45 PM, "Dan Licata" notifications@github.com wrote:

I regard X : Y. as two sentences, and X : y. as one sentence. I.e. I believe that colon can separate sentences as well as clauses.

I've never heard of such a thing, or of it being acceptable to capitalize the word following a colon.

dlicata335 commented 11 years ago

http://www.apvschicago.com/2011/04/capitalization-after-colons.html

anyway I really don't care so if it bothers you please change it.