Preservation of (co)limits by the sheaf Yoneda functor

instance instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] {F : CategoryTheory.Functor K C} [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimit F.op X.obj] : CategoryTheory.Limits.PreservesColimit F J.yoneda

instance instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimitsOfShape Kᵒᵖ X.obj] : CategoryTheory.Limits.PreservesColimitsOfShape K J.yoneda

instance instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] {F : CategoryTheory.Functor K C} [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesLimit F.op X.obj] : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)

instance instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesLimitsOfShape Kᵒᵖ X.obj] : CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)

instance instPreservesLimitsOfShapeSheafTypeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] : CategoryTheory.Limits.PreservesLimitsOfShape K J.yoneda

instance instPreservesLimitsOfShapeSheafTypeUliftYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)

instance instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1 {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] {F : CategoryTheory.Functor K C} [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesLimit F.op X.obj] : CategoryTheory.Limits.PreservesColimit F J.yoneda

instance instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] [∀ (X : CategoryTheory.Sheaf J (Type v)), CategoryTheory.Limits.PreservesFiniteProducts X.obj] : CategoryTheory.Limits.PreservesFiniteCoproducts J.yoneda

instance instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesFiniteProducts X.obj] : CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)