C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
this : HasLimit (Functor.empty D)
⊢ HasLimit F
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
⊢ HasLimit F
haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
this : HasLimit (Functor.empty D)
⊢ HasLimit F
apply hasLimitOfIso F.uniqueFromEmpty.symm