∀ {α : Type} [inst : Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B),
  [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π),
      ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE