A seminar talk presented (online) at USD Categories and Type Theory Seminar.

Abstract

In this talk, I present/report on work in progress with the aim of constructing a “homotopy theory of univalent category theory”. More formally, I aim to construct a model structure whose fibrant objects are precisely the univalent categories and the fibrant replacement is given by the Rezk completion. In order to consider (structured) categories as objects, one is forced to leave the framework of (1-)categories and work in the setting of bicategories. Hence, a first challenge is to define a suitable notion of model structure on a bicategory. A definition of a model bicategory has already been presented in the literature. However, it seems that this definition is not immediately suitable for our problem. Hence, I will sketch a definition of a different notion of a model structure. I first explain my interest/motivation in the question/construction (and solution). After providing some intuition, I present the definition of a model structure. Furthermore, I conjecture a construction of a suitable model structure on the bicategory of categories, that also generalizes to other bicategories of structured categories. After this, I discuss some future work and related work.