using `FullSubcategory`

Stream: mathlib4

[Jireh Loreaux]

From what I can tell, we have docs#CategoryTheory.FullSubcategory, but it isn't actually used to implement any categories, per loogle below. Can someone explain the rational? For example, why is docs#CommMonCat not implemented as a full subcategory of docs#MonCat, and instead just goes via docs#CategoryTheory.Bundled ?

[Jireh Loreaux]

@loogle |- CategoryTheory.FullSubcategory ?Z

[loogle]

:search: CategoryTheory.FullSubcategory.mk

[Christian Merten]

This just does not appear in the type signature, e.g. docs#DiscreteContAction, docs#LeftExactFunctor and many more use docs#CategoryTheory.FullSubcategory.

[Christian Merten]

(grep FullSubcategory.category -r gives some more examples)

[Jireh Loreaux]

I see. Is this because you need type synonyms everywhere for type safety reasons? (or just convenience?)

[Jireh Loreaux]

Also, it doesn't quite explain why some things are not implemented in this way (e.g., CommMonCat). I would have assumed it was easier to just lift everything from the API for FullSubcategory rather than implementing from scratch.

[Christian Merten]

Jireh Loreaux said:

I see. Is this because you need type synonyms everywhere for type safety reasons? (or just convenience?)

I suppose some of those could be abbrevs instead, but I am not sure if this causes performance issues.

[Jireh Loreaux]

Sure, I guess it could cause performance issues since the head would be FullSubcategory everywhere, that makes sense.

[Johan Commelin]

Jireh, my guess is that Bundled gives more API for free than FullSubcategory does... Ideally one would get both.