1860
Comment:
|
2716
|
Deletions are marked like this. | Additions are marked like this. |
Line 1: | Line 1: |
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. | = 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. |
Line 11: | Line 13: |
Organizer: [[mailto:skilpat@mpi-sws.org|Scott Kilpatrick]] | Organizers: [[mailto:rwh@cs.cmu.edu|Bob Harper]] and [[mailto:skilpat@mpi-sws.org|Scott Kilpatrick]] |
Line 18: | Line 20: |
|| 1 || 2011-08-03, 2PM || Intro to HDTT and homotopy. || || 2 || 2011-08-05, 1PM || ? || |
|| 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 || KL || ? || |
Line 24: | Line 27: |
* References at HTT: [[http://homotopytypetheory.org/references/]] | |
Line 25: | Line 29: |
* nLab - like a Wikipedia for (higher) category theory: [[http://ncatlab.org/nlab/show/HomePage]] | |
Line 38: | Line 43: |
=== 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. |
Higher-Dimensional Type Theory Seminar
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
Organizers: Bob Harper and Scott Kilpatrick
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 |
KL |
? |
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. 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.
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.