Zulip Chat Archive

Stream: Is there code for X?

Topic: Functorial version of obj


view this post on Zulip Adam Topaz (Apr 10 2021 at 20:30):

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

view this post on Zulip David Wärn (Apr 10 2021 at 20:38):

docs#category_theory.evaluation ?

view this post on Zulip Adam Topaz (Apr 10 2021 at 20:39):

Thanks!

view this post on Zulip Adam Topaz (Apr 10 2021 at 20:40):

I was expecting to find it in category_theory.functor_category

view this post on Zulip Scott Morrison (Apr 10 2021 at 23:36):

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. :-)


Last updated: May 16 2021 at 05:21 UTC