Filtered colimits and cofiltered limits in C and Cᵒᵖ

We construct filtered colimits and cofiltered limits in the opposite categories.

instance CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits {C : Type u₁} [Category.{v₁, u₁} C] [HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C] : HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

theorem CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] : HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C

instance CategoryTheory.Limits.has_filtered_colimits_op_of_has_cofiltered_limits {C : Type u₁} [Category.{v₁, u₁} C] [HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C] : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

theorem CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C