Logo

Mathematical Sciences Research Institute

Home » Online Seminar: Homotopy type theory and internal languages of higher categories

Seminar

Online Seminar: Homotopy type theory and internal languages of higher categories May 18, 2020 (10:00 AM PDT - 11:30 AM PDT)
Parent Program:
Location: MSRI: Online/Virtual
Speaker(s) Chris Kapulkin (University of Western Ontario)
Description No Description
Video

Homotopy Type Theory And Internal Languages Of Higher Categories

Abstract/Media

Zoom link.

https://msri.zoom.us/s/585445592

 

Homotopy type theory is often referred to as the internal logic of higher toposes (or higher categories). This slogan was recently made precise in joint work with Peter Lumsdaine, which establishes a system of conjectures relating different type theories to different classes of higher categories. In this talk, I will introduce the main ideas of homotopy type theory, explain the connection to higher category theory, and report on the progress towards proving these conjectures.

The last part is joint work with Karol Szumilo.

No Notes/Supplements Uploaded

Homotopy Type Theory And Internal Languages Of Higher Categories

H.264 Video 25065_28460_8352_Homotopy_Type_Theory_and_Internal_Languages_of_Higher_Categories.mp4