∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {ι : Type u_1} (X : ι → C) {c : CategoryTheory.Limits.Cofan X}
  (H : CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt)
  (heq :
    ∀ (s : CategoryTheory.Limits.Cofan fun i => J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
      CategoryTheory.CategoryStruct.comp a (c.inj i) = CategoryTheory.CategoryStruct.comp b (c.inj j) →
        (s.inj i).val.app (Opposite.op Y) a = (s.inj j).val.app (Opposite.op Y) b)
  (s : CategoryTheory.Limits.Cofan fun i => J.yoneda.obj (X i))
  (m : (CategoryTheory.Limits.Cofan.mk (J.yoneda.obj c.pt) fun i => J.yoneda.map (c.inj i)).pt ⟶ s.pt),
  (∀ (j : ι),
      CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Limits.Cofan.mk (J.yoneda.obj c.pt) fun i => J.yoneda.map (c.inj i)).inj j) m =
        s.inj j) →
    m =
      {
        val :=
          ⋯.extend
            {
              app := fun Y g =>
                (s.inj (CategoryTheory.Sieve.ofArrows.i ⋯)).val.app Y (CategoryTheory.Sieve.ofArrows.h ⋯),
              naturality := ⋯ } }