The typeclass category C describes morphisms associated to objects of type C : Type u.

The universe levels of the objects and morphisms are independent, and will often need to be specified explicitly, as category.{v} C.

Typically any concrete example will either be a small_category, where v = u, which can be introduced as

universes u
variables {C : Type u} [small_category C]

or a large_category, where u = v+1, which can be introduced as

universes u
variables {C : Type (u+1)} [large_category C]

In order for the library to handle these cases uniformly, we generally work with the unconstrained category.{v u}, for which objects live in Type u and morphisms live in Type v.

Because the universe parameter u for the objects can be inferred from C when we write category C, while the universe parameter v for the morphisms can not be automatically inferred, through the category theory library we introduce universe parameters with morphism levels listed first, as in

universes v u

or

universes v₁ v₂ u₁ u₂

when multiple independent universes are needed.

This has the effect that we can simply write category.{v} C (that is, only specifying a single parameter) while u will be inferred.

Often, however, it's not even necessary to include the .{v}. (Although it was in earlier versions of Lean.) If it is omitted a "free" universe will be used.

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.

Many proofs in the category theory library use the dsimp, simp pattern, which typically isn't necessary elsewhere.

One would usually hope that the same effect could be achieved simply with simp.

The essential issue is that composition of morphisms involves dependent types. When you have a chain of morphisms being composed, say f : X ⟶ Y and g : Y ⟶ Z, then simp can operate succesfully on the morphisms (e.g. if f is the identity it can strip that off).

However if we have an equality of objects, say Y = Y', then simp can't operate because it would break the typing of the composition operations. We rarely have interesting equalities of objects (because that would be "evil" --- anything interesting should be expressed as an isomorphism and tracked explicitly), except of course that we have plenty of definitional equalities of objects.

dsimp can apply these safely, even inside a composition.

After dsimp has cleared up the object level, simp can resume work on the morphism level --- but without the dsimp step, because simp looks at expressions syntactically, the relevant lemmas might not fire.

There's no bound on how many times you potentially could have to switch back and forth, if the simp introduced new objects we again need to dsimp. In practice this does occur, but only rarely, because simp tends to shorten chains of compositions (i.e. not introduce new objects at all).