Induced map on homs

Stream: Is there code for X?

[Ken Lee]

Say I have (C : Type u) [category.{v} C](c d d1 : C) (f : d1 --> d), I need the induced map (d --> c) -> (d1 --> c) but I can't seem to find it in the library.

[Scott Morrison]

src#category_theory.yoneda

[Ken Lee]

Ah of course it's in the Yoneda file. Thanks!

[Scott Morrison]

As defined Yoneda is a bit clunky to use, as it is functorial in both variables. If you just need what you wrote above, you can of course just write λ g, f ≫ g without needing it to be in the library!