Background

[Alejandro Serrano Mena]

Hi all,

I think we are really going to enjoy this group :)

However, as a first step I think we should arrange which background will be assumed in the group, and in case we need something more, how we are going to get it.

Here are some topics that we may need to know prior to starting readin HoTT:

• Lambda calculus and type theory: I think we can assume that everybody knows about basic lambda calculus, and Hindley-Milner-style type systems
• Dependent types: knowledge of Agda and Coq may be needed to understand the book
• Category theory: maybe a more knowledgeable reader could tell us if we need to know more than the basic of category theory to understand the book

[Ben]

hello --

good idea. i would add to this list

* some basic homotopy theory (including simplicial sets and maybe a little basic topology for intuition)
* very basic mathematical logic (intuitionistic, etc.)

however, i propose people just start diving in and reading and doing exercises. from what i've read the HoTT book is really accessible and they've done an admirable job in presentation and keeping things self-contained. if people get stuck we can figure out what we need at that point. also the HoTT people have unconventional views on all of these topics, so they might have different ways of presenting things anyways. finally, all of these background topics go on endlessly, we could easily go off the deep end on toposes and logic for example.

as for background, i'm happy to explain what little i know about homotopy theory and category theory; i can also draw on some heavy hitters if we have deeper questions. category theory was invented for topologists so there's a lot of overlap there. i can add next to nothing about logic, lambda calculus / type theory, dependent types, etc. if someone wants to pipe up on those subjects that'd be great.

for resources, i've greatly enjoyed (though haven't come close to finishing) "Lectures on the Curry Howard Isomorphism" by Sorensen and Urzyczyn which is freely available on the web (the lecture version, i think there's also a book.) that has a bunch of exercises which would be great if anyone wanted to discuss. Benjamin Pierce's "Types and Programming Languages" and the sequel are often lauded, neither of which i have read. coming from chicago i learned category theory from MacLane (but i've heard good things about Awodey's book, he's a chicago guy too i think and one of the founders of HoTT), and homotopy theory from Peter May's "A Concise Course in Algebraic Topology" but that's probably way too abstract to be useful for first timers. i think most people suggest "Algebraic Topology" by Hatcher. i unfortunately have zero suggestions for mathematical logic, but some of that is covered by the Sorensen and Urzyczyn (and probably Pierce) as well.

happy reading!

best, ben

> --
> You received this message because you are subscribed to the Google Groups "HoTT Amateurs" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-amateur...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Alejandro Serrano Mena]

For a first approximation to logic and proof theory, I recommend "Handbook of Proof Theory", whose first chapters are available at http://www.math.ucsd.edu/~sbuss/ResearchWeb/HandbookProofTheory/

2013/6/26 Ben <midf...@gmail.com>

[Francesco Mazzoli]

For what concerns type theory, the best resources I've found are 'Type Theory and Functional Programming' http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ and 'Programming in Martin-Löf Type Theory: An Introduction.' http://www.cse.chalmers.se/research/group/logic/book/ .  Although from a skim the HoTT book itself seems to be fairly accessible in that regard.

Francesco

[Ben]

allan hatcher's algebraic topology : http://www.math.cornell.edu/~hatcher/AT/ATpage.html
peter may's a concise course in algebraic topology : http://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf

but again, these are probably not necessary to get started.

b

[Alp Mestanogullari]

I have read and kind of teached Hatcher's material, it's great but maybe a bit terse and fast for people who don't know much about that kind of topics and don't have some intuition already.

--
Alp Mestanogullari

[Michael Shulman]

Hi,

Ben invited me to lurk on this list and occasionally pipe up with help if I have time. We actually tried *not* to assume most of those things as background when writing the book. So while they might help, they oughtn't to be necessary if we did our job well. I think the only one we really did assume was some category theory (but really only the basics, like functors, natural transformations, and limits and colimits). Knowing a bit of algebraic topology would probably make it easier, but we did try to include some explanation of that, aimed at computer scientists. So I would encourage you to just start reading, and see if and when you get stuck.

Mike