F.cones is the functor assigning to an object X the type of natural transformations from the constant functor with value X to F. An object representing this functor is a limit of F.
F.cocones is the functor assigning to an object X the type of natural transformations from F to the constant functor with value X. An object corepresenting this functor is a colimit of F.
Functorially associated to each functor J ⥤ C, we have the C-presheaf consisting of cones with a given cone point.
Contravariantly associated to each functor J ⥤ C, we have the C-copresheaf consisting of cocones with a given cocone point.
A c : cone F is:
cone F is equivalent, via cone.equiv below, to Σ X, F.cones.obj X.
A c : cocone F is
cocone F is equivalent, via cone.equiv below, to Σ X, F.cocones.obj X.
A map to the vertex of a cone induces a cone by composition.
Naturality of a cone over functors to a concrete category.
A map from the vertex of a cocone induces a cocone by composition.
Naturality of a cocone over functors into a concrete category.
To give an isomorphism between cones, it suffices to give an isomorphism between their vertices which commutes with the cone maps.
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
The image of a cone in C under a functor G : C ⥤ D is a cone in D.
The image of a cocone in C under a functor G : C ⥤ D is a cocone in D.