{J : CategoryTheory.Limits.MulticospanShape} →
  (motive :
      (b : J.R) →
        (a : J.L) →
          (CategoryTheory.Limits.WalkingMulticospan.left a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b) →
            J.fst b = a → J.snd b = a → Sort u_3) →
    (b : J.R) →
      (a : J.L) →
        (x : CategoryTheory.Limits.WalkingMulticospan.left a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b) →
          (h₁ : J.fst b = a) →
            (h₂ : J.snd b = a) →
              ((a : J.R) →
                  (h₁ : J.fst a = J.fst a) →
                    (h₂ : J.snd a = J.fst a) →
                      motive a (J.fst a) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst a) h₁ h₂) →
                ((a : J.R) →
                    (h₁ : J.fst a = J.snd a) →
                      (h₂ : J.snd a = J.snd a) →
                        motive a (J.snd a) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd a) h₁ h₂) →
                  motive b a x h₁ h₂