Natural transformations

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Natural transformations

Given two parallel functors F, G : K → K⁰, a natural transformation from F to G τ : F → G

is a family τ = hτ_A: F(A) → G(A)i_A∈|K| of K⁰-morphisms such that for all f : A → B in K (with A, B ∈ |K|), τ_A;G(f ) = F(f );τ_B

Then, τ is a natural isomorphism if for all A ∈ |K|, τ_A is an isomorphism.

K: K⁰:

A F(A) G(A)

B F(B) G(B)

τ_A -

τ_B -

? f

? F(f )

? G(f )

Andrzej Tarlecki: Category Theory, 2021 - 95 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

For all f : X → Y ,

sing_X;P(f ) = Id_Set(f );sing_Y , i.e. sing_X; ~f = f ;sing_Y ,

i.e. for x ∈ X, ~f ({x}) = {f (x)}.

X Id_Set(X) -P(X) sing_X

Y Id_Set(Y ) -P(Y ) sing_Y

? f

? Id_Set(f )

? P(f )

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

For all f : X → Y ,

sing_X;P(f ) = Id_Set(f );sing_Y , i.e. sing_X; ~f = f ;sing_Y ,

i.e. for x ∈ X, ~f ({x}) = {f (x)}.

X Id_Set(X) -P(X) sing_X

Y Id_Set(Y ) -P(Y ) sing_Y

? f

? Id_Set(f )

? P(f )

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

For all f : X → Y ,

sing_X;P(f ) = Id_Set(f );sing_Y , i.e. sing_X; ~f = f ;sing_Y ,

i.e. for x ∈ X, ~f ({x}) = {f (x)}.

X X - 2^X

sing_X

Y Y - 2^Y

sing_Y

? f

? f

? f~

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

For all f : X → Y ,

sing_X;P(f ) = Id_Set(f );sing_Y , i.e. sing_X; ~f = f ;sing_Y ,

i.e. for x ∈ X, f ({x}) = {f (x)}.~

X X - 2^X

sing_X

Y Y - 2^Y

sing_Y

? f

? f

? f~

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

• singleton-list functions: sing^List: Id_Set → |List| ( : Set → Set), where

|List| = List;| | : Set(→ Monoid) → Set, and for all X ∈ |Set|,

sing^List_X : X → X∗ is a function defined by sing^List_X (x) = hxi for x ∈ X

• append functions: append : |List|;CP → |List| ( : Set → Set), where for all X ∈ |Set|, append_X : (X∗ × X∗) → X∗ is the usual append function (list concatenation) polymorphic functions between algebraic types

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

• singleton-list functions: sing^List: Id_Set → |List| ( : Set → Set), where

|List| = List;| | : Set(→ Monoid) → Set, and for all X ∈ |Set|,

sing^List_X : X → X∗ is a function defined by sing^List_X (x) = hxi for x ∈ X

• append functions: append : |List|;CP → |List| ( : Set → Set), where for all X ∈ |Set|, append_X : (X∗ × X∗) → X∗ is the usual append function (list concatenation) polymorphic functions between algebraic types

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Examples

• identity transformations: id_F: F → F, where F : K → K⁰ , for all objects A ∈ |K|, (id_F)_A = id_A: F(A) → F(A)

• singleton functions: sing : Id_Set → P ( : Set → Set), where for all X ∈ |Set|, sing_X : X → P(X) is a function defined by sing_X(x) = {x} for x ∈ X.

• singleton-list functions: sing^List: Id_Set → |List| ( : Set → Set), where

|List| = List;| | : Set(→ Monoid) → Set, and for all X ∈ |Set|,

sing^List_X : X → X∗ is a function defined by sing^List_X (x) = hxi for x ∈ X

• append functions: append : |List|;CP → |List| ( : Set → Set), where for all X ∈ |Set|, append_X : (X∗ × X∗) → X∗ is the usual append function (list concatenation) polymorphic functions between algebraic types

X X∗ × X∗ X∗

Y Y ∗ × Y ∗ Y ∗

- append_X

- append_Y

? f

? f ∗ × f ∗

? f ∗

Andrzej Tarlecki: Category Theory, 2021 - 96 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T , built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T , built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

· [[α_i]](X₁, . . . , X_n) = X_i

· [[int]](X₁, . . . , X_n) = {. . . , −2, −1, 0, 1, 2, . . .}

· [[T₁ × T₂]](X₁, . . . , X_n) = [[T₁]](X₁, . . . , X_n) × [[T₂]](X₁, . . . , X_n)

· [[T₁ + T₂]](X₁, . . . , X_n) = [[T₁]](X₁, . . . , X_n) + [[T₂]](X₁, . . . , X_n)

· · · ·

· . . . recursive type definitions work as well. . .

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

− argue that in a representative subset of Standard ML, for each polymorphic expression E : ∀α₁ . . . α_n · T → T⁰ its semantics is a natural transformation [[E]] : [[T ]] → [[T⁰]]

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

− argue that in a representative subset of Standard ML, for each polymorphic expression E : ∀α₁ . . . α_n · T → T⁰ its semantics is a natural transformation [[E]] : [[T ]] → [[T⁰]]

· by induction on the structure of well-typed expressions

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

− argue that in a representative subset of Standard ML, for each polymorphic expression E : ∀α₁ . . . α_n · T → T⁰ its semantics is a natural transformation [[E]] : [[T ]] → [[T⁰]]

− Then for f₁: X₁ → Y₁, . . . , f_n: X_n → Y_n:

[[T ]](f₁, . . . , f_n);[[E]]_hY1,...,Yni = [[E]]_hX1,...,Xni;[[T⁰]](f₁, . . . , f_n)

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

