∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithInitial Cᵒᵖ) → (x ⟶ y) → Sort u_3)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithInitial.of (Opposite.op x) ⟶ CategoryTheory.WithInitial.of (Opposite.op y)) →
        motive (CategoryTheory.WithInitial.of (Opposite.op x)) (CategoryTheory.WithInitial.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of (Opposite.op unop)) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of (Opposite.op unop)) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x => h_2 unop x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_3 x