{J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan J) C} →
        (left :
            (i : J.L) →
              F.obj (CategoryTheory.Limits.WalkingMultispan.left i) ≅
                G.obj (CategoryTheory.Limits.WalkingMultispan.left i)) →
          (right :
              (i : J.R) →
                F.obj (CategoryTheory.Limits.WalkingMultispan.right i) ≅
                  G.obj (CategoryTheory.Limits.WalkingMultispan.right i)) →
            autoParam
                (∀ (i : J.L),
                  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i))
                      (right (J.fst i)).hom =
                    CategoryTheory.CategoryStruct.comp (left i).hom
                      (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst i)))
                CategoryTheory.Limits.WalkingMultispan.functorExt._auto_1 →
              autoParam
                  (∀ (i : J.L),
                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i))
                        (right (J.snd i)).hom =
                      CategoryTheory.CategoryStruct.comp (left i).hom
                        (G.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd i)))
                  CategoryTheory.Limits.WalkingMultispan.functorExt._auto_3 →
                (F ≅ G)