Alternative notions of displayed categories

Stream: Displayed Categories

[Fernando Chu]

The very notion of displayed categories requires some casting operation between the hom-over types X ⟶[f] Y and X ⟶[g] Y, whenever f = g. While this was good for unimath, since they do a lot of casting everywhere, this doesn't really fit into the mathlib approach of developing application specific lemmas, so as to make automation as powerful as possible.

Another reasonable approach, is considering semi-displayed categories (Example 8.14 here). Essentially, only the objects are indexed, whereas the hom-over types are independent of the ones below. This allows for removing all casts, while keeping the fiber (of objects) to be judgmentally over their base. An analogous notion makes the objects indexed, but requires the Sigma to be a category (this was suggested to me by @Christian Merten ). I call this the total semi-displayed version below.

Still, I wanted to see a clear comparison so I partially formalized that the grothendieck construction is a fibration, in three of the available options. Here are my conclusions:

	Current Mathlib approach (Functor into C)	Semi-displayed (total)	Semi-displayed	Displayed
Doesn't involve casts between morphisms	Yes	Yes	Yes	No
Fiber over c is judgmentally over it. I.e. (x : Fiber c) implies pi x defeqs c.	No	Yes	Yes	Yes
Morphisms over f:c⟶d are judgmentally over it.	No	No	No	Yes
Composition in the total/base category (i.e. the one that maps to C) is ≫	Yes	Yes	No	No
Machinery already defined can be easily used (e.g. functors, nattrans, etc)	Yes	Yes (kindof)	No	No
Approach extends to other structures (e.g. bicats, double cats, ncats, etc)	Yes	No	No	Yes

The properties are intended to be roughly ordered from more to less important. Given this, I'm doubting quite a bit displayed cats are a good fit for mathlib. I instead am thinking that the semi-displayed total version is the better one.

Any comments on this are very much appreciated. May interest you @Niels van der Weide .

[Pim Otte]

Awsome, nice comparison!

Some questions that arose for me:

• Does requiring the Sigma to be a category limit applications? I'm guessing this is fine in our case, but for general applicability? I think it just limits the homovers to be sets, right?
• Are the "judgemental over" rows something that can be mitigated/solved with automation? If yes, that might suggest that the current mathlib approach might be the best even for us.

[Christian Merten]

Re 1: No, it does not limit the homovers to be sets. You can ask for the sigma type to be a category with Hom types in an arbitrary universe, independent of the universe of objects.

[Christian Merten]

Re 2: This is attempted with the docs#CategoryTheory.IsHomLiftAux type, it fails when the appearing terms are not free variables though. The "I wish to be in set theory tactic" we tried to write, was precisely an attempt at solving this with automation, but we failed miserably.

[Fernando Chu]

Re 1: It does not limit applications, but it does make some things slightly cumbersome. E.g., if one wants to use some fact about fibrations for some functor C => D, they will have to replace C by its Sigma version (this also happens in the other non-current-mathlib approaches). It is not completely clear to me that the single improvement (second row) outweighs this and the other problems...

[Fernando Chu]

My conjecture is that row 2 is mostly useful for results about abstract categories (i.e. variable C : Cat), and that actual concrete categories will satisfy row 2 by construction; e.g., this happens in the Grothendieck construction. But for abstract cats, the current mathlib approach will also give some version of row 2 by their IsHomLiftAux trick (not clear to me yet how this precisely compares to other approaches).

[Christian Merten]

Ultimately, your project will show that every fibred / displayed category is equivalent to one where row 2 holds.

[Fernando Chu]

I guess, but this is a very roundabout way of showing that. This can also be seen immediately because you don't need to show that the fiber function is a pseudofunctor, and you just define a category structure on the sigma by hom((x,y),(x',y')) := hom(y,y'). The resulting cat will be isomorphic to the original one.

[Christian Merten]

I don't understand what hom(y, y') means. Are y and y' even objects of the same category? In other words, what is the indexing type and the components of the sigma type?

[Fernando Chu]

Maybe a clearer way to see it is that for any function f : B -> A, if we write f⁻¹ : A -> Type for the fiber function, then Sigma f⁻¹ is isomorphic (as a type) to B. So now if f is a functor, we can define the category structure of the Sigma to be the one induced by this isomorphism

[Fernando Chu]

Wondering if you have any thoughts about this @Sina Hazratpour 𓃵 . In particular, did you have some plan on how to deal with casts of morphisms? I'm currently inclined to drop the displayed approach and only use the current in mathlib together with the HasFibers class.

[Max New]

Fernando Chu said:

this doesn't really fit into the mathlib approach of developing application specific lemmas, so as to make automation as powerful as possible.

Could you say a bit more about this? I'm experienced with displayed categories in Agda and would like to understand why this would be bad for tactics

[Fernando Chu]

Max New said: ...

Hi Max! I didn't mean to imply this is bad for tactics in general, just bad for the tactics that have already been developed in mathlib. Transport/HEq is avoided whenever possible, and in particular for categories the current approach is using eqToHoms everywhere to avoid mention of transports. So, a lot of (simp) lemmas have been developed and will be continued to be developed for results about eqToHom.

So, instead of redeveloping the analogue of these for transports, I think it's better to just adapt and extend the current eqToHom approach for fibered categories. Unless one intends to do huge amounts of fibered category theory I think this is much more time efficient, while also contributing to other non-fibered application.

Also, just 3 days ago the HasFibers class was introduced, which can be used for recovering some judgemental equalities for concrete examples (see there for further discussions).

By the way, what is your use case for displayed stuff? Is it for displayed virtual equipments?

[Max New]

I've been trying to formalize properties about fibrations to do logical relations proofs in a more re-usable/compositional way. Some of it is upstreamed into the cubical library and a lot of it is in my extension my students and I work on: https://github.com/maxsnew/cubical-categorical-logic . The most complete result is constructing canonicity proofs for free cartesian categories: https://github.com/maxsnew/cubical-categorical-logic/blob/main/Gluing/CartesianCategory.agda . I also did the coherence theorem for monoidal categories using displayed categories here: https://github.com/maxsnew/cubical-categorical-logic/blob/main/Cubical/Categories/Constructions/Free/Monoidal/Coherence.agda

[Fernando Chu]

Cool! I don't really know the displayed cats approach to these results, but I'd imagine that the HasFibers class will be very useful for this :)