C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J (StructuredArrow X F)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ HasFiniteLimits (StructuredArrow X F)
apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ HasLimitsOfShape J (StructuredArrow X F)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
⊢ ∀ (J : Type v₁) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J (StructuredArrow X F)
intro J sJ fJ
case has_limit
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ autoParam (∀ (F_1 : J ⥤ StructuredArrow X F), HasLimit F_1) _auto✝
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ HasLimitsOfShape J (StructuredArrow X F)
constructor
no goals
case has_limit
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
X : D
J : Type v₁
sJ : SmallCategory J
fJ : FinCategory J
⊢ autoParam (∀ (F_1 : J ⥤ StructuredArrow X F), HasLimit F_1) _auto✝
infer_instance