Index of the slides:

Program (1) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Program (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Functions, explicitly . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Functions that return functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Groups as structure plus properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Groups as structure plus properties (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Groups as structure plus properties (3) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Categories as structure plus properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 Categories as structure plus properties (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Set as a category . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Finite subcategories of Set, explicitly . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Well-positioned subsets of ℕ^{2} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Well-positioned subsets of ℕ^{2} (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 BPM(K) is not a protocategory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 BPM^{∗}(K) is a protocategory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 BPM*(K) is a category . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .17 Two categories generated by graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Commutative diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Coherence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .20 A terminal object in Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Products in Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Terminals, categorically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Products, categorically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 A category without products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Terminals are isomorphic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Products are isomorphic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .27 A category without terminals and products . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Categories with terminals and products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .29 A functor in Set: Ax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 A natural transformation in Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Exponentials in Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .32 Exponentials, categorically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Adjoints are isomorphic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2. Program (1)

(Original draft, oct/2011...)

(1) Categorias como "estrutura" (objetos, Hom, identidade, composiç~ ao)
e "propriedades" (a composiç~ ao é associativa, identidades se
comportam como deveriam). Comparaç~ ao com grupos, anéis, etc;
"dependent types".
(2) Nossas categorias preferidas: Set, categorias finitas dadas
explicitamente, posets, categorias de grupos, anéis, espaços
topológicos, categorias de subobjetos.
(3) Funtores e transformaç~ oes naturais. Diagramas e condiç~ oes de
coer^encia. Introduç~ ao ao lambda-cálculo tipado (em Set). Notaç~ ao
lambda para morfismos. Beta-reduç~ ao (para composiç~ ao). Produtos de
objetos. Produtos como "estrutura" + "propriedades". Prova de que
dois produtos P e P' s~ ao isomorfos. Como deixar em segundo plano a
prova de que as compostas P->P'->P e P'->P->P' s~ ao identidades.
Como isolar as "construç~ oes". Análise de provas do MacLane, do
Awodey e do Beck.
(4) Categorias cartesianas. A linguagem interna de uma categoria
cartesiana: uplas e projeç~ oes. Traduç~ ao entre linguagem interna e
linguagem categórica.
(5) Uma categoria cartesiana abstrata: a CC livre gerada pelos objetos
A_1,...,A_n. A definiç~ ao formal (categórica) de "livre".
(6) Os funtores (×B) e (B->) em Set. A adjunç~ ao (×B)-|(B->). Adjunç~ oes
como "estrutura" e "propriedades". Proto-adjunç~ oes (só a parte
"estrutura" das adjunç~ oes). Unidades e counidades. O teorema sobre
vários modos equivalentes de especificar uma adjunç~ ao. Categorias
cartesianas fechadas ("CCC"s). A linguagem interna de uma CCC.
Traduç~ ao entre linguagem interna e linguagem categórica. Em que
sentido esta traduç~ ao é "fiel".

3. Program (2)

(7) Adjunç~ oes em posets. Como calcular "P->Q" num certo poset. Posets
como espaços de valores de verdade. Cálculo proposicional num
poset. Como calcular a "coimplicaç~ ao" neste poset. A relaç~ ao entre
adjunç~ oes e produtos.
(8) A traduç~ ao entre cálculo de seqüentes, deduç~ ao natural e operaç~ oes
numa CCC. Uma traduç~ ao correspondente para lambda-cálculo.
Curry-Howard. Reduç~ oes em demonstraç~ oes em deduç~ ao natural.
(9) Outros posets nos quais podemos fazer cálculo proposicional
(intuicionista). Categorias de funtores. Categorias da forma 2^D,
onde D é um poset finito "plano". Representaç~ ao gráfica explícita
dos objetos destas categorias. Valores de verdade como subobjetos.
Lógica modal (S4) nestas categorias. "Necessário" como "interior".
Cálculo proposicional num espaço topológico qualquer.
(10) Introduç~ ao à noç~ ao de "feixe": coberturas, colagens, duas noç~ oes
de saturaç~ ao. Categorias da forma Set^D ("prefeixes"). Exemplos de
prefeixes que s~ ao e que n~ ao s~ ao feixes.
(11) O classificador de subobjetos em categorias da forma Set^D.
Introduç~ ao à linguagem interna de um topos.
(12) O lema de Yoneda (vers~ ao "proto"). Funtores representáveis.
(13) M^onadas e álgebras. As categorias de Kleisli e Eilenberg-Moore de
uma m^onada. O teorema da comparaç~ ao (vers~ ao "proto").
(14) M^onadas em linguagens funcionais.
(15) Morfismos geométricos num caso particular. Feixificaç~ ao num caso
particular.

4. Functions, explicitly

The two functions below,

\begin{aligned}f & : & ℕ & → & ℕ \\ & & n & ↦ & 3 + n \end{aligned}

and

\begin{aligned}g & : & ℕ & → & ℕ \\ & & n & ↦ & 1 + (n + 2) \end{aligned}

are mathematically the \underline{same} function, even though they are \underline{syntactically different} and they correspond to different algorithms...

Mathematicians tend to think that functions \underline{are} their graphs — i.e., sets of ordered pairs.

For example, if

\begin{aligned}h & : & ℕ & → & ℕ \\ & & n & ↦ & 10n \end{aligned}

Then h = {(2, 20), (3, 30)}. We will often write this as \begin{matrix}2↦20 \\ 3↦30 \end{matrix}

or as \{ \begin{matrix}2↦20 \\ 3↦30 \end{matrix} \}.

5. Functions that return functions

We will often have to deal with functions that return functions. For example:

\begin{aligned}m & : & \{2, 3\} & → & ℕ^{\{10,100\}} \\ & & a & ↦ & \binom{m_{a} : \{10, 100\} → ℕ}{b ↦ ab} \end{aligned}

Then (m(2))(10) = m_{2}(10) = 2 · 10 = 20, m = {(2, m_{2}), (3, m_{3})}, m = {(2, {(10, 20), (100, 200)}), (3, {(10, 20), (100, 200)})}.

Using the other notation,

m = \{ \begin{matrix}2↦\{ \begin{matrix}10↦20 \\ 100↦200 \end{matrix} \} \\ 3↦\{ \begin{matrix}10↦30 \\ 100↦300 \end{matrix} \} \end{matrix} \}

6. Groups as structure plus properties

A group G is (formally) a tuple, whose components are:

• an underlying set, usually also called G,

• a binary operation, · : G × G → G,

• an identity element, e ∈ G,

• a unary operation, (·)^{−1} : G → G,

• the guarantee that e “behaves as expected”,

• the guarantee that · “behaves as expected”,

• the guarantee that (·)^{−1} “behaves as expected”.

So: G = (G, ·, e, (·)^{−1}; idLR, assoc, invLR), where: idLR ≡ (∀a ∈ G. ea = a) ∧ (∀a ∈ G. ae = a), assoc ≡ (∀a ∈ G. ∀b ∈ G. ∀c ∈ G. a(bc) = (ab)c), invLR ≡ (∀a ∈ G. aa^{−1} = e) ∧ (∀a ∈ G. a^{−1}a = e),

Let’s clean this up... G = (G_{0}, ·, e, (·)^{−1}; idLR, assoc, invLR), where:

• G_{0} : Sets,

• e : G_{0},

• · : G_{0} × G_{0} → G_{0},

• (·)^{−1} : G_{0} → G_{0},

• idLR is a proof of (∀a ∈ G_{0}. ea = a) ∧ (∀a ∈ G_{0}. ae = a),

• assoc is a proof of (∀a ∈ G_{0}. ∀b ∈ G_{0}. ∀c ∈ G_{0}. a(bc) = (ab)c),

• invLR is a proof of (∀a ∈ G_{0}. aa^{−1} = e) ∧ (∀a ∈ G_{0}. a^{−1}a = e).

More generally: G = (G_{0}, ·_{G}, e_{G}, (·)_{G}^{−1}; idLR_{G}, assoc_{G}, invLR_{G}).

7. Groups as structure plus properties (2)

G = (G_{0}, ·, e, (·)^{−1}; idLR, assoc, invLR), where:

• G_{0} : Sets,

• e : G_{0},

• · : G_{0} × G_{0} → G_{0},

• (·)^{−1} : G_{0} → G_{0},

• idLR is a proof of (∀a ∈ G_{0}. ea = a) ∧ (∀a ∈ G_{0}. ae = a),

• assoc is a proof of (∀a ∈ G_{0}. ∀b ∈ G_{0}. ∀c ∈ G_{0}. a(bc) = (ab)c),

• invLR is a proof of (∀a ∈ G_{0}. aa^{−1} = e) ∧ (∀a ∈ G_{0}. a^{−1}a = e).

Constructing (exhibiting) a group G means:

• choosing a set G_{0},

• choosing an element e : G_{0}

• choosing a function · : G_{0} × G_{0} → G_{0}

• choosing a function (·)^{−1} : G_{0} → G_{0},

• proving that (∀a ∈ G_{0}. ea = a) ∧ (∀a ∈ G_{0}. ae = a),

• proving that (∀a ∈ G_{0}. ∀b ∈ G_{0}. ∀c ∈ G_{0}. a(bc) = (ab)c),

• proving that (∀a ∈ G_{0}. aa^{−1} = e) ∧ (∀a ∈ G_{0}. a^{−1}a = e).

Note: ‘:’ is roughly the same as ‘∈’, so e : G_{0} is roughly the same as e ∈ G_{0}; Sets is the class of all sets (the “set of all sets”), so G_{0} : Sets means that G_{0} is a set; A → B will be regarded as the set B^{A}, so f : A → B means f ∈ B^{A}, i.e., f is an element of the set of all functions from A to B.

8. Groups as structure plus properties (3)

Fact 1: when we see the name of an object we often know which type it is expected to have. (We will not formalize this!)

Fact 2: it is possible to define the set of proofs of (∀a ∈ G_{0}. ea = a) ∧ (∀a ∈ G_{0}. ae = a), and then say: idLR : Proofs[(∀a ∈ G_{0}. ea = a) ∧ (∀a ∈ G_{0}. ae = a)]. (We will not formalize this, either.)

Fact 3: it is sometimes sufficient to say just this, G = (G_{0}, ·, e, (·)^{−1}; idLR, assoc, invLR), and our interlocutors will be able to figure out by themselves the (implicit) types of all the components.

The first four components of the tuple G = (G_{0}, ·, e, (·)^{−1}; idLR, assoc, invLR) will be called the “structure” part of G; their types involve just known objects (the class Sets), and ‘:’, ‘×’, ‘→’.

Note that after ‘G_{0} : Sets’ the value of G_{0} is a “known object”, and the declaration ‘· : G_{0} × G_{0} → G_{0}’ makes sense.

The last three components of the tuple G = (G_{0}, ·, e, (·)^{−1}; idLR, assoc, invLR) will be called the “properties” part of G; their types involve ‘Proofs’, quantifiers, equalities, equations...

Conventions:

• a ‘;’ separates the “structure” from the “properties”

• G = (G_{0}, ·, e, (·)^{−1}; idLR, assoc, invLR) is a group,

• G^{−} = (G_{0}, ·, e, (·)^{−1}) is a proto-group;

• each definition of a structure will have a corresponding proto-structure.

9. Categories as structure plus properties

Informally, a Category is a directed graph in which the arrows can be composed (when they “match”), the composition is associative, and we have identity arrows, that behave as expected.

A bit more formally: C = {C_{0}, Hom_{C}, ∘_{C}, id_{C}; assoc_{C}, idLR_{C}} where:

• C_{0} is the set of vertices,

• Hom_{C}(A, B) is the set of arrows from A to B,

• for any A, B, C ∈ C_{0} we have

∘_{C ABC} : Hom_{C}(B, C) × Hom_{C}(A, B) → Hom_{C}(A, C)
(g_{BC}, f_{AB})  ↦ g_{BC} ∘ f_{AB}

[figure: A; B; f_{AB}; B; C; g_{BC}; A; C; g_{BC}∘f_{AB}; A; C; f_{AB};g_{BC}]

• for any A ∈ C_{0} we have an “identity arrow” id_{C}(A) ∈ Hom_{C}(A, B),

• for any A, B, C, D ∈ C_{0} and arrows f_{AB}, g_{BC}, h_{CD} we have:

[figure: A; B; f_{AB}; B; C; g_{BC}; C; D; h_{CD}; A; C; f_{AB};g_{BC}; B; D; g_{BC};h_{CD}; A; D; f_{AB};(g_{BC};h_{CD})=(f_{AB};g_{BC});h_{CD}]

• for any A, B ∈ C_{0} and f_{AB} we have id_{A}; f_{AB} = f_{AB} = f_{AB}; id_{B}.

[figure: A; B; f_{AB}; A; _{id_{A}}; B; _{id_{B}}]

10. Categories as structure plus properties (2)

C = {C_{0}, Hom, ∘, id; assoc, idLR}, where:

• C_{0} : Sets (in our “small categories”)

• Hom : C_{0} × C_{0} → Set

• for any A, B, C we have ∘_{ABC} : Hom(B, C) → Hom(A, B) → Hom(A, C)

• for any A we have id(A) : Hom(A, A)

• assoc is a proof of

∀A, B, C, D, f_{AB}, g_{BC}, h_{CD}. (f_{AB}; g_{BC}); h_{CD} = f_{AB}; (g_{BC}; h_{CD})

• idLR is a proof of ∀A, B, f_{AB}. id_{A}; f_{AB} = f_{AB} = f_{AB}; id_{B} 11. Set as a category

Our archetypical category is Set.

• Set_{0} = Sets (the objects of Set are sets),

• Hom_{Set}(A, B) = the set of all functions from A to B,

• f ∘_{Set} g is the composition of functions, f ∘ g

• id_{Set}(A) is the identity map id_{A} : A → A.

[EXERCISE: prove assoc_{Set} and idLR_{Set}].

When we look at Set as a graph (with composition and ids), it is a HUGE graph — to many vertices, too many arrows. Let’s see two simple ways to define smaller categories.

12. Finite subcategories of Set, explicitly

A subcategory of C ⊂ Set is one in which:

• C_{0} ⊂ Set_{0},

• for any A, B ∈ C_{0} we have Hom_{C}(A, B) ⊂ Hom_{Set}(A, B),

• the operations ∘_{C} and id_{C} and “inherited” from Set.

For example, let C be:

[figure: \{2, 3\}; \{4, 5, 6\}; \begin{matrix}2↦4 \\ 3↦5 \end{matrix}; \{2, 3\}; \{4, 5, 6\}; \begin{matrix}2↦5 \\ 3↦4 \end{matrix}; \{4, 5, 6\}; \{7, 8\}; \begin{matrix}4↦7 \\ 5↦7 \\ 6↦8 \end{matrix}; \{4, 5, 6\}; \{7, 8\}; \begin{matrix}4↦7 \\ 5↦7 \\ 6↦7 \end{matrix}; \{2, 3\}; \{7, 8\}; \begin{matrix}2↦7 \\ 3↦7 \end{matrix}]

(The identity maps are not shown).

In this example C_{0} = { {2, 3}, {4, 5, 6}, {7, 8} },

Hom_{C}(\{2, 3\}, \{4, 5, 6\}) = \{ \begin{matrix}2↦4 \\ 3↦5 \end{matrix} , \begin{matrix}2↦5 \\ 3↦4 \end{matrix} \},

Hom_{C}(\{2, 3\}, \{2, 3\}) = \{ \begin{matrix}2↦2 \\ 3↦3 \end{matrix} \},

etc.

13. Well-positioned subsets of ℕ^{2}

By abuse of language, let’s write ‘ℕ^{2}’ for ℕ + iℕ and ‘ℤ^{2}’ for ℤ + iℤ.

Example: α = 1 + 3i β = 0 + 2i γ = 2 + 2i δ = 1 + 1i ϵ = 1 + 0i

Let K = { α, β, γ, δ, ϵ } ⊂ ℕ^{2} (mnemonic: \underline{K}ite).

[figure: (1 + 3i); (0 + 2i); (1 + 3i); (2 + 2i); (0 + 2i); (1 + 1i); (2 + 2i); (1 + 1i); (1 + 1i); (1 + 0i); α; β; α; γ; β; δ; γ; δ; δ; ϵ]

We will say that a subset D ⊂ ℤ^{2} is well-positioned when inf(ℜ𝔢(D)) = 0 and inf(ℑ𝔪(D)) = 0.

inf(ℜ𝔢(K)) = inf(ℜ𝔢({α, β, γ, δ, ϵ}))
= inf({1, 0, 2, 1, 1})
= 0
inf(ℑ𝔪(K)) = inf(ℑ𝔪({α, β, γ, δ, ϵ}))
= inf({3, 2, 2, 1, 0})
= 0

K is well-positioned.

14. Well-positioned subsets of ℕ^{2} (2)

Def: an ℕ^{2}-set is a finite, well-positioned subset of ℕ^{2}. We will denote ℕ^{2}-sets (with few elements) by bullet diagrams:

K = ^{•}^{•}^{•}_{•}_{•}, V =^{•}^{•} •.

Def: to list the elements of an ℕ^{2}-set in reading order is to list them from top to bottom, and from left to right. Example: K = { α, β, γ, δ, ϵ }.

[figure: (1 + 3i); (0 + 2i); (1 + 3i); (2 + 2i); (0 + 2i); (1 + 1i); (2 + 2i); (1 + 1i); (1 + 1i); (1 + 0i); α; β; α; γ; β; δ; γ; δ; δ; ϵ]

We are interested in regarding ℕ^{2}-sets as (the vertices of) directed (acyclical) graphs.

Def: an arrow z → w between points of ℕ^{2} is a black pawn’s move when it moves at most one unit horizontally and exactly one unit down; black pawn’s moves are short arrows of shape ↙, ↓ or ↘.

The set of black pawn’s moves \underline{on a subset} D ⊂ ℕ^{2}, BPM(D), is defined in the obvious way:

BPM(D) = { (z, w) ∈ D^{2} | z → w is a black pawn’s move }.

Example: BPM(K) = {α → β, α → γ, β → δ, γ → δ, δ → ϵ}.

15. BPM(K) is not a protocategory

...because BPM(K) is just a set of arrows, not a tuple of the form {K_{0}, Hom, ∘, id; assoc, idLR}... What happens when we try to fix this?

Let’s try:

• K_{0} = {α, β, γ, δ, ϵ}

• Hom_{K}(α, β) = {(α, β)}, Hom_{K}(α, δ) = { }, ...

16. BPM^{∗}(K) is a protocategory 17. BPM*(K) is a category 18. Two categories generated by graphs 19. Commutative diagrams 20. Coherence In a linear diagram like

[figure: A; B; f_{AB}; B; C; f_{BC}; C; D; f_{CD}; D; E; f_{DE}; A; _{id_{A}}; B; _{id_{B}}; C; _{id_{C}}; D; _{id_{D}}; E; _{id_{E}}]

all ways to define an arrow that “deserves the name f_{AE}” give the same result.

[EXPLAIN WD]

In a planar diagram like the one below, in which each cell commutes, i.e., wd[f_{AE}], wd[f_{BF}], wd[f_{DH}], wd[f_{EI}], all ways to define an arrow that “deserves the name f_{AI}” give the same result.

[figure: A; B; f_{AB}; B; C; f_{BC}; D; E; f_{DE}; E; F; f_{EF}; G; H; f_{GH}; H; I; f_{HI}; A; D; f_{AD}; D; G; f_{DG}; B; E; f_{BE}; E; H; f_{EH}; C; F; f_{CF}; F; I; f_{F I}]

[EXERCISES] 21. A terminal object in Set

Standard definition: A terminal object in C is an object T ∈ C such that for each object A ∈ C there is exactly one map (called t_{A}) from A to T.

Equivalent definition: A terminal in C is a triple (T, t; uniq) where:

• T ∈ C,

• for each A ∈ C we have that t(A) is a map from A to T,

• uniq is a proof for ∀A. ∀f_{AT} . f_{AT} = t(A).

Fact 1: {200} is a terminal object in Set. EXERCISE: find the unique map from {2, 3, 4} to {200}. EXERCISE: T, t, uniq { 8 } is a terminal in Set.

22. Products in Set

[figure: \{1, 2\}; \{3, 4\}; \begin{matrix}1↦3 \\ 2↦4 \end{matrix}; \{1, 2\}; \{ \begin{matrix}35,36 \\ 45,46 \end{matrix} \}; \begin{matrix}1↦35 \\ 2↦45 \end{matrix}; \{1, 2\}; \{5, 6\}; \begin{matrix}1↦5 \\ 2↦5 \end{matrix}; \{ \begin{matrix}35,36 \\ 45,46 \end{matrix} \}; \{3, 4\}; \begin{matrix}35↦3 \\ 36↦3 \\ 45↦4 \\ 46↦4 \end{matrix}; \{ \begin{matrix}35,36 \\ 45,46 \end{matrix} \}; \{5, 6\}; \begin{matrix}35↦5 \\ 36↦6 \\ 45↦5 \\ 46↦6 \end{matrix}]

23. Terminals, categorically 24. Products, categorically 25. A category without products 26. Terminals are isomorphic 27. Products are isomorphic 28. A category without terminals and products 29. Categories with terminals and products 30. A functor in Set: Ax 31. A natural transformation in Set 32. Exponentials in Set 33. Exponentials, categorically 34. Adjunctions 35. Adjoints are isomorphic