forked from BartoszMilewski/DaoFP
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path9-NaturalTransformations.tex
1713 lines (1383 loc) · 81.3 KB
/
9-NaturalTransformations.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}{8}
\chapter{Natural Transformations}
We've seen that, when two objects $a$ and $b$ are isomorphic, they generate bijections between sets of arrows, which we can now express as isomorphisms between hom-sets. For all $x$, we have:
\begin{align*}
\mathcal{C}(a, x) &\cong \mathcal{C}(b, x) \\
\mathcal{C}(x, a) &\cong \mathcal{C}(x, b)
\end{align*}
The converse is not true, though. An isomorphism between hom-sets does not result in an isomorphism between object \emph{unless} additional naturality conditions are satisfied. We'll now re-formulate these naturality conditions in progressively more general settings.
\section{Natural Transformations Between Hom-Functors}
One way an isomorphism between two objects can be established is by directly providing two arrows---one the inverse of the other. But quite often it's easier to do it indirectly, by defining bijections between arrows, either the ones impinging on the two objects, or the ones emanating from the two objects.
For instance, as we've seen before, we may have, for every $x$, an invertible mapping of arrows $\alpha_x$.
\[
\begin{tikzcd}
\node(x) at (0, 2) {x};
\node(a) at (-2, 0) {a};
\node(b) at (2, 0) {b};
\node(c1) at (-1, 1.5) {};
\node(c2) at (-1.5, 1) {};
\node(c3) at (-1, 2) {};
\node(c4) at (-2, 1) {};
\node(d1) at (1, 1.5) {};
\node(d2) at (1.5, 1) {};
\node(d3) at (1, 2) {};
\node(d4) at (2, 1) {};
\node (aa) at (-1, 0.75) {};
\node (bb) at (1, 0.75) {};
\draw[->] (x) .. controls (c1) and (c2) .. (a); % bend
\draw[->, green] (x) .. controls (c3) and (c4) .. (a); % bend
\draw[->, blue] (x) -- (a);
\draw[->] (x) .. controls (d1) and (d2) .. (b); % bend
\draw[->, green] (x) .. controls (d3) and (d4) .. (b); % bend
\draw[->, blue] (x) -- (b);
\draw[->, red, dashed] (aa) -- node[above]{\alpha_x} (bb);
\end{tikzcd}
\]
In other words, for every $x$, there is a mapping of hom-sets:
\[ \alpha_x \colon \mathcal{C}(x, a) \to \mathcal{C}(x, b) \]
When we vary $x$, the two hom-sets become two (contravariant) functors, $\cat C(-, a)$ and $\cat C(-, b)$, and $\alpha$ can be seen as a mapping between them. Such a mapping of functors, called a transformation, is really a family of individual mappings $\alpha_x$, one per each object $x$ in the category $\mathcal{C}$.
The functor $\mathcal{C}(-, a)$ describes the way the worlds sees $a$, and the functor $\mathcal{C}(-, b)$ describes the way the world sees $b$.
The transformation $\alpha$ switches back and forth between these two views. Every component of $\alpha$, the bijection $\alpha_x$, shows that the view of $a$ from $x$ is isomorphic to the view of $b$ from $x$.
The naturality condition we discussed before was the condition:
\[ \alpha_y \circ (- \circ g) = (- \circ g) \circ \alpha_x \]
It relates components of $\alpha$ taken at different objects. In other words, it relates the views from two different observers $x$ and $y$, who are connected by an arrow $g \colon y \to x$.
Both sides of this equation are acting on the hom-set $\mathcal{C}(x, a)$. The result is in the hom-set $\mathcal{C}(y, b)$. We can rewrite the two sides as:
\begin{align*}
\cat C(x, a) \xrightarrow{(- \circ g)} \cat C(y, a) \xrightarrow{\alpha_y} \cat C(y, b) \\
\cat C(x, a) \xrightarrow{\alpha_x} \cat C(x, b) \xrightarrow{(- \circ g)}\cat C(y, b)
\end{align*}
Precomposition with $g \colon y \to x$ is also a mapping of hom-sets. In fact it is the lifting of $g$ by the contravariant hom-functor. We can write it as $\mathcal{C}(g, a)$ and $\mathcal{C}(g, b)$, respectively.
\begin{align*}
\cat C(x, a) \xrightarrow{\cat C(g, a)} \cat C(y, a) \xrightarrow{\alpha_y} \cat C(y, b) \\
\cat C(x, a) \xrightarrow{\alpha_x} \cat C(x, b) \xrightarrow{\cat C(g, b)}\cat C(y, b)
\end{align*}
The naturality condition can therefore be rewritten as:
\[ \alpha_y \circ \mathcal{C}(g, a) = \mathcal{C}(g, b) \circ \alpha_x \]
It can be illustrated by this commuting diagram:
\[
\begin{tikzcd}
\mathcal{C}(x, a)
\arrow[d, "\alpha_x"]
\arrow[r, "{\mathcal{C}(g, a)}"]
&
\mathcal{C}(y, a)
\arrow[d, "\alpha_y"]
\\
\mathcal{C}(x, b)
\arrow[r, "{\mathcal{C}(g, b)}"]
& \mathcal{C}(y, b)
\end{tikzcd}
\]
We can now re-formulate our previous result: An invertible transformation $\alpha$ between the functors $\mathcal{C}(-, a)$ and $\mathcal{C}(-, b)$ that satisfies the naturality condition is equivalent to an isomorphism between $a$ and $b$.
We can follow exactly the same reasoning for the outgoing arrows. This time we start with a transformation $\beta$ whose components are:
\[ \beta_x \colon \mathcal{C}(a, x) \to \mathcal{C}(b, x) \]
The two (covariant) functors $\mathcal{C}(a, -)$ and $\mathcal{C}(b, -)$ describe the view of the world from the perspective of $a$ and $b$, respectively. The invertible transformation $\beta$ tells us that these two views are equivalent, and the naturality condition
\[ (g \circ -) \circ \beta_x = \beta_y \circ (g \circ -) \]
tells us that they behave nicely when we switch focus.
Here's the commuting diagram that illustrates the naturality condition:
\[
\begin{tikzcd}
\mathcal{C}(a, x)
\arrow[d, "\beta_x"]
\arrow[r, "{\mathcal{C}(a, g)}"]
&
\mathcal{C}(a, y)
\arrow[d, "\beta_y"]
\\
\mathcal{C}(b, x)
\arrow[r, "{\mathcal{C}(b, g)}"]
& \mathcal{C}(b, y)
\end{tikzcd}
\]
Again, such an invertible natural transformation $\beta$ establishes the isomorphism between $a$ and $b$.
\section{Natural Transformation Between Functors}
The two hom-functors from the previous section were
\begin{align*}
F x &= \mathcal{C}(a, x) \\
G x &= \mathcal{C}(b, x)
\end{align*}
They both map the category $\mathcal{C}$ to $\mathbf{Set}$, because that's where the hom-sets live. We can say that they create two different \emph{models} of $\mathcal{C}$ inside $\mathbf{Set}$.
A natural transformation is a structure-preserving mapping between two such models.
\[
\begin{tikzcd}
&& \cat C(a, x)
\arrow[dd, "\beta_x"]
\\
x
\arrow[rru, dashed, "{\cat C(a, -)}"]
\arrow[rrd, dashed, "{\cat C(b, -)}"']
\\
&& \cat C(b, x)
\end{tikzcd}
\]
This idea naturally extends to functors between any pair of categories. Any two functors
\begin{align*}
F &\colon \mathcal{C} \to \mathcal{D} \\
G &\colon \mathcal{C} \to \mathcal{D}
\end{align*}
may be seen as two different models of $\mathcal{C}$ inside $\mathcal{D}$.
To transform one model into another we connect the corresponding dots using arrows in $\mathcal{D}$. For every object $x$ in $\mathcal{C}$ we pick an arrow that goes from $F x$ to $G x$:
\[ \alpha_x \colon F x \to G x \]
A natural transformation thus maps objects to arrows.
\[
\begin{tikzcd}
&& F x
\arrow[dd, "\alpha_x"]
\\
x
\arrow[rru, dashed, "F"]
\arrow[rrd, dashed, "G"']
\\
&& G x
\end{tikzcd}
\]
The structure of a model, though, has as much to do with objects as it does with arrows, so let's see what happens to arrows. For every arrow $f \colon x \to y$ in $\mathcal{C}$, we have two corresponding arrows in $\mathcal{D}$:
\begin{align*}
F f &\colon F x \to F y \\
G f &\colon G x \to G y
\end{align*}
These are the two liftings of $f$. We can use them to move within the bounds of each of the two models. Then there are the components of $\alpha$ which let us switch \emph{between} models.
Naturality says that it shouldn't matter whether you first move inside the first model and then jump to the second one, or first jump to the second one and then move within it. This is illustrated by the commuting \emph{naturality square}:
\[
\begin{tikzcd}
F x
\arrow[d, "\alpha_x"]
\arrow[r, "F f"]
&
F y
\arrow[d, "\alpha_y"]
\\
G x
\arrow[r, "G f"]
& G y
\end{tikzcd}
\]
Such a family of arrows $\alpha_x$ that satisfies the naturality condition is called a \emph{natural transformation}.
This is a diagram that shows a pair of categories, two functors between them, and a natural transformation $\alpha$ between the functors:
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[bend left=50]{r}[name=U, label=above:$F$]{}
\arrow[bend right=50]{r}[name=D, label=below:$G$]{}
&
\mathcal{D}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U) -- node[label=left:$\alpha$] {} (D)}]{}
\end{tikzcd}
\]
Since for every arrow in $\mathcal{C}$ there is a corresponding naturality square, we can say that a natural transformation maps objects to arrows, and arrows to commuting squares.
If every component $\alpha_x$ of a natural transformation is an isomorphism, $\alpha$ is called a \emph{natural isomorphism}.
We can now restate the main result about isomorphisms: Two objects are isomorphic if and only if there is a natural isomorphism between their hom-functors (either the covariant, or the contravariant ones---either one will do).
Natural transformations provide a very convenient high-level way of expressing commuting conditions in a variety of situations. We'll use them in this capacity to reformulate the definitions of algebraic data types.
\section{Natural Transformations in Programming}
A natural transformation is a family of arrows parameterized by objects. In programming, this corresponds to a family of functions parameterized by types, that is a \emph{polymorphic function}.
The type of the argument to a natural transformation is described using one functor, and the return type using another.
In Haskell, we can define a data type that accepts two type constructors representing two functors, and produces a type of natural transformations:
\begin{haskell}
data Natural :: (Type -> Type) -> (Type -> Type) -> Type where
Natural :: (forall a. f a -> g a) -> Natural f g
\end{haskell}
The \hask{forall} quantifier tells the compiler that the function is polymorphic---that is, it's defined for every type \hask{a}. As long as \hask{f} and \hask{g} are functors, this formula defines a natural transformation.
The types defined by \hask{forall} are very special, though. The are polymorphic in the sense of \index{parametric polymorphism}\emph{parametric polymorphism}. It means that a single formula is used for all types. We've seen the example of the identity function, which can be written as:
\begin{haskell}
id :: forall a. a -> a
id x = x
\end{haskell}
The body of this function is very simple, just the variable \hask{x}. It doesn't matter what type \hask{x} is, the formula remains the same.
This is in contrast to \index{ad-hoc polymorphism}\emph{ad-hoc polymorphism}. An ad-hoc polymorphic function may use different implementations for different types. An example of such a function is \hask{fmap}, the member function of the \hask{Functor} typeclass. There is one implementation of \hask{fmap} for lists, a different one for \hask{Maybe}, and so on, case by case.
The standard definition of a (parametric) natural transformation in Haskell uses a \emph{type synonym:}
\begin{haskell}
type Natural f g = forall a. f a -> g a
\end{haskell}
A \index{\hask{type} synonym}\hask{type} declaration introduces an alias, a shorthand, for the right-hand-side.
It turns out that limiting the type of a natural transformation to adhere to parametric polymorphism has far-reaching consequences. Such a function automatically satisfies naturality conditions. It's an example of \index{parametricity}parametricity producing so called \index{theorems for free}\emph{theorems for free}.
We can't express equalities of arrows in Haskell, but we can use naturality to transform programs. In particular, if \hask{alpha} is a natural transformation, we can replace:
\begin{haskell}
fmap h . alpha
\end{haskell}
with:
\begin{haskell}
alpha . fmap h
\end{haskell}
Here, the compiler will automatically figure out what versions of \hask{fmap} and which components of \hask{alpha} to use.
We can also use more advanced language options to make the choices explicit. We can express naturality using a pair of functions:
\begin{haskell}
oneWay ::
forall f g a b. (Functor f, Functor g) =>
Natural f g -> (a -> b) -> f a -> g b
oneWay alpha h = fmap @g h . alpha @a
\end{haskell}
\begin{haskell}
otherWay ::
forall f g a b. (Functor f, Functor g) =>
Natural f g -> (a -> b) -> f a -> g b
otherWay alpha h = alpha @b . fmap @f h
\end{haskell}
The annotations \hask{@a} and \hask{@b} specify the components of the parametrically polymorphic function \hask{alpha}, and the annotations \hask{@f} and \hask{@g} specify the functors for which the ad-hoc polymorphic \hask{fmap} is instantiated.
Here's an example of a useful function that is a natural transformation between the list functor and the \hask{Maybe} functor:
\begin{haskell}
safeHead :: Natural [] Maybe
safeHead [] = Nothing
safeHead (a : as) = Just a
\end{haskell}
(The standard library \hask{head} function is ``unsafe'' in that it faults when given an empty list.)
Another example is the function \hask{reverse}, which reverses a list. It's a natural transformation from the list functor to the list functor:
\begin{haskell}
reverse :: Natural [] []
reverse [] = []
reverse (a : as) = reverse as ++ [a]
\end{haskell}
Incidentally, this is a very inefficient implementation. The actual library function uses an optimized algorithm.
A useful intuition for understanding natural transformations builds on the idea that functors acts like containers for data. There are two completely orthogonal things that you can do with a container: You can transform the data it contains, without changing the shape of the container. This is what \hask{fmap} does. Or you can transfer the data, without modifying it, to another container. This is what a natural transformation does: It's a procedure for moving ``stuff'' between containers without knowing what kind of ``stuff'' it is.
In other words, a natural transformation repackages the contents of one container into another container. It does it in a way that is agnostic of the type of the contents, which means it cannot inspect, create, or modify the contents. All it can do is to move it to a new location, or drop it.
Naturality condition enforces the orthogonality of these two operations. It doesn't matter if you first modify the data and then move it to another container; or first move it, and then modify.
This is another example of successfully decomposing a complex problem into a sequence of simpler ones. Keep in mind, though, that not every operation with containers of data can be decomposed in that way. Filtering, for instance, requires both examining the data, as well as changing the size or even the shape of the container.
On the other hand, almost every parametrically polymorphic function is a natural transformation. In some cases you may have to consider the identity or the constant functor as either source or the target. For instance, the polymorphic identity function can be thought of as a natural transformation between two identity functors.
\subsection{Vertical composition of natural transformations}
Natural transformations can only be defined between \emph{parallel} functors, that is functors that share the same source category and the same target category. Such parallel functors form a \emph{functor category}. The standard notation for a functor category between two categories $\mathcal{C}$ and $\mathcal{D}$ is $[\mathcal{C}, \mathcal{D}]$. You just put the names of the two categories between square brackets.
The objects in $[\mathcal{C}, \mathcal{D}]$ are functors, the arrows are natural transformations.
To show that this is indeed a category, we have to define the composition of natural transformations. This is easy if we keep in mind that components of natural transformations are regular arrows in the target category. These arrows compose.
Indeed, suppose that we have a natural transformation $\alpha$ between two functors $F$ and $G$. We want to compose it with another natural transformation $\beta$ that goes from $G$ to $H$.
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[bend left=60]{rr}[name=U, label=above:$F$]{}
\arrow[]{rr}[name=M, label={[xshift=15pt, yshift=-5pt]:$G$}]{}
\arrow[bend right=60]{rr}[name=D, label=below:$H$]{}
&&
\mathcal{D}
\arrow[shorten <=8pt, shorten >=8pt,Rightarrow, to path={(U) -- node[label=left:$\alpha$] {} (M)}]{}
\arrow[shorten <=8pt, shorten >=8pt,Rightarrow, to path={(M) -- node[label=left:$\beta$] {} (D)}]{}
\end{tikzcd}
\]
Let's look at the components of these transformations at some object $x$
\[ \alpha_x \colon F \, x \to G \, x \]
\[ \beta_x \colon G \, x \to H \, x \]
These are just two arrows in $\mathcal{D}$ that are composable. So we can define a composite natural transformation $\gamma$ as follows:
\[ \gamma \colon F \to H\]
\[ \gamma_x = \beta_x \circ \alpha_x \]
This is called the \emph{vertical composition} of natural transformations. You'll see it written using a dot $\gamma = \beta \cdot \alpha$ or a simple juxtaposition $\gamma = \beta \alpha$.
Naturality condition for $\gamma$ can be shown by pasting together (vertically) two naturality squares for $\alpha$ and $\beta$:
\[
\begin{tikzcd}
F x
\arrow[d, "\alpha_x"]
\arrow[r, "F f"]
\arrow[dd, bend right = 60, "\gamma_x"']
&
F y
\arrow[d, "\alpha_y"]
\arrow[dd, bend left = 60, "\gamma_y"]
\\
G x
\arrow[r, "G f"]
\arrow[d, "\beta_x"]
& G y
\arrow[d, "\beta_y"]
\\
H x
\arrow[r, "H f"]
& H y
\end{tikzcd}
\]
In Haskell, vertical composition of natural transformation is just regular function composition applied to polymorphic functions. Using the intuition that natural transformations move items between containers, vertical composition combines two such moves, one after another.
\subsection{Functor categories}
Since the composition of natural transformations is defined in terms of composition of arrows, it is automatically associative.
There is also an identity natural transformation $id_F$ defined for every functor $F$. Its component at $x$ is the usual identity arrow at the object $F x$:
\[ (id_F)_x = id_{F x} \]
To summarize, for every pair of categories $\mathcal{C}$ and $\mathcal{D}$ there is a category of functors $[\mathcal{C}, \mathcal{D}]$ with natural transformations as arrows.
The hom-set in that category is the set of natural transformations between two functors $F$ and $G$. Following the standard notational convention, we write it as:
\[ [\mathcal{C}, \mathcal{D}](F, G) \]
with the name of the category followed by the names of the two objects (here, functors) in parentheses.
In category theory objects and arrows are drawn differently. Objects are dots and arrows are pointy lines.
In $\mathbf{Cat}$, the category of categories, functors are drawn as arrows. But in a functor category $[\cat C, \cat D]$ functors are dots and natural transformations are arrows.
What is an arrow in one category could be an object in another.
\begin{exercise}
Prove the naturality condition of the composition of natural transformations:
\[ \gamma_y \circ F f = H f \circ \gamma_x \]
Hint: Use the definition of $\gamma$ and the two naturality conditions for $\alpha$ and $\beta$.
\end{exercise}
\subsection{Horizontal composition of natural transformations}
The second kind of composition of natural transformations is induced by the composition of functors. Suppose that we have a pair of composable functors
\begin{align*}
F \colon \mathcal{C} \to \mathcal{D}
&&G \colon \mathcal{D} \to \mathcal{E}
\end{align*}
and, in parallel, another pair of composable functors:
\begin{align*}
F' \colon \mathcal{C} \to \mathcal{D}
&& G' \colon \mathcal{D} \to \mathcal{E}
\end{align*}
We also have two natural transformations:
\begin{align*}
\alpha \colon F \to F'
&& \beta \colon G \to G'
\end{align*}
Pictorially:
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[bend left=50]{r}[name=U, label=above:$F$]{}
\arrow[bend right=50]{r}[name=D, label=below:$F'$]{}
&
\mathcal{D}
\arrow[bend left=50]{r}[name=U1, label=above:$G$]{}
\arrow[bend right=50]{r}[name=D1, label=below:$G'$]{}
&
\mathcal{E}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U) -- node[label=left:$\alpha$] {} (D)}]{}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U1) -- node[label=left:$\beta$] {} (D1)}]{}
\end{tikzcd}
\]
The \emph{horizontal composition} $\beta \circ \alpha$ maps $G \circ F$ to $G' \circ F'$.
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[bend left=50]{r}[name=U, label=above:$G \circ F$]{}
\arrow[bend right=50]{r}[name=D, label=below:$G' \circ F'$]{}
&
\mathcal{E}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U) -- node[label=left:$\beta \circ \alpha$] {} (D)}]{}
\end{tikzcd}
\]
Let's pick an object $x$ in $\mathcal{C}$ and try to define the component of the composite $(\beta \circ \alpha)$ at $x$. It should be a morphism in $\cat E$:
\[ (\beta \circ \alpha)_x \colon G ( F x) \to G' ( F' x) \]
We can use $\alpha$ to map $x$ to an arrow
\[ \alpha_x \colon F x \to F' x \]
We can lift this arrow using $G$
\[ G (\alpha_x) \colon G (F x) \to G (F' x) \]
To get from there to $G' (F' x)$ we can use the appropriate component of $\beta$
\[ \beta_{F' x} \colon G (F' x) \to G' (F' x) \]
Altogether, we have
\[ (\beta \circ \alpha)_x = \beta_{F' x} \circ G (\alpha_x) \]
But there is another equally plausible candidate:
\[ (\beta \circ \alpha)_x = G'(\alpha_x) \circ \beta_{F x}\]
Fortunately, they are equal due to naturality of $\beta$.
\[
\begin{tikzcd}
&& G(F x)
\arrow[dd, red, "G(\alpha_x)"]
\arrow[dr, blue, "\beta_{F x}"]
\\
& F x
\arrow[rr, bend right=10, dashed, gray]
\arrow[ur, bend right=10, dashed]
\arrow[dd, red, "\alpha_x"]
&& G' (F x)
\arrow[dd, red, "G'(\alpha_x)"]
\\
x
\arrow[ur, dashed]
\arrow[dr, gray, dashed]
&& G(F' x)
\arrow[dr, blue, "\beta_{F' x}"]
\\
&F' x
\arrow[rr, bend right=10, dashed, gray]
\arrow[ur, bend right=10, dashed]
&& G'(F' x)
\end{tikzcd}
\]
The proof of naturality of $\beta \circ \alpha$ is left as an exercise to a dedicated reader.
We can translate this directly to Haskell. We start with two natural transformations:
\begin{haskell}
alpha :: forall x. F x -> F' x
beta :: forall x. G x -> G' x
\end{haskell}
Their horizontal composition has the following type signature:
\begin{haskell}
beta_alpha :: forall x. G (F x) -> G' (F' x)
\end{haskell}
It has two equivalent implementations. The first one is:
\begin{haskell}
beta_alpha = beta . fmap alpha
\end{haskell}
The compiler will automatically pick the correct version of \hask{fmap}, the one for the functor \hask{G}. The second implementation is:
\begin{haskell}
beta_alpha = fmap alpha . beta
\end{haskell}
Here, the compiler will pick the version of \hask{fmap} for the functor \hask{G'}.
What's the intuition for horizontal composition? We've seen before that a natural transformation can be seen as repackaging data between two containers--functors. Here we are dealing with nested containers. We start with the outer container described by \hask{G} that is filled with inner containers, each described by \hask{F}. We have two natural transformations, \hask{alpha} for transfering the contents of \hask{F} to \hask{F'}, and \hask{beta} for moving the contents of \hask{G} to \hask{G'}. There are two ways of moving data from \hask{G (F x)} to \hask{G'(F' x)}. We can use \hask{fmap alpha} to repackage all inner containers, and then use \hask{beta} to repackage the outer container.
\[
\begin{tikzpicture}
\filldraw[fill=blue!50!green!20, draw=white] (0, 0) ellipse (1.2 and 1.8);
\filldraw[fill=orange!70, draw=white] (-0.5, -0.5) rectangle (0.5, 0.5);
\node at (0, 0) {$F$};
\node at (0, -1.3) {$G$};
\end{tikzpicture}
\hspace{20pt}
\begin{tikzpicture}
\filldraw[fill=blue!50!green!20, draw=white] (0, 0) ellipse (1.2 and 1.8);
\filldraw[fill=orange!30, draw=white] (0, 0) ellipse (0.8 and 0.4);
\node at (0, 0) {$F'$};
\node at (0, -1.3) {$G$};
\end{tikzpicture}
\hspace{20pt}
\begin{tikzpicture}
\filldraw[fill=blue!10, draw=white] (0, 0) circle (1.2);
\filldraw[fill=orange!30, draw=white] (0, 0) ellipse (0.8 and 0.4);
\node at (0, 0) {$F'$};
\node at (0, -0.8) {$G'$};
\end{tikzpicture}
\]
Or we can first use \hask{beta} to repackage the outer container, and then apply \hask{fmap alpha} to repackage all the inner containers. The end result is the same.
\[
\begin{tikzpicture}
\filldraw[fill=blue!50!green!20, draw=white] (0, 0) ellipse (1.2 and 1.8);
\filldraw[fill=orange!70, draw=white] (-0.5, -0.5) rectangle (0.5, 0.5);
\node at (0, 0) {$F$};
\node at (0, -1.3) {$G$};
\end{tikzpicture}
\hspace{20pt}
\begin{tikzpicture}
\filldraw[fill=blue!10, draw=white] (0, 0) circle (1.2);
\filldraw[fill=orange!70, draw=white] (-0.5, -0.5) rectangle (0.5, 0.5);
\node at (0, 0) {$F$};
\node at (0, -0.9) {$G'$};
\end{tikzpicture}
\hspace{20pt}
\begin{tikzpicture}
\filldraw[fill=blue!10, draw=white] (0, 0) circle (1.2);
\filldraw[fill=orange!30, draw=white] (0, 0) ellipse (0.8 and 0.4);
\node at (0, 0) {$F'$};
\node at (0, -0.9) {$G'$};
\end{tikzpicture}
\]
\begin{exercise}
Implement two versions of horizontal composition of \hask{safeHead} after \hask{reverse}. Compare their results acting on various arguments.
\end{exercise}
\begin{exercise}
Do the same with the horizontal composition of \hask{reverse} after \hask{safeHead}.
\end{exercise}
\subsection{Whiskering}
Quite often horizontal composition is used with one of the natural transformations being the identity. There is a shorthand notation for such composition. For instance, $\beta \circ id_F$ is written as $\beta \circ F$.
Because of the characteristic shape of the diagram, such composition is called ``whiskering''.
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[r, "F"]
&
\mathcal{D}
\arrow[bend left=50]{r}[name=U1, label=above:$G$]{}
\arrow[bend right=50]{r}[name=D1, label=below:$G'$]{}
&
\mathcal{E}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U1) -- node[label=left:$\beta$] {} (D1)}]{}
\end{tikzcd}
\]
In components, we have:
\[ (\beta \circ F)_x = \beta_{F x} \]
Let's consider how we would translate this to Haskell. A natural transformation is a polymorphic function. Because of parametricity, it's defined by the same formula for all types. So whiskering on the right doesn't change the formula, it changes the function signature.
For instance, if this is the declaration of \hask{beta}:
\begin{haskell}
beta :: forall x. G x -> G' x
\end{haskell}
then its whiskered version would be:
\begin{haskell}
beta_f :: forall x. G (F x) -> G' (F x)
beta_f = beta
\end{haskell}
Because of Haskell's type inference, this shift is implicit. When a polymorphic function is called, we don't have to specify which component of the natural transformation is executed--the type checker figures it out by looking at the type of the argument.
The intuition in this case is that we are repackaging the outer container leaving the inner containers intact.
Similarly, $id_H \circ \alpha$ is written as $H \circ \alpha$.
\[
\begin{tikzcd}[column sep=huge]
\mathcal{D}
\arrow[bend left=50]{r}[name=U, label=above:$G$]{}
\arrow[bend right=50]{r}[name=D, label=below:$G'$]{}
&
\mathcal{E}
\arrow[r, "H"]
&
\mathcal{F}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U) -- node[label=left:$\alpha$] {} (D)}]{}
\end{tikzcd}
\]
In components:
\[(H \circ \alpha)_x = H (\alpha_x) \]
In Haskell, the lifting of $\alpha_x$ by $H$ is done using \hask{fmap}, so given:
\begin{haskell}
alpha :: forall x. G x -> G' x
\end{haskell}
the whiskered version would be:
\begin{haskell}
h_alpha :: forall x. H (G x) -> H (G' x)
h_alpha = fmap alpha
\end{haskell}
Again, Haskell's type inference engine figures out which version of \hask{fmap} to use (here, it's the one from the \hask{Functor} instance of \hask{G}).
The intuition is that we are repackaging the contents of the inner containers leaving the outer container intact.
Finally, in many applications a natural transformation is whiskered on both sides:
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[r, "F"]
&
\mathcal{D}
\arrow[bend left=50]{r}[name=U1, label=above:$G$]{}
\arrow[bend right=50]{r}[name=D1, label=below:$G'$]{}
&
\mathcal{E}
\arrow[shorten <=10pt,shorten >=10pt,Rightarrow,to path={(U1) -- node[label=left:$\alpha$] {} (D1)}]{}
\arrow[r, "H"]
&
\mathcal{F}
\end{tikzcd}
\]
In components, we have:
\[ (H \circ \alpha \circ F) x = H (\alpha_{F x})\]
and in Haskell:
\begin{haskell}
h_alpha_f :: forall x. H (G (F x)) -> H (G' (F x))
h_alpha_f = fmap alpha
\end{haskell}
Here the intuition is that we have a triple layer of containers; and we are rearranging the middle one, leaving the outer container and all the inner containers intact.
\subsection{Interchange law}
We can combine vertical composition with horizontal composition, as seen in the following diagram:
\[
\begin{tikzcd}[column sep=huge]
\mathcal{C}
\arrow[bend left=60]{rr}[name=U, label=above:$F$]{}
\arrow[]{rr}[name=M, label={[xshift=15pt, yshift=-5pt]:$G$}]{}
\arrow[bend right=60]{rr}[name=D, label=below:$H$]{}
&&
\mathcal{D}
\arrow[bend left=60]{rr}[name=U1, label=above:$F'$]{}
\arrow[]{rr}[name=M1, label={[xshift=15pt, yshift=-5pt]:$G'$}]{}
\arrow[bend right=60]{rr}[name=D1, label=below:$H'$]{}
&&
\mathcal{E}
\arrow[shorten <=8pt, shorten >=8pt,Rightarrow, to path={(U) -- node[label=left:$\alpha$] {} (M)}]{}
\arrow[shorten <=8pt, shorten >=8pt,Rightarrow, to path={(M) -- node[label=left:$\beta$] {} (D)}]{}
\arrow[shorten <=8pt, shorten >=8pt,Rightarrow, to path={(U1) -- node[label=left:$\alpha'$] {} (M1)}]{}
\arrow[shorten <=8pt, shorten >=8pt,Rightarrow, to path={(M1) -- node[label=left:$\beta'$] {} (D1)}]{}
\end{tikzcd}
\]
The interchange law states that the order of composition doesn't matter: we can first do vertical compositions and then the horizontal one, or first do the horizontal compositions and then the vertical one.
\section{Universal Constructions Revisited}
Lao Tzu says, the simplest pattern is the clearest.
We've seen definitions of sums, products, exponentials, natural numbers, and lists.
The old-school approach to defining such data types is to explore their internals. It's the set-theory way: we look at how the elements of new sets are constructed from the elements of old sets. An element of a sum is either an element of the first set, or the second set. An element of a product is a pair of elements. And so on. We are looking at objects from the engineering point of view.
In category theory we take the opposite approach. We are not interested in what's inside the object or how it's implemented. We are interested in the purpose of the object, how it can be used, and how it interacts with other objects. We are looking at objects from the utilitarian point of view.
Both approaches have their advantages. The categorical approach came later, because you need to study a lot of examples before clear patterns emerge. But once you see the patterns, you discover unexpected connections between things, like the duality between sums and products.
Defining particular objects through their connections requires looking at possibly infinite numbers of objects with which they interact.
``Tell me your relation to the Universe, and I'll tell you who you are.''
Defining an object by its mappings-out or mappings-in with respect to all objects in the category is called a \emph{universal construction}.
Why are natural transformations so important? It's because most categorical constructions involve commuting diagrams. If we can re-cast these diagrams as naturality squares, we move one level up the abstraction ladder and gain new valuable insights.
Being able to compress a lot of facts into small elegant formulas helps us see new patterns. We'll see, for instance, that natural isomorphisms between hom-sets pop up all over category theory and eventually lead to the idea of an adjunction.
But first we'll study several examples in greater detail to get some understanding of the terse language of category theory. We'll try, for instance, to decode the statement that the sum, or the coproduct of two objects, is defined by the following natural isomorphism:
\[ [\mathbf{2}, \mathcal{C}](D, \Delta_x) \cong \mathcal{C}(a + b, x) \]
\subsection{Picking objects}
Even such a simple task as pointing at an object has a special interpretation in category theory. We have already seen that pointing at an element of a set is equivalent to selecting a function from the singleton set to it. Similarly, picking an object in a category is equivalent to selecting a functor from the single-object category. Alternatively, it can be done using a constant functor from another category.
Quite often we want to pick a pair of objects. That, too, can be accomplished by selecting a functor from a two-object stick-figure category. Similarly, picking an arrow is equivalent to selecting a functor from the ``walking arrow'' category, and so on.
By judiciously selecting our functors and natural transformations between them, we can reformulate all the universal constructions we've seen so far.
\subsection{Cospans as natural transformations}
The definition of a sum requires the selection of two objects to be summed; and a third one to serve as the target of the mapping out.
\[
\begin{tikzcd}
a
\arrow[dr, bend left, "\text{Left}"']
\arrow[ddr, bend right, "f"']
&& b
\arrow[dl, bend right, "\text{Right}"]
\arrow[ddl, bend left, "g"]
\\
&a + b
\arrow[d, dashed, "h"]
\\
& c
\end{tikzcd}
\]
This diagram can be further decomposed into two simpler shapes called \emph{cospans}:
\[
\begin{tikzcd}
a
\arrow[dr, ""']
&& b
\arrow[dl, ""]
\\
& x
\end{tikzcd}
\]
To construct a cospan we first have to pick a pair of objects. To do that we'll start with a two-object category $\mathbf{2}$. We'll call its objects $1$ and $2$.
We'll use a functor
\[ D \colon \mathbf{2} \to \mathcal{C}\]
to select the objects $a$ and $b$:
\begin{align*}
D\, 1 &= a \\
D\, 2 &= b
\end{align*}
($D$ stands for ``diagram'', since the two objects form a very simple diagram consisting of two dots in $\mathcal{C}$.)
We'll use the constant functor
\[ \Delta_x \colon \mathbf{2} \to \mathcal{C} \]
to select the object $x$. This functor maps both $1$ and $2$ to $x$ (and the two identity arrows to $id_x$).
Since both functors go from $\mathbf{2}$ to $\mathcal{C}$, we can define a natural transformation $\alpha$ between them. In this case, it's just a pair of arrows:
\begin{align*}
\alpha_1 \colon D \, 1 \to \Delta_x 1 \\
\alpha_2 \colon D \, 2 \to \Delta_x 2
\end{align*}
These are exactly the two arrows in the cospan.
Naturality condition for $\alpha$ is trivial, since there are no arrows (other than identities) in $\mathbf{2}$.
There may be many cospans sharing the same three objects---meaning: there may be many natural transformations between the two functors $D$ and $\Delta_x$. These natural transformations form a hom-set in the functor category $[\mathbf{2}, \mathcal{C}]$, namely:
\[ [\mathbf{2}, \mathcal{C}](D, \Delta_x) \]
\subsection{Functoriality of cospans}
Let's consider what happens when we start varying the object $x$ in a cospan. We have a mapping $F$ that takes $x$ to the set of cospans over $x$:
\[ F x = [\mathbf{2}, \mathcal{C}](D, \Delta_x) \]
This mapping turns out to be functorial in $x$.
To see that, consider an arrow $m \colon x \to y$. The lifting of this arrow is a mapping between two sets of natural transformations:
\[ [\mathbf{2}, \mathcal{C}](D, \Delta_x) \to [\mathbf{2}, \mathcal{C}](D, \Delta_{y}) \]
This might look very abstract until you remember that natural transformations have components, and these components are just regular arrows. An element of the left-hand side is a natural transformation:
\[ \mu \colon D \to \Delta_x \]
It has two components corresponding to the two objects in $\mathbf{2}$. For instance, we have
\[ \mu_1 \colon D \, 1 \to \Delta_x 1 \]
or, using the definitions of $D$ and $\Delta$:
\[ \mu_1 \colon a \to x \]
This is just the left leg of our cospan.
Similarly, the element of the right-hand side is a natural transformation:
\[ \nu \colon D \to \Delta_{y} \]
Its component at $1$ is an arrow
\[ \nu_1 \colon a \to y \]
We can get from $\mu_1$ to $\nu_1$ simply by post-composing it with $m \colon x \to y$. So the lifting of $m$ is a component-by-component post-compositon $(m \circ -)$:
\begin{align*}
\nu_1 = m \circ \mu_1 \\
\nu_2 = m \circ \mu_2 \\
\end{align*}
\subsection{Sum as a universal cospan}
Of all the cospans that you can build on the pair $a$ and $b$, the one with the arrows we called $\text{Left}$ and $\text{Right}$ converging on $a + b$ is very special. There is a unique mapping out of it to any other cospan---a mapping that makes two triangles commute.
\[
\begin{tikzcd}
a
\arrow[dr, bend left, "\text{Left}"']
\arrow[ddr, bend right, "f"']
&& b
\arrow[dl, bend right, "\text{Right}"]
\arrow[ddl, bend left, "g"]
\\
&a + b
\arrow[d, dashed, "h"]
\\
& x
\end{tikzcd}
\]
We are now in the position to translate this condition to a statement about natural transformations and hom-sets. The arrow $h$ is an element of the hom-set
\[ \mathcal{C}(a + b, x)\]
A cospan over $x$ is a natural transformation, that is an element of the hom-set in the functor category:
\[ [\mathbf{2}, \mathcal{C}](D, \Delta_x) \]
Both are hom-sets in their respective categories. And both are just sets, that is objects in the category $\mathbf{Set}$. This category forms a bridge between the functor category $[\mathbf{2}, \mathcal{C}]$ and a ``regular'' category $\mathcal{C}$, even though, conceptually, they seem to be at very different levels of abstraction.
Paraphrasing Sigmund Freud, ``Sometimes a set is just a set.''
Our universal construction is the bijection or the isomorphism of sets:
\[ [\mathbf{2}, \mathcal{C}](D, \Delta_x) \cong \mathcal{C}(a + b, x) \]
Moreover, if we vary the object $x$, the two sides behave like functors from $\mathcal{C}$ to $\mathbf{Set}$. Therefore it makes sense to ask if this mapping of functors is a natural isomorphism.
Indeed, it can be shown that the naturality condition for this isomorphism translates into commuting conditions for the triangles in the definition of the sum. So the definition of the sum can be replaced by a single equation.
\subsection{Product as a universal span}
An analogous argument can be made about the universal construction for the product. Again, we start with the stick-figure category $\mathbf{2}$ and the functor $D$. But this time we use a natural transformation going in the opposite direction
\[ \alpha \colon \Delta_x \to D \]
Such a natural transformation is a pair of arrows that form a \emph{span}:
\[
\begin{tikzcd}
&x
\arrow[dl, "f"']
\arrow[dr, "g"]
\\
a
&& b
\end{tikzcd}
\]
Collectively, these natural transformations form a hom-set in the functor category :
\[[\mathbf{2}, \mathcal{C}](\Delta_x, D) \]
Every element of this hom-set is in one-to-one correspondence with a unique mapping $h$ into the product $a \times b$. Such a mapping is a member of the hom-set $\mathcal{C}(x, a \times b)$. This correspondence is expressed as the isomorphism:
\[ [\mathbf{2}, \mathcal{C}](\Delta_x, D) \cong \mathcal{C}(x, a \times b) \]
It can be shown that the naturality of this isomorphism guarantees that the triangles in this diagram commute:
\[
\begin{tikzcd}
& x
\arrow[d, dashed, "h"]
\arrow[ddl, bend right, "f = \alpha_1"']
\arrow[ddr, bend left, "g = \alpha_2"]
\\
&a \times b
\arrow[dl, "\text{fst}"]
\arrow[dr, "\text{snd}"']
\\
a = D\, 1 && b = D \, 2
\end{tikzcd}
\]
\subsection{Exponentials}
The exponentials, or function objects, are defined by this commuting diagram:
\[
\begin{tikzcd}
x \times a
\arrow[d, dashed, "h \times id_a"']
\arrow[rd, "f"]
\\
b^a \times a
\arrow[r, "\varepsilon_{a b}"']
& b
\end{tikzcd}
\]
Here, $f$ is an element of the hom-set $\mathcal{C}(x \times a, b)$ and $h$ is an element of $\mathcal{C}(x, b^a)$.
The isomorphism between these sets, natural in $x$, defines the exponential object.
\[\mathcal{C}(x \times a, b) \cong \mathcal{C}(x, b^a)\]
The $f$ in the diagram above is an element of the left-hand side, and $h$ is the corresponding element of the right-hand side. The transformation $\alpha_x$ (which also depends on $a$ and $b$) maps $f$ to $h$.
\[ \alpha_x \colon \mathcal{C}(x \times a, b) \to \mathcal{C}(x, b^a) \]
In Haskell, we call it \hask{curry}. Its inverse, $\alpha^{-1}$ is known as \hask{uncurry}.
Unlike in the previous examples, here both hom-sets are in the same category, and it's easy to analyze the isomorphism in more detail. In particular, we'd like to see how the commuting condition:
\[ f = \varepsilon_{a b} \circ (h \times id_a) \]
arises from naturality.
The standard Yoneda trick is to make a substitution for $x$ that would reduce one of the hom-sets to an endo-hom-set, that is a hom-set whose source is the same the target. This will allow us to pick a canonical element of that hom-set, that is the identity arrow.
In our case, substituting $b^a$ for $x$ will allow us to pick $h = id_{(b^a)}$.
\[
\begin{tikzcd}
b^a \times a
\arrow[d, dashed, "id_{(b^a)} \times id_a"']
\arrow[rd, "f"]
\\
b^a \times a
\arrow[r, "\varepsilon_{a b}"']
& b
\end{tikzcd}
\]
The commuting condition in this case tells us that $f = \varepsilon_{a b}$. In other words, we get the formula for $\varepsilon_{a b}$ in terms of $\alpha$:
\[ \varepsilon_{a b} = \alpha_{x}^{-1} (id_{x}) \]
where $x$ is equal to $b^a$.
Since we recognize $\alpha^{-1}$ as \hask{uncurry}, and $\varepsilon$ as function application, we can write it in Haskell as:
\begin{haskell}
apply :: (a -> b, a) -> b
apply = uncurry id
\end{haskell}
This my be surprising at first, until you realize that the currying of \hask{(a->b,a)->b} leads to \hask{(a->b)->(a->b)}.
We can also encode the two sides of the main isomorphism as Haskell functors:
\begin{haskell}
data LeftFunctor a b x = LF ((x, a) -> b)
\end{haskell}
\begin{haskell}
data RightFunctor a b x = RF (x -> (a -> b))
\end{haskell}
They are both contravariant functors in the type variable \hask{x}.
\begin{haskell}
instance Contravariant (LeftFunctor a b) where
contramap g (LF f) = LF (f . bimap g id)
\end{haskell}
This says that the lifting of $g \colon x \to y$ is given by the following pre-composition:
\[ \mathcal{C}(y \times a, b) \xrightarrow{(- \circ (g \times id_a)) } \mathcal{C}(x \times a, b)\]
Similarly:
\begin{haskell}
instance Contravariant (RightFunctor a b) where
contramap g (RF h) = RF (h . g)
\end{haskell}
translates to:
\[ \mathcal{C}(y, b^a) \xrightarrow{ (- \circ g) } \mathcal{C}(x, b^a) \]
The natural transformation $\alpha$ is just a thin encapsulation of \hask{curry}; and its inverse is \hask{uncurry}:
\begin{haskell}
alpha :: forall a b x. LeftFunctor a b x -> RightFunctor a b x
alpha (LF f) = RF (curry f)
\end{haskell}
\begin{haskell}
alpha_1 :: forall a b x. RightFunctor a b x -> LeftFunctor a b x
alpha_1 (RF h) = LF (uncurry h)
\end{haskell}
Using the two formulas for the lifting of $g \colon x \to y$, here's the naturality square:
\[
\begin{tikzcd}
\mathcal{C}(y \times a, b)
\arrow[rr, "(- \circ (g \times id_a))"]
\arrow[d, "\alpha_y"]
& &
\mathcal{C}(x \times a, b)
\arrow[d, "\alpha_x"]
\\
\mathcal{C}(y, b^a)
\arrow[rr, "(- \circ g)"]
& &
\mathcal{C}(x, b^a)
\end{tikzcd}
\]
Let's now apply the Yoneda trick to it and replace $y$ with $b^a$. This also allows us to substitute $g$---which now goes for $x$ to $b^a$---with $h$.
\[
\begin{tikzcd}
\mathcal{C}(b^a \times a, b)
\arrow[rr, "(- \circ (h \times id_a))"]
\arrow[d, "\alpha_{(b^a)}"]
& &
\mathcal{C}(x \times a, b)
\arrow[d, "\alpha_x"]
\\
\mathcal{C}(b^a, b^a)
\arrow[rr, "(- \circ h)"]
& &
\mathcal{C}(x, b^a)
\end{tikzcd}
\]
We know that the hom-set $\mathcal{C}(b^a, b^a)$ contains at least the identity arrow, so we can pick the element $id_{(b^a)}$ in the lower left corner.
Reversing the arrow on the left, we know that $\alpha^{-1}$ acting on identity produces $\varepsilon_{a b}$ in the upper left corner (that's the \hask{uncurry id} trick).
Pre-composition with $h$ acting on identity produces $h$ in the lower right corner.
$\alpha^{-1}$ acting on $h$ produces $f$ in the upper right corner.
\[
\begin{tikzcd}[
every arrow/.style={draw,mapsto}
]
\varepsilon_{a b}
\arrow[rr, "(- \circ (h \times id_a))"]
& &
f
\\
id_{(b^a)}
\arrow[u, "\alpha^{-1}"]
\arrow[rr, "(- \circ h)"]
& &
h
\arrow[u, "\alpha^{-1}"']
\end{tikzcd}
\]
(The $\mapsto$ arrows denote the action of functions on elements of sets.)