{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {motive : (a a_1 : CategoryTheory.Bicone J) → CategoryTheory.BiconeHom J a a_1 → Sort u} →
      {a a_1 : CategoryTheory.Bicone J} →
        (t : CategoryTheory.BiconeHom J a a_1) →
          motive CategoryTheory.Bicone.left CategoryTheory.Bicone.left CategoryTheory.BiconeHom.left_id →
            motive CategoryTheory.Bicone.right CategoryTheory.Bicone.right CategoryTheory.BiconeHom.right_id →
              ((j : J) →
                  motive CategoryTheory.Bicone.left (CategoryTheory.Bicone.diagram j)
                    (CategoryTheory.BiconeHom.left j)) →
                ((j : J) →
                    motive CategoryTheory.Bicone.right (CategoryTheory.Bicone.diagram j)
                      (CategoryTheory.BiconeHom.right j)) →
                  ({j k : J} →
                      (f : j ⟶ k) →
                        motive (CategoryTheory.Bicone.diagram j) (CategoryTheory.Bicone.diagram k)
                          (CategoryTheory.BiconeHom.diagram f)) →
                    motive a a_1 t