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
commented
1 year ago
In #50, limits are definined as terminal cones.
Implement an alternative (a priori stronger) characterization of limits:
cone : (f : A -> B) -> (b : B) -> U.cone-precomp b x : cone f x -> hom B b x -> cone f b.limit (f : A->B) := Sigma ( x: X, c : cone f x ), (b : B) -> is-equiv (cone-precomp b x c)(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.