∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {inst_1 : CategoryTheory.Category.{t, w} J}
  {X : C} {diag : CategoryTheory.Functor J C} {π : (CategoryTheory.Functor.const J).obj X ⟶ diag}
  {isLimit : CategoryTheory.Limits.IsLimit { pt := X, π := π }} {diag_1 : CategoryTheory.Functor J C}
  {π_1 : (CategoryTheory.Functor.const J).obj X ⟶ diag_1}
  {isLimit_1 : CategoryTheory.Limits.IsLimit { pt := X, π := π_1 }},
  { diag := diag, π := π, isLimit := isLimit } = { diag := diag_1, π := π_1, isLimit := isLimit_1 } →
    diag = diag_1 ∧ π ≍ π_1 ∧ isLimit ≍ isLimit_1