Fredrik Bakke: Segal Spaces in Homotopy Type Theory

Date of publication: 15. 5. 2024
Mathematics and theoretical computing seminar
10:00 - 12:00
Jadranska 21, predavalnica 3.07

Fredrik Bakke (Norwegian University of Science and Technology)

Abstract: Homotopy Type Theory is a language for doing homotopy invariant mathematics. As such one would expect it to be a good setting for doing ∞-category theory. Indeed, by extending the type theory with a directed interval object we get a type theory where every type is automatically equipped with simplicial structure and every construction preserves this structure in the appropriate sense. In this setting we can define and work with ∞-categories synthetically. We will have a look at some of the basic aspects of category theory in this setting.