{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G :
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
                (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))} →
            (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶
                CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G) →
              (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) → P ⟶ F.op.comp (G.obj P)