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
$hom(-,c) : C^{op} \to Set,$where $C^{op}$ is the opposite category to $C$, which sends any object $x \in C^{op}$ to the hom-set $hom(x,c)$.
If you write it like this, should you really call it “contravariant”? When you write $C^{op}$, I thought you should call it just “functor” or “covariant”. By saying it is contravariant AND writing $C^{op}$, 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: $Hom(-,c),Hom(c,-)$ or $Hom(-,-)$. 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 $C^{op}\times C\to Set$ is also a profunctor $C ⇸ C$.
That’s right Eric:
The hom-functor $C^{op} \times C \to Set$ is the identity profunctor $Id : C ⇸ C$ !
Whoa :)
Ok. Changed it to
Relation to profunctors
A hom-functor $C^{op}\times C\to Set$ is also the identity profunctor $1_C: C ⇸ C$.
:)
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 $hom$ 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