This is part 28 of Categories for Programmers. Previously: Kan Extensions. See the Table of Contents.

A category is *small* if its objects form a set. But we know that there are things larger than sets. Famously, a set of all sets cannot be formed within the standard set theory (the Zermelo-Fraenkel theory, optionally augmented with the Axiom of Choice). So a category of all sets must be large. There are mathematical tricks like Grothendieck universes that can be used to define collections that go beyond sets. These tricks let us talk about large categories.

A category is *locally small* if morphisms between any two objects form a set. If they don’t form a set, we have to rethink a few definitions. In particular, what does it mean to compose morphisms if we can’t even pick them from a set? The solution is to bootstrap ourselves by replacing hom-sets, which are objects in **Set**, with *objects* from some other category *V*. The difference is that, in general, objects don’t have elements, so we are no longer allowed to talk about individual morphisms. We have to define all properties of an *enriched* category in terms of operations that can be performed on hom-objects as a whole. In order to do that, the category that provides hom-objects must have additional structure — it must be a monoidal category. If we call this monoidal category *V*, we can talk about a category *C* enriched over *V*.

Beside size reasons, we might be interested in generalizing hom-sets to something that has more structure than mere sets. For instance, a traditional category doesn’t have the notion of a distance between objects. Two objects are either connected by morphisms or not. All objects that are connected to a given object are its neighbors. Unlike in real life; in a category, a friend of a friend of a friend is as close to me as my bosom buddy. In a suitably enriched category, we can define distances between objects.

There is one more very practical reason to get some experience with enriched categories, and that’s because a very useful online source of categorical knowledge, the nLab, is written mostly in terms of enriched categories.

## Why Monoidal Category?

When constructing an enriched category we have to keep in mind that we should be able to recover the usual definitions when we replace the monoidal category with **Set** and hom-objects with hom-sets. The best way to accomplish this is to start with the usual definitions and keep reformulating them in a point-free manner — that is, without naming elements of sets.

Let’s start with the definition of composition. Normally, it takes a pair of morphisms, one from `C(b, c)`

and one from `C(a, b)`

and maps it to a morphism from `C(a, c)`

. In other words it’s a mapping:

C(b, c) × C(a, b) -> C(a, c)

This is a function between sets — one of them being the cartesian product of two hom-sets. This formula can be easily generalized by replacing cartesian product with something more general. A categorical product would work, but we can go even further and use a completely general tensor product.

Next come the identity morphisms. Instead of picking individual elements from hom-sets, we can define them using functions from the singleton set **1**:

j_{a}::1-> C(a, a)

Again, we could replace the singleton set with the terminal object, but we can go even further by replacing it with the unit `i`

of the tensor product.

As you can see, objects taken from some monoidal category *V* are good candidates for hom-set replacement.

## Monoidal Category

We’ve talked about monoidal categories before, but it’s worth restating the definition. A monoidal category defines a tensor product that is a bifunctor:

⊗ :: V × V -> V

We want the tensor product to be associative, but it’s enough to satisfy associativity up to natural isomorphism. This isomorphism is called the associator. Its components are:

α_{a b c}:: (a ⊗ b) ⊗ c -> a ⊗ (b ⊗ c)

It must be natural in all three arguments.

A monoidal category must also define a special unit object `i`

that serves as the unit of the tensor product; again, up to natural isomorphism. The two isomorphisms are called, respectively, the left and the right unitor, and their components are:

λ_{a}:: i ⊗ a -> a ρ_{a}:: a ⊗ i -> a

The associator and the unitors must satisfy coherence conditions:

A monoidal category is called *symmetric* if there is a natural isomorphism with components:

γ_{a b}:: a ⊗ b -> b ⊗ a

whose “square is one”:

γ_{b a}∘ γ_{a b}= id_{a⊗b}

and which is consistent with the monoidal structure.

