C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsSeparating 𝒢
this : Small ↑(Set.op 𝒢)
⊢ HasTerminal C
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsSeparating 𝒢
⊢ HasTerminal C
haveI : Small.{v₁} 𝒢.op := small_of_injective (Set.opEquiv_self 𝒢).injective
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsSeparating 𝒢
this✝ : Small ↑(Set.op 𝒢)
this : HasInitial Cᵒᵖ
⊢ HasTerminal C
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsSeparating 𝒢
this : Small ↑(Set.op 𝒢)
⊢ HasTerminal C
haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating ((isCoseparating_op_iff _).2 h𝒢)
no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsSeparating 𝒢
this✝ : Small ↑(Set.op 𝒢)
this : HasInitial Cᵒᵖ
⊢ HasTerminal C
exact hasTerminal_of_hasInitial_op