HomeAboutPeopleEventsResearchRTGPositionsGuest ProgrammeImpressum

Abstract: Homotopy type theory (HoTT), due to Voevdsky, Awodey--Warren et. al., is a foundation system alternative to set theory in which one can do homotopy theory synthetically. The basic objects can be understood as ∞-groupoids (modeling homotopy types, i.e. spaces up-to-homotopy). All the constructions performed are automatically invariant under homotopy equivalence.

However, doing (∞,1)-category theory synthetically in standard HoTT has remained an open problem. In this talk, I present such a development in a simplicial extension of HoTT by Riehl--Shulman from 2017. The synthetic development in type theory draws heavily from Riehl--Verity's ∞-cosmos theory.

By Shulman's major result from 2019 standard HoTT can be interpreted in any (∞,1)-topos (in the sense of Grothendieck--Rezk--Lurie). From this it follows that our results apply to internal (∞,1)-categories (implemented by Segal or Rezk objects) relative to any given (∞,1)-topos.

The talk assumes no previous knowledge about type theory.

The material consists of joint work with Buchholtz (https://arxiv.org/abs/2105.01724) and my PhD thesis (https://tuprints.ulb.tu-darmstadt.de/20716/).