{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        {ι : Type u_1} →
          (X : ι → C) →
            {c : CategoryTheory.Limits.Cofan X} →
              CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt →
                [∀ (i : ι), CategoryTheory.Mono (c.inj i)] →
                  (∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) →
                    (∀ {i j : ι},
                        i ≠ j →
                          ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j),
                            CategoryTheory.CategoryStruct.comp a (c.inj i) =
                                CategoryTheory.CategoryStruct.comp b (c.inj j) →
                              Nonempty (CategoryTheory.Limits.IsInitial Y)) →
                      CategoryTheory.Limits.IsColimit
                        (CategoryTheory.Limits.Cofan.mk (J.yoneda.obj c.pt) fun i => J.yoneda.map (c.inj i))