Commit 2025-12-01 19:09 fae0f6ae

feat(Mathlib/Tactic/CategoryStar): Category* (#30797) We introduce Category*, an elaborator for introducing category instances which behaves analogously to Type*. Specifically, when writing Category* C this elaborator does the following:

1. It creates a new universe parameter v, and the elaborated term becomes Category.{v} C.
2. It places v just before the universe parameters appearing in C or its type, as commonly done in the category theory library. Basic usage:

variable (C : Type*) [Category* C]
variable (D : Type*) [Category* D]

This is essentially equivalent to:

universe v_1 u_1
variable (C : Type u_1) [Category.{v_1} C]
universe v_2 u_2
variable (D : Type u_2) [Category.{v_2} D]