David Corfield

Edward Kmett

It is exactly what you find when you look for a left or right adjoint to functor post composition.


(- , e) -| (e -> -)


(- . E) -| Ran E -

Then Ran looks like curried functor composition:

(KE ~> H) ~ (K ~> Ran E H)


Lan E - -| (- . E)

lives on the left.

Away from that realm of rigor, Take F : C -> D, G : C -> E, connected tail to tail, and try to figure out how you’d build something from D -> E. I’d want to go backwards along F_inverse before going along G from C -> E. 2 canonical such candidates are adjoints to F if they exist.

If we pick F = 1, then we find Yoneda in terms of Ran 1, and that inverse to 1 exists on the nose, so nothing is gained or lost by heading along its adjoint, 1 -| 1. Since no information is gained or lost

K ~ Ran 1 K ~ Y K

Similarly, by playing with the terminal functor (!) from C to the 1 object category with 1 arrow, we can define limits/colimits in terms of Ran/Lan along (!).

This starts to give shape to the notion “all concepts (in 1-category theory) are Kan extensions.”

Going back to that ‘head back along the adjoint to F if it exists’ narrative, that’s why, say Codensity ((->) e) ~ Ran ((->) e) ((->) e) ~ State e a: the prod-hom adjunction let’s us exploit the power of the adjoint to ((->) e) to do exactly that idealized story.

And we get lift :: M ~> Codensity M from “currying” join :: MM ~> M using that initial observation about how Ran acts like ‘curried functor composition.’

Created on September 27, 2021 at 07:38:32. See the history of this page for a list of all contributions to it.