∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  {I : Type v₁} {ℐ : CategoryTheory.SmallCategory I} {hI : CategoryTheory.IsFiltered I}
  {F₁ F₂ : CategoryTheory.Functor I C} {ι₁ : F₁.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A}
  {isColimit₁ : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁ }}
  {ι₂ : F₂.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj B}
  {isColimit₂ : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂ }} {φ ψ : F₁ ⟶ F₂}
  {hf : f = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight φ CategoryTheory.yoneda)}
  {hg : g = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight ψ CategoryTheory.yoneda)}
  {I_1 : Type v₁} {ℐ_1 : CategoryTheory.SmallCategory I_1} {hI_1 : CategoryTheory.IsFiltered I_1}
  {F₁_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 }}
  {ι₂_1 : F₂_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj B}
  {isColimit₂_1 : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂_1 }} {φ_1 ψ_1 : F₁_1 ⟶ F₂_1}
  {hf_1 : f = isColimit₁_1.map { pt := B, ι := ι₂_1 } (CategoryTheory.Functor.whiskerRight φ_1 CategoryTheory.yoneda)}
  {hg_1 : g = isColimit₁_1.map { pt := B, ι := ι₂_1 } (CategoryTheory.Functor.whiskerRight ψ_1 CategoryTheory.yoneda)},
  { I := I, ℐ := ℐ, hI := hI, F₁ := F₁, F₂ := F₂, ι₁ := ι₁, isColimit₁ := isColimit₁, ι₂ := ι₂,
        isColimit₂ := isColimit₂, φ := φ, ψ := ψ, hf := hf, hg := hg } =
      { I := I_1, ℐ := ℐ_1, hI := hI_1, F₁ := F₁_1, F₂ := F₂_1, ι₁ := ι₁_1, isColimit₁ := isColimit₁_1, ι₂ := ι₂_1,
        isColimit₂ := isColimit₂_1, φ := φ_1, ψ := ψ_1, hf := hf_1, hg := hg_1 } →
    I = I_1 ∧
      ℐ ≍ ℐ_1 ∧
        F₁ ≍ F₁_1 ∧
          F₂ ≍ F₂_1 ∧ ι₁ ≍ ι₁_1 ∧ isColimit₁ ≍ isColimit₁_1 ∧ ι₂ ≍ ι₂_1 ∧ isColimit₂ ≍ isColimit₂_1 ∧ φ ≍ φ_1 ∧ ψ ≍ ψ_1