Limits and colimits

[mikeshulman]

The Limits and Colimits directories should be generalizable from Type to arbitrary wild categories.

[Alizter]

Do we want to put initiality:

Definition IsInitial {A : Type} `{Is0Coh2Cat A} (x : A)
  := forall (y : A), {f : x $-> y & forall g, f $== g}.

Existing Class IsInitial.

In it's own file in limits?

---

The Diagrams folder contains Cones, Cocones, Diagrams and graphs. We should generalize Diagrams to live in a wild category. The only issue is that there is some funext being used with diagrams, cones and cocones that needs to be removed.

I guess we would need to construct a wild category of cones or cocones and then show there is an initial or terminal such one, in order to state the property of having certain limits or colimits.

[Alizter]

So if we are going to define Diagrams as functors, cones as natural transformations, then we ought to define the category of cones as a comma category.

[Alizter]

This should be doable now that we have comma categories and "left adjoints". We need to define the diagonal functor into Fun11 and then define having colimits/limits as left/right adjoint to the diagonal functor into (Fun11 J C) of some diagram J.

It would then be a good idea to look at generalizing some stuff we have developed in theories/Limits(/Colimits).