Stream: Is there code for X?
Topic: Functorial version of obj
Adam Topaz (Apr 10 2021 at 20:30):
I'm sure we have this somewhere... Given an object in a category , the functor from to which, on objects, is .
David Wärn (Apr 10 2021 at 20:38):
Adam Topaz (Apr 10 2021 at 20:39):
Adam Topaz (Apr 10 2021 at 20:40):
I was expecting to find it in category_theory.functor_category
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