∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C}
  (iso : (i j : ι) → I.left (i, j) ≅ I.left (j, i))
  (iso_hom_fst : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.fst (j, i)) = I.snd (i, j))
  (iso_hom_snd : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.snd (j, i)) = I.fst (i, j))
  (fst_eq_snd : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)) (iso_1 : (i j : ι) → I.left (i, j) ≅ I.left (j, i))
  (iso_hom_fst_1 : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso_1 i j).hom (I.fst (j, i)) = I.snd (i, j))
  (iso_hom_snd_1 : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso_1 i j).hom (I.snd (j, i)) = I.fst (i, j))
  (fst_eq_snd_1 : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)),
  ({ iso := iso, iso_hom_fst := iso_hom_fst, iso_hom_snd := iso_hom_snd, fst_eq_snd := fst_eq_snd } =
      { iso := iso_1, iso_hom_fst := iso_hom_fst_1, iso_hom_snd := iso_hom_snd_1, fst_eq_snd := fst_eq_snd_1 }) =
    (iso = iso_1)