# Homotopy Type Theory

Kobi Kremnitzer ( Mathematical Instituteq )

- 14:00 24th February 2012 ( week 6, Hilary Term 2012 )Lecture Theatre B, Department of Computer Science

In recent years, surprising connections between type theory and homotopy theory have been discovered. In this talk I will recall the notions of intensional type theories and identity types. I will describe "infinity groupoids", formal algebraic models of topological spaces, and explain how identity types carry the structure of an infinity groupoid. I will finish by discussing categorical semantics of intensional type theories.