Quantum Topology / Hopf Algebra Seminar
Alexander Berenbeim
UIC
Motivations For Homotopy Type Theory
Abstract: There are always $\omega$-groupoids lurking about. In part 1 of a thrilling two parter, we are going to start from scratch and talk about (i) categorical deductive systems and (ii) the (typed) $\lambda$-calculus. Highlights include: the adjunction between the category of directed graphs and the category of Cartesian Closed Categories; the functional completeness of Kleisi Categories; what this all has to do with groupoids; the importance of induction principles; and an introduction to the basic type formers used in Homotopy Type Theory (including the illustrious identity types).
Thursday March 16, 2017 at 2:00 PM in SEO 612