Commit 2025-10-28 20:32 807c8846

chore(CategoryTheory/EssentiallySmall): adding an instance (#30534) Before this PR, example (C : Type w) [SmallCategory C] : EssentiallySmall.{w} C := inferInstance would not work. We fix this by making essentiallySmall_of_small_of_locallySmall an instance. Consequently, we need to make certain universes explicit in a few proofs. Some instances in Sites.Equivalence are transformed into lemmas because it seems they shadowed more basic instances.