[HoTT-reading-group] Background reading in homotopy theory and higher category theory?

Mon Jan 6 23:11:39 EST 2014

* A link to Bob Harper's HoTT grad course with full lecture videos and notes was requested:

  http://www.cs.cmu.edu/~rwh/courses/hott/

* Also a link to an actual use of proof relevance outside of pure math, and in the realm of program reasoning:

  http://research.microsoft.com/en-us/um/people/nick/setoids.pdf

Although it does not reference univalence, I could imagine a full mechanization of the work would end up needing it

-Ian
----- Original Message -----
From: "Dmitry Vagner" <dmitryvagner at gmail.com>
To: "Jason Gross" <jasongross9 at gmail.com>
Cc: "hott-reading-group" <hott-reading-group at mit.edu>
Sent: Monday, January 6, 2014 9:38:03 PM GMT -05:00 US/Canada Eastern
Subject: Re: [HoTT-reading-group] Background reading in homotopy theory and higher category theory?

I should have just included the link 

http://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf 
— 
Sent from Mailbox for iPhone 

On Mon, Jan 6, 2014 at 9:19 PM, Jason Gross < jasongross9 at gmail.com > wrote: 

Topology, by Munkres , is a good intro to point-set topology 
Algebraic Topology, by Hatcher , is a good intro to algebraic topology 
Category Theory for the Working Mathematician, by Mac Lane , is the canonical intro to category theory; David Spivak wrote Category Theory for Scientists ; Homotopy theories and model categories, by Dwyer and Spalinski , contains a 10 page crash course on basic category theory, as well as some expository Quillen model categories, which generalize the idea of homotopy. (I heard somewhere that the only results provable in HoTT are the ones that are true in all Quillen model categories.) 
Wikipedia is a decent source on the Curry-Howard isomorphism; Bob Harper has a blog post on computational trinitarianism , which is an extreme and interesting view on the Curry-Howard isomorphism. 

Dan Licata gave a presentation "Git as a HIT" about applying higher inductive types to version control. 

There's the Homotopy Type Theory google groups (also a mailing list), which is primarily for research-level HoTT questions and discussions. Thierry Coquand announced his cubical sets evaluator on it (where this is also a lot of discussion on canonicity); it's available on github . The linked 

There's also the HoTT amateurs google group . If you have questions about things in the book, you should feel free to email and cc both hott-reading-group at mit.edu and hott-amateurs at googlegroups.com . 

-Jason 

On Mon, Jan 6, 2014 at 5:31 PM, Joe Hannon < hannon at math.bu.edu > wrote: 

That paper also has an explanation of the periodic table of categories, including -1-categories and -2-categories, which might give some context to today's discussion of what a -1-type should be. 

As a counterpart to Chris's call for references for some math discussions held today (which must've occurred after I left), as a math student I felt a little out of my depth during some of the more CS-y discussions. Is there some nice reference I could look at for this Howard-Curry theorem? Will that be relevant to our discussions going forward? 

Joe 

On Jan 6, 2014, at 17:13, Dmitry Vagner < dmitryvagner at gmail.com > wrote: 

Thank you Jason for the wonderful group and for including us remotely! Chris, I learned a lot about the homotopy/groupoid/category theory interface from this amazing expository paper by John Baez: 

http://arxiv.org/pdf/math/0608420v2.pdf 

For our purposes, section 2 is where all of the interesting (and most accessible) information is. Only the basic definitions of category theory (along with your foundational algebraic topology understanding) may be required to get a lot out of this section. Of particular interest is section 2.3 - it's on this thing called the "homotopy hypothesis" - which roughly says that "homotopy n-types are the same as n-groupoids" - taking n to the limit yields what you are interested in, that from the homotopical perspective, "topological spaces are the same as (weak) infinity-groupoids." I feel like this paper does a great job of expositing these ideas, including what exactly a homotopy n-type is, without much technical background. 

Hope that helps, 
Dmitry 

On Mon, Jan 6, 2014 at 4:47 PM, Peng Wang < wangp.thu at gmail.com > wrote: 

On Mon, Jan 6, 2014 at 4:41 PM, Chris Jeris < cjeris at gmail.com > wrote: 

First of all, thanks very much to Jason for putting the group together and also making it accessible to us remote participants! 

I am intrigued by the statement that "infinity-groupoids are the natural models of homotopy theory", but I know little about homotopy theory and nothing about higher category theory. I have algebraic topology at about the level of Massey's first course (rusty by some years) and basic category theory. Can anyone suggest some expository works in this area as background or further reading? 

Adding to Chris' question, I don't even know about topology or algebraic topology, so is there some introductory material on that? (Or is that needed?) 

thanks, Chris Jeris (freenode: ystael) 
_______________________________________________ 
HoTT-reading-group mailing list 
HoTT-reading-group at mit.edu 
http://mailman.mit.edu/mailman/listinfo/hott-reading-group 

-- 
Peng Wang (王鹏) 

CSAIL, The Stata Center, MIT 
77 Massachusetts Ave, 32-G822 
Cambridge, MA 02139 
Phone: (617)803-2025 
Email: wangpeng at csail.mit.edu 
_______________________________________________ 
HoTT-reading-group mailing list 
HoTT-reading-group at mit.edu 
http://mailman.mit.edu/mailman/listinfo/hott-reading-group 

_______________________________________________ 
HoTT-reading-group mailing list 
HoTT-reading-group at mit.edu 
http://mailman.mit.edu/mailman/listinfo/hott-reading-group 

_______________________________________________ 
HoTT-reading-group mailing list 
HoTT-reading-group at mit.edu 
http://mailman.mit.edu/mailman/listinfo/hott-reading-group 

_______________________________________________
HoTT-reading-group mailing list
HoTT-reading-group at mit.edu
http://mailman.mit.edu/mailman/listinfo/hott-reading-group