How to define `GrothendieckCategory`

Stream: mathlib4

[Markus Himmel]

In #18510 we're getting the definition of Grothendieck categories. A Grothendieck category is an abelian category that satisfies Grothendieck's axiom AB5 and has a generator. Here is the definition from the PR:

variable (C : Type u) [Category.{v} C]

/--
An abelian category `C` is called a Grothendieck category provided that it has `AB5` and a
separator (see `HasSeparator`).
-/
class GrothendieckCategory [Abelian C] [HasFilteredColimits C] [AB5 C] [HasSeparator C] : Prop where

I'll admit that I am completely clueless about design tradeoffs in typeclass hierarchies. My first instinct for the definition might have been something like

variable (C : Type u) [Category.{v} C]
class GrothendieckCategory [Abelian C] extends HasFilteredColimits C, AB5 C, HasSeparator C : Prop where

except that this doesn't work because AB5 C is actually data (because PreservesLimit is data), but arguably it shouldn't be and AB5 should wrap the PreservesLimit in a Nonempty. Of course another option could be to put some of the typeclasses as structure fields of GrothendieckCategory.

I'm sure there are some heuristics that mathlib's hierarchy experts have developed that help decide how best to define a typeclass that is logically the conjunction of several other typeclasses and nothing else. Is there a good place to learn about this? Does anyone have advice?

cc @Paul Reichert

[Joël Riou]

I also think everything apart from Abelian Cshould be a field of GrothendieckCategory (whether by extends or by introducing explicit fields; I do not care very much about this detail).
As for now, I think it is ok if this is not a Prop. The reason is that eventually, I believe that in general PreservesLimit should be made a Prop: I do not think we have any construction which rely on the data in these instances. Then, when we do this refactor, Lean will complain that a class that can be reduced to a Prop is not declared as a Prop, and the fix will be easy.