Tingxiang Zou
(ILLC)
An Invitation to Homotopy Type Theory
December 12th at 18:00, in F1.15 ILLC seminar room
In the last decade, a number of deep connections between a form of type theory and homotopy theory have been discovered, which leads to a new research area: Homotopy Type Theory (HoTT) that attracts theoretical computer scientists, topologists, logicians and categorical theorists. In this talk, I will give a very brief introduction for HoTT: Martin Löf's dependent type theory; homotopy theory; their connections and maybe Voevodsky's Univalence Axiom.