Support for Category* C.

In the category theory library, it is common to introduce a (universe polymorphic) general category as follows:

universe v u
variable (C : Type u) [Category.{v} C]

We tend to put the universe level v of the morphisms ahead of the level u for objects because it makes it easier to specify explicit universes when needed.

The elaborator Category* provides analogous behavior to Type* for introducing category instances. The term elaborator Category* C creates a universe parameter v, and places it just before any universe parameters appearing in C and its type. If C and its type have no parameters, v becomes the last level parameter. The elaborated term is then Category.{v} C.

Basic usage:

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

def «termCategory*__» : Lean.ParserDescr

The syntax Category* C creates a new distinct implicit universe parameter v, placed just before any parameters appearing in C and its type, and elaborates to Category.{v} C.

Equations

• One or more equations did not get rendered due to their size.