{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
        {motive : I.SymmStruct → Sort u_1} →
          (t : I.SymmStruct) →
            ((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)) →
                      motive
                        { iso := iso, iso_hom_fst := iso_hom_fst, iso_hom_snd := iso_hom_snd,
                          fst_eq_snd := fst_eq_snd }) →
              motive t