mathlib

03894dff - feat(category_theory/limits/creates): Add has_(co)limit defs (#4239)

feat(category_theory/limits/creates): Add has_(co)limit defs (#4239) This PR adds four `def`s: 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