J : Type v'
inst✝⁸ : Category J
C : Type u
inst✝⁷ : Category C
X Y : C
D : Type u''
inst✝⁶ : Category D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsIsomorphisms F
this : ReflectsLimitsOfShape WalkingCospan F
⊢ FinitaryExtensive C
J : Type v'
inst✝⁸ : Category J
C : Type u
inst✝⁷ : Category C
X Y : C
D : Type u''
inst✝⁶ : Category D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsIsomorphisms F
⊢ FinitaryExtensive C
haveI : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShapeOfReflectsIsomorphisms
J : Type v'
inst✝⁸ : Category J
C : Type u
inst✝⁷ : Category C
X Y : C
D : Type u''
inst✝⁶ : Category D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsIsomorphisms F
this✝ : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive C
J : Type v'
inst✝⁸ : Category J
C : Type u
inst✝⁷ : Category C
X Y : C
D : Type u''
inst✝⁶ : Category D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsIsomorphisms F
this : ReflectsLimitsOfShape WalkingCospan F
⊢ FinitaryExtensive C
haveI : ReflectsColimitsOfShape (Discrete WalkingPair) F :=
  reflectsColimitsOfShapeOfReflectsIsomorphisms
no goals
J : Type v'
inst✝⁸ : Category J
C : Type u
inst✝⁷ : Category C
X Y : C
D : Type u''
inst✝⁶ : Category D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsIsomorphisms F
this✝ : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive C
exact finitaryExtensive_of_preserves_and_reflects F