Welcome & Intro

Stream: Displayed Categories

[Sina Hazratpour 𓃵]

This channel is a space to discuss the formalization of categorical and 2-categorical aspects of fibrations via displayed categories.

A displayed category over a category C is a structure equivalent to "a category D and functor F : D ⥤ C", but instead of having a single collection of objects of D with a map F.obj to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. Similarly, Grothendieck fibrations can be formulated in a "displayed" way, and this formulation crucially avoids any reference to equality on objects, in contrast to the standard definition of Grothendieck fibrations. Working with equality of objects and rewriting along them leads one to the so-called dependent hell for rewriting. The hope is that we can use displayed categories to avoid the dependent hell while developing the theory of fibrations.

A definition of displayed categories, its basic API, and the notion of displayed Grothedieck fibration is formalized in

https://github.com/sinhp/displayed_categories

[Robin Carlier]

Hello! I took the liberty to register to this channel because I am interested in getting the equivalence between fibrations over C and pseudofunctors to Cat in mathlib at some point. So I figured the topic would interest me.
Fyi, while this is not directly related to displayed categories nor fibrations, I am currently working (privately for now) on bringing a nice API for "categorical pullback" of categories (i.e pullbacks in the (2,1)-category sense, in which the square only commutes up to a specified natural isomorphism), and I hope to include a proof that (co)cartesian fibrations (aka (co)fibered categories) are stable under such pullbacks.

[Sina Hazratpour 𓃵]

Robin Carlier said:

Hello! I took the liberty to register to this channel because I am interested in getting the equivalence between fibrations over C and pseudofunctors to Cat in mathlib at some point. So I figured the topic would interest me.
Fyi, while this is not directly related to displayed categories nor fibrations, I am currently working (privately for now) on bringing a nice API for "categorical pullback" of categories (i.e pullbacks in the (2,1)-category sense, in which the square only commutes up to a specified natural isomorphism), and I hope to include a proof that (co)cartesian fibrations (aka (co)fibered categories) are stable under such pullbacks.

great, while hereafter i am mostly going to be involved reviewing PRs I know that @Fernando Chu is also interested in formalizing the equivalence you mentioned, so maybe a good idea to coordinate with him here about this. Feel free to PR any new changes.

[Sina Hazratpour 𓃵]

(deleted)