An interesting thing about monoidal categories is that you may be able to define the internal hom (the function object) as the right adjoint to the tensor product. You may recall that the standard definition of the function object, or the exponential, was through the right adjoint to the categorical product. A category in which such an object existed for any pair of objects was called cartesian closed. Here is the adjunction that defines the internal hom in a monoidal category:

V(a ⊗ b, c) ~ V(a, [b, c])

Following G. M. Kelly, I’m using the notation `[b, c]`

for the internal hom. The counit of this adjunction is the natural transformation whose components are called evaluation morphisms:

ε_{a b}:: ([a, b] ⊗ a) -> b

Notice that, if the tensor product is not symmetric, we may define another internal hom, denoted by `[[a, c]]`

, using the following adjunction:

V(a ⊗ b, c) ~ V(b, [[a, c]])

A monoidal category in which both are defined is called biclosed. An example of a category that is not biclosed is the category of endofunctors in **Set**, with functor composition serving as tensor product. That’s the category we used to define monads.

## Enriched Category

A category *C* enriched over a monoidal category *V* replaces hom-sets with hom-objects. To every pair of objects `a`

and `b`

in *C* we associate an object `C(a, b)`

in *V*. We use the same notation for hom-objects as we used for hom-sets, with the understanding that they don’t contain morphisms. On the other hand, *V* is a regular (non-enriched) category with hom-sets and morphisms. So we are not entirely rid of sets — we just swept them under the rug.

Since we cannot talk about individual morphisms in *C*, composition of morphisms is replaced by a family of morphisms in *V*:

∘ :: C(b, c) ⊗ C(a, b) -> C(a, c)

Similarly, identity morphisms are replaced by a family of morphisms in *V*:

j_{a}:: i -> C(a, a)

where `i`

is the tensor unit in *V*.

Associativity of composition is defined in terms of the associator in *V*:

Unit laws are likewise expressed in terms of unitors:

## Preorders

A preorder is defined as a thin category, one in which every hom-set is either empty or a singleton. We interpret a non-empty set `C(a, b)`

as the proof that `a`

is less than or equal to `b`

. Such a category can be interpreted as enriched over a very simple monoidal category that contains just two objects, 0 and 1 (sometimes called False and True). Besides the mandatory identity morphisms, this category has a single morphism going from 0 to 1, let’s call it `0->1`

. A simple monoidal structure can be established in it, with the tensor product modeling the simple arithmetic of 0 and 1 (i.e., the only non-zero product is `1⊗1`

). The identity object in this category is 1. This is a strict monoidal category, that is, the associator and the unitors are identity morphisms.

Since in a preorder the-hom set is either empty or a singleton, we can easily replace it with a hom-object from our tiny category. The enriched preorder *C* has a hom-object `C(a, b)`

for any pair of objects `a`

and `b`

. If `a`

is less than or equal to `b`

, this object is 1; otherwise it’s 0.

Let’s have a look at composition. The tensor product of any two objects is 0, unless both of them are 1, in which case it’s 1. If it’s 0, then we have two options for the composition morphism: it could be either `id`

or _{0}`0->1`

. But if it’s 1, then the only option is `id`

. Translating this back to relations, this says that if _{1}`a <= b`

and `b <= c`

then `a <= c`

, which is exactly the transitivity law we need.

What about the identity? It’s a morphism from 1 to `C(a, a)`

. There is only one morphism going from 1, and that’s the identity `id`

, so _{1}`C(a, a)`

must be 1. It means that `a <= a`

, which is the reflexivity law for a preorder. So both transitivity and reflexivity are automatically enforced, if we implement a preorder as an enriched category.

## Metric Spaces

An interesting example is due to William Lawvere. He noticed that metric spaces can be defined using enriched categories. A metric space defines a distance between any two objects. This distance is a non-negative real number. It’s convenient to include inifinity as a possible value. If the distance is infinite, there is no way of getting from the starting object to the target object.

