The obviously tactic is a "replaceable" tactic, which means that its meaning is defined by tactics that are defined later with the @[obviously] attribute. It is intended for use with auto_params for structure fields.

The typeclass category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as category.{v} C. (See also large_category and small_category.)

A large_category has objects in one universe level higher than the universe level of the morphisms. It is useful for examples such as the category of types, or the category of groups, etc.

A small_category has objects and morphisms in the same universe level.