Date : Wednesday, January 5, 2022
Time : 3.30pm -- 4.30pm
Higher category theory and homotopy type theory
Chaitanya Leena Subramaniam
University of San Diego.
Higher category theory is the right conceptual setting for homotopy theory, higher algebra and derived geometry, just as (ordinary) category theory is the right setting for logic, algebra and geometry. However, whereas ordinary category theory is founded on set theory, higher category theory suffers from a lack of suitably general "model-independent" foundations. Given a particular model of a higher category, sifting true higher category-theoretic information from the irrelevant structure and properties of the model is a laborious and ad hoc process.
A primary requirement for higher category theory is a formal theory of spaces ("space" = topological space, simplicial set etc. up to weak equivalence). An excellent candidate for this formal "space theory" is Homotopy Type Theory (HoTT). HoTT has a canonical interpretation in the ∞-topos of spaces, and indeed in any ∞-topos. Fundamental constructions of homotopy theory such as homotopy fibres, homotopy pushouts, suspensions, joins, smashes, loop spaces, connectivity, truncation etc. all admit natural definitions in HoTT, which moreover have the correct ∞-category theoretic universal property.
This talk will introduce higher toposes and Homotopy Type Theory simultaneously, showing how the homotopy theory of an ∞-topos is represented internally in HoTT in a model-independent way.
About the speaker
Chaitanya Leena Subramaniam completed his PhD in 2021 at IRIF, Université Paris Diderot, under the supervision of Paul-André Melliès. His thesis was titled "From dependent type theory to higher algebraic structures". He is currently a post-doc at the University of San Diego. His interests include (∞-)category theory, (∞-)topoi, homotopy type theory (HoTT), categorical logic, algebraic topology/homotopy theory, and (higher) algebra.
This is an introductory talk. If the audience wishes to know more about some of the topics, we can schedule a follow-up talk on Jan 12, 2022, from 3.30pm--4.30pm.