∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ {B₁ B₂ : C} (f : B₂ ⟶ B₁) (α : Type) [Finite α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁),
      CategoryTheory.EffectiveEpiFamily X₁ π₁ →
        ∃ β,
          ∃ (_ : Finite β),
            ∃ X₂ π₂,
              CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧
                ∃ i ι,
                  ∀ (b : β),
                    CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f) →
    CategoryTheory.Precoherent C