Commit 2020-09-24 16:49 03894dff

feat(category_theory/limits/creates): Add has_(co)limit defs (#4239) This PR adds four defs:

1. has_limits_of_shape_of_has_limits_of_shape_creates_limits_of_shape
2. has_limits_of_has_limits_creates_limits
3. has_colimits_of_shape_of_has_colimits_of_shape_creates_colimits_of_shape
4. has_colimits_of_has_colimits_creates_colimits These show that a category C has (co)limits (of a given shape) given a functor F : C ⥤ D which creates (co)limits (of the given shape) where D has (co)limits (of the given shape). See the associated zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/has_limits.20of.20has_limits.20and.20creates_limits/near/211083395