= Higher-Dimensional Type Theory Seminar =

WHAT? This lecture series conducted by [[http://www.cs.cmu.edu/~rwh/|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? See schedule below.

WHERE? MPI-SWS Kaiserslautern/Wartburg

HOW? Mailing list for this series (and other type theory discussion): [[mailto:type-theory@mpi-sws.org|type-theory@mpi-sws.org]]

Organizers: [[mailto:rwh@cs.cmu.edu|Bob Harper]] and [[mailto:skilpat@mpi-sws.org|Scott Kilpatrick]]

Videos: The videos of lectures 2-4 are [[http://www.mpi-sws.org/seminars/higher_dimensional_type_theory/|available online]]. Altogether they're around 850mb. Use [[http://www.videolan.org/vlc/|VLC]] to play them if you're having trouble. They're password protected; email Scott for the credentials.

## [[http://www.mpi-sws.org/seminars/pl_seminar/|Videos of the talks]]
## (login: plv password: Pr0gr4mm!ng)

== Schedule ==

|| 1 || 2011-08-03, 2PM || SB || Intro to HDTT and homotopy. ||
|| 2 || 2011-08-05, 1PM || SB || Intro to dependent type theory and equality types. ||
|| 3 || 2011-08-10, 1PM || SB || More on equality in dependent type theory. ||
|| 4 || 2011-08-19, 1PM || SB || Univalence, 2DTT, inductive definitions, and concluding remarks. ||

== Resources ==
=== Blogs and Websites ===
 * Homotopy type theory: [[http://homotopytypetheory.org/]]
   * References at HTT: [[http://homotopytypetheory.org/references/]]
 * n-category cafe blog (sometimes related): [[http://golem.ph.utexas.edu/category/]]
 * nLab - like a Wikipedia for (higher) category theory: [[http://ncatlab.org/nlab/show/HomePage]]
=== Papers ===
 * Martin Hofmann. ''[[http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.36.8985&rep=rep1&type=pdf|Syntax and semantics of dependent types]].'' 1997. Describes the interpretation of dependent type theory into category theory.
 * Martin Hofmann, Thomas Streicher. ''[[http://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/|The groupoid interpretation of type theory]].'' 1995. The first construction of a model in which identity types are non-trivial.
 * Daniel R. Licata and Robert Harper. ''[[http://www.cs.cmu.edu/~rwh/papers/2dtt-can/paper.pdf|Canonicity for 2-Dimensional Type Theory]].'' 2011. (submitted for publication)

== 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.

=== Meeting #2 ===
 * Basics of dependent type theory.
 * Type-indexed families of types.
 * Natural numbers type and recursion.
 * Identity types as "least reflexive relation."
 * Elimination of identity types -- the J operator.
 * Substitution operator (think Coq's rewrite tactic), and how to encode it with J.
 * Discreteness axioms for adding extensionality; cutting off discreteness, e.g., for uniqueness of equality proofs of other equality types.

=== Meeting #3 ===
 * Groupoid structure of identity types.
 * Encoding of transitivity and symmetry terms of identity type.
 * More on discreteness conditions. All types discrete in NuPRL; only identity types in 2-D type theories.
 * The `Set` universe. Individual sets are discrete, but `Set` is indiscrete.
 * More structure in the type `A` means fewer identities in `Id_A(-,-)`.
 * Identify sets up to isomorphism. Introduction of `iso` term of type `Id_Set(-,-)` but no computational interpretation!

=== Meeting #4 ===
 * Alternative notion of `Id`: Paulin's "one-sided elimination."
 * 2-dimensional type theory (see Bob and Dan's paper above) as an extension to NuPRL-like semantics.
 * Internalize identity as judgment `Γ ⊢ α : M ≃ N : A` and recover an `Id` type.
 * Now we can define `subst` on `iso`s gotten from univalence.
 * Brief look at inductive definitions in 2DTT.