The other topic I wanted to cover in this post is Kan extensions, another concept I’ve seen repeatedly yet not really understood. So there’s the Haskell-as-semi-formal-notation approach in Kmett’s posts (starting here) that give lots of examples, but for me to understand something I really need to see it in more traditional mathematical form. Going back to Mac Lane, we see that there are both left and right Kan extensions. We’ll start by describing the right kind.
A right Kan extension for a pair of functors and is a functor and a natural transformation such that is a universal arrow to in the appropriate functor category. What does this actually mean, though? Well, my guess is that this right Kan extension generalizes the concept of extending the map to a map . The interesting thing, to me, is that we’re not requiring that the composition of is just that there’s a consistent way to transform back to . If we squint for a moment and consider sets as categories with only trivial arrows, then it seems like for an arbitrary and any 1-1 function then we’ll have a right Kan extension for it, which will be the function that sends the image of to the image of and maps everything not in the image of to a single point.
There’s also the left Kan extension, which is just the same as the right Kan extension but with the direction of swapped and the universality swapped as well. If the right Kan extension generalizes extending a function to a larger domain through an embedding, then I would guess that the left Kan extension generalizes restriction through an onto function. In this case, the natural transformation would be a “contraction” of sorts that takes the image of and shrinks it to the image of the restriction.
So that’s neat, but what’s the point of Kan extensions in general? Well, I’d always heard the line from Mac Lane “all concepts are Kan extensions” but what exactly does that mean? In section 7 of “Categories…”, he gives a number of examples how other constructions can be described as Kan extensions. For example, a functor has a colimit exactly when there is a left Kan extension for and , here we’re considering as the above and as our . Why does this exactly work? Well, if you consider that a left Kan extension for these functors means that we have a functor which just selects out the object from and a natural transformation from to the functor then we’ve just described the universal cone for which is precisely how we defined the colimit. Similarly, right Kan extensions correspond to limits. We can also use Kan extensions to describe adjoints.
Of course, the problem I have in a sense is what else do you actually use Kan extensions for other than unifying other existing constructions? Now, generalizing is always nice but usually generalizations also expand what you can describe. Here I’m still at a loss for good examples.
I feel slightly guilty that the last two posts I don’t think will have much value for the reader, but they’re at least my attempt to review topics that didn’t sink in on first reading.
Next time I think we’ll finish the simplicial sets paper we’ve been going through and then move onto other things more directly about type theory.