Commit 2025-12-13 14:21 dd97bd1c

chore: use Category* everywhere (#32842) Use the new Category* syntax that landed in #30797.

• Import the syntax in the CategoryTheory/Functor/Basic.lean file: this is the first file in the hierarchy after CategoryTheory/Category/Basic.lean. This makes it available in basically every file which uses category theory.
• All occurences of [Category …] have been replaced by [Category* …]. Cases of [Category.{…} …] remain untouched. This change did uncover a few "bad uses" of [Category …]
• The most notable one is the (J: Type*) [Category J] [FinCategory J] pattern: in that pattern, [FinCategory J] actually requires a SmallCategory, so it was silently setting the universe metavariable in [Category J] to make it equal to the level of J. This pattern has been replaced by (J: Type*) [SmallCategory J] [FinCategory J].
• Some similar uses of [Category …] (where later declarations would silently set the universe levels have been found in CategoryTheory/Category/Cat.lean and CategoryTheory/Category/ReflQuiv.lean: here, the levels have been clarified. The only notable "breakage" is that the way Category* sets levels in a specific order did change the universes level order for PresheafedSpace (and perhaps, silently, some other declarations), which was sometimes called with explicit levels, so PresheafedSpace.{u, v, w} becomes PresheafedSpace.{v, u, w} (as expected, universe levels for morphisms come first). Happy to revert if this is deemed too inconvenient (in practice, PresheafedSpace is often written PresheafedSpace.{_, _, v}, so this did not break a lot.) Finally, minor adjustement in a few files had to be made as adding the * character broke through the 100char width limit.