{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₃ Y₃ : C₃} →
                    {f₃ : X₃ ⟶ Y₃} →
                      {motive : G.PullbackObjObj f₁ f₃ → Sort u} →
                        ((pt : C₂) →
                            (fst : pt ⟶ (G.obj (Opposite.op X₁)).obj X₃) →
                              (snd : pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃) →
                                (isPullback :
                                    CategoryTheory.IsPullback fst snd ((G.obj (Opposite.op X₁)).map f₃)
                                      ((G.map f₁.op).app Y₃)) →
                                  motive { pt := pt, fst := fst, snd := snd, isPullback := isPullback }) →
                          (t : G.PullbackObjObj f₁ f₃) → motive t