WHAT? This lecture series conducted by Bob Harper will cover various topics in higher-dimensional type theory, including higher category theory and homotopy theory. It is not for the faint of heart.
WHO? This is some hardcore PL stuff. You should know dependent type theory and at least some category theory.
WHEN? Wednesdays and Fridays?
WHERE? MPI-SWS Kaiserslautern/Wartburg
HOW? Mailing list for this series (and other type theory discussion): type-theory@mpi-sws.org
Organizer: Scott Kilpatrick
Schedule
1 |
2011-08-03, 2PM |
Intro to HDTT and homotopy. |
2 |
2011-08-05, 1PM |
? |
Resources
Blogs and Websites
Homotopy type theory: http://homotopytypetheory.org/
n-category cafe blog (sometimes related): http://golem.ph.utexas.edu/category/
Papers
Martin Hofmann. Syntax and semantics of dependent types. 1997. Describes the interpretation of dependent type theory into category theory.
Martin Hofmann, Thomas Streicher. The groupoid interpretation of type theory. 1995. The first construction of a model in which identity types are non-trivial.
Topics
Meeting #1
- Intro to higher-dimensional type theory.
- Intro to homotopy theory.
- Intro to (higher) category theory.
- Basic interpretation of type theory in category theory.
Different notions of equivalence (definitional and propositional).
- What's going on in the field right now.