C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
this : HasColimit (Functor.empty D)
⊢ HasColimit F
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
⊢ HasColimit F
haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
this : HasColimit (Functor.empty D)
⊢ HasColimit F
apply hasColimitOfIso F.uniqueFromEmpty