Functors equifibered over a fixed functor is closed under limits

instance CategoryTheory.NatTrans.instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom {J : Type u_1} {C : Type u_3} {D : Type u_4} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] [Category.{v_4, u_4} 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.instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomDiscretePUnitOfHasProductsOfShapeHom {J : Type u_1} {C : Type u_3} {D : Type u_4} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] [Category.{v_4, u_4} D] (F : Functor C D) [∀ (a b : C), Limits.HasProductsOfShape (a ⟶ b) D] : ObjectProperty.IsClosedUnderColimitsOfShape (fun (f : Under F) => Coequifibered f.hom) J