Limits in the over category

Declare instances for limits in the over category: If C has finite wide pullbacks, Over B has finite limits, and if C has arbitrary wide pullbacks then Over B has limits.

instance CategoryTheory.Over.instHasPullbacks {C : Type u} [Category.{v, u} C] {B : C} [Limits.HasPullbacks C] : Limits.HasPullbacks (Over B)

Make sure we can derive pullbacks in Over B.

instance CategoryTheory.Over.instHasEqualizers {C : Type u} [Category.{v, u} C] {B : C} [Limits.HasEqualizers C] : Limits.HasEqualizers (Over B)

Make sure we can derive equalizers in Over B.

instance CategoryTheory.Over.hasFiniteLimits {C : Type u} [Category.{v, u} C] {B : C} [Limits.HasFiniteWidePullbacks C] : Limits.HasFiniteLimits (Over B)

instance CategoryTheory.Over.hasLimits {C : Type u} [Category.{v, u} C] {B : C} [Limits.HasWidePullbacks C] : Limits.HasLimitsOfSize.{w, w, v, max u v} (Over B)