Functors equifibered over a fixed functor is closed under limits

instance CategoryTheory.NatTrans.instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomOfHasCoproductsOfShapeHom {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) [∀ (a b : C), Limits.HasCoproductsOfShape (a ⟶ b) D] : ObjectProperty.IsClosedUnderLimitsOfShape (fun (f : Over F) => Equifibered f.hom) J

instance CategoryTheory.NatTrans.instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomOfHasProductsOfShapeHom {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Category.{v_3, u_3} D] (F : Functor C D) [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] : ObjectProperty.IsClosedUnderColimitsOfShape (fun (f : Under F) => Coequifibered f.hom) J