Online seminář z algebry - 26.11.2020 PDF Tisk

Další seminář z algebry se koná 26.11.2020 od 13.00 online na platformě ZOOM. Informace pro připojení a další program semináře je zde.

Martin Bidlingmaier (Aarhus University)

Model categories of lcc categories and the gros model of dependent type theory

In this talk we discuss various model categories of locally cartesian closed (lcc) categories and their relevance to coherence problems, in particular the coherence problem of categorical semantics of dependent type theory. We begin with Lcc, the model category of locally cartesian closed (lcc) sketches. Its fibrant objects are precisely the lcc categories, though without assigned choices of universal objects. We then obtain a Quillen equivalent model category sLcc of strict lcc categories as the category of algebraically fibrant objects of Lcc. Strict lcc categories are categories with assigned choice of lcc structure, and their morphisms preserve these choices on the nose. Conjecturally, sLcc is precisely Lack’s model category of algebras for a  2-monad T, where T is instantiated with the free lcc category functor on Cat. We then discuss the category of algebraically cofibrant objects of sLcc and show how it can serve as a “gros” model of dependent type theory.

Aktualizováno Středa, 25 Listopad 2020 10:33