search

mikeshulman / Coq-HoTT

Homotopy type theory
http://homotopytypetheory.org/
Other
12 stars 4 forks source link

Limits and colimits #27

Open mikeshulman opened 4 years ago

mikeshulman commented 4 years ago

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

Alizter commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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).