Functorial version of obj

Stream: Is there code for X?

[Adam Topaz]

I'm sure we have this somewhere... Given an object $j$ in a category $J$, the functor from $J \Rightarrow C$ to $C$ which, on objects, is $F \mapsto F(j)$.

[David Wärn]

docs#category_theory.evaluation ?

[Adam Topaz]

Thanks!

[Adam Topaz]

I was expecting to find it in category_theory.functor_category

[Scott Morrison]

That is a weird home for it. I guess the day I wrote it I needed the uncurried version, so it ended up alongside that. Feel free to move it. :-)