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

[Jason Gross]

Topology, by Munkres<http://www.amazon.com/Topology-2nd-Edition-James-Munkres/dp/0131816292>,
is
a good intro to point-set topology
Algebraic Topology, by
Hatcher<http://www.math.cornell.edu/~hatcher/AT/AT.pdf>, is
a good intro to algebraic topology
Category Theory for the Working Mathematician, by Mac
Lane<http://www.maths.ed.ac.uk/~aar/papers/maclanecat.pdf>,
is the canonical intro to category theory; David Spivak wrote Category
Theory for Scientists <http://arxiv.org/abs/1302.6946>; Homotopy theories
and model categories, by Dwyer and
Spalinski<http://folk.uio.no/paularne/SUPh05/DS.pdf>,
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<http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation>is
a decent source on the Curry-Howard isomorphism; Bob
Harper has a blog post on computational
trinitarianism<http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/>,
which is an extreme and interesting view on the Curry-Howard isomorphism.

Dan Licata gave a presentation "Git as a
HIT"<http://dlicata.web.wesleyan.edu/pubs/l13git/git.pdf> about
applying higher inductive types to version control.

There's the Homotopy Type Theory google
groups<https://groups.google.com/forum/#!forum/homotopytypetheory>
(also
a mailing list), which is primarily for research-level HoTT questions and
discussions.  Thierry Coquand announced his cubical sets
evaluator<https://groups.google.com/forum/#!topic/homotopytypetheory/GmXKEArD3HY>on
it (where this is also a lot of discussion on canonicity); it's
available
on github <https://github.com/simhu/cubical>.  The linked

There's also the HoTT amateurs google
group<https://groups.google.com/forum/#!forum/hott-amateurs>.
 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140106/d2187562/attachment.htm