mathlib documentation

category_theory.category.Cat.limit

The category of small categories has all small limits. #

An object in the limit consists of a family of objects, which are carried to one another by the functors in the diagram. A morphism between two such objects is a family of morphisms between the corresponding objects, which are carried to one another by the action on morphisms of the functors in the diagram.

Future work #

Can the indexing category live in a lower universe?

@[protected, instance]

The category of small categories has all small limits.