3 Natural Transformation🔗ℹ

In this chapter, we extend our exploration of category theory by introducing the concept of natural transformations. Natural transformations offer a formal framework for understanding how functors between two categories correspond and interact with each other.

Building on our foundation of categories and functors, this chapter presents natural transformations in a unique way: they are defined similarly to functors, as functions that map morphisms in the domain category to corresponding morphisms in the codomain category, with the naturality condition that certain commutative diagrams hold.

This approach highlights that functors themselves can be viewed as special natural transformations, much like objects can be viewed as special morphisms, specifically as identity morphisms.

As in the previous chapter, we’ll leverage Typed Racket to illustrate the core principles, allowing us to express these abstract mathematical concepts through practical programming constructs.

3.1 Natural Transformation🔗ℹ

In a sense, α(f) can be considered a commutative square.

A natural transformation α between parallel functors F and G from 𝒞 to 𝒟, denoted by α : F ⇒ G : 𝒞 → 𝒟, maps each morphism f : a → b : 𝒞 to a corresponding morphism α(f) : F(a) → G(b) : 𝒟. This mapping must adhere to the naturality condition, expressed as

α(f) = α(b)∘F(f) = G(f)∘α(a)

ensuring that the following diagram is commutative:

The morphism α(a) in 𝒟 for an object a in 𝒞 is the component of α at a.

For a natural transformation α, there is an opposite natural transformation αop : Gop ⇒ Fop : 𝒞op → 𝒟op such that the following diagram is commutative:

Exercise: For a morphism i : b → a : 𝒞. Prove that Hom𝒞(i, -) is a hom natural transformation from Hom𝒞(a, -) to Hom𝒞(b, -).

(: 𝒞 𝐂𝐚𝐭) (: b 𝒞) (: a 𝒞) (: i (→𝒞 b a))

(: |(→𝒞 i _)| (∀ ([x : 𝒞] [y : 𝒞]) (→ (→𝒞 x y) (→ (→𝒞 a x) (→𝒞 b y)))))

(define (|(→𝒞 i _)| j)

(define |(→𝒞 i j)| (λ (f) (∘𝒞 j f i)))

|(→𝒞 i j)|)

Exercise: For a morphism j : x → y : 𝒞. Prove that Hom𝒞(-, j) is a hom natural transformation from Hom𝒞(-, x) to Hom𝒞(-, y).

(: 𝒞 𝐂𝐚𝐭) (: x 𝒞) (: y 𝒞) (: j (→𝒞 x y))

(: |(→𝒞 _ j)| (∀ ([a : 𝒞] [b : 𝒞]) (→ (→𝒞 b a) (→ (→𝒞 a x) (→𝒞 b y)))))

(define (|(→𝒞 _ j)| i)

(define |(→𝒞 i j)| (λ (f) (∘𝒞 j f i)))

|(→𝒞 i j)|)

To verify the properties of natural transformations, we define some check procedures to automate the testing of the naturality a natural transformation has:

"code/natural_transformation/check.rkt"

#lang racket/base

(require rackunit)

(provide (all-defined-out))

(define (check-ntf 𝒞 𝒟)

(define-values (dom𝒞 cod𝒞 ∘𝒞 ?𝒞 =𝒞) (𝒞))

(define-values (dom𝒟 cod𝒟 ∘𝒟 ?𝒟 =𝒟) (𝒟))

(λ (F G)

(λ (α)

(λ (a b f)

(check-pred ?𝒞 a) (check-pred ?𝒟 (α a))

(check-pred ?𝒞 b) (check-pred ?𝒟 (α b))

(check-pred ?𝒞 f) (check-pred ?𝒟 (α f))

;; Naturality condition

(check-true (=𝒟 (dom𝒟 (α f)) (dom𝒟 (F f)) (F a)))

(check-true (=𝒟 (cod𝒟 (α f)) (cod𝒟 (G f)) (G b)))

(check-true (=𝒟 (α f) (∘𝒟 (α b) (F f)) (∘𝒟 (G f) (α a))))))))

The following example illustrates how to implement natural transformations in Racket:

"code/natural_transformation/Set=>Rel.rkt"

#lang typed/racket/base/no-check

(require "../category/Set.rkt"

"../category/Rel.rkt"

racket/promise)

