Effective epimorphisms in LightProfinite

This file proves that EffectiveEpi and Surjective are equivalent in LightProfinite. As a consequence we deduce from the material in Mathlib.Topology.Category.CompHausLike.EffectiveEpi that LightProfinite is Preregular and Precoherent.

theorem LightProfinite.effectiveEpi_iff_surjective {X Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑f

instance LightProfinite.instPreregular : CategoryTheory.Preregular LightProfinite