Peter LeFanu Lumsdaine: Introduction to HoTT, for logicians
Time: Wed 2014-09-10 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
(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.