Contravariance of function types
I've been reading through markdominus' archives, and I came across this post from last year. It starts off as a rant about OO terminology, and then ends with the observation that function types are contravariant in their first argument: in other words, if you have some function f:A → B, this induces, not a map from (A → C) to (B → C), but rather a map from (B → C) to (A → C) [you get the map by precomposing everything with f; g maps to g.f.]. He ends with the statement that "I suspect that the use of "covariant" and "contravariant" here suggests some connection with category theory, and with the notions of covariant and contravariant functors, but I don't know what the connection is."
At this point, my compulsive need to teach grandmothers to suck eggs educate everyone around me kicked in, and I sent him an email. It's kicked in again, so I'm posting it here:Hi Mark,
I just came across your post about contravariance of function types: http://blog.plover.com/2006/07/
[Wrong link. Oops.]You may well have had the mystery revealed to you by now, but I couldn't find an update. You're entirely right, there is a connection to category theory. In fact, if you know enough about category theory to know the terms "contravariant" and "covariant", I'm surprised you hadn't seen this example!
Let C be a category. We'll use the notation C(A,B) for the set of arrows in C from A to B, and [C,D] for the category of functors from C to D (which we could write as Cat(C,D), I suppose, but the notation's standard and useful). Then C(-,-) is a functor Cop x C → Set; hence, for any A in C,
We can curry C(-,-), to get a functor Cop → [C,Set], and another functor C → [Cop,Set]. These functors are the two Yoneda embeddings, and they're the subject of the moderately-famous Yoneda Lemma:
[Cop, Set](C(-,A), X) =~ XA naturally in (X ∈ [Cop, Set]) and (A ∈ C),
And, dually,
[C,Set](C(A,-), X) =~ XA naturally in (X ∈ [C, Set] and (A ∈ C).
The first one means that the set of natural transformations from the contravariant functor C(-,A) to some other contravariant functor X is isomorphic to the set XA, and that this isomorphism is canonical in an appropriate sense. The proof's pretty much a straightforward definition-chase.
The Yoneda embeddings also have a more interesting property, which is in some sense dual to the Yoneda Lemma [Edit: actually it's a consequence - I was thinking of something else. D'oh.]. The Yoneda embedding A → C(-,A) is indeed an embedding, in the sense that C(-,A) is isomorphic to C(-,B) iff A is isomorphic to B, and the natural transformations C(-,A) → C(-,B) are in one-to-one correspondence with the functions A→B (they're all given by function composition). Furthermore, every contravariant functor from C to Set is a colimit of functors of the form C(-,A) (so-called "representable" functors). If you haven't come across colimits, then they're an abstraction of most of the common "glue several objects together and possibly quotient bits out" processes one encounters in pure mathematics. And conversely, every possible colimit of objects in C is given by some functor Cop → Set: formally, the Yoneda embedding is left adjoint to the forgetful functor from the category of categories-with-all-colimits to Cat, and one could think of it as the "free cocompletion" functor, analogous to, say, the "free group" functor Set→Grp.
[Analogous results hold for the covariant Yoneda embedding.]
Some of the objects used in algebraic geometry (schemes, IIRC) are formal colimits of objects in CommRingop: hence, you can think of them as functors CommRing→Set. I don't know if anyone does in practice, though :-)
Incidentally, would anyone reading this who thinks category theory is "only a language" care to explain to me how the result that [Cop, Set] is the free cocompletion of C is not a significant, deep, surprising and interesting theorem? Frankly, if it isn't, then those four words have no meaning.
At this point, my compulsive need to teach grandmothers to suck eggs educate everyone around me kicked in, and I sent him an email. It's kicked in again, so I'm posting it here:Hi Mark,
I just came across your post about contravariance of function types: http://blog.plover.com/2006/07/
[Wrong link. Oops.]You may well have had the mystery revealed to you by now, but I couldn't find an update. You're entirely right, there is a connection to category theory. In fact, if you know enough about category theory to know the terms "contravariant" and "covariant", I'm surprised you hadn't seen this example!
Let C be a category. We'll use the notation C(A,B) for the set of arrows in C from A to B, and [C,D] for the category of functors from C to D (which we could write as Cat(C,D), I suppose, but the notation's standard and useful). Then C(-,-) is a functor Cop x C → Set; hence, for any A in C,
- C(A,-) is a covariant functor C → Set;
- C(-,A) is a contravariant functor C → Set, or (equivalently) a functor Cop → Set.
We can curry C(-,-), to get a functor Cop → [C,Set], and another functor C → [Cop,Set]. These functors are the two Yoneda embeddings, and they're the subject of the moderately-famous Yoneda Lemma:
[Cop, Set](C(-,A), X) =~ XA naturally in (X ∈ [Cop, Set]) and (A ∈ C),
And, dually,
[C,Set](C(A,-), X) =~ XA naturally in (X ∈ [C, Set] and (A ∈ C).
The first one means that the set of natural transformations from the contravariant functor C(-,A) to some other contravariant functor X is isomorphic to the set XA, and that this isomorphism is canonical in an appropriate sense. The proof's pretty much a straightforward definition-chase.
The Yoneda embeddings also have a more interesting property, which is in some sense dual to the Yoneda Lemma [Edit: actually it's a consequence - I was thinking of something else. D'oh.]. The Yoneda embedding A → C(-,A) is indeed an embedding, in the sense that C(-,A) is isomorphic to C(-,B) iff A is isomorphic to B, and the natural transformations C(-,A) → C(-,B) are in one-to-one correspondence with the functions A→B (they're all given by function composition). Furthermore, every contravariant functor from C to Set is a colimit of functors of the form C(-,A) (so-called "representable" functors). If you haven't come across colimits, then they're an abstraction of most of the common "glue several objects together and possibly quotient bits out" processes one encounters in pure mathematics. And conversely, every possible colimit of objects in C is given by some functor Cop → Set: formally, the Yoneda embedding is left adjoint to the forgetful functor from the category of categories-with-all-colimits to Cat, and one could think of it as the "free cocompletion" functor, analogous to, say, the "free group" functor Set→Grp.
[Analogous results hold for the covariant Yoneda embedding.]
Some of the objects used in algebraic geometry (schemes, IIRC) are formal colimits of objects in CommRingop: hence, you can think of them as functors CommRing→Set. I don't know if anyone does in practice, though :-)
Incidentally, would anyone reading this who thinks category theory is "only a language" care to explain to me how the result that [Cop, Set] is the free cocompletion of C is not a significant, deep, surprising and interesting theorem? Frankly, if it isn't, then those four words have no meaning.