(: 𝒮 𝐂𝐚𝐭)

(: dom𝒮 (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) a)))

(: cod𝒮 (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) b)))

(: ∘𝒮 (∀ ([a : 𝒮] [b : 𝒮] [c : 𝒮] ... [z : 𝒮]) (→ (× (→𝒮 a b) (→𝒮 b c) ...) (→𝒮 a z))))

(: ?𝒮 (pred (∀ ([a : 𝒮] [b : 𝒮]) (→𝒮 a b))))

(: =𝒮 (∀ ([a : 𝒮] [b : 𝒮] [c : 𝒮] [d : 𝒮] ...) (→ (× (→𝒮 a b) (→𝒮 c d) ...) Boolean)))

(define (𝒮 m) m)

(define-values (dom𝒮 cod𝒮 ∘𝒮 ?𝒮 =𝒮) (𝐒𝐞𝐭))

(: ℛ 𝐂𝐚𝐭)

(: domℛ (∀ ([a : ℛ] [b : ℛ]) (→ (→ℛ a b) a)))

(: codℛ (∀ ([a : ℛ] [b : ℛ]) (→ (→ℛ a b) b)))

(: ∘ℛ (∀ ([a : ℛ] [b : ℛ] [c : ℛ] ... [z : ℛ]) (→ (× (→ℛ a b) (→ℛ b c) ...) (→ℛ a z))))

(: ?ℛ (pred (∀ ([a : ℛ] [b : ℛ]) (→ℛ a b))))

(: =ℛ (∀ ([a : ℛ] [b : ℛ] [c : ℛ] [d : ℛ] ...) (→ (× (→ℛ a b) (→ℛ c d) ...) Boolean)))

(define (ℛ m) m)

(define-values (domℛ codℛ ∘ℛ ?ℛ =ℛ) (𝐑𝐞𝐥))

;; Functors from 𝒮 to ℛ

(: F (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) (→ℛ (F a) (F b)))))

(define F

(let ()

(define (F.map m) (for/set ([(x y) (in-hash m)]) (cons x y)))

(λ (f)

(define a (dom𝒮 f))

(define b (cod𝒮 f))

(define a.map (function-map a))

(define b.map (function-map b))

(define f.map (function-map f))

(define Fa (relation (lazy Fa) (lazy Fa) (F.map a.map)))

(define Fb (relation (lazy Fb) (lazy Fb) (F.map b.map)))

(define Ff (relation (lazy Fa) (lazy Fb) (F.map f.map)))

Ff)))

(: G (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) (→ℛ (G a) (G b)))))

(define G

(let ()

(define (G.map m) (for/set ([(x y) (in-hash m)]) (cons (list x) (list y))))

(λ (f)

(define a (dom𝒮 f))

(define b (cod𝒮 f))

(define a.map (function-map a))

(define b.map (function-map b))

(define f.map (function-map f))

(define Ga (relation (lazy Ga) (lazy Ga) (G.map a.map)))

(define Gb (relation (lazy Gb) (lazy Gb) (G.map b.map)))

(define Gf (relation (lazy Ga) (lazy Gb) (G.map f.map)))

Gf)))

;; Natural Transformations from F to G

(: α (∀ ([a : 𝒮] [b : 𝒮]) (→ (→𝒮 a b) (→ℛ (F a) (G b)))))

(define α

(let ()

(define (F.map m) (for/set ([(x y) (in-hash m)]) (cons       x        y)))

(define (G.map m) (for/set ([(x y) (in-hash m)]) (cons (list x) (list y))))

(define (α.map m) (for/set ([(x y) (in-hash m)]) (cons       x  (list y))))

(λ (f)

(define a (dom𝒮 f))

(define b (cod𝒮 f))

(define a.map (function-map a))

(define b.map (function-map b))

(define f.map (function-map f))

(define Fa (relation (lazy Fa) (lazy Fa) (F.map a.map)))

(define Gb (relation (lazy Gb) (lazy Gb) (G.map b.map)))

(define αf (relation (lazy Fa) (lazy Gb) (α.map f.map)))

αf)))

(module+ test

(require "check.rkt")

;; Objects in 𝒮

(: a 𝒮) (define a (function (lazy a) (lazy a) #hash([x0 . x0] [x1 . x1])))

(: b 𝒮) (define b (function (lazy b) (lazy b) #hash([y0 . y0] [y1 . y1])))

;; Morphisms in 𝒮

(: f (→𝒮 a b)) (define f (function (lazy a) (lazy b) #hash([x0 . y0] [x1 . y0])))

(define check-𝐒𝐞𝐭⇒𝐑𝐞𝐥 (check-ntf 𝐒𝐞𝐭 𝐑𝐞𝐥))

(define check-F⇒G (check-𝐒𝐞𝐭⇒𝐑𝐞𝐥 F G))

(define check-α (check-F⇒G α))

(check-α a b f))

3.1.1 Composition🔗ℹ

In this section, we explore two types of composition for natural transformations: horizontal composition and vertical composition. These forms of composition are fundamental to understanding how natural transformations interact and provide a deeper insight into their algebraic properties.

3.1.1.1 Horizontal Composition🔗ℹ

Given that natural transformations are defined as mappings of morphisms, it is natural to consider whether and how they can be composed, similar to the composition of functors. In fact, a key insight is that functors themselves can be viewed as special types of natural transformations. This leads us to define a type of composition for natural transformations, known as horizontal composition.

Consider two natural transformations α : F ⇒ G : 𝒞 → 𝒟 and β : H ⇒ K : 𝒟 → ℰ. The horizontal composition

β∘α : H∘F ⇒ K∘G : 𝒞 → ℰ

is a new natural transformation that, for each morphism f : a → b : 𝒞, maps it to

β∘α(f) = β(α(f)) : H∘F(a) → K∘G(b) : ℰ

Exercise: Prove α = α∘id𝒞 = id𝒟∘α.

Exercise: Show the types of H∘α, K∘α, β∘F, and β∘G.

We often omit the composition symbol ∘ when dealing with functors and natural transformations. For instance, β∘α(f) are typically simplified to βα(f) or βαf. This simplification makes it easier to reason about complex structures involving multiple functors and natural transformations, reducing visual clutter and improving readability.

Exercise: Prove that the horizontal composition of natural transformations ensures that the resulting diagram is commutative.

For βα, its type is HF ⇒ KG, where HF and KG are functors from 𝒞 to ℰ. Additionally, there are three important commutative squares associated with βα:

1. βα(f) : HF(f) ⇒ KG(f)

2. βα(f) : Hα(f) ⇒ Kα(f)

3. βα(f) : βF(f) ⇒ βG(f)

Note that Hα, Kα, βF, and βG are all natural transformations, not functors. These three commutative squares arise naturally because βα(f) is the body diagonal of a commutative cube, and there are precisely three faces of this cube whose face diagonals coincide with this body diagonal. Each of these faces also has a cube edge that starts from HF(a), which uniquely identifies them among all the cube’s faces:

Exercise: Prove that horizontal composition is associative.

3.1.1.2 Vertical Composition🔗ℹ

Since two adjacent commutative squares can themselves be composed to form a larger commutative square, it naturally suggests that two natural transformations that share a common functor can also be composed to form a new natural transformation. This leads us to define a type of composition for natural transformations, known as vertical composition.

Consider two natural transformations α : F ⇒ G : 𝒞 → 𝒟 and β : G ⇒ H : 𝒞 → 𝒟. The vertical composition

β∙α : F ⇒ H : 𝒞 → 𝒟

is a new natural transformation that, for each morphism f : a → b : 𝒞, maps it to

β∙α(f) : F(a) → H(b) : 𝒟

Exercise: Prove α = α∙F = G∙α.

Exercise: Prove that the vertical composition of natural transformations ensures that the resulting diagram is commutative.

Exercise: Prove that vertical composition is associative.

3.1.1.3 Interchange Law🔗ℹ

The interchange law states that if natural transformations can be composed both horizontally and vertically, then the natural transformations with identical domains and codomains yielded by distinct composition sequences must be equal.

To see why, observe that each composition sequence builds a larger commutative square by combining smaller squares from the naturality condition. Since all composite squares must be commutative, the diagonals of these larger squares are forced to coincide,

Consider the natural transformations α0 : F ⇒ G : 𝒞 → 𝒟, β0 : G ⇒ H : 𝒞 → 𝒟, α1 : K ⇒ L : 𝒟 → ℰ, and β1 : L ⇒ M : 𝒟 → ℰ. The commutative diagram below illustrates the relationships between them:

In some category theory texts, ∘ denotes vertical composition and ∗ denotes horizontal composition:

(β1∗β0)∘(α1∗α0) = (β1∘α1)∗(β0∘α0)

We can vertically compose α0 with β0, and α1 with β1, as well as horizontally compose α0 with α1, and β0 with β1. The IL states that the horizontal composition of two vertical compositions is equal to the vertical composition of two horizontal compositions. More precisely, the interchange law (IL) can be written as:

(β1∘β0)∙(α1∘α0) = (β1∙α1)∘(β0∙α0)

Here are some important commutative squares that arise:

1. (β1∘β0)∙(α1∘α0)(f) : KF(f) ⇒ MH(f)

2. (β1∙α1)∘(β0∙α0)(f) : KF(f) ⇒ MH(f)

3. (β1∙α1)∘(β0∙α0)(f) : K(β0∙α0)(f) ⇒ M(β0∙α0)(f)

4. (β1∙α1)∘(β0∙α0)(f) : (β1∙α1)F(f) ⇒ (β1∙α1)H(f)

3.1.2 Structure of 𝐂𝐚𝐭🔗ℹ

In the previous chapter, we introduced what we referred to as 𝐂𝐚𝐭, which consists of categories as objects and functors as morphisms. Strictly speaking, this was actually the base category of 𝐂𝐚𝐭, denoted by 𝐂𝐚𝐭ᵇ.

With the introduction of natural transformations, we can now see that functors are actually a special case of natural transformations. This observation reveals that the full structure of 𝐂𝐚𝐭 is richer and more complex compared to other categories, as it includes natural transformations in addition to functors.

The complete 𝐂𝐚𝐭 can be understood as being composed of two additional interrelated categories: the horizontal category and the vertical category. These categories give us deeper insights into the complex structure of 𝐂𝐚𝐭 and how the different components (categories, functors, and natural transformations) interact with each other.

In Racket, to distinguish between operations in the base category, horizontal category, and vertical category, we introduce the following notions:

• domᵇ, codᵇ, and ∘ for operations in 𝐂𝐚𝐭ᵇ

• domʰ, codʰ, and ∘ for operations in 𝐂𝐚𝐭ʰ

• domᵛ, codᵛ, and ∙ for operations in 𝐂𝐚𝐭ᵛ

3.1.2.1 Horizontal Category🔗ℹ

The horizontal category of 𝐂𝐚𝐭, denoted by 𝐂𝐚𝐭ʰ, can be viewed as an extension of 𝐂𝐚𝐭ᵇ. In 𝐂𝐚𝐭ᵇ, objects are categories and morphisms are functors between categories. In 𝐂𝐚𝐭ʰ, the objects remain the same but the morphisms are generalized to include all natural transformations between functors.

In 𝐂𝐚𝐭ʰ, horizontal composition serves as the composition operation for morphisms in it. This perspective allows us to see that horizontal composition essentially works like the composition of functions: both functors and natural transformations are kinds of functions between categories.

3.1.2.2 Vertical Category🔗ℹ

The vertical category of 𝐂𝐚𝐭, denoted by 𝐂𝐚𝐭ᵛ, provides a perspective that focuses on the relationships between functors through natural transformations. In 𝐂𝐚𝐭ᵛ, objects are functors between categories and morphisms are natural transformations between functors. An isomorphism α : F ⇒ G in 𝐂𝐚𝐭ᵛ is called a natural isomorphism, and F and G are naturally isomorphic to each other.

Exercise: Prove that a natural transformation α : F ⇒ G : 𝒞 → 𝒟 is a natural isomorphism iff each component of α is an isomorphism in 𝒟.

Exercise: For a natural isomorphism α : F ⇒ G : 𝒞 → 𝒟 and a morphism f : a → b : 𝒞. Prove F(f) = α–1(b)∘G(f)∘α(a) and G(f) = α(b)∘F(f)∘α–1(a).

In 𝐂𝐚𝐭ᵛ, vertical composition serves as the composition operation for morphisms in it. This perspective helps us understand why functors can be viewed as a special case of natural transformations.

Consider a functor category [𝒞 → 𝒟] (exponential category 𝒟𝒞), which has all the functors from 𝒞 to 𝒟 as objects, and all the natural transformations between those functors as morphisms. In this category, every functor F : 𝒞 → 𝒟 can be viewed as the identity natural transformation idF : F ⇒ F, which acts as the identity morphism.

Exercise: For objects 𝒜, ℬ, and 𝒞 in 𝐂𝐚𝐭. Prove the exponential laws:

• 𝒜0 ≅ 1𝒜 ≅ 1

• 𝒜1 ≅ 𝒜

• 𝒜𝒞×ℬ𝒞 ≅ (𝒜×ℬ)𝒞

• 𝒞𝒜×ℬ ≅ (𝒞ℬ)𝒜

• 𝒞𝒜+ℬ ≅ 𝒞𝒜×𝒞ℬ

Exercise: Think about what structure an endofunctor category [𝒞 → 𝒞] exhibits when considering horizontal composition.

Exercise: Try to define make-vertical-compose so that we can define the compose operator in 𝒟𝒞 like this:

(define ∙ (make-vertical-compose 𝒞 𝒟))

3.2 Comma Category🔗ℹ

In previous content, we examined how natural transformations provide a framework for studying relationships between two functors with the same domain and codomain. Now, we consider a more general question: can we use a similar structure to investigate functors with different domains but the same codomain?

As a function that maps morphisms, a natural transformation α : F ⇒ G : 𝒞 → 𝒟 establishes a relationship between F and G through the naturality condition. Specifically, for each morphism f in 𝒞, α(f) corresponds uniquely to a commutative square. In this sense, studying the relationship between F and G via α essentially constructs an arrow category, where objects are the components of α, and morphisms are the commutative squares that satisfy the naturality condition.

Inspired by this approach, we can investigate the relationship between two functors F: 𝒞 → ℰ and G: 𝒟 → ℰ by constructing an arrow category that represents the interactions between F and G. In such a category, objects are triples (a, x, α), where a is an object in 𝒞, x is an object in 𝒟, and α : F(a) → G(x) is a morphism in ℰ. The morphisms in this category are pairs (i, j), where i : a → b is a morphism in 𝒞 and j : x → y is a morphism in 𝒟, such that the following diagram is commutative:

This category is called a comma category of F and G, denoted by F/G (F↓G).

Exercise: Try using comma category to define arrow category and (co)slice category.

To explore the relationships between F/G, 𝒞, 𝒟, and ℰ, we introduce two forgetful functors HF : F/G → 𝒞 and HG : F/G → 𝒟. HF maps (a, x, α) to a and (i, j) to i, while HG maps (a, x, α) to x and (i, j) to j. Furthermore, these functors are connected by a natural transformation θ : F∘HF ⇒ G∘HG, which maps (a, x, α) to α.

Building on the earlier motivation, we saw that comma categories can be used to study relationships between two functors with the same codomain. Since natural transformations describe relationships between functors with the same domain and codomain, it is natural to explore their connection with comma categories.

Given a natural transformation α : F ⇒ G : 𝒞 → 𝒟, we can construct a functor A : 𝒞 → F/G such that HF∘A = HG∘A = id𝒞. Conversely, given such a functor A, we can construct a natural transformation α.

3.3 Yoneda Lemma🔗ℹ

Philosophically speaking, one might say that the essence of an entity lies in the totality of its relationships with other entities. In category theory, this idea extends to morphisms, which can be seen as fundamental "entities" within a category.

We can express this concept by examining the relationships between a morphism f : a → x in a category 𝒞 and other morphisms in 𝒞. Specifically, we use the natural transformations

Hom𝒞(f, -) : Hom𝒞(x, -) ⇒ Hom𝒞(a, -) : 𝒞 → 𝐒𝐞𝐭

and

Hom𝒞(-, f) : Hom𝒞(-, a) ⇒ Hom𝒞(-, x) : 𝒞op → 𝐒𝐞𝐭

to describe how f interacts with other morphisms in 𝒞.

This naturally leads us to ask about the connection between f, Hom𝒞(f, -), and Hom𝒞(-, f). The Yoneda Lemma, a cornerstone of category theory, addresses this question by establishing that these perspectives are in one-to-one correspondence with each other.

The Yoneda Lemma sets up a one-to-one correspondence between elements of F(S), where S : 𝒞 and F : 𝒞 → 𝐒𝐞𝐭, and variable elements of F, parametrized by Hom𝒞(S, -). Specifically, an element s ∈ F(S) uniquely corresponds to a natural transformation ρ : Hom𝒞(S, -) ⇒ F.

To better understand the Yoneda Lemma, let’s revisit the TDFA ℳ defined in Typed Deterministic Finite Automaton. We denote the free category of the typed alphabet 𝒢 as 𝒞, and let F : 𝒞 → 𝐒𝐞𝐭 represent the typed action φ*. In this context, consider the run function, which takes an input sequence w and returns a final state F(w)(s0) after processing w, starting from the start state s0.

According to the Yoneda Lemma, we see that each component of a natural transformation ρ : Hom𝒞(S, -) ⇒ F at an object T : 𝒞 can be understood as a run function starting from a state s ∈ F(S):

∀w ∈ Hom𝒞(S, T), ρ(T)(w) = F(w)(s)

Here, F(T) can be interpreted as the set of final states.

To illustrate this correspondence, we use Racket code to define two procedures: s->ρ and ρ->s. They demonstrate how an element s of F(S) can be transformed into a natural transformation ρ, and vice versa, providing a concrete way to visualize the one-to-one correspondence described by the Yoneda Lemma.

"code/natural_transformation/s<->run.rkt"

#lang typed/racket/base/no-check

(require "../../exercises/functor/make-path.rkt"

(only-in "../functor/TDFA.rkt" 𝒢 [F𝒢 𝒞]))

(require/typed "../functor/TDFA.rkt"

[(φ* F) (∀ ([X : 𝒞] [Y : 𝒞]) (→ (→𝒞 X Y) (→ (F X) (F Y))))])

(module+ test (require rackunit))

(define-values (dom𝒞 cod𝒞 ∘𝒞 ?𝒞 =𝒞) (𝒞))

(: S 𝒞) (define S (make-path 𝒢 'S0 ""))

(: |(→𝒞 S _)| (∀ ([X : 𝒞] [Y : 𝒞]) (→ (→𝒞 X Y) (→ (→𝒞 S X) (→𝒞 S Y)))))

(define (|(→𝒞 S _)| j)

(define |(→𝒞 S j)| (λ (f) (∘𝒞 j f)))

|(→𝒞 S j)|)

(: s->ρ (→ (F S) (⇒ |(→𝒞 S _)| F)))

(define (s->ρ s)

(: ρ (∀ ([X : 𝒞] [Y : 𝒞]) (→ (→𝒞 X Y) (→ (→𝒞 S X) (F Y)))))

(define (ρ j) (λ (f) ((F (∘𝒞 j f)) s)))

ρ)

(: ρ->s (→ (⇒ |(→𝒞 S _)| F) (F S)))

(define (ρ->s ρ)

(define s ((ρ S) S))

s)

(module+ test

(for ([s (in-list '(s0 a0 r0))])

(define ρ (s->ρ s))

(check-eq? s (ρ->s ρ))

(for ([w (in-list (list (make-path 𝒢 'S0 "1xyxyxx")))])

(define T (cod𝒞 w))

(check-eq? ((ρ T) w) ((F w) s)))))

This correspondence also holds for contravariant hom functors. There is a one-to-one correspondence between elements of G(T), where T : 𝒞op and G : 𝒞op → 𝐒𝐞𝐭, and variable elements of G, parametrized by Hom𝒞(-, T). Specifically, an element t ∈ G(T) uniquely corresponds to a natural transformation ρ : Hom𝒞(-, T) ⇒ G.

Exercise: Try to define two procedures using Racket code: t->ρ and ρ->t.

Forgetful functors to 𝐒𝐞𝐭 are very often representable.

The definition of the Yoneda Lemma can be generalized by replacing the hom functor Hom𝒞(S, -) with any functor that is naturally isomorphic to it. Such a functor is called a representable functor and we say that S represents this functor.

Exercise: For a functor F : 𝒞 → 𝐒𝐞𝐭. Prove that if objects a and x in 𝒞 both represent F, then a ≅ x.

3.3.1 Yoneda Embedding🔗ℹ

The Yoneda Lemma establishes a powerful correspondence: a natural transformation ρ : Hom𝒞(S, -) ⇒ F uniquely corresponds to an element s ∈ F(S). By carefully selecting functor F, we can choose to study specific entities within the corresponding set F(S) and examine the relationship between these entities and natural transformations.

For example, if we let F be a hom functor, then the elements of F(S) are precisely the morphisms in 𝒞 that start from or end to S. An important corollary of the Yoneda Lemma is that any natural transformation between hom functors in a category 𝒞 must be a hom natural transformation because it corresponds exactly to a morphism in 𝒞.

To illustrate this, consider two hom functors Hom𝒞(x, −) and Hom𝒞(a, −), where a and x are objects in 𝒞. According to the Yoneda Lemma, an element f ∈ Hom𝒞(a, x), which is also a morphism in 𝒞, uniquely corresponds to the hom natural transformation Hom𝒞(f, -) : Hom𝒞(x, -) ⇒ Hom𝒞(a, -).

This shows that any natural transformation between hom functors is directly determined by a morphism in 𝒞. Thus, the Yoneda Lemma establishes a one-to-one correspondence between a morphism f and a hom natural transformation Hom𝒞(f, -).

Exercise: Show the one-to-one correspondence between f and Hom𝒞(-, f).

Exercise: Prove that f is an isomorphism in 𝒞 iff Hom𝒞(f, -) is a natural isomorphism, and iff Hom𝒞(-, f) is a natural isomorphism.

Building on the correspondence established by the Yoneda Lemma, we can define a functor Y : 𝒞op → [𝒞 → 𝐒𝐞𝐭] that maps each object a : 𝒞 to the covariant hom functor Hom𝒞(a, -), and each morphism i : b → a : 𝒞 to the hom natural transformation Hom𝒞(i, -) : Hom𝒞(a, -) ⇒ Hom𝒞(b, -). This functor is known as the Yoneda embedding for 𝒞.

(: Y (∀ ([a : 𝒞] [b : 𝒞]) (→ (→𝒞 b a) (∀ ([x : 𝒞] [y : 𝒞]) (→ (→𝒞 x y) (→ (→𝒞 a x) (→𝒞 b y)))))))

(define Y (curry |(→𝒞 _ _)|))

Exercise: Prove that Y is an embedding.

Here is another Yoneda embedding J : 𝒞 → [𝒞op → 𝐒𝐞𝐭] that maps each object x : 𝒞 to the contravariant hom functor Hom𝒞(-, x), and each morphism j : x → y : 𝒞 to the hom natural transformation Hom𝒞(-, j) : Hom𝒞(-, x) ⇒ Hom𝒞(-, y).

(: J (∀ ([x : 𝒞] [y : 𝒞]) (→ (→𝒞 x y) (∀ ([a : 𝒞] [b : 𝒞]) (→ (→𝒞 b a) (→ (→𝒞 a x) (→𝒞 b y)))))))

(define J (curryr |(→𝒞 _ _)|))

Exercise: Prove that J is an embedding.

In Cayley’s Theorem, we explored the categorical version of Cayley’s theorem, which provides a way to represent an object b : 𝒞 via the functor H, such that H(b) = ∐a∈𝒞0Hom𝒞(a, b).

Building on this idea, the Yoneda embedding generalizes Cayley’s theorem. The functor J represents an object b : 𝒞 as a hom functor, such that J(b) = Hom𝒞(-, b). Moreover, any representable functors naturally isomorphic to Hom𝒞(-, b) can also be used to represent b.

The Yoneda embedding has interesting connections to programming paradigms, such as Continuation-Passing Style (CPS). Specifically, when applied to 𝐒𝐞𝐭, the Yoneda embedding J maps a set x to the endofunctor Hom𝐒𝐞𝐭(-, x), which encapsulates computations that use functions as continuations to produce results in x.

To illustrate this, consider a result type x. In Typed Racket, the type of J(x) can be expressed as: (∀ (a b) (→ (→ b a) (→ (→ a x) (→ b x)))). By uncurrying it, we obtain a procedure cps:

(: cps (∀ (a b) (→ (→ b a) (→ b (→ a x) x))))

(define (cps i) (λ (m k) (k (i m))))