strengthen definition of limits/colimits

[TashiWalde]

In #50, limits are definined as terminal cones.

Implement an alternative (a priori stronger) characterization of limits:

• Define cocone not as a single Sigma type, but as a type family cone : (f : A -> B) -> (b : B) -> U.
• Define the canonical composition map cone-precomp b x : cone f x -> hom B b x -> cone f b.
• Define limit (f : A->B) := Sigma ( x: X, c : cone f x ), (b : B) -> is-equiv (cone-precomp b x c)
• Alternatively, if one wants to avoid inputting the composition map (which would require a Segal type),
  one could directly ask for an equivalence of dependent types (b:B) -> Equiv (hom B b x) (cone f b)
  and then show that for a Segal type this equivalence needs to be given by composition.

[cesarbm03]

Noted.