3939
Comment:

← Revision 15 as of 20110824 15:58:47 ⇥
4241

Deletions are marked like this.  Additions are marked like this. 
Line 14:  Line 14: 
Videos: The videos of lectures 24 are [[http://www.mpisws.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. 
HigherDimensional Type Theory Seminar
WHAT? This lecture series conducted by Bob Harper will cover various topics in higherdimensional 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? MPISWS Kaiserslautern/Wartburg
HOW? Mailing list for this series (and other type theory discussion): typetheory@mpisws.org
Organizers: Bob Harper and Scott Kilpatrick
Videos: The videos of lectures 24 are available online. Altogether they're around 850mb. Use VLC to play them if you're having trouble. They're password protected; email Scott for the credentials.
Schedule
1 
20110803, 2PM 
SB 
Intro to HDTT and homotopy. 
2 
20110805, 1PM 
SB 
Intro to dependent type theory and equality types. 
3 
20110810, 1PM 
SB 
More on equality in dependent type theory. 
4 
20110819, 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/
ncategory 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. 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 nontrivial.
Daniel R. Licata and Robert Harper. Canonicity for 2Dimensional Type Theory. 2011. (submitted for publication)
Topics
Meeting #1
 Intro to higherdimensional 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.
 Typeindexed 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 2D 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 "onesided elimination."
 2dimensional type theory (see Bob and Dan's paper above) as an extension to NuPRLlike semantics.
Internalize identity as judgment Γ ⊢ α : M ≃ N : A and recover an Id type.
Now we can define subst on isos gotten from univalence.
 Brief look at inductive definitions in 2DTT.