University of Regensburg
Faculty of Mathematics

HomeAboutPeopleEventsResearchPositionsGuest ProgrammeImpressum

From SFB1085 - Higher Invariants
Jump to navigationJump to search

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 ( and my PhD thesis (

Personal Tools
  • Log in

  • Wiki Tools
  • Page
  • Discussion
  • View source
  • History