<span id="mailbox-conversation">I should have just included the link<div><br></div>
<div><a href="http://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf">http://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf</a></div></span><div class="mailbox_signature">—<br>Sent from <a href="https://www.dropbox.com/mailbox">Mailbox</a> for iPhone</div>
<br><br><div class="gmail_quote"><p>On Mon, Jan 6, 2014 at 9:19 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br></p><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div dir="ltr">
<a href="http://www.amazon.com/Topology-2nd-Edition-James-Munkres/dp/0131816292">Topology, by Munkres</a>, is a good intro to point-set topology<div>
<a href="http://www.math.cornell.edu/~hatcher/AT/AT.pdf">Algebraic Topology, by Hatcher</a>, is a good intro to algebraic topology</div>
<div>
<a href="http://www.maths.ed.ac.uk/~aar/papers/maclanecat.pdf">Category Theory for the Working Mathematician, by Mac Lane</a>, is the canonical intro to category theory; <a href="http://arxiv.org/abs/1302.6946">David Spivak wrote Category Theory for Scientists</a>; <a href="http://folk.uio.no/paularne/SUPh05/DS.pdf">Homotopy theories and model categories, by Dwyer and Spalinski</a>, 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.)</div>
<div>
<a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation">Wikipedia</a> is a decent source on the Curry-Howard isomorphism; <a href="http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/">Bob Harper has a blog post on computational trinitarianism</a>, which is an extreme and interesting view on the Curry-Howard isomorphism.</div>
<div><br></div>
<div>Dan Licata gave a <a href="http://dlicata.web.wesleyan.edu/pubs/l13git/git.pdf">presentation "Git as a HIT"</a> about applying higher inductive types to version control.</div>
<div><br></div>
<div>There's the <a href="https://groups.google.com/forum/#!forum/homotopytypetheory">Homotopy Type Theory google groups</a> (also a mailing list), which is primarily for research-level HoTT questions and discussions. Thierry Coquand <a href="https://groups.google.com/forum/#!topic/homotopytypetheory/GmXKEArD3HY">announced his cubical sets evaluator</a> on it (where this is also a lot of discussion on canonicity); it's <a href="https://github.com/simhu/cubical">available on github</a>. The linked </div>
<div><br></div>
<div>There's also the <a href="https://groups.google.com/forum/#!forum/hott-amateurs">HoTT amateurs google group</a>. If you have questions about things in the book, you should feel free to email and cc both <a href="mailto:hott-reading-group@mit.edu">hott-reading-group@mit.edu</a> and <a href="mailto:hott-amateurs@googlegroups.com">hott-amateurs@googlegroups.com</a>.</div>
<div><br></div>
<div>-Jason</div>
<div><br></div>
</div>
<div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Jan 6, 2014 at 5:31 PM, Joe Hannon <span dir="ltr"><<a href="mailto:hannon@math.bu.edu">hannon@math.bu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="auto">
<div>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. </div>
<div><br></div>
<div>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?</div>
<span class="HOEnZb"><font color="#888888"><div><br></div>
<div>Joe</div></font></span><div><div class="h5">
<div>
<br>On Jan 6, 2014, at 17:13, Dmitry Vagner <<a href="mailto:dmitryvagner@gmail.com">dmitryvagner@gmail.com</a>> wrote:<br><br></div>
<blockquote type="cite"><div>
<div dir="ltr">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:<br><br><a href="http://arxiv.org/pdf/math/0608420v2.pdf" style="font-family:arial,sans-serif;font-size:13px">http://arxiv.org/pdf/math/0608420v2.pdf</a><br><br>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.<br><br>Hope that helps,<div>Dmitry</div>
</div>
<div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Jan 6, 2014 at 4:47 PM, Peng Wang <span dir="ltr"><<a href="mailto:wangp.thu@gmail.com">wangp.thu@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<br><div class="gmail_extra">
<br><br><div class="gmail_quote">
<div>On Mon, Jan 6, 2014 at 4:41 PM, Chris Jeris <span dir="ltr"><<a href="mailto:cjeris@gmail.com">cjeris@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">First of all, thanks very much to Jason for putting the group together and also making it accessible to us remote participants!<div>
<br></div>
<div>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?</div>
</div></blockquote>
<div><br></div>
</div>
<div>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?)</div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
<div dir="ltr">
<div><br></div>
<div>thanks, Chris Jeris (freenode: ystael)</div>
</div>
<br></div>_______________________________________________<br>
HoTT-reading-group mailing list<br><a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a><br><a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br><br></blockquote>
</div>
<span><font color="#888888"><br><br clear="all"><div><br></div>-- <br>Peng Wang (王鹏)<div>
<div>CSAIL, The Stata Center, MIT</div>
<div>77 Massachusetts Ave, 32-G822</div>
<div>Cambridge, MA 02139</div>
<div>Phone: <a href="tel:%28617%29803-2025">(617)803-2025</a>
</div>
<div>Email: <a href="mailto:wangpeng@csail.mit.edu">wangpeng@csail.mit.edu</a>
</div>
</div>
</font></span>
</div>
</div>
<br>_______________________________________________<br>
HoTT-reading-group mailing list<br><a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a><br><a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br><br></blockquote>
</div>
<br></div>
</div></blockquote>
<blockquote type="cite"><div>
<span>_______________________________________________</span><br><span>HoTT-reading-group mailing list</span><br><span><a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a></span><br><span><a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a></span><br></div></blockquote>
</div></div>
</div>
<br>_______________________________________________<br>
HoTT-reading-group mailing list<br><a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a><br><a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br><br></blockquote>
</div>
<br></div>
</blockquote></div><br>