A cone t on F is a limit cone if each cone on F admits a unique cone morphism to t.

Limit cones on F are unique up to isomorphism.

Two morphisms into a limit are equal if their compositions with each cone morphism are equal.

The universal property of a limit cone: a map W ⟶ X is the same as a cone on F with vertex W.

The limit of F represents the functor taking W to the set of cones on F with vertex W.

If G : C → D is a faithful functor which sends t to a limit cone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.

If F.cones is represented by X, each morphism f : Y ⟶ X gives a cone with cone point Y.

If F.cones is represented by X, each cone s gives a morphism s.X ⟶ X.

If F.cones is represented by X, the cone corresponding to the identity morphism on X will be a limit cone.

If F.cones is represented by X, the cone corresponding to a morphism f : Y ⟶ X is the limit cone extended by f.

If F.cones is represented by X, any cone is the extension of the limit cone by the corresponding morphism.

If F.cones is representable, then the cone corresponding to the identity morphism on the representing object is a limit cone.

A cocone t on F is a colimit cocone if each cocone on F admits a unique cocone morphism from t.

Limit cones on F are unique up to isomorphism.

Two morphisms out of a colimit are equal if their compositions with each cocone morphism are equal.

The universal property of a colimit cocone: a map X ⟶ W is the same as a cocone on F with vertex W.

The colimit of F represents the functor taking W to the set of cocones on F with vertex W.

If G : C → D is a faithful functor which sends t to a colimit cocone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.

If F.cocones is corepresented by X, each morphism f : X ⟶ Y gives a cocone with cone point Y.

If F.cocones is corepresented by X, each cocone s gives a morphism X ⟶ s.X.

If F.cocones is corepresented by X, the cocone corresponding to the identity morphism on X will be a colimit cocone.

If F.cocones is corepresented by X, the cocone corresponding to a morphism f : Y ⟶ X is the colimit cocone extended by f.

If F.cocones is corepresented by X, any cocone is the extension of the colimit cocone by the corresponding morphism.

If F.cocones is corepresentable, then the cocone corresponding to the identity morphism on the representing object is a colimit cocone.

has_limit F represents a particular chosen limit of the diagram F.

C has limits of shape J if we have chosen a particular limit of every functor F : J ⥤ C.

C has all (small) limits if it has limits of every shape.

If a functor G has the same collection of cones as a functor F which has a limit, then G also has a limit.

limit F is functorial in F, when C has all limits of shape J.

has_colimit F represents a particular chosen colimit of the diagram F.

C has colimits of shape J if we have chosen a particular colimit of every functor F : J ⥤ C.

C has all (small) colimits if it has colimits of every shape.

We have lots of lemmas describing how to simplify colimit.ι F j ≫ _, and combined with colimit.ext we rely on these lemmas for many calculations.

However, since category.assoc is a @[simp] lemma, often expressions are right associated, and it's hard to apply these lemmas about colimit.ι.

We thus use reassoc to define additional @[simp] lemmas, with an arbitrary extra morphism. (see tactic/reassoc_axiom.lean)

If a functor G has the same collection of cocones as a functor F which has a colimit, then G also has a colimit.

colimit F is functorial in F, when C has all colimits of shape J.