[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasPullbacks C
⊢ HasPullbacks (Over B)
[PROOFSTEP]
letI : HasLimitsOfShape (ULiftHom.{v} (ULift.{v} WalkingCospan)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v} _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasPullbacks C
this : HasLimitsOfShape (ULiftHom (ULift WalkingCospan)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingCospan)
⊢ HasPullbacks (Over B)
[PROOFSTEP]
letI : Category (ULiftHom.{v} (ULift.{v} WalkingCospan)) := inferInstance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasPullbacks C
this✝ : HasLimitsOfShape (ULiftHom (ULift WalkingCospan)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingCospan)
this : Category.{v, v} (ULiftHom (ULift WalkingCospan)) := inferInstance
⊢ HasPullbacks (Over B)
[PROOFSTEP]
exact hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v, v} _).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasEqualizers C
⊢ HasEqualizers (Over B)
[PROOFSTEP]
letI : HasLimitsOfShape (ULiftHom.{v} (ULift.{v} WalkingParallelPair)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v} _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasEqualizers C
this : HasLimitsOfShape (ULiftHom (ULift WalkingParallelPair)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingParallelPair)
⊢ HasEqualizers (Over B)
[PROOFSTEP]
letI : Category (ULiftHom.{v} (ULift.{v} WalkingParallelPair)) := inferInstance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasEqualizers C
this✝ : HasLimitsOfShape (ULiftHom (ULift WalkingParallelPair)) C :=
  hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv WalkingParallelPair)
this : Category.{v, v} (ULiftHom (ULift WalkingParallelPair)) := inferInstance
⊢ HasEqualizers (Over B)
[PROOFSTEP]
exact hasLimitsOfShape_of_equivalence (ULiftHomULiftCategory.equiv.{v, v} _).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteLimits (Over B)
[PROOFSTEP]
apply @hasFiniteLimits_of_hasEqualizers_and_finite_products _ _ ?_ ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_finiteProducts_of_finiteWidePullbacks
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasEqualizers (Over B)
[PROOFSTEP]
apply @hasEqualizers_of_hasPullbacks_and_binary_products _ _ ?_ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
haveI : HasPullbacks C := ⟨inferInstance⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
this : HasPullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_binaryProduct_of_pullback
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasLimitsOfSize.{w, ?u.4486, v, max u v} (Over B)
[PROOFSTEP]
apply @has_limits_of_hasEqualizers_and_products _ _ ?_ ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_products_of_widePullbacks
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasEqualizers (Over B)
[PROOFSTEP]
apply @hasEqualizers_of_hasPullbacks_and_binary_products _ _ ?_ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
haveI : HasPullbacks C := ⟨inferInstance⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
this : HasPullbacks C
⊢ HasBinaryProducts (Over B)
[PROOFSTEP]
exact ConstructProducts.over_binaryProduct_of_pullback
