∀ (X : Profinite),
  [CategoryTheory.EffectiveEpi (Profinite.presentation.π X), CategoryTheory.Epi (Profinite.presentation.π X),
        Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Profinite.presentation.π X))][0]? =
    some (CategoryTheory.EffectiveEpi (Profinite.presentation.π X))