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?
Auxiliary definition: the diagram whose limit gives the morphism space between two objects of the limit category.
Instances For
Auxiliary definition: the limit category.
Instances For
Auxiliary definition: the cone over the limit category.
Instances For
Auxiliary definition: the universal morphism to the proposed limit cone.
Instances For
Auxiliary definition: the proposed cone is a limit cone.
Instances For
The category of small categories has all small limits.