1st Semester 2024/25: Effective Kan fibrations: A categorical adventure

Instructors

Benno van den Berg

ECTS

6

Description

This projects aim to give an introduction to the research programme I have been working on in the last couple of years and to which various MoL students have also contributed. The aim of this programme is to give a constructive account of Voevodsky's model of Homotopy Type Theory in simplicial sets, a certain presheaf category.

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 project 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.

Organisation

Every week there will be one lecture (2 hours), and one or more presentations by students on selected topics (max 2 hours). For both the lecture and the presentations, there will be homework assignments. Attendance at the student presentations is mandatory.

Prerequisites

Knowledge of Category Theory as can be obtained through the Category Theory course. Knowledge of Type Theory is not required.

Assessment

In order to pass students have to:

• Give a presentation, and
• Solve homework assignments.

References

1. Van den Berg and Faber, Effective Kan fibrations in simplicial sets. Springer, 2022.

2. Geerligs and van den Berg, Examples and cofibrant generation of effective Kan fibrations in simplicial sets. To appear in JPAA (Journal of Pure and Applied Algebra).

3. Bourke and Garner, Algebraic weak factorisation systems I: Accessible AWFS. JPAA, 220 (2016), no. 1, 108-147.

4. Bourke, An orthogonal approach to algebraic weak factorisation systems, JPAA, 227 (2023), no. 6, 107294.

5. The MSc thesis of Lingyuan Ye. Available from https://msclogic.illc.uva.nl/theses/recent/

6. The MSc thesis of Paul Seip. Available from https://msclogic.illc.uva.nl/theses/recent/