∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {I : Type v}
  {ℐ : CategoryTheory.SmallCategory I} {hI : CategoryTheory.IsFiltered I} {F : CategoryTheory.Functor I C}
  {ι : F.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A}
  {isColimit : CategoryTheory.Limits.IsColimit { pt := A, ι := ι }} {I_1 : Type v}
  {ℐ_1 : CategoryTheory.SmallCategory I_1} {hI_1 : CategoryTheory.IsFiltered I_1} {F_1 : CategoryTheory.Functor I_1 C}
  {ι_1 : F_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj A}
  {isColimit_1 : CategoryTheory.Limits.IsColimit { pt := A, ι := ι_1 }},
  { I := I, ℐ := ℐ, hI := hI, F := F, ι := ι, isColimit := isColimit } =
      { I := I_1, ℐ := ℐ_1, hI := hI_1, F := F_1, ι := ι_1, isColimit := isColimit_1 } →
    I = I_1 ∧ ℐ ≍ ℐ_1 ∧ F ≍ F_1 ∧ ι ≍ ι_1 ∧ isColimit ≍ isColimit_1