search

HoTT / book

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

Think about the beginning of chapter 2 #740

Open mikeshulman opened 10 years ago

mikeshulman commented 10 years ago

We seem to get a fair number of people who hit the beginning of chapter 2 and think "oh no, I don't know what an ∞-groupoid is" and get stuck (e.g. here). I would like the message of the book to be that you don't need to already know what an ∞-groupoid is; you can learn what one is by learning to work with types. But even with that goal, it seems that we have to give some intuitive picture of what this is supposed to mean, and we also have to make connections for the readers who do know what an ∞-groupoid is. Maybe for the 2nd edition we can find some better way of reconciling these goals.

lancejpollard commented 9 years ago

Awesome, yeah ran into this exact thing too. I am just a regular programmer coming from the JavaScript world, and have been slowly learning Haskell. I was able to follow the first few sections of the book so far pretty well. But yeah saw this ∞-groupoid but don't really know where to start in understanding that. Tried searching wikipedia, but that led to Kan fibration which says is part of the theory of simplical sets, but not having a background in category theory I'm not sure where to start in trying to get an intuition about simplical sets. Going to try checking out the Dover book Topoi: The Categorial Analysis of Logic, seems like there may be some helpful background there.

Maybe if there is no easy way to provide some intuition on what it is, it would be pretty helpful pointing to which field of math/theory we should dig into, and a good intro blog post, wikipedia page, or simpler math book that could get us started (thinking along the lines of a Dover book). Since the people who don't understand ∞-groupoid I'm guessing are probably not that familiar with category theory, the simpler the reference the better :)

Btw excited to see how active this repo is with questions! I've been slowly reading through the first chapter of this book and this issue list will be of great help.

mikeshulman commented 9 years ago

@lancejpollard, have you tried going on through chapter 2 with the perspective I suggested above, that you don't need to already know what an ∞-groupoid is?

lancejpollard commented 9 years ago

Not yet, will try that too once I finish this first chapter. I only saw because I read through the intros to every chapter first (after reading the book introduction), to try to get a general sense of the background math I would need / how deep each chapter would go. So will try your suggestion!