{ι : Type u_1} →
  (motive : CategoryTheory.Pairwise ι → Sort u_2) →
    (x : CategoryTheory.Pairwise ι) →
      ((i : ι) → motive (CategoryTheory.Pairwise.single i)) →
        ((i j : ι) → motive (CategoryTheory.Pairwise.pair i j)) → motive x