forked from BartoszMilewski/DaoFP
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path19-Kan.tex
1114 lines (953 loc) · 46.9 KB
/
19-Kan.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{18}
\chapter{Kan Extensions}
If category theory keeps raising levels of abstraction it's because it's all about discovering patterns. Once patterns are discovered, it's time to study patterns formed by these patterns, and so on.
We've seen the same recurring concepts described more and more tersely at higher and higher levels of abstraction.
For instance, we first defined the product using a universal construction. Then we saw that the spans in the definition of the product were natural transformations. That led to the interpretation of the product as a limit. Then we saw that we could define it using adjunctions. We were able to combine it with the coproduct in one terse formula:
\[ (+) \dashv \Delta \dashv (\times) \]
Lao Tzu said: ``If you want to shrink something, you must first allow it to expand."
Kan extensions raise the level of abstraction even higher. Mac Lane said: ``All concepts are Kan extensions.''
\section{Closed Monoidal Categories}
We've seen how a function object can be defined as the right adjoint to the categorical product:
\[ \cat C (a \times b, c) \cong \cat C (a, [b, c]) \]
Here I used the alternative notation $[b, c]$ for the internal hom---the exponential $c^b$.
An adjunction between two functors can be thought of as one being the pseudo-inverse of the other. They don't compose to identity, but their composition \emph{is} related to the identity functor through unit and counit. For instance, if you squint hard enough, the counit of the currying adjunction:
\[ \varepsilon_{b c} \colon [b, c] \times b \to c \]
suggests that $[b, c]$ embodies, in a sense, the inverse of multiplication. It plays a similar role as $c/b$ in:
\[ c/b \times b = c \]
In a typical categorical manner, we may ask the question: What if we replace the product with something else? The obvious thing, replacing it with a coproduct, doesn't work (thus we have no analog of subtraction). But maybe there are other well-behaved binary operations that have a right adjoint.
A natural setting for generalizing a product is a monoidal category with a tensor product $\otimes$ and a unit object $I$. If we have an adjunction:
\[ \cat C (a \otimes b, c) \cong \cat C (a, [b, c]) \]
we'll call the category \emph{closed monoidal}. In a typical categorical abuse of notation, unless it leads to confusion, we'll use the same symbol (a pair of square brackets) for the monoidal internal hom as we did for the cartesian hom. There is an alternative \index{lollipop}lollipop notation for the right adjoint to the tensor product:
\[ \cat C (a \otimes b, c) \cong \cat C (a, b \multimap c) \]
It is often used in the context of \index{linear types}linear types.
The definition of the internal hom works well for a symmetric monoidal category. If the tensor product is not symmetric, the adjunction defines a \emph{left closed} monoidal category. The left internal hom is adjoint to the ``post-multiplication'' functor $(- \otimes b)$. The right-closed structure is defined as the right adjoint to the ``pre-multiplication'' functor $(b \otimes -)$. If both are defined than the category is called \index{bi-closed monoidal category}\emph{bi-closed}.
\subsection{Internal hom for Day convolution}
As an example, consider the symmetric monoidal structure in the category of co-presheaves with Day convolution:
\[ (F \star G) x = \int^{a, b} \cat C (a \otimes b, x) \times F a \times G b \]
We are looking for the adjunction:
\[ [\cat C, \Set] (F \star G, H) \cong [\cat C, \Set] (F, [G, H]_{\text{Day}}) \]
The natural transformation on the left-hand side can be written as an end over $x$:
\[ \int_x \Set \big( \int^{a, b} \cat C (a \otimes b, x) \times F a \times G b, H x \big) \]
We can use co-continuity to pull out the coends:
\[ \int_{x, a, b} \Set \big( \cat C (a \otimes b, x) \times F a \times G b, H x \big) \]
We can then use the currying adjunction in $\Set$ (the square brackets stand for the internal hom in $\Set$):
\[ \int_{x, a, b} \Set \big( F a, [\cat C (a \otimes b, x) \times G b, H x] \big) \]
Finally, we use the continuity of the hom-set to move the two ends inside the hom-set:
\[ \int_{a} \Set \big( F a, \int_{x, b} [\cat C (a \otimes b, x) \times G b, H x] \big) \]
We discover that the right adjoint to Day convolution is given by:
\[ \big([G, H]_{\text{Day}}\big) a = \int_{x, b} \big[\cat C(a \otimes b, x), [G b, H x]\big] \cong \int_b [G b, H (a \otimes b)]\]
The last transformation is the application of the Yoneda lemma in $\Set$.
\begin{exercise}
Implement the internal hom for Day convolution in Haskell. Hint: Use a type alias.
\end{exercise}
\begin{exercise}
Implement witnesses to the adjunction:
\begin{haskell}
ltor :: (forall a. Day f g a -> h a) -> (forall a. f a -> DayHom g h a)
rtol :: Functor h =>
(forall a. f a -> DayHom g h a) -> (forall a. Day f g a -> h a)
\end{haskell}
\end{exercise}
\subsection{Powering and co-powering}
In the category of sets, the internal hom (the function object, or the exponential) is isomorphic to the external hom (the set of morphisms between two objects):
\[ C^B \cong Set(B, C) \]
We can therefore rewrite the currying adjunction that defines the internal hom in $\Set$ as:
\[ \Set (A \times B, C) \cong \Set \big(A, \Set (B, C)\big) \]
We can generalize this adjunction to the case where $B$ and $C$ are not sets but objects in some category $\cat C$. The external hom in any category is always a set. But the left-hand side is no longer defined by a product. Instead it defines the action of a set $A$ on an object $b$:
\[ \cat C (A \cdot b, c) \cong \Set \big( A, \cat C (b, c)\big) \]
that is called a \emph{co-power}.
You may think of this action as adding together (taking a coproduct of) $A$ copies of $b$. For instance, if $A$ is a two-element set $\mathbf 2$, we get:
\[ \cat C (\mathbf 2 \cdot b, c) \cong \Set \big( \mathbf 2, \cat C (b, c)\big) \cong \cat C(b, c) \times \cat C(b, c) \cong \cat C(b + b, c) \]
In other words,
\[ \mathbf 2 \cdot b \cong b + b \]
In this sense a co-power defines multiplication in terms of iterated addition, the way we learned it in school.
If we multiply $b$ by the hom-set $\cat C (b, c)$ and take the coend over $b$'s, the result is isomorphic to $c$:
\[ \cat \int^b C(b, c) \cdot b \cong c \]
Indeed, the mappings to an arbitrary $x$ from both sides are isomorphic due to the Yoneda lemma:
\[ \cat C \big( \int^b \cat C(b, c) \cdot b, x\big) \cong \int_b \Set \big( \cat C(b, c), \cat C (b, x)\big) \cong \cat C (c, x)\]
As expected, in $\Set$, the co-power decays to the cartesian product.
\[ \Set (A \cdot B, C) \cong \Set \big( A, \Set(B, C)\big) \cong \Set (A \times B, C) \]
Similarly, we can express powering as iterated multiplication. We use the same right-hand side, but this time we use the mapping-in to define the \emph{power}:
\[ \cat C (b, A \pitchfork c) \cong \Set \big(A, \cat C(b, c)\big) \]
You may think of the power as multiplying together $A$ copies of $c$. Indeed, replacing $A$ with $\mathbf 2$ results in:
\[ \cat C (b, \mathbf 2 \pitchfork c) \cong \Set \big(\mathbf 2, \cat C(b, c)\big) \cong \cat C(b, c) \times \cat C(b, c) \cong \cat C (b, c \times c)\]
In other words:
\[ \mathbf 2 \pitchfork c \cong c \times c \]
which is a fancy way of writing $c^2$.
If we power $c$ by the hom-set $\cat C(c', c)$ and take the end over all $c$'s, the result is isomorphic to $c'$:
\[ \int_c \cat C (c', c) \pitchfork c \cong c' \]
This follows from the Yoneda lemma. Indeed the mappings from any $x$ to both sides are isomorphic:
\[ \cat C \big(x, \int_c \cat C (c', c) \pitchfork c\big) \cong \int_c \Set \big( \cat C(c', c), \cat C(x, c)\big) \cong \cat C (x, c') \]
In $\Set$, the power decays to the exponential, which is isomorphic to the hom-set:
\[ A \pitchfork C \cong C^A \cong \Set (A, C) \]
This is the consequence of the symmetry of the product.
\[ \Set(B, A \pitchfork C) \cong \Set (A, \Set(B, C)) \cong \Set (A \times B, C) \]
\[ \cong \Set (B \times A, C) \cong \Set (B, \Set (A, C))\]
\section{Inverting a functor}
One aspect of category theory is to discard information by performing lossy transformations; the other is recovering the lost information. We've seen examples of making up for lost data with free functors---the adjoints to forgetful functors. Kan extensions are another example. Both make up for data that is lost by a functor that is not invertible.
There are two reasons why a functor might not be invertible. One is that it may map multiple objects or arrows into a single object or arrow. In other words, it's not injective on objects or arrows. The other reason is that its image may not cover the whole target category. In other words, it's not surjective on objects or arrows.
Consider for instance an adjunction $L \dashv R$. Suppose that $R$ is not injective, and it collapses two object $c$ and $c'$ into a single object $d$
\begin{align*}
R c &= d \\
R c' &= d
\end{align*}
$L$ has no chance of undoing it. It can't map $d$ to both $c$ and $c'$ at the same time. The best it can do is to map $d$ to a ``more general'' object $L d$ that has arrows to both $c$ and $c'$. These arrows are needed to define the components of the counit of the adjunction:
\begin{align*}
\varepsilon_c &\colon L d \to c
\\
\varepsilon_{c'} &\colon L d \to c'
\end{align*}
where $L d$ is both $L (R c)$ and $L (R c')$
\[
\begin{tikzcd} [row sep=0.5cm, column sep=1cm]
L d
\arrow[d, "\varepsilon_c"]
\arrow[dd, bend right, "\varepsilon_{c'}"']
\\
c
\arrow[rr, red, dashed, ""]
&& d
\arrow[ull, blue, bend right, dashed, "L"']
\\
c'
\arrow[urr, red, bend right, dashed, "R"]
\end{tikzcd}
\]
Moreover, if $R$ is not surjective on objects, the functor $L$ must somehow be defined on those objects of $\cat D$ that are not in the image of $R$. Again, naturality of the unit and counit will constrain possible choices, as long as there are arrows connecting these objects to the image of $R$.
Obviously, all these constraints mean that an adjunction can only be defined in very special cases.
Kan extensions are even weaker than adjunctions.
If adjoint functors work like inverses, Kan extensions work like fractions.
This is best seen if we redraw the diagrams defining the counit and the unit of an adjunction. In the first diagram, $L$ seems to play the role of $1/R$. In the second diagram $R$ pretends to be $1/L$.
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat C
\arrow[rr, "\text{Id}", "" {name=ID, below} ]
\arrow[d, bend right, "R"']
&& \cat C
\\
\cat D
\arrow[urr, bend right, "L"']
\arrow[Rightarrow, "\varepsilon", to=ID]
\end{tikzcd}
\qquad
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat D
\arrow[rr, "\text{Id}", "" {name=ID, below} ]
\arrow[d, bend right, "L"']
&& \cat D
\\
\cat C
\arrow[urr, bend right, "R"']
\arrow[Rightarrow, "\eta", from=ID]
\end{tikzcd}
\]
The right Kan extension $\text{Ran}_P F$ and the left Kan extension $\text{Lan}_P F$ generalize these by replacing the identity functor with some functor $F \colon \cat E \to \cat C$. The Kan extensions then play the role of fractions $F/P$. Conceptually, they undo the action of $P$ and follow it with the action of $F$.
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat E
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "P"']
&& \cat C
\\
\cat B
\arrow[urr, bend right, "\text{Ran}_P F"']
\arrow[Rightarrow, "\varepsilon", to=ID]
\end{tikzcd}
\qquad
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat E
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "P"']
&& \cat C
\\
\cat B
\arrow[urr, bend right, "\text{Lan}_P F"']
\arrow[Rightarrow, "\eta", from=ID]
\end{tikzcd}
\]
Just like with adjunctions, the ``undoing'' is not complete. The composition $\text{Ran}_P F \circ P$ doesn't reproduce $F$; instead it's related to it through the natural transformation $\varepsilon$ called the counit. Similarly, the composition $\text{Lan}_P F \circ P$ is related to $F$ through the unit $\eta$.
Notice that the more information $F$ discards, the easier it is for Kan extensions to ``invert'' the functor $P$. In as sense, it only has to invert $P$ ``modulo $F$''.
Here's the intuition behind Kan extensions. We start with a functor $F$:
\[
\begin{tikzcd} \cat E
\arrow[r, "F"]
& \cat C
\end{tikzcd}
\]
There is a second functor $P$ that squishes $\cat E$ in another category $\cat B$. This may be an embedding that is lossy and non-surjective. Our task is to somehow \emph{extend} the definition of $F$ to cover the whole of $\cat B$.
In the ideal world we would like the following diagram to commute:
\[
\begin{tikzcd} \cat E
\arrow[r, "F"]
\arrow[d, "P"']
& \cat C
\\
\cat B
\arrow[ur, "Kan_P F"']
\end{tikzcd}
\]
But that would involve equality of functors, which is something we try to avoid at all cost.
The next best thing would be to ask for a natural isomorphism between the two paths through this diagram. But even that seems like asking too much. So we finally settle down on demanding that one path be deformable into another, meaning there is a one-way natural transformation between them. The direction of this transformation distinguishes between right and left Kan extensions.
\section{Right Kan extension}
The right Kan extension is a functor $\text{Ran}_P F$ equipped with a natural transformation $\varepsilon$, called the counit of the Kan extension, defined as:
\[ \varepsilon \colon (\text{Ran}_P F) \circ P \to F\]
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat E
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "P"']
&& \cat C
\\
\cat B
\arrow[urr, blue, bend right, "\text{Ran}_P F"']
\arrow[Rightarrow, blue, "\varepsilon", to=ID]
\end{tikzcd}
\]
The pair $(\text{Ran}_P F, \varepsilon)$ is universal among such pairs $(G, \alpha)$, where $G$ is a functor $G \colon \cat B \to \cat C$ and $\alpha$ is a natural transformation:
\[ \alpha \colon G \circ P \to F \]
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat E
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "P"']
&& \cat C
\\
\cat B
\arrow[urr, red, bend right, "G"']
\arrow[Rightarrow, red, "\alpha", to=ID]
\end{tikzcd}
\]
Universality means that for any such $(G, \alpha)$ there is a unique natural transformation $\sigma \colon G \to \text{Ran}_P F$
\[
\begin{tikzcd}[row sep=2cm, column sep=2cm]
\cat E \ar[d, bend right, "P"', "" {name=P}]
\ar[r, "F", "" {name=F, below, near start, bend right}]
&
\cat C
\\
\cat B
\ar[ur, red, bend left, "G", "" {name=G, below}]
\ar[ur, blue, bend right, "\text{Ran}_P F"', "" {name=Ran}]
\arrow[Rightarrow, "\sigma", from=G, to=Ran]
\end{tikzcd}
\]
which factorizes $\alpha$, that is:
\[ \alpha = \varepsilon \cdot (\sigma \circ P) \]
This is a combination of vertical and horizontal compositions of natural transformations in which $\sigma \circ P$ is the whiskering of $\sigma$. Here's the same equation drawn in terms of string diagrams:
\[
\begin{tikzpicture}
\def \dx {0.7}
\def \dy {0.7}
\def \xa{-3 * \dx};
\def \xb{-2 * \dx};
\def \xc{-1 * \dx};
\def \xd{0};
\def \xe{1 * \dx};
\def \ya{0};
\def \yb{1 * \dy};
\def \yc{2 * \dy};
\def \yd{3 * \dy};
\def \ye{4 * \dy};
% left background
\filldraw[fill=blue!50!green!20, draw=white] (\xa, \ye) rectangle (\xc, \ya);
% right background
\filldraw[fill=orange!30, draw=white] (\xc, \ye) rectangle (\xe, \ya);
% fill shape\yb
\path [fill=orange!10, draw=white] (\xb, \ya) to (\xb, \yb) to [out=90, in=180] (\xc, \yc) to [out=0, in=90] (\xd, \yb) to (\xd, \ya);
% cup
\draw (\xb, \ya) to (\xb, \yb) to [out=90, in=180] (\xc, \yc) to [out=0, in=90] (\xd, \yb) to (\xd, \ya);
\draw (\xc, \yc) -- (\xc, \ye);
% natural transformations
\filldraw[black] (\xc, \yc) circle (1 pt);
\node [below] at (\xc, \yc) {$\alpha$};
% categories
\node[right] at (\xa, \ye - 0.3) {$\cat E$};
\node[left] at (\xe, \ye - 0.3) {$\cat C$};
\node[above] at (\xc, \ya) {$\cat B$};
% functors
\node [below] at (\xb, \ya) {$P$};
\node [below] at (\xd, \ya) {$G$};
\node [above] at (\xc, \ye) {$F$};
%-----------------
\node (eq) at (3 * \dx, \yc) {$=$};
% right diagram
\def \xa{5 * \dx};
\def \xb{6 * \dx};
\def \xc{7 * \dx};
\def \xd{8 * \dx};
\def \xe{9 * \dx + 0.3};
% left background
\filldraw[fill=blue!50!green!20, draw=white] (\xa, \ye) rectangle (\xc, \ya);
% right background
\filldraw[fill=orange!30, draw=white] (\xc, \ye) rectangle (\xe, \ya);
% fill shape
\path [fill=orange!10, draw=white] (\xb, \ya) to (\xb, \yc) to [out=90, in=180] (\xc, \yd) to [out=0, in=90] (\xd, \yc) to (\xd, \ya);
% cup
\draw (\xb, \ya) to (\xb, \yc) to [out=90, in=180] (\xc, \yd) to [out=0, in=90] (\xd, \yc) to (\xd, \ya);
\draw (\xc, \yd) -- (\xc, \ye);
% natural transformations
\filldraw[black] (\xc, \yd) circle (1 pt);
\node [below] at (\xc, \yd) {$\varepsilon$};
\filldraw[black] (\xd, \yb) circle (1 pt);
\node [right] at (\xd, \yb) {$\sigma$};
% categories
\node[right] at (\xa, \ye - 0.3) {$\cat E$};
\node[left] at (\xe, \ye - 0.3) {$\cat C$};
\node[above] at (\xc, \ya) {$\cat B$};
% functors
\node [below] at (\xb, \ya) {$P$};
\node [below] at (\xd, \ya) {$G$};
\node [above] at (\xc, \ye) {$F$};
\node [right] at (\xd, \yc) {$\text{Ran}$};
\end{tikzpicture}
\]
If the right Kan extension along $P$ is defined for every functor $F$, then the universal construction can be generalized to an adjunction---this time it's an adjunction between two functor categories:
\[ [\cat E, \cat C](G \circ P, F) \cong [\cat B, \cat C](G, \text{Ran}_P F) \]
For every $\alpha$ that is an element of the left-hand side, there is a unique $\sigma$ that is an element of the right-hand side.
In other words, the right Kan extension, if it exists for every $F$, is the right adjoint to functor pre-composition:
\[ (- \circ P) \dashv \text{Ran}_P \]
The component of the counit of this adjunction at $F$ is $\varepsilon$.
This is somewhat reminiscent of the currying adjunction:
\[ \cat E (a \times b, c) \cong \cat E (a, [b, c]) \]
in which the product is replaced by functor composition. (The analogy is not perfect, since composition can be considered a tensor product only in the category of endofunctors.)
\subsection{Right Kan extension as an end}
Recall the ninja Yoneda lemma:
\[ F b \cong \int_{e} \mathbf{Set} (\cat B(b, e), F e) \]
Here, $F$ is a co-presheaf, that is a functor from $\cat B$ to $\Set$. The right Kan extensions of $F$ along $P$ generalizes this formula:
\[ (\text{Ran}_P F) b \cong \int_e \Set \big( \cat B (b, P e), F e\big) \]
This works for a co-presheaf. In general we are interested in $F \colon \cat E \to \cat C$, so we need to replace the hom-set in $\Set$ by a \index{power}power. Thus he right Kan extension is given by the following end (if it exists):
\[ (\text{Ran}_P F) b \cong \int_e \cat B (b, P e) \pitchfork F e \]
The proof essentially writes itself: at every step there is only one thing to do. We start with the adjunction:
\[ [\cat E, \cat C](G \circ P, F) \cong [\cat B, \cat C](G, \text{Ran}_P F) \]
and rewrite it using ends:
\[ \int_e \cat C \big(G ( P e), F e\big) \cong \int_b \cat C\big(G b, (\text{Ran}_P F) b\big) \]
We plug in our formula to get:
\[ \cong \int_b \cat C\big(G b,\int_e \cat B (b, P e) \pitchfork F e \big)\]
We use the continuity of the hom-functor to pull the end to the front:
\[ \cong \int_b \int_e \cat C\big(G b, \cat B (b, P e) \pitchfork F e \big) \]
Then we use the definition of power:
\[ \int_b \int_e \Set \big( \cat B (b, P e), \cat C (G b, F e) \big) \]
and apply the Yoneda lemma:
\[ \int_e \cat C \big(G (P e), F e\big) \]
This result is indeed the left-hand side of the adjunction.
If $F$ is a co-presheaf, the power in the formula for the right Kan extension decays to the exponential/hom-set:
\[ (\text{Ran}_P F) b \cong \int_e \Set \big( \cat B (b, P e), F e\big) \]
Notice also that, if $P$ has a left adjoint, let's call it $P^{-1}$, that is:
\[ \cat B(b, P e) \cong \cat E(P^{-1} b, e) \]
we could use the ninja Yoneda lemma to evaluate the end in:
\[ (\text{Ran}_P F) b \cong \int_e \Set \big( \cat B (b, P e), F e\big) \cong \int_e \Set(\cat E(P^{-1} b, e), F e) \cong F(P^{-1} b)\]
to get:
\[ \text{Ran}_P F \cong F \circ P^{-1} \]
Since the adjunction is a weakening of the idea of an inverse, this result is in agreement with the intuition that the Kan extension ``inverts'' $P$ and follows it with $F$.
\subsection{Right Kan extension in Haskell}
The end formula for the right Kan extension can be immediately translated to Haskell:
\begin{haskell}
newtype Ran p f b = Ran (forall e. (b -> p e) -> f e)
\end{haskell}
The counit $\varepsilon$ of the right Kan extension is a natural transformation from the composition of \hask{(Ran p f)} after \hask{p} to \hask{f}:
\begin{haskell}
counit :: forall p f e'. Ran p f (p e') -> f e'
\end{haskell}
To implement it, we have to produce the value of the type \hask{(f c')} given a polymorphic function
\begin{haskell}
h :: forall e. (p e' -> p e) -> f e
\end{haskell}
We do it by instantiating this function at the type \hask{e = e'} and calling it with the identity on \hask{(p e')}:
\begin{haskell}
counit (Ran h) = h id
\end{haskell}
The computational power of the right Kan extension comes from its universal property. We start with a functor $G$ equipped with a natural transformation:
\[ \alpha \colon G \circ P \to F \]
This can be expressed as a Haskell data type:
\begin{haskell}
type Alpha p f g = forall e. g (p e) -> f e
\end{haskell}
Universality tells us that there is a unique natural transformation $\sigma$ from this functor to the corresponding right Kan extension:
\begin{haskell}
sigma :: Functor g => Alpha p f g -> forall b. (g b -> Ran p f b)
sigma alpha gb = Ran (\b_pe -> alpha $ fmap b_pe gb)
\end{haskell}
that factorizes $\alpha$ through the counit $\varepsilon$:
\[ \alpha = \varepsilon \cdot (\sigma \circ P) \]
Recall that whiskering means that we instantiate \hask{sigma} at \hask{b = p c}. It is then followed by \hask{counit}. The factorization of $\alpha$ is thus given by:
\begin{haskell}
factorize' :: Functor g => Alpha p f g -> forall e. g (p e) -> f e
factorize' alpha gpc = alpha gpc
\end{haskell}
The components of the three natural transformations are all morphism in the target category $\cat C$:
\[
\begin{tikzpicture}
\def\Xa{0};
\def\Xm{1.3}
\def\Xb{2.25};
\def\Xc{3};
\def\Yc{2.5};
\def\Yb{1.75};
\def\Ya{0};
\node at ( \Xa, \Yc) { $\cat E$ };
\node at ( \Xa, \Ya) { $\cat B$ };
\node (1) at (\Xb, \Yc) {};
\node (2) at (\Xb, \Yb - 0.25) {};
\node (3) at (\Xb + 1, \Yb - 0.25) {};
\draw (\Xc - 0.3, \Yc - 0.6)[fill=blue!50!green!20] ellipse (1 and 1);
% F
\node at ( \Xm-0.25, \Yc + 0.25) { $F$ };
\draw[->, dashed](\Xa + 0.25, \Yc) -- (1);
% P
\node at (\Xa - 0.25, \Yb - 0.25) { $P$ };
\draw[->, dashed](\Xa, \Yc - 0.25) -- (\Xa, \Ya + 0.25);
% Ran
\node at (\Xm - 0.5, \Yb - 0.5) { $\text{Ran}$ };
\draw[->, dashed](\Xa + 0.25, \Ya + 0.25) -- (2);
% G
\node at (\Xb - 0.2, \Ya) { $\text{G}$ };
\draw[->, dashed](\Xa + 0.25, \Ya + 0.25) to [out=-1, in=-90] (3);
\draw[->] (2) -- (1) node[midway, left] {$\varepsilon$};
\draw[->] (3) -- (2) node[midway, below] {$\sigma \circ P$};
\draw[->] (3) to [out=90, in=0] (1);
\node at (\Xb + 1, \Yb + 0.5) {$\alpha$};
\end{tikzpicture}
\]
\begin{exercise}
Implement the \hask{Functor} instance for \hask{Ran}.
\end{exercise}
\subsection{Limits as Kan extensions}
We have previously defined limits as universal cones. The definition of a cone involves two categories: the indexing category $\cat J$ that defines the shape of the diagram, and the target category $\cat C$. A diagram is a functor $D \colon \cat J \to \cat C$ that embeds the shape in the target category.
We can introduce a third category $\mathbf 1$: the terminal category that contains a single object and a single identity arrow. We can then use a functor $X$ from that category to pick the apex $x$ of the cone in $\cat E$. Since $\mathbf 1$ is terminal in $\mathbf{Cat}$, we also have the unique functor from $\cat J$ to it, which we'll call $!$. It maps all objects to the only object of $\mathbf 1$, and all arrows to its identity arrow.
It turns out that the limit of $D$ is the right Kan extension of the diagram $D$ along $!$. First, let's observe that the composition $X \circ !$ maps the shape $\cat J$ to a single object $x$, so it does the job of the constant functor $\Delta_x$. It thus picks the apex of a cone. A cone with the apex $x$ is a natural transformation $\gamma$:
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat J
\arrow[rr, "D", "" {name=ID, below} ]
\arrow[d, bend right, "!"']
&& \cat C
\\
\mathbf 1
\arrow[urr, bend right, "X"']
\arrow[Rightarrow, "\gamma", to=ID]
\end{tikzcd}
\]
The following diagrams illustrate this. On the left we have two categories: $\mathbf 1$ with a single object $*$, and $\cat J$ with three objects forming the shape for the diagram. On the right we have the image of $D$ and the image of $X \circ !$, which is the apex $x$. The three components of $\gamma$ connect the apex $x$ to the diagram. Naturality of $\gamma$ ensures that the triangles that form the sides of the cone commute.
\[
\begin{tikzcd}
& *
\\
\\
1
\arrow[rr, red]
\arrow[rd, red]
&& 2
\arrow[dl, red]
\\
& 3
\end{tikzcd}
\qquad
\begin{tikzcd}
& x
\arrow[ddr, "\gamma_2"]
\arrow[ddl, "\gamma_1"']
\arrow[ddd, "\gamma_3"]
\\
\\
D 1
\arrow[rr, red]
\arrow[rd, red]
&& D 2
\arrow[dl, red]
\\
& D 3
\end{tikzcd}
\]
The right Kan extension $(\text{Ran}_! D, \varepsilon)$ is the universal such cone. $\text{Ran}_! D$ is a functor from $\mathbf 1$ to $\cat C$, so it selects an object in $\cat C$. This is indeed the apex, $\text{Lim} D$, of the universal cone.
Universality means that for any pair $(X, \gamma)$ there is a natural transformation $\sigma \colon X \to \text{Ran}_! D$
\[
\begin{tikzcd}[row sep=2cm, column sep=2cm]
\cat J \ar[d, "!"', "" {name=P}]
\ar[r, "D", "" {name=F, below, near start, bend right}]
&
\cat C
\\
\mathbf 1
\ar[ur, bend left, "X", "" {name=G, below}]
\ar[ur, bend right, "\text{Ran}_! D"', "" {name=Ran}]
\arrow[Rightarrow, "\sigma", from=G, to=Ran]
\end{tikzcd}
\]
which factorizes $\gamma$.
The transformation $\sigma$ has only one component $\sigma_*$, which is an arrow $h$ connecting the apex $x$ to the apex $\text{Lim} D$. The factorization:
\[ \gamma = \varepsilon \cdot (\sigma \circ !) \]
reads, in components:
\[ \gamma_i = \varepsilon_i \circ h \]
It makes the triangles in the following diagram commute:
\[
\begin{tikzcd}[row sep=1cm]
& x
\arrow[dddl, "\gamma_1"']
\arrow[ddddr, "\gamma_3"]
\arrow[dddrr, "\gamma_2"]
\arrow[dd, dashed, "h"']
\\
\\
& \text{Lim} D
\arrow[dl, blue, "\varepsilon_1"]
\arrow[ddr, blue, "\varepsilon_3"']
\arrow[drr, blue, "\varepsilon_2"]
\\
D 1
\arrow[rrr, red]
\arrow[rrd, red]
&&& D 2
\arrow[dl, red]
\\
&& D 3
\end{tikzcd}
\]
This universal condition makes $\text{Lim} D$ the limit of the diagram $D$.
\subsection{Left adjoint as a right Kan extension}
We started by describing Kan extensions as a generalization of adjunctions. Looking at the pictures, if we have a pair of adjoint functors $L \dashv R$, we expect the left functor to be the right Kan extension of the identity along the right functor.
\[ L \cong \text{Ran}_R \text{Id} \]
Indeed, the counit of the Kan extension is the same as the counit of the adjunction:
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat C
\arrow[rr, "\text{Id}", "" {name=ID, below} ]
\arrow[d, bend right, "R"']
&& \cat C
\\
\cat D
\arrow[urr, bend right, "L"']
\arrow[Rightarrow, "\varepsilon", to=ID]
\end{tikzcd}
\]
We also have to show universality:
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat C
\arrow[rr, "\text{\text{Id}}", "" {name=ID, below} ]
\arrow[d, bend right, "R"']
&& \cat C
\\
\cat D
\arrow[urr, bend right, "G"']
\arrow[Rightarrow, "\alpha", to=ID]
\end{tikzcd}
\qquad %----%
\begin{tikzcd}[row sep=2cm, column sep=2cm]
\cat C \ar[d, "R"', "" {name=P}]
\ar[r, "R", "" {name=F, below, near start, bend right}]
&
\cat D
\\
\cat D
\ar[ur, bend left, "G", "" {name=G, below}]
\ar[ur, bend right, "L"', "" {name=Ran}]
\arrow[Rightarrow, "\sigma", from=G, to=Ran]
\end{tikzcd}
\]
To do that, we have at our disposal the unit of the adjunction:
\[ \eta \colon \text{Id} \to R \circ L \]
We construct $\sigma$ as the composite:
\[ G \rightarrow G \circ \text{Id} \xrightarrow{G \circ \eta} G \circ R \circ L \xrightarrow{\alpha \circ L} \text{Id} \circ L \rightarrow L\]
In other words, we define $\sigma$ as:
\[ \sigma = (\alpha \circ L) \cdot (G \circ \eta) \]
We could ask the converse question: if $\text{Ran}_R \text{Id}$ exists, is it automatically the left adjoint to $R$? It turns out that we need one more condition for that: The Kan extension must be preserved by $R$, that is:
\[ R \circ \text{Ran}_R \text{Id} \cong \text{Ran}_R R \]
We'll see in the next section that the right-hand side of this condition defines the codensity monad.
\begin{exercise}
Show the factorization condition:
\[ \alpha = \varepsilon \cdot (\sigma \circ R) \]
for the $\sigma$ that was defined above. Hint: draw the corresponding string diagrams and use the triangle identity for the adjunction.
\end{exercise}
\subsection{Codensity monad}
We've seen that every adjunction $L \dashv F$ produces a monad $F \circ L$. It turns out that this monad is the right Kan extension of $F$ along $F$. Interestingly, even if $F$ doesn't have a left adjoint, the Kan extension $\text{Ran}_F F$ is still a monad called the \emph{codensity monad} denoted by $T^F$:
\[ T^F = \text{Ran}_F F \]
If we were serious about the interpretation of Kan extensions as fractions, a codensity monad would correspond to $F/F$. A functor for which this ``fraction'' is equal to identity is called codense.
To see that $T^F$ is a monad, we have to define monadic unit and multiplication:
\[ \eta \colon \text{Id} \to T^F \]
\[ \mu \colon T^F \circ T^F \to T^F \]
Both follow from universality. For every $(G, \alpha)$ we have a $\sigma$:
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat D
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "F"']
&& \cat C
\\
\cat C
\arrow[urr, bend right, "G"']
\arrow[Rightarrow, "\alpha", to=ID]
\end{tikzcd}
\qquad
\begin{tikzcd}[row sep=2cm, column sep=2cm]
\cat D \ar[d, "F"', "" {name=P}]
\ar[r, "F", "" {name=F, below, near start, bend right}]
&
\cat C
\\
\cat C
\ar[ur, bend left, "G", "" {name=G, below}]
\ar[ur, bend right, "T^F = \text{Ran}_F F"', "" {name=Ran}]
\arrow[Rightarrow, "\sigma", from=G, to=Ran]
\end{tikzcd}
\]
To get the unit, we replace $G$ with the identity functor $\text{Id}$ and $\alpha$ with the identity natural transformation.
To get multiplication, we replace $G$ with $T^F \circ T^F$ and note that we have at our disposal the counit of the Kan extension:
\[ \varepsilon \colon T^F \circ F \to F \]
We can chose $\alpha$ of the type:
\[ \alpha \colon T^F \circ T^F \circ F \to F \]
to be the composite:
\[ T^F \circ T^F \circ F \xrightarrow{id \circ \varepsilon} T^F \circ F \xrightarrow{\varepsilon} F\]
or, using the whiskering notation:
\[ \alpha = \varepsilon \cdot (T^F \circ \varepsilon) \]
The corresponding $\sigma$ gives us the monadic multiplication.
Let's now show that, if we start from an adjunction:
\[ \cat D(L c, d) \cong \cat C (c, F d) \]
the codensity monad is given by $F \circ L$. Let's start with the mapping from an arbitrary functor $G$ to $F \circ L$:
\[ [\cat C, \cat C](G, F \circ L) \cong \int_c \cat C (G c, F (L c)) \]
We can rewrite it using the Yoneda lemma:
\[ \cong \int_c \int_d \Set\big(\cat D(L c, d), \cat C (G c, F d)\big) \]
Here, taking the end over $d$ has the effect of replacing $d$ with $L c$. We can now use the adjunction:
\[ \cong \int_c \int_d \Set\big(\cat C(c, F d), \cat C (G c, F d)\big) \]
and perform the ninja-Yoneda integration over $c$ to get:
\[ \cong \int_d \cat C (G (F d), F d) \]
This, in turn, defines a set of natural transformations:
\[ \cong [\cat D, \cat C](G \circ F, F) \]
The pre-composition by $F$ is the left adjoint to the right Kan extension:
\[ [\cat D, \cat C](G \circ F, F) \cong [\cat C, \cat C] (G, \text{Ran}_F F)\]
Since $G$ was arbitrary, we conclude that $F \circ L$ is indeed the codensity monad $\text{Ran}_F F$.
Since every monad can be derived from some adjunction, it follows that \emph{every monad is a codensity monad} for some adjunction.
\subsection{Codensity monad in Haskell}
Translating the codensity monad to Haskell, we get:
\begin{haskell}
newtype Codensity f c = C (forall d. (c -> f d) -> f d)
\end{haskell}
together with the extractor:
\begin{haskell}
runCodensity :: Codensity f c -> forall d. (c -> f d) -> f d
runCodensity (C h) = h
\end{haskell}
This looks very similar to a continuation monad. In fact it turns into continuation monad if we choose \hask{f} to be the identity functor. We can think of \hask{Codensity} as taking a callback \hask{(c -> f d)} and calling it when the result of type \hask{c} becomes available.
Here's the monad instance:
\begin{haskell}
instance Monad (Codensity f) where
return x = C (\k -> k x)
m >>= kl = C (\k -> runCodensity m (\a -> runCodensity (kl a) k))
\end{haskell}
Again, this is almost exactly like the continuation monad:
\begin{haskell}
instance Monad (Cont r) where
return x = Cont (\k -> k x)
m >>= kl = Cont (\k -> runCont m (\a -> runCont (kl a) k))
\end{haskell}
This is why \hask{Codensity} has the performance advantages of the continuation passing style. Since it nests continuations ``inside out,'' it can be used to optimize long chains of binds that are produced by \hask{do} blocks.
This property is especially important when working with free monads, which accumulate binds in tree-like structures. When we finally interpret a free monad, these accumulated binds require traversing the ever-growing tree. For every bind, the traversal starts at the root. Compare this with the earlier example of reversing a list, which was optimized by accumulating functions in a FIFO queue. The codensity monad offers the same kind of performance improvement.
\begin{exercise}
Implement the \hask{Functor} instance for \hask{Codensity}.
\end{exercise}
\begin{exercise}
Implement the \hask{Applicative} instance for \hask{Codensity}.
\end{exercise}
\section{Left Kan extension}
Just like the right Kan extension was defined as a \emph{right} adjoint to functor pre-compositon, the left Kan extension is defined as the \emph{left} adjoint to functor pre-composition:
\[ [\cat B, \cat C](\text{Lan}_P F , G) \cong [\cat E, \cat C] (F, G \circ P) \]
(There are also adjoints to \emph{post}-composition: they are called Kan lifts.)
Alternatively, $\text{Lan}_P F$ can be defined as a functor equipped with a natural transformation called the unit:
\[ \eta \colon F \to \text{Lan}_P F \circ P \]
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat E
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "P"']
&& \cat C
\\
\cat B
\arrow[urr, blue, bend right, "\text{Lan}_P F"']
\arrow[Rightarrow, blue, "\eta", from=ID]
\end{tikzcd}
\]
Notice that the direction of the unit of the left Kan extension is opposite of that of the counit of the right Kan extension.
The pair $(\text{Lan}_P F, \eta)$ is universal, meaning that, for any other pair $(G, \alpha)$, where
\[ \alpha \colon F \to G \circ P\]
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat E
\arrow[rr, "F", "" {name=ID, below} ]
\arrow[d, bend right, "P"']
&& \cat C
\\
\cat B
\arrow[urr, red, bend right, "G"']
\arrow[Rightarrow, red, "\alpha", from=ID]
\end{tikzcd}
\]
there is a unique mapping $\sigma \colon \text{Lan}_P F \to G$
\[
\begin{tikzcd}[row sep=2cm, column sep=2cm]
\cat E \ar[d, "P"', "" {name=P}]
\ar[r, "F", "" {name=F, below, near start, bend right}]
&
\cat C
\\
\cat B
\ar[ur, red, bend left, "G", "" {name=G, below}]
\ar[ur, blue, bend right, "\text{Lan}_P F"', "" {name=Lan}]
\arrow[Rightarrow, "\sigma", from=Lan, to=G]
\end{tikzcd}
\]
that factorizes $\alpha$:
\[ \alpha = (\sigma \circ P) \cdot \eta \]
Again, the direction of $\sigma$ is reversed with respect to the right Kan extension.
Using string diagrams, we can picture the universal condition as:
\[
\begin{tikzpicture}
\def \dx {0.7}
\def \dy {-0.7}
\def \xa{-3 * \dx};
\def \xb{-2 * \dx};
\def \xc{-1 * \dx};
\def \xd{0};
\def \xe{1 * \dx};
\def \ya{0};
\def \yb{1 * \dy};
\def \yc{2 * \dy};
\def \yd{3 * \dy};
\def \ye{4 * \dy};
% left background
\filldraw[fill=blue!50!green!20, draw=white] (\xa, \ye) rectangle (\xc, \ya);
% right background
\filldraw[fill=orange!30, draw=white] (\xc, \ye) rectangle (\xe, \ya);
% fill shape\yb
\path [fill=orange!10, draw=white] (\xb, \ya) to (\xb, \yb) to [out=270, in=180] (\xc, \yc) to [out=0, in=270] (\xd, \yb) to (\xd, \ya);
% cup
\draw (\xb, \ya) to (\xb, \yb) to [out=270, in=180] (\xc, \yc) to [out=0, in=270] (\xd, \yb) to (\xd, \ya);
\draw (\xc, \yc) -- (\xc, \ye);
% natural transformations
\filldraw[black] (\xc, \yc) circle (1 pt);
\node [above] at (\xc, \yc) {$\alpha$};
% categories
\node[right] at (\xa, \ye + 0.3) {$\cat E$};
\node[left] at (\xe, \ye + 0.3) {$\cat C$};
\node[above] at (\xc, \ya - 0.6) {$\cat B$};
% functors
\node [above] at (\xb, \ya) {$P$};
\node [above] at (\xd, \ya) {$G$};
\node [below] at (\xc, \ye) {$F$};
%-----------------
\node (eq) at (3 * \dx, \yc) {$=$};
% right diagram
\def \xa{5 * \dx};
\def \xb{6 * \dx};
\def \xc{7 * \dx};
\def \xd{8 * \dx};
\def \xe{9 * \dx + 0.3};
% left background
\filldraw[fill=blue!50!green!20, draw=white] (\xa, \ye) rectangle (\xc, \ya);
% right background
\filldraw[fill=orange!30, draw=white] (\xc, \ye) rectangle (\xe, \ya);
% fill shape
\path [fill=orange!10, draw=white] (\xb, \ya) to (\xb, \yc) to [out=270, in=180] (\xc, \yd) to [out=0, in=270] (\xd, \yc) to (\xd, \ya);
% cup
\draw (\xb, \ya) to (\xb, \yc) to [out=270, in=180] (\xc, \yd) to [out=0, in=270] (\xd, \yc) to (\xd, \ya);
\draw (\xc, \yd) -- (\xc, \ye);
% natural transformations
\filldraw[black] (\xc, \yd) circle (1 pt);
\node [above] at (\xc, \yd) {$\eta$};
\filldraw[black] (\xd, \yb) circle (1 pt);
\node [right] at (\xd, \yb) {$\sigma$};
% categories
\node[right] at (\xa, \ye + 0.3) {$\cat E$};
\node[left] at (\xe, \ye + 0.3) {$\cat C$};
\node[above] at (\xc, \ya - 0.6) {$\cat B$};
% functors
\node [above] at (\xb, \ya) {$P$};
\node [above] at (\xd, \ya) {$G$};
\node [below] at (\xc, \ye) {$F$};
\node [right] at (\xd, \yc) {$\text{Lan}$};
\end{tikzpicture}
\]
This establishes the one-to-one mapping between two sets of natural transformations. For every $\alpha$ on the left there is a unique $\sigma$ on the right:
\[ [\cat E, \cat C] (F, G \circ P) \cong [\cat B, \cat C](\text{Lan}_P F , G) \]
\subsection{Left Kan extension as a coend}
Recall the ninja co-Yoneda lemma. For every co-presheaf $F$, we have:
\[ F b \cong \int^{c} \cat B(c, b) \times F c \]
The left Kan extension generalizes this formula to:
\[ (\text{Lan}_P F)\, b \cong \int^{e} \cat B (P e, b) \times F e \]
For a general functor $F \colon \cat E \to \cat C$, we replace the product with the \index{copower}copower:
\[ (\text{Lan}_P F)\, b \cong \int^{e} \cat B(P e, b) \cdot F e \]
As long as the coend in question exists, we can prove this formula by considering a mapping out to some functor $G$. We represent the set of natural transformations as the end over $b$:
\[\int_b \cat C \big(\int^e \cat B(P e, b) \cdot F e, G b\big) \]
Using cocontinuity, we pull out the coend, turning it into an end:
\[\int_b \int_e \cat C \big(\cat B(P e, b) \cdot F e, G b\big) \]
and we plug in the definition of co-power:
\[\int_b \int_e \cat C \big(\cat B(P e, b), \cat C (F e, G b)\big) \]
We can now use the Yoneda lemma to integrate over $b$, replacing $b$ with $P e$:
\[\int_e \cat C (F e, G (P e))\big) \cong [\cat E, \cat C] (F, G \circ P) \]
This indeed gives us the left adjoint to functor pre-composition:
\[ [\cat B, \cat C](\text{Lan}_P F , G) \cong [\cat E, \cat C] (F, G \circ P) \]
In $\Set$, the co-power decays to a cartesian product, so we get a simpler formula:
\[ (\text{Lan}_P F)\, b \cong \int^{e} \cat B (P e, b) \times F e \]
Notice that, if the functor $P$ has a right adjoint, let's call it $P^{-1}$:
\[ \cat B(P e , b) \cong \cat E(e, P^{-1} b) \]
we can use the ninja co-Yoneda lemma to get:
\[ (\text{Lan}_P F)\, b \cong (F \circ P^{-1}) b \]
thus reinforcing the intuition that a Kan extension inverts $P$ and follows it with $F$.
\subsection{Left Kan extension in Haskell}
When translating the formula for the left Kan extension to Haskell, we replace the coend with the existential type. Symbolically:
\begin{haskell}
type Lan p f b = exists e. (p e -> b, f e)
\end{haskell}
This is how we would encode the existential using \hask{GADT}'s:
\begin{haskell}
data Lan p f b where
Lan :: (p e -> b) -> f e -> Lan p f b
\end{haskell}
The unit of the left Kan extension is a natural transformation from the functor \hask{f} to the composition of \hask{(Lan p f)} after \hask{p}:
\begin{haskell}
unit :: forall p f e'.
f e' -> Lan p f (p e')
\end{haskell}
To implement the unit, we start with a value of the type \hask{(f e')}. We have to come up with some type \hask{e}, a function \hask{p e -> p e'}, and a value of the type \hask{(f e)}. The obvious choice is to pick \hask{e = e'} and use the identity at \hask{(p e')}:
\begin{haskell}
unit fe = Lan id fe
\end{haskell}
The computational power of the left Kan extension lies in its universal property. Given a functor \hask{g} and a natural transformation from \hask{f} to the composition of \hask{g} after \hask{p}:
\begin{haskell}
type Alpha p f g = forall e. f e -> g (p e)
\end{haskell}
there is a unique natural transformation $\sigma$ from the corresponding left Kan extension to \hask{g}:
\begin{haskell}
sigma :: Functor g => Alpha p f g -> forall b. (Lan p f b -> g b)
sigma alpha (Lan pe_b fe) = fmap pe_b (alpha fe)
\end{haskell}
that factorizes $\alpha$ through the unit $\eta$:
\[ \alpha = (\sigma \circ P) \cdot \eta \]
The whiskering of $\sigma$ means instantiating it at \hask{b = p e}, so the factorization of $\alpha$ is implemented as:
\begin{haskell}
factorize :: Functor g => Alpha p f g -> f e -> g (p e)
factorize alpha = sigma alpha . unit
\end{haskell}
\begin{exercise}
Implement the \hask{Functor} instance for \hask{Lan}.
\end{exercise}
\subsection{Colimits as Kan extensions}
Just like limits can be defined as right Kan extensions, colimits can be defined as left Kan extension.
We start with an indexing category $\cat J$ that defines the shape of the colimit. The functor $D$ selects this shape in the target category $\cat C$. The apex of the cocone is selected by a functor from the terminal single-object category $\Cat 1$. The natural transformation defines a cocone from $D$ to $X$:
\[
\begin{tikzcd} [row sep=1cm, column sep=1cm]
\cat J
\arrow[rr, "D", "" {name=ID, below} ]
\arrow[d, bend right, "!"']
&& \cat C
\\
\Cat 1
\arrow[urr, bend right, "X"']
\arrow[Rightarrow, "\gamma", from=ID]
\end{tikzcd}
\]
Here's an illustrative example of a simple shape consisting of three objects and three morphisms (not counting identities). The object $x$ is the image of the single object $*$ under the functor $X$:
\[
\begin{tikzcd}
1
\arrow[rr, red]
\arrow[rd, red]
&& 2