You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Avi Craimer (Sep 29 2020 at 19:27):I have started learning Dependent Type Theory and would like to learn Homotopy Type Theory. Is there a good introductory text to Homotopy Theory that does not require prior mastery of traditional topology. I have some basic category theory under my belt, so an introduction that uses the language of categories and functors to explain homotopy would be most helpful.
Related, I've seen a lot of references to the idea of infinity groupoids as the categorical way to make sense of homotopy. Is there an introduction to the concept of infinity groupoids that does not pre-suppose knowledge of higher category theory (maybe building up to it starting from ordinary category theory)?
Perhaps the answer is that the HoTT book is the best such introduction, in which case it would be great to have confirmation of that.
Nathanael Arkor (Sep 29 2020 at 19:36):The HoTT book is very nicely written and begins quite gently, so I would definitely recommend taking a look if you haven't done yet.
Dan Doel (Sep 29 2020 at 19:38):I, at least, have no formal training in homotopy theory, and have just gleaned things from fiddling around with HoTT, and reading parts of the book. But I knew a lot about type theory before that.
Avi Craimer (Sep 29 2020 at 19:53):I found this video quite helpful as an introduction: https://youtu.be/E3steS2Hr1Y
Fawzi Hreiki (Sep 29 2020 at 20:56):I think Egbert Rijke's notes (soon to become a book) are easier going than the HoTT book. You can find it at: https://github.com/EgbertRijke/HoTT-Intro. Also, the first two chapters of Michael Warren's PhD are quite clear.
Avi Craimer (Sep 29 2020 at 21:40):Fawzi Hreiki said:
Also, the first two chapters of Michael Warren's PhD are quite clear.
Thanks, I found the thesis: http://mawarren.net/papers/phd.pdf
I look forward to trying to read this.
Dan Doel (Sep 29 2020 at 22:43):I thought the Voevodsky talk was going to mention this, but I think it actually didn't. -groupoids are basically a way of organizing all those things into a single structure.
Dan Doel (Sep 29 2020 at 22:53):So instead of the -th homotopy group of a space at a point, you have the homotopy -groupoid of the whole space. And you arrange it (I think) so that you can imagine that the 0-th level is "all the points" (because there are homotopy groups using every point as a "base"), or you can imagine that the 0-th level is just the connected pieces (like he does in the talk; because it doesn't matter which point you pick in a connected part), or anywhere in between, and doing so will give you 'the same' -groupoid.
Dan Doel (Sep 29 2020 at 22:55):And similarly at each of the higher levels.
Henry Story (Sep 30 2020 at 07:33):The HoTT book is indeed great. I was able to read the first few chapters 5 years ago, knowing nearly nothing about Category Theory, though I did have programming experience in Scala, ie. with a (path dependent) typed language. But I think the book could even be a great introduction to programming with (dependent) types. Indeed I learn a lot about Scala that I had not understood before reading the book.
(Note: you can compile the latest version from github, but I think there are precompiled pdfs of the latest version available somewhere). There are also a couple of philosophical papers on HoTT that can help with interpretations, if needed. From a practical programming point of view it is worth skimming at the first few pages of Cubical Agda: a dependently typed programming language with univalence and higher inductive types. I don't find that easy to read, but the example is very interesting. The point is made that proof assistants such as say Lean work with Peano numbers (Ie numbers defined with 0 and the successor relation), since these are very easy to build proofs with and give a standard normal form. But of course this is completely unwieldy for making operations of large numbers - a computer would soon run out of memory. So for efficiency Lean also provides a different binary machine encoding, but when programming that way the mathematical guarantees of the proofs are lost. So you either have mathematical certainty or you have efficiency.
By proving that binary numbers are equivalent to Peano numbers all the proofs can be transported from Peano to the binary representation. This opens the promise that future compilers would be able to compile proofs transporting them to the best computer representation to execute them. (Perhaps Cubical Agda can already do some of that, I don't know).
Avi Craimer (Sep 30 2020 at 15:29):I've been going through the Rijke notes and they are very helpful. I found the Warren thesis a bit too advanced for now.
https://github.com/EgbertRijke/HoTT-Intro/blob/master/pdfs/2019-summer-school.pdf
Henry Story (Sep 30 2020 at 15:45):On this note, what is the best document (intro) to read on cubical HoTT?
Fawzi Hreiki (Sep 30 2020 at 22:46):I found this quite understandable: https://arxiv.org/abs/1911.05844v1