HoTT / book

A textbook on informal homotopy type theory
2.03k stars 359 forks source link

Pointers for the impatient #121

Closed mikeshulman closed 11 years ago

mikeshulman commented 11 years ago

This book is really long. It would be nice if we could say somewhere to an impatient reader which sections of Part I could be skipped or skimmed if they want to get to the meat of Part II as quickly as possible.

For instance, for basically all of the book it doesn't matter what the definition of isEquiv is, only that it has the properties described in section 2.4, so a lot of Chapter 3 is not necessary. Similarly, not much of Chapter 4 is ever needed later on.

andrejbauer commented 11 years ago

This should go in the Preface, or we have an early 'How to read this book?' in the Introduction.

awodey commented 11 years ago

Or a separate Foreword?

Sent from my iPhone

On Apr 12, 2013, at 3:35 PM, Andrej Bauer notifications@github.com wrote:

This should go in the Preface, or we have an early 'How to read this book?' in the Introduction.

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

andrejbauer commented 11 years ago

Preface, Foreword, Introduction? What would be in the Foreword? What is the difference betweeen Preface and Foreword?

RobertHarper commented 11 years ago

the preface is written by the author, any foreword by an-other. maybe vv would write a foreword.

bob

Sent from tablet

On Apr 12, 2013, at 16:51, Andrej Bauer notifications@github.com wrote:

Preface, Foreword, Introduction? What would be in the Foreword? What is the difference betweeen Preface and Foreword?

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

awodey commented 11 years ago

Ok- thats not what I meant. More like "how to read this book".

Sent from my iPhone

On Apr 12, 2013, at 6:16 PM, Robert Harper notifications@github.com wrote:

the preface is written by the author, any foreword by an-other. maybe vv would write a foreword.

bob

Sent from tablet

On Apr 12, 2013, at 16:51, Andrej Bauer notifications@github.com wrote:

Preface, Foreword, Introduction? What would be in the Foreword? What is the difference betweeen Preface and Foreword?

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

RobertHarper commented 11 years ago

of course i contradicted myself with the suggestion, so never mind that. it's not obvious to me that there is someone who would write a foreword.

bob

On Apr 12, 2013, at 9:13 PM, Steve Awodey wrote:

Ok- thats not what I meant. More like "how to read this book".

Sent from my iPhone

On Apr 12, 2013, at 6:16 PM, Robert Harper notifications@github.com wrote:

the preface is written by the author, any foreword by an-other. maybe vv would write a foreword.

bob

Sent from tablet

On Apr 12, 2013, at 16:51, Andrej Bauer notifications@github.com wrote:

Preface, Foreword, Introduction? What would be in the Foreword? What is the difference betweeen Preface and Foreword?

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

mikeshulman commented 11 years ago

I started writing a "how to read this book" at the end of the introduction. It's rough and incomplete, but I committed it because I have to go home for dinner.

awodey commented 11 years ago

OK, thanks for letting us know. I will now begin lightly revising the intro for modesty (i.e. in response to Thierry and Andre's comments).

S

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

I started writing a "how to read this book" at the end of the introduction. It's rough and incomplete, but I committed it because I have to go home for dinner.

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

mikeshulman commented 11 years ago

I already made one change along those lines, replacing "is the best way to do it" with "has independent advantages". I do agree that calling something "the best" without qualification is asking for trouble.

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

OK, thanks for letting us know. I will now begin lightly revising the intro for modesty (i.e. in response to Thierry and Andre's comments).

S

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

I started writing a "how to read this book" at the end of the introduction. It's rough and incomplete, but I committed it because I have to go home for dinner.

— 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/121#issuecomment-16472598 .

awodey commented 11 years ago

I think I had already changed that to something like "the best way we know how to do it" or some such.

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

I already made one change along those lines, replacing "is the best way to do it" with "has independent advantages". I do agree that calling something "the best" without qualification is asking for trouble.

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

OK, thanks for letting us know. I will now begin lightly revising the intro for modesty (i.e. in response to Thierry and Andre's comments).

S

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

I started writing a "how to read this book" at the end of the introduction. It's rough and incomplete, but I committed it because I have to go home for dinner.

— 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/121#issuecomment-16472598 .

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

mikeshulman commented 11 years ago

I think "best way we know how" is still too strong. E.g. personally, I'm not 100% convinced that the HIIT Cauchy reals are "better" than the Dedekind ones, or that the HIT cumulative hierarchy is better than (or even different from) the one we should be able to construct using extensional well-founded relations.

awodey commented 11 years ago

fair enough

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

I think "best way we know how" is still too strong. E.g. personally, I'm not 100% convinced that the HIIT Cauchy reals are "better" than the Dedekind ones, or that the HIT cumulative hierarchy is better than (or even different from) the one we should be able to construct using extensional well-founded relations.

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

awodey commented 11 years ago

can this be closed? Mike has written a "how to read this book" at the end of the intro.

mikeshulman commented 11 years ago

That section isn't done.