Effective epimorphisms in CompHausLike

In any category of compact Hausdorff spaces, continuous surjections are effective epimorphisms.

We deduce that if the converse holds and explicit pullbacks exist, then CompHausLike P is preregular.

If furthermore explicit finite coproducts exist, then CompHausLike P is precoherent.

noncomputable def CompHausLike.effectiveEpiStruct {P : TopCat → Prop} {B X : CompHausLike P} (π : X ⟶ B) (hπ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)) : CategoryTheory.EffectiveEpiStruct π

If π is a surjective morphism in CompHausLike P, then it is an effective epi.

theorem CompHausLike.preregular {P : TopCat → Prop} [HasExplicitPullbacks P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Preregular (CompHausLike P)

theorem CompHausLike.precoherent {P : TopCat → Prop} [HasExplicitPullbacks P] [HasExplicitFiniteCoproducts P] (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Precoherent (CompHausLike P)