Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
On the page hom-functor, it says
There is also a contravariant hom-functor
where is the opposite category to , which sends any object to the hom-set .
If you write it like this, should you really call it “contravariant”? When you write , I thought you should call it just “functor” or “covariant”. By saying it is contravariant AND writing , it seems like double counting.
I hope to add some illustrations to these pages. It is a shame there are not more illustrations on the nLab since nStuff is so amenable to nice pictures.
One could argue that the functor is just called the ”contravariant hom-functor, to distinguish it, as saying ’hom-functor’ could mean one of three things: or . But I don’t really know the rationale.
Thanks for spotting this.
I completely rewrote the page, and expanded it.
Also created a stub for product category.
Nice. Thanks :)
Edit: For a second, I changed functor to profunctor, but realized it wasn’t quite right so changed it back. It would be interesting to relate hom-functor and profunctor somehow though (I just did it wrong).
Edit^2: Added a blurb:
Relation to profunctors
A hom-functor is also a profunctor .
That’s right Eric:
The hom-functor is the identity profunctor !
Whoa :)
Ok. Changed it to
Relation to profunctors
A hom-functor is also the identity profunctor .
:)
Whoa :)
Yeah, speaking of striking category theory. ;-)
I added to hom-functor some remarks on why this is the case. And also to the beginning of profunctor.
A good warm-up excercise if you want to play around with the Yoneda embedding.
Eric, this statement (that is a unit profunctor) is also essentially the key fact of Yoneda reduction (which I really need to get into better shape).
Thanks. The reason I’m reading this page on hom-functor is that I’m working on Yoneda lemma from Vistoli’s paper. His explanation of Yoneda lemma is very nice. As usual, I will not understand until I’ve drawn some pictures so was hoping to add some illustrations to the nLab.
(Just testing to see if I can post here)
Test
Wait, there is nothing specific to homotopy type theory in what you just added. You are essentially just re-stating the usual definition.
It’s great that you are copying material from the HoTT-wiki, but let’s do it a little less mechanically, more with an eye towards retaining logic and cosistency of existing entries.
1 to 13 of 13