There are some obvious properties that have to be satisfied by distances. One of them is that the distance from an object to itself must be zero. The other is the triangle inequality: the direct distance is no larger than the sum of distances with intermediate stops. We don’t require the distance to be symmetric, which might seem weird at first but, as Lawvere explained, you can imagine that in one direction you’re walking uphill, while in the other you’re going downhill. In any case, symmetry may be imposed later as an additional constraint.

So how can a metric space be cast into a categorical language? We have to construct a category in which hom-objects are distances. Mind you, distances are not morphisms but hom-objects. How can a hom-object be a number? Only if we can construct a monoidal category *V* in which these numbers are objects. Non-negative real numbers (plus infinity) form a total order, so they can be treated as a thin category. A morphism between two such numbers `x`

and `y`

exists if and only if `x >= y`

(note: this is the opposite direction to the one traditionally used in the definition of a preorder). The monoidal structure is given by addition, with zero serving as the unit object. In other words, the tensor product of two numbers is their sum.

A metric space is a category enriched over such monoidal category. A hom-object `C(a, b)`

from object `a`

to `b`

is a non-negative (possibly infinite) number that we will call the distance from `a`

to `b`

. Let’s see what we get for identity and composition in such a category.

By our definitions, a morphism from the tensorial unit, which is the number zero, to a hom-object `C(a, a)`

is the relation:

0 >= C(a, a)

Since `C(a, a)`

is a non-negative number, this condition tells us that the distance from `a`

to `a`

is always zero. Check!

Now let’s talk about composition. We start with the tensor product of two abutting hom-objects, `C(b, c)⊗C(a, b)`

. We have defined the tensor product as the sum of the two distances. Composition is a morphism in *V* from this product to `C(a, c)`

. A morphism in *V* is defined as the greater-or-equal relation. In other words, the sum of distances from `a`

to `b`

and from `b`

to `c`

is greater than or equal to the distance from `a`

to `c`

. But that’s just the standard triangle inequality. Check!

By re-casting the metric space in terms of an enriched category, we get the triangle inequality and the zero self-distance “for free.”

## Enriched Functors

The definition of a functor involves the mapping of morphisms. In the enriched setting, we don’t have the notion of individual morphisms, so we have to deal with hom-objects in bulk. Hom-objects are objects in a monoidal category *V*, and we have morphisms between them at our disposal. It therefore makes sense to define enriched functors between categories when they are enriched over the same monoidal category *V*. We can then use morphisms in *V* to map the hom-objects between two enriched categories.

An *enriched functor* `F`

between two categories *C* and *D*, besides mapping objects to objects, also assigns, to every pair of objects in *C*, a morphism in *V*:

F_{a b}:: C(a, b) -> D(F a, F b)

A functor is a structure-preserving mapping. For regular functors it meant preserving composition and identity. In the enriched setting, the preservation of composition means that the following diagram commute:

The preservation of identity is replaced by the preservation of the morphisms in *V* that “select” the identity:

## Self Enrichment

A closed symmetric monoidal category may be self-enriched by replacing hom-sets with internal homs (see the definition above). To make this work, we have to define the composition law for internal homs. In other words, we have to implement a morphism with the following signature:

[b, c] ⊗ [a, b] -> [a, c]

This is not much different from any other programming task, except that, in category theory, we usually use point free implementations. We start by specifying the set whose element it’s supposed to be. In this case, it’s a member of the hom-set:

V([b, c] ⊗ [a, b], [a, c])

This hom-set is isomorphic to:

V(([b, c] ⊗ [a, b]) ⊗ a, c)

I just used the adjunction that defined the internal hom `[a, c]`

. If we can build a morphism in this new set, the adjunction will point us at the morphism in the original set, which we can then use as composition. We construct this morphism by composing several morphisms that are at our disposal. To begin with, we can use the associator `α`

to reassociate the expression on the left:_{[b, c] [a, b] a}

([b, c] ⊗ [a, b]) ⊗ a -> [b, c] ⊗ ([a, b] ⊗ a)

