(C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) →
      (x y : CategoryTheory.WithTerminal Cᵒᵖ) →
        (f : x ⟶ y) →
          ((x y : C) →
              (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
                motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y))
                  f) →
            ((unop : C) →
                (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive x y f