Seminar
| Parent Program: | |
|---|---|
| Location: | SLMath: Online/Virtual |
Keywords and Mathematics Subject Classification (MSC)
Primary Mathematics Subject Classification
No Primary AMS MSC
Secondary Mathematics Subject Classification
No Secondary AMS MSC
Homotopy Type Theory And Internal Languages Of Higher Categories
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.
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 |