9.2 Functors and transformations

The following definitions are fairly obvious, and need no modification.

Definition 9.2.1.

Let $A$ and $B$ be precategories. A functor $F\mathrm{:}A\mathrm{\to }B$ consists of

1. A function $F_0:A_0\to B_0$, generally also denoted $F$.

2. For each $a,b:A$, a function $F_{a,b}:{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_B(Fa,Fb)$, generally also denoted $F$.

3. For each $a:A$, we have $F(1_a)=1_{Fa}$.

4. For each $a,b,c:A$ and $f:{\mathrm{hom}}_A(a,b)$ and $g:{\mathrm{hom}}_B(b,c)$, we have

   $$F(g\circ f)=Fg\circ Ff.$$

Note that by induction on identity, a functor also preserves $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}$.

Definition 9.2.2.

For functors $F\mathrm{,}G\mathrm{:}A\mathrm{\to }B$, a natural transformation $\gamma \mathrm{:}F\mathrm{\to }G$ consists of

1. For each $a:A$, a morphism ${\gamma }_a:{\mathrm{hom}}_B(Fa,Ga)$ (the “components”).

2. For each $a,b:A$ and $f:{\mathrm{hom}}_A(a,b)$, we have $Gf\circ {\gamma }_a={\gamma }_b\circ Ff$ (the “naturality axiom”).

Since each type ${\mathrm{hom}}_B(Fa,Gb)$ is a set, its identity type is a mere proposition. Thus, the naturality axiom is a mere proposition, so identity of natural transformations is determined by identity of their components. In particular, for any $F$ and $G$, the type of natural transformations from $F$ to $G$ is again a set.

Similarly, identity of functors is determined by identity of the functions $A_0\to B_0$ and (transported along this) of the corresponding functions on hom-sets.

Definition 9.2.3.

For precategories $A\mathrm{,}B$, there is a precategory $B^A$ defined by

• ${(B^A)}_0$ is the type of functors from $A$ to $B$.

• ${\mathrm{hom}}_{B^A}(F,G)$ is the type of natural transformations from $F$ to $G$.

Proof.

We define ${(1_F)}_a:\equiv 1_{Fa}$. Naturality follows by the unit axioms of a precategory. For $\gamma :F\to G$ and $\delta :G\to H$, we define ${(\delta \circ \gamma )}_a:\equiv {\delta }_a\circ {\gamma }_a$. Naturality follows by associativity. Similarly, the unit and associativity laws for $B^A$ follow from those for $B$. ∎

Lemma 9.2.4.

A natural transformation $\gamma \mathrm{:}F\mathrm{\to }G$ is an isomorphism in $B^A$ if and only if each ${\gamma }_a$ is an isomorphism in $B$.

Proof.

If $\gamma$ is an isomorphism, then we have $\delta :G\to F$ that is its inverse. By definition of composition in $B^A$, ${(\delta \gamma )}_a\equiv {\delta }_a{\gamma }_a$ and similarly. Thus, $\delta \gamma =1_F$ and $\gamma \delta =1_G$ imply ${\delta }_a{\gamma }_a=1_{Fa}$ and ${\gamma }_a{\delta }_a=1_{Ga}$, so ${\gamma }_a$ is an isomorphism.

Conversely, suppose each ${\gamma }_a$ is an isomorphism, with inverse called ${\delta }_a$, say. We define a natural transformation $\delta :G\to F$ with components ${\delta }_a$; for the naturality axiom we have

$$Ff\circ {\delta }_a={\delta }_b\circ {\gamma }_b\circ Ff\circ {\delta }_a={\delta }_b\circ Gf\circ {\gamma }_a\circ {\delta }_a={\delta }_b\circ Gf.$$

Now since composition and identity of natural transformations is determined on their components, we have $\gamma \delta =1_G$ and $\delta \gamma =1_F$. ∎

The following result is fundamental.

Theorem 9.2.5.

If $A$ is a precategory and $B$ is a category, then $B^A$ is a category.

Proof.

Let $F,G:A\to B$; we must show that $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}:(F=G)\to (F\cong G)$ is an equivalence.

To give an inverse to it, suppose $\gamma :F\cong G$ is a natural isomorphism. Then for any $a:A$, we have an isomorphism ${\gamma }_a:Fa\cong Ga$, hence an identity $\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}({\gamma }_a):Fa=Ga$. By function extensionality, we have an identity $\overline{\gamma }:F_0{=}_{(A_0\to B_0)}{G}_0$.

Now since the last two axioms of a functor are mere propositions, to show that $F=G$ it will suffice to show that for any $a,b:A$, the functions

$F_{a,b}$ $:{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_B(Fa,Fb)\mathit{\hspace{1em}\hspace{1em}}\text{and}$

$G_{a,b}$ $:{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_B(Ga,Gb)$

become equal when transported along $\overline{\gamma }$. By computation for function extensionality, when applied to $a$, $\overline{\gamma }$ becomes equal to $\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}({\gamma }_a)$. But by ct:idtoiso-trans, transporting $Ff:{\mathrm{hom}}_B(Fa,Fb)$ along $\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}({\gamma }_a)$ and $\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}({\gamma }_b)$ is equal to the composite ${\gamma }_b\circ Ff\circ {({\gamma }_a)}^{-1}$, which by naturality of $\gamma$ is equal to $Gf$.

This completes the definition of a function $(F\cong G)\to (F=G)$. Now consider the composite

$$(F=G)\to (F\cong G)\to (F=G).$$

