This is part 15 of Categories for Programmers. Previously: The Yoneda Lemma . See theTable of Contents.
We’ve seen previously that, when we fix an object
a in the category C , the mapping
C(a, _) is a (covariant) functor from C to Set .
x -> C(a, x)
(The codomain is Set because the hom-set C(a, x)is a set .) We call this mapping a hom-functor — we have previously defined its action on morphisms as well.
Now let’s vary
a in this mapping. We get a new mapping that assigns the hom- functor
C(a, _) to any
a -> C(a, _)
It’s a mapping of objects from category C to functors, which are objects in the functor category
Fun(C, Set) (see the section about functor categories in Natural Transformations ). You may also recall that hom-functors are the prototypical representable functors .
Every time we have a mapping of objects between two categories, it’s natural to ask if such a mapping is also a functor. In other words whether we can lift a morphism from one category to a morphism in the other category. A morphism in C is just an element of
C(a, b) , but a morphism in the functor category
Fun(C, Set) is a natural transformation. So we are looking for a mapping of morphisms to natural transformations.
Let’s see if we can find a natural transformation corresponding to a morphism
f :: a->b . First, lets see what
b are mapped to. They are mapped to two functors:
C(a, _) and
C(b, _) . We need a natural transformation between those two functors.
And here’s the trick: we use the Yoneda lemma:
Nat(C(a, _), F) ≅ F a
and replace the generic
F with the hom-functor
C(b, _) . We get:
Nat(C(a, _), C(b, _)) ≅ C(b, a)
This is exactly the natural transformation between the two hom-functors we were looking for, but with a little twist: We have a mapping between a natural transformation and a morphism — an element of
C(b, a) — that goes in the “wrong” direction. But that’s okay; it only means that the functor we are looking at is contravariant.
Actually, we’ve got even more than we bargained for. The mapping from C to
Fun(C, Set) is not only a contravariant functor — it is a fully faithful functor. Fullness and faithfulness are properties of functors that describe how they map hom-sets.
A faithful functor is injective on hom-sets, meaning that it maps distinct morphisms to distinct morphisms. In other words, it doesn’t coalesce them.
A full functor is surjective on hom-sets, meaning that it maps one hom-set onto the other hom-set, fully covering the latter.
A fully faithful functor
F is a bijection on hom-sets — a one to one matching of all elements of both sets. For every pair of objects
b in the source category C there is a bijection between
C(a, b) and
D(F a, F b) , where D is the target category of
F (in our case, the functor category,
Fun(C, Set) ). Notice that this doesn’t mean that
F is a bijection on objects . There may be objects in D that are not in the image of
F , and we can’t say anything about hom-sets for those objects.
The (contravariant) functor we have just described, the functor that maps objects in C to functors in
Fun(C, Set) :
a -> C(a, _)
defines the Yoneda embedding . It embeds a category C (strictly speaking, the category C op , because of contravariance) inside the functor category
Fun(C, Set) . It not only maps objects in C to functors, but also faithfully preserves all connections between them.
This is a very useful result because mathematicians know a lot about the category of functors, especially functors whose codomain is Set . We can get a lot of insight about an arbitrary category C by embedding it in the functor category.
Of course there is a dual version of the Yoneda embedding, sometimes called the co-Yoneda embedding. Observe that we could have started by fixing the target object (rather than the source object) of each hom-set,
C(_, a) . That would give us a contravariant hom-functor. Contravariant functors from C to Set are our familiar presheaves (see, for instance,Limits and Colimits). The co-Yoneda embedding defines the embedding of a category C in the category of presheaves. Its action on morphisms is given by:
Nat(C(_, a), C(_, b)) ≅ C(a, b)
Again, mathematicians know a lot about the category of presheaves, so being able to embed an arbitrary category in it is a big win.
Application to Haskell
In Haskell, the Yoneda embedding can be represented as the isomorphism between natural transformations amongst reader functors on the one hand, and functions (going in the opposite direction) on the other hand:
forall x. (a -> x) -> (b -> x) ≅ b -> a
(Remember, the reader functor is equivalent to
((->) a) .)
The left hand side of this identity is a polymorphic function that, given a function from
x and a value of type
b , can produce a value of type
x (I’m uncurrying — dropping the parentheses around — the function
b -> x ). The only way this can be done for all
x is if our function knows how to convert a
b to an
a . It has to secretly have access to a function
Given such a converter,
btoa , one can define the left hand side, call it
fromY , as:
fromY :: (a -> x) -> b -> x fromY f b = f (btoa b)
Conversely, given a function
fromY we can recover the converter by calling
fromY with the identity:
fromY id :: b -> a
This establishes the bijection between functions of the type
An alternative way of looking at this isomorphism is that it’s a CPS encoding of a function from
a . The argument
a->x is a continuation (the handler). The result is a function from
x which, when called with a value of type
b , will execute the continuation precomposed with the function being encoded.
The Yoneda embedding also explains some of the alternative representations of data structures in Haskell. In particular, it provides a very useful representation of lenses from the
This example was suggested by Robert Harper. It’s the application of the Yoneda embedding to a category defined by a preorder. A preorder is a set with an ordering relation between its elements that’s traditionally written as
<= (less than or equal). The “pre” in preorder is there because we’re only requiring the relation to be transitive and reflexive but not necessarily antisymmetric (so it’s possible to have cycles).
A set with the preorder relation gives rise to a category. The objects are the elements of this set. A morphism from object
b either doesn’t exist, if the objects cannot be compared or if it’s not true that
a <= b ; or it exists if
a <= b , and it points from
b . There is never more than one morphism from one object to another. Therefore any hom-set in such a category is either an empty set or a one-element set. Such a category is called thin .
It’s easy to convince yourself that this construction is indeed a category: The arrows are composable because, if
a <= b and
b <= c then
a <= c ; and the composition is associative. We also have the identity arrows because every element is (less than or) equal to itself (reflexivity of the underlying relation).
We can now apply the co-Yoneda embedding to a preorder category. In particular, we’re interested in its action on morphisms:
Nat(C(_, a), C(_, b)) ≅ C(a, b)
The hom-set on the right hand side is non-empty if and only if
a <= b — in which case it’s a one-element set. Consequently, if
a <= b , there exists a single natural transformation on the left. Otherwise there is no natural transformation.
So what’s a natural transformation between hom-functors in a preorder? It should be a family of functions between sets
C(_, a) and
C(_, b) . In a preorder, each of these sets can either be empty or a singleton. Let’s see what kind of functions are there at our disposal.
There is a function from an empty set to itself (the identity acting on an empty set), a function
absurd from an empty set to a singleton set (it does nothing, since it only needs to be defined for elements of an empty set, of which there are none), and a function from a singleton to itself (the identity acting on a one-element set). The only combination that is forbidden is the mapping from a singleton to an empty set (what would the value of such a function be when acting on the single element?).
So our natural transformation will never connect a singleton hom-set to an empty hom-set. In other words, if
x <= a (singleton hom-set
C(x, a) ) then
C(x, b) cannot be empty. A non-empty
C(x, b) means that
x is less or equal to
b . So the existence of the natural transformation in question requires that, for every
x , if
x <= a then
x <= b .
for all x, x ≤ a ⇒ x ≤ b
On the other hand, co-Yoneda tells us that the existence of this natural transformation is equivalent to
C(a, b) being non-empty, or to
a <= b . Together, we get:
a ≤ b if and only if for all x, x ≤ a ⇒ x ≤ b
We could have arrived at this result directly. The intuition is that, if
a <= b then all elements that are below
a must also be below
b . Conversely, when you substitute
x on the right hand side, it follows that
a <= b . But you must admit that arriving at this result through the Yoneda embedding is much more exciting.
The Yoneda lemma establishes the isomorphism:
Nat(C(a, _), F) ≅ F a
This isomorphism turns out to be natural in both
a . In other words, it’s natural in
(F, a) , a pair taken from the product category
Fun(C, Set) × C . Notice that we are now treating
F as an object in the functor category.
Let’s think for a moment what this means. A natural isomorphism is an invertible natural transformation between two functors. And indeed, the right hand side of our isomorphism is a functor. It’s a functor from
Fun(C, Set) × C to Set . Its action on a pair
(F, a) is a set — the result of evaluating the functor
F at the object
a . This is called the evaluation functor.
The left hand side is also a functor that takes
(F, a) to a set of natural transformations
Nat(C(a, _), F) .
To show that these are really functors, we should also define their action on morphisms. But what’s a morphism between a pair
(F, a) and
(G, b) ? It’s a pair of morphisms,
(Φ, f) ; the first being a morphism between functors — a natural transformation — the second being a regular morphism in C .
The evaluation functor takes this pair
(Φ, f) and maps it to a function between two sets,
F a and
G b . We can easily construct such a function from the component of
a (which maps
F a to
G a ) and the morphism
f lifted by
(G f) ∘ Φa
Notice that, because of naturality of
Φ , this is the same as:
Φb ∘ (F f)
I’m not going to prove the naturality of the whole isomorphism — after you’ve established what the functors are, the proof is pretty mechanical. It follows from the fact that our isomorphism is built up from functors and natural transformations. There is simply no way for it to go wrong.
- Express the co-Yoneda embedding in Haskell.
- Show that the bijection we established between
btoais an isomorphism (the two mappings are the inverse of each other).
- Work out the Yoneda embedding for a monoid. What functor corresponds to the monoid’s single object? What natural transformations correspond to monoid morphisms?
- What is the application of the covariant Yoneda embedding to preorders? (Question suggested by Gershom Bazerman.)
- Yoneda embedding can be used to embed an arbitrary functor category
Fun(C, D)in the functor category
Fun(Fun(C, D), Set). Figure out how it works on morphisms (which, in this case, are natural transformations).
I’d like to thank Gershom Bazerman for checking my math and logic, and André van Meulebrouck, who has been volunteering his editing help throughout this series of posts.