Research Project on Path Categories

Path Categories form a categorical framework for homotopy theory that gives a semantics for type theory. Path categories are simple compared to other semantics but contain enough structure to prove homotopy theoretical results. It is a notion that is closely connected to two established frameworks: Brown’s categories of fibrant objects and Quillen’s model categories.

A path category is a category \(\mathcal C\) with two classes of maps: fibrations and (weak) equivalences. If a fibration is an equivalence then we call it acyclic. In addition, the following principles should hold:

In a path category we can define a lot of homotopy theory and prove statements such as: every map can be written as an equivalence followed by a fibration, the weak equivalences are precisely the homotopy equivalences, and the fact that the equivalences are orthogonal to the fibrations (up to fibered homotopy).

The goal of this project is to gather the existing literature in one place and to describe it in a unified and structured way.

6 ECTS, Spring 2024
Supervisors: Benno van den Berg and Daniël Otten.