If a functor preserves limits, so does the induced functor in the Over or Under category

Suppose we are given categories C and D, and object X : C, and a functor F : C ⥤ D. F induces a functor Over.post F : Over X ⥤ Over (F.obj X). If F preserves limits of a certain shape WithTerminal J, then Over.post F preserves limits of shape J. As a corollary, if F preserves finite limits, or limits of a certain size, so does Over.post F.

Dually, if F preserves certain colimits, Under.post F will preserve certain colimits as well.

instance CategoryTheory.Limits.PreservesLimitsOfShape.ofWidePullbacks {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {J : Type u_1} [PreservesLimitsOfShape (WidePullbackShape J) F] : PreservesLimitsOfShape (WithTerminal (Discrete J)) F

instance CategoryTheory.Limits.PreservesLimitsOfShape.overPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {F : Functor C D} [PreservesLimitsOfShape (WithTerminal J) F] : PreservesLimitsOfShape J (Over.post F)

instance CategoryTheory.Limits.PreservesFiniteLimits.overPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {F : Functor C D} [PreservesFiniteLimits F] : PreservesFiniteLimits (Over.post F)

instance CategoryTheory.Limits.PreservesLimitsOfSize.overPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {F : Functor C D} [PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : PreservesLimitsOfSize.{w', w, v₁, v₂, max u₁ v₁, max u₂ v₂} (Over.post F)

instance CategoryTheory.Limits.PreservesColimitsOfShape.underPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] {X : C} {F : Functor C D} [PreservesColimitsOfShape (WithInitial J) F] : PreservesColimitsOfShape J (Under.post F)

instance CategoryTheory.Limits.PreservesFiniteColimits.underPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {F : Functor C D} [PreservesFiniteColimits F] : PreservesFiniteColimits (Under.post F)

instance CategoryTheory.Limits.PreservesColimitsOfSize.underPost {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {F : Functor C D} [PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] : PreservesColimitsOfSize.{w', w, v₁, v₂, max u₁ v₁, max u₂ v₂} (Under.post F)