We can follow it with the co-unit of the adjunction `ε`

:_{a b}

[b, c] ⊗ ([a, b] ⊗ a) -> [b, c] ⊗ b

And use the counit `ε`

again to get to _{b c}`c`

. We have thus constructed a morphism:

ε_{b c}. (id_{[b, c]}⊗ ε_{a b}) . α_{[b, c] [a, b] a}

that is an element of the hom-set:

V(([b, c] ⊗ [a, b]) ⊗ a, c)

The adjunction will give us the composition law we were looking for.

Similarly, the identity:

j_{a}:: i -> [a, a]

is a member of the following hom-set:

V(i, [a, a])

which is isomorphic, through adjunction, to:

V(i ⊗ a, a)

We know that this hom-set contains the left identity `λ`

. We can define _{a}`j`

as its image under the adjunction._{a}

A practical example of self-enrichment is the category **Set** that serves as the prototype for types in programming languages. We’ve seen before that it’s a closed monoidal category with respect to cartesian product. In **Set**, the hom-set between any two sets is itself a set, so it’s an object in **Set**. We know that it’s isomorphic to the exponential set, so the external and the internal homs are equivalent. Now we also know that, through self-enrichment, we can use the exponential set as the hom-object and express composition in terms of cartesian products of exponential objects.

## Relation to 2-Categories

I talked about 2-categories in the context of **Cat**, the category of (small) categories. The morphisms between categories are functors, but there is an additional structure: natural transformations between functors. In a 2-category, the objects are often called zero-cells; morphisms, 1-cells; and morphisms between morphisms, 2-cells. In **Cat** the 0-cells are categories, 1-cells are functors, and 2-cells are natural transformations.

But notice that functors between two categories form a category too; so, in **Cat**, we really have a *hom-category* rather than a hom-set. It turns out that, just like **Set** can be treated as a category enriched over **Set**, **Cat** can be treated as a category enriched over **Cat**. Even more generally, just like every category can be treated as enriched over **Set**, every 2-category can be considered enriched over **Cat**.

Next: Topoi.

May 13, 2017 at 6:35 am

A little tweak: the swap in a symmetric m.c. needs to satisfy a coherence condition: $s_{BA}\circ s_{AB} = 1_{A\otimes B}$. Without that condition what you have is a “braided” m.c. which gives rise to representations of the braid category (and is particularly interesting in terms of anyons and topological QFTs).

May 14, 2017 at 3:25 am

You’re right. I tried to sweep it under the rug of “consistent with monoidal structure,” but braiding is also consistent.

June 1, 2017 at 8:25 am

“If they don’t form a set, we have to rethink a few definitions. In particular, what does it mean to compose morphisms if we can’t even pick them from a set?”

What do you mean by ‘pick them’ in this context? Or, why can’t you pick them from things that are larger than sets?

June 1, 2017 at 9:17 am

A set is pretty much defined as something that has elements. Picking an element means defining an x to be an element of X. But if X is not a set, what does it mean to be an element of X? It all depends on what theory you use to define the entities that are larger than sets (classes, collections?). The beauty of category theory is that it doesn’t force you to commit to a particular foundation.

June 1, 2017 at 11:09 pm

Ok, I see it. So instead of generalising via “picking elements for things greater than sets”, we generalise substituting sets by objects in another category and “redefining” the idea of picking an element.

Thanks !!!

June 8, 2017 at 5:27 pm

Thanks for the series, Bartosz. The first paragraph is a little bumpy. Maybe the following comments help.

