∀ {X Y Z : Type u_1} (f : X ⟶ Y) (g : Y ⟶ Z),
  { val := CategoryTheory.yoneda.map (CategoryTheory.CategoryStruct.comp f g) } =
    CategoryTheory.CategoryStruct.comp { val := CategoryTheory.yoneda.map f } { val := CategoryTheory.yoneda.map g }