essentiallySmall_ofSmall_ofLocallySmall

Stream: mathlib4

[Robert Maxton]

Is there any specific reason that docs#CategoryTheory.essentiallySmall_of_small_of_locallySmall isn't already an instance, or can I just PR that?

[Yury G. Kudryashov]

Does it lead to cycles in the instance graph?

[Robert Maxton]

How do I find out?

[Yury G. Kudryashov]

Assume essentially small + one of small and locally small and try to synthesize the other one.

[Yury G. Kudryashov]

Note: I know nothing about this part of the library.

[Robert Maxton]

Mm. I see. Yes, EssentiallySmall "decomposes" into Small and LocallySmall.

[Robert Maxton]

Unfortunate that we can't have it both ways there.

[Yury G. Kudryashov]

We can, but it comes with a performance hit.