{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.yoneda.comp ((CategoryTheory.Functor.whiskeringLeft C Cᵒᵖᵒᵖ (Type v₁)).obj (CategoryTheory.opOp C)) ≅
      CategoryTheory.coyoneda