Given the setup and examples, you want speak of categories where you first define objects (the sets) in some way and then consider such sets as the type of objects for the category you look at. Now whether a set can be proven to exist depends entirely on the theory you choose to use, a collection of axioms written down in some logic. In Kripke–Platek set theory, you can’t proof that for every set X, the a set PX (“the power set of X”) exists. In ZFC you do can show existence of such sets. In ZFC you can’t show the existence of large cardinals or e.g. Grothendieck universes, but they are consistent with it, and so it’s consistent to add the stronger axioms to the theory, respectively. ZFC can be speaking of those notions of set universes too, if none of its axioms is in constradictions with them. So there are e.g. cardinally speaking bigger and smaller models for ZFC. Demanding existence of larger sets in the axioms means choosing stronger conditions and thus restricting what your theory talks about (just like talking about commutative groups only restricts your theory of groups, but makes more theorems possible). In that case your new theory of sets is one only talking about quite cardinally large objects. Passing from ZFC to a stronger theory where there provable exist sets called Grothendieck universes is not a trick to speak of objects “larger than sets”, it merely empowers you to prove the existence of different (or “more”) “sets” (taking the theory “of sets” to something which is further away from the most naive theory of sets). There are also (so called non-wellfounded) set theories with axioms that e.g. say the set with the property x={x} exists, some infinite loop of inheritance. ZFC actually disproves the existence of the latter fairly directly by one of it’s axioms, but my point here is that this is also an object that you may naively specify, but which is not a set, and not because it’s cardinally too large. Although mostly the sets that you can’t prove in ZFC to exist are really just “too large”, cardinally speaking. I.e. you can’t surjectively map the cardinally speaking smaller into the larger one.

Okay, I hope that wasn’t too long winded. You start “A category is small if its objects form a set” and later you use “large”, which I guess shall mean non-small here (not a priori of larger cardinality, even if that’s what it’s mostly about). You then go on with “But we know that there are things larger than sets.” Well, you may choose to be somewhat dogmatic about ZFC as is and say all the objects I can prove there are sets and when I can embed a model of them into a class of things with extra terms (that are out of reach of provability of ZFC) then those other things aren’t sets. In that case the sentence merely means that there are axioms that let you write down a theory of sets which goes far beyond taking powersets. But then you have just created another stronger theory of “sets”, and in turn the claim there’s something “larger than sets” (in either of the two ways of reading the word) lost it’s footing.

If you take a set theory with big Grothendieck universes and take such a universe as your type of objects, your cateogry is not ZFC-small, but it’s a set in another theory. The class “trick” is just to get an object that you can’t get inside the model, i.e. one that can’t be an element. The topoi abstract common features of set theories and thus end up sharing models with them.

All that being said, I don’t think wanting to be able to speak about extra large categories is a relevant motivator for your type theory centered needs anyway.

Keep up the good work.

July 2, 2017 at 2:19 pm

Przepraszam, ze tu piszę, ale obejrzałem sobie twój filmik na Youtube gdzie mowisz o tkategorii dla programistów.

wydaje mi sie, ze warto bylo by powiedziec, ze strzałki moga być z zewnątrz (ze sceny) oraz zamiast id chyba lepiej mówić o niezmiennikach

July 20, 2017 at 12:11 am

Thank you for your work and the material presented. I translate the chapters of your book into Russian, and now I’m waiting for the next chapter about topoi. I posted the translation of all the chapters to WordPress at “henrychern.wordpress.com“. I dared to make the text coloring, trying to pick out separately mathematical expressions and separately program fragments. Is it interesting to see such a representation? (I can all lead to your text style.)

July 20, 2017 at 2:43 am

@HenryChern: Wow, your translation looks better than the original. Great job!

January 17, 2018 at 4:58 pm

Reading this, I am not clear on these 2 definitions:

Is the association

`C x C -> V :: <a, b> -> C(a, b)`

required to be functorial (i.e. profunctor)?

If so, is the composition

`∘ :: C(b, c) ⊗ C(a, b) -> C(a, c)`

required to be natural?

Thank you for another great post/chapter!

January 18, 2018 at 2:31 am

No, these definitions are not functorial. At this point it’s not even clear what functoriality would mean, since C is not a category. There are no morphisms to be lifted.