∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {I : Type u_3} {Z Y : I → C} {X : C}
  (g : (i : I) → Z i ⟶ Y i) (f : (i : I) → Y i ⟶ X)
  [inst_1 : CategoryTheory.EffectiveEpiFamily Z fun i => CategoryTheory.CategoryStruct.comp (g i) (f i)]
  [∀ (i : I), CategoryTheory.Epi (g i)] {W : C} (φ : (a : I) → Y a ⟶ W)
  (h :
    ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂),
      CategoryTheory.CategoryStruct.comp g₁ (f a₁) = CategoryTheory.CategoryStruct.comp g₂ (f a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (φ a₁) = CategoryTheory.CategoryStruct.comp g₂ (φ a₂))
  (i : I),
  CategoryTheory.CategoryStruct.comp (f i)
      (CategoryTheory.EffectiveEpiFamily.desc Z (fun i => CategoryTheory.CategoryStruct.comp (g i) (f i))
        (fun i => CategoryTheory.CategoryStruct.comp (g i) (φ i)) ⋯) =
    φ i