Přednášky se konají v období 21.10. - 25.10.2024, v budově ÚMS (M5 a seminární místnost, 2. patro)

Benno van den Berg, University of Amsterdam

Effective Kan Fibrations

Po 21.10. 14:00-15:00 (seminární místnost, 2. patro)
Út 22.10. 13:00-14:00 (seminární místnost, 2. patro)
St 23.10, 14-15 (M5)
Pá 25.10. 13:00-14:00 (seminární místnost, 2. patro)

Abstract: Simplicial techniques are important in homotopy theory and (higher) category theory. They are also important in type theory, because they were used by Voevodsky to construct a new model of type theory. This model validates principles like the Univalence Axiom and Higher-Inductive Types, leading to a new form of type theory, which goes by the name of Homotopy Type Theory. This model construction uses a  fundamental result about simplicial sets: that it carries a Quillen model structure in which the fibrations are the Kan fibrations.

It turns out that the standard proofs of the existence of the model structure as well as the model of homotopy type theory use non-constructive principles; however, in this series of lectures I want to outline an approach that aims to give a constructive account of these results. For this, a key ingredient is the theory of algebraic weak factorisation systems, as developed by Garner, Riehl, Bourke and others; this theory is used to formulate a more explicit variant of the traditional Kan fibrations: the effective Kan fibrations, as introduced by Faber and myself. I will explain these notions and indicate how far we are in giving constructive and explicit proofs of the fundamental results in simplicial homotopy theory. I will also explain the relation to other approaches, in particular one due to Henry and Gambino.

Tato série přednášek bude přístupná publiku doktorandů a výzkumníků v matematice se základním výcvikem v teorii kategorií.