Since hom-sets are sets, their identity types are mere propositions, so to show that two identities $p,q:F=G$ are equal, it suffices to show that $p{=}_{F_0=G_0}q$. But in the definition of $\overline{\gamma }$, if $\gamma$ were of the form $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(p)$, then ${\gamma }_a$ would be equal to $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}(p_a)$ (this can easily be proved by induction on $p$). Thus, $\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}({\gamma }_a)$ would be equal to $p_a$, and so by function extensionality we would have $\overline{\gamma }=p$, which is what we need.

Finally, consider the composite

$$(F\cong G)\to (F=G)\to (F\cong G).$$

Since identity of natural transformations can be tested componentwise, it suffices to show that for each $a$ we have $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\overline{\gamma })}_a={\gamma }_a$. But as observed above, we have $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\overline{\gamma })}_a=\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}({(\overline{\gamma })}_a)$, while ${(\overline{\gamma })}_a=\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}({\gamma }_a)$ by computation for function extensionality. Since $\mathrm{𝗂𝗌𝗈𝗍𝗈𝗂𝖽}$ and $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}$ are inverses, we have $\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}{(\overline{\gamma })}_a={\gamma }_a$ as desired. ∎

In particular, naturally isomorphic functors between categories (as opposed to precategories) are equal.

We now define all the usual ways to compose functors and natural transformations.

Definition 9.2.6.

For functors $F\mathrm{:}A\mathrm{\to }B$ and $G\mathrm{:}B\mathrm{\to }C$, their composite $G\mathrm{\circ }F\mathrm{:}A\mathrm{\to }C$ is given by

• The composite $(G_0\circ F_0):A_0\to C_0$

• For each $a,b:A$, the composite

  $$(G_{Fa,Fb}\circ F_{a,b}):{\mathrm{hom}}_A(a,b)\to {\mathrm{hom}}_C(GFa,GFb).$$

It is easy to check the axioms.

Definition 9.2.7.

For functors $F\mathrm{:}A\mathrm{\to }B$ and $G\mathrm{,}H\mathrm{:}B\mathrm{\to }C$ and a natural transformation $\gamma \mathrm{:}G\mathrm{\to }H$, the composite $\mathrm{(}\gamma \mathit{}F\mathrm{)}\mathrm{:}G\mathit{}F\mathrm{\to }H\mathit{}F$ is given by

• For each $a:A$, the component ${\gamma }_{Fa}$.

Naturality is easy to check. Similarly, for $\gamma$ as above and $K\mathrm{:}C\mathrm{\to }D$, the composite $\mathrm{(}K\mathit{}\gamma \mathrm{)}\mathrm{:}K\mathit{}G\mathrm{\to }K\mathit{}H$ is given by

• For each $b:B$, the component $K({\gamma }_b)$.

Lemma 9.2.8.

For functors $F\mathrm{,}G\mathrm{:}A\mathrm{\to }B$ and $H\mathrm{,}K\mathrm{:}B\mathrm{\to }C$ and natural transformations $\gamma \mathrm{:}F\mathrm{\to }G$ and $\delta \mathrm{:}H\mathrm{\to }K$, we have

$$(\delta G)(H\gamma )=(K\gamma )(\delta F).$$

Proof.

It suffices to check componentwise: at $a:A$ we have

${((\delta G)(H\gamma ))}_a$ $\equiv {(\delta G)}_a{(H\gamma )}_a$

$\equiv {\delta }_{Ga}\circ H({\gamma }_a)$

$=K({\gamma }_a)\circ {\delta }_{Fa}$ (by naturality of $\delta$)

$\equiv {(K\gamma )}_a\circ {(\delta F)}_a$

$\equiv {((K\gamma )(\delta F))}_a.\mathit{∎}$

Classically, one defines the “horizontal composite” of $\gamma :F\to G$ and $\delta :H\to K$ to be the common value of $(\delta G)(H\gamma )$ and $(K\gamma )(\delta F)$. We will refrain from doing this, because while equal, these two transformations are not definitionally equal. This also has the consequence that we can use the symbol $\circ$ (or juxtaposition) for all kinds of composition unambiguously: there is only one way to compose two natural transformations (as opposed to composing a natural transformation with a functor on either side).

Lemma 9.2.9.

Composition of functors is associative: $H\mathit{}\mathrm{(}G\mathit{}F\mathrm{)}\mathrm{=}\mathrm{(}H\mathit{}G\mathrm{)}\mathit{}F$.

Proof.

Since composition of functions is associative, this follows immediately for the actions on objects and on homs. And since hom-sets are sets, the rest of the data is automatic. ∎

The equality in ct:functor-assoc is likewise not definitional. (Composition of functions is definitionally associative, but the axioms that go into a functor must also be composed, and this breaks definitional associativity.) For this reason, we need also to know about coherence for associativity.

Lemma 9.2.10.

ct:functor-assoc is coherent, i.e. the following pentagon of equalities commutes:

Proof.

As in ct:functor-assoc, this is evident for the actions on objects, and the rest is automatic. ∎

We will henceforth abuse notation by writing $H\circ G\circ F$ or $HGF$ for either $H(GF)$ or $(HG)F$, transporting along ct:functor-assoc whenever necessary. We have a similar coherence result for units.

Lemma 9.2.11.

For a functor $F\mathrm{:}A\mathrm{\to }B$, we have equalities $\mathrm{(}{\mathrm{1}}_B\mathrm{\circ }F\mathrm{)}\mathrm{=}F$ and $\mathrm{(}F\mathrm{\circ }{\mathrm{1}}_A\mathrm{)}\mathrm{=}F$, such that given also $G\mathrm{:}B\mathrm{\to }C$, the following triangle of equalities commutes.

See ct:pre2cat,ct:2cat for further development of these ideas.

Title	9.2 Functors and transformations