Peter LeFanu Lumsdaine: Introduction to HoTT, for logicians

(In this talk, I will assume some familiarity with dependent type theory.)

What is Homotopy Type Theory? Many things! It can be seen as (non-exhaustively):

• various new homotopy-theoretic models of (traditional) dependent type theory;
• a complex of new concepts and definitions within (traditional) dependent type theory, motivated by these models;
• new axioms (univalence, HIT), motivated by these models;
• the use of DTT with these new axioms as a foundation for mathematics.

I will survey all of these, with a focus on the second point: concepts such as truncatedness and connectedness, which are motivated by homotopy-theoretic models, but can already be expressed and developed in plain dependent type theory.