∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} (η : F ⟶ A)
  {X Y Z : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
  (fun u => u.map₂ (CategoryTheory.CategoryStruct.comp f g).unop.left ⋯) =
    CategoryTheory.CategoryStruct.comp (fun u => u.map₂ f.unop.left ⋯) fun u => u.map₂ g.unop.left ⋯