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.instHasPullbacksOverInstCategoryOver {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Limits.HasPullbacks (CategoryTheory.Over B)

Make sure we can derive pullbacks in Over B.

Equations

• (_ : CategoryTheory.Limits.HasPullbacks (CategoryTheory.Over B)) = (_ : CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.Over B))

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

Make sure we can derive equalizers in Over B.

Equations

• (_ : CategoryTheory.Limits.HasEqualizers (CategoryTheory.Over B)) = (_ : CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Over B))

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

Equations

• (_ : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over B)) = (_ : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over B))

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

Equations

• One or more equations did not get rendered due to their size.