− argue that in a representative subset of Standard ML, for each polymorphic expression E : ∀α₁ . . . α_n · T → T⁰ its semantics is a natural transformation [[E]] : [[T ]] → [[T⁰]]

− Then for f₁: X₁ → Y₁, . . . , f_n: X_n → Y_n:

[[T ]](f₁, . . . , f_n);[[E]]_hY1,...,Yni = [[E]]_hX1,...,Xni;[[T⁰]](f₁, . . . , f_n) For instance, for rev : α list → α list,

even : int → bool and l : int list:

rev (even∗(l)) = even∗(rev (l))

Theorems for free!

(see Wadler 89)

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Polymorphic functions

Work out the following generalisation of the last two examples:

− for each algebraic type scheme ∀α₁ . . . α_n · T, built in Standard ML using at least products and algebraic data types (no function types though), define the corresponding functor [[T ]] : Setⁿ → Set

− argue that in a representative subset of Standard ML, for each polymorphic expression E : ∀α₁ . . . α_n · T → T⁰ its semantics is a natural transformation [[E]] : [[T ]] → [[T⁰]]

− Then for f₁: X₁ → Y₁, . . . , f_n: X_n → Y_n:

[[T ]](f₁, . . . , f_n);[[E]]_hY1,...,Yni = [[E]]_hX1,...,Xni;[[T⁰]](f₁, . . . , f_n) For instance, for rev : α list → α list,

even : int → bool and l : int list:

rev (even∗(l)) = even∗(rev (l))

Theorems for free!

(see Wadler 89)

Andrzej Tarlecki: Category Theory, 2021 - 97 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A) EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A) EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A) EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A) EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A)

EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A)

EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Yoneda lemma

Given a locally small category K, functor F : K → Set and object A ∈ |K|:

Nat (Hom_K(A, ), F) ∼= F(A)

natural transformations from Hom_K(A, ) to F, between functors from K to Set, are given exactly by the elements of the set F(A)

EXERCISES:

• Dualise: for G : K^op → Set,

Nat (Hom_K( , A), G) ∼= G(A) .

• Characterise all natural transformations from Hom_K(A, ) to Hom_K(B, ), for all objects A, B ∈ |K|.

Andrzej Tarlecki: Category Theory, 2021 - 98 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

Note: F(f ) : F(A) → F(B) in Set, so F(f )(a) ∈ F(B).

F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

- τ_A

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ :

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Proof

• For a ∈ F(A), define τ^a : Hom_K(A, ) → F, as the family of functions

τ_B^a : K(A, B) → F(B), B ∈ |K|, given by τ_B^a(f ) = F(f )(a) for f : A → B in K.

This is a natural transformation, since for g : B → C and then f : A → B, F(g)(τ_B^a(f ))= F(g)(F(f )(a))

= F(f ;g)(a) = τ_C^a(f ;g)

= τ_C^a(Hom_K(A, g)(f ))

Then τ_A^a(id_A) = a, and so for distinct a, a⁰ ∈ F(A), τ^a and τ^a0 differ.

K: Set:

B K(A, B) F(B)

C K(A, C) F(C)

- τ_B^a

- τ_C^a

? g

?

( );g = Hom_K(A, g)

? F(g)

• If τ : Hom_K(A, ) → F is a natural transformation then τ = τ^a, where we put a = τ_A(id_A), since for B ∈ |K| and f : A → B, τ_B(f ) = F(f )(τ_A(id_A)) by naturality of τ:

A K(A, A) F(A)

B K(A, B) F(B)

τ_A -

τ_B -

? f

?

( );f = Hom_K(A, f )

? F(f )

Andrzej Tarlecki: Category Theory, 2021 - 99 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Compositions

vertical composition:

From:

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ to:

K K⁰

 

? F

 6

F⁰⁰

ñññññññò

τ ;σ

horizontal composition:

From:

K K⁰

 

? F

 6

F⁰

ñññññññò

τ K⁰⁰

 

? G

 6

G⁰

ñññññññò

σ

to:

K

 

? F;G

 6

F⁰;G⁰

ñññññññò

τ ·σ K⁰⁰

Andrzej Tarlecki: Category Theory, 2021 - 100 -

Vertical composition

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ

The vertical composition of natural transformations τ : F → F⁰ and σ : F⁰ → F⁰⁰ between parallel functors F, F⁰, F⁰⁰: K → K⁰

τ ;σ : F → F⁰⁰

is a natural transformation given by (τ ;σ)_A = τ_A;σ_A for all A ∈ |K|.

K: K⁰:

A F(A) F⁰(A) F⁰⁰(A)

B F(B) F⁰(B) F⁰⁰(B)

τ_A -

- τ_B

σ_A -

- σ_B

? f

? F(f )

? F⁰(f )

?

F⁰⁰(f )

Andrzej Tarlecki: Category Theory, 2021 - 101 -

Vertical composition

K K⁰

 

? F

F⁰-

 6

F⁰⁰

ññò

τ

ññò

σ

The vertical composition of natural transformations τ : F → F⁰ and σ : F⁰ → F⁰⁰ between parallel functors F, F⁰, F⁰⁰: K → K⁰

τ ;σ : F → F⁰⁰

is a natural transformation given by (τ ;σ)_A = τ_A;σ_A for all A ∈ |K|.

K: K⁰:

A F(A) F⁰(A) F⁰⁰(A)

B F(B) F⁰(B) F⁰⁰(B)

τ_A -

- τ_B

σ_A -

- σ_B

? f

? F(f )

? F⁰(f )

?

F⁰⁰(f )

Andrzej Tarlecki: Category Theory, 2021 - 101 -