# 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 $F:A\to B$ consists of

1. 1.

$F_{0}:A_{0}\to B_{0}$, generally also denoted $F$.

2. 2.

For each $a,b:A$, a function $F_{a,b}:\hom_{A}(a,b)\to\hom_{B}(Fa,Fb)$, generally also denoted $F$.

3. 3.

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

4. 4.

For each $a,b,c:A$ and $f:\hom_{A}(a,b)$ and $g:\hom_{B}(b,c)$, we have

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

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

1. 1.

For each $a:A$$\gamma_{a}:\hom_{B}(Fa,Ga)$ (the “components”).

2. 2.

For each $a,b:A$ and $f:\hom_{A}(a,b)$, we have $Gf\circ\gamma_{a}=\gamma_{b}\circ Ff$ (the “naturality axiom”).

Since each type $\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,B$, there is a precategory $B^{A}$ defined by

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

• $\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$. ∎

###### 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 $\mathsf{idtoiso}:(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 $\mathsf{isotoid}(\gamma_{a}):Fa=Ga$. By function extensionality, we have an identity $\bar{\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

 $\displaystyle F_{a,b}$ $\displaystyle:\hom_{A}(a,b)\to\hom_{B}(Fa,Fb)\mathrlap{\qquad\text{and}}$ $\displaystyle G_{a,b}$ $\displaystyle:\hom_{A}(a,b)\to\hom_{B}(Ga,Gb)$

become equal when transported along $\bar{\gamma}$. By computation for function extensionality, when applied to $a$, $\bar{\gamma}$ becomes equal to $\mathsf{isotoid}(\gamma_{a})$. But by \autorefct:idtoiso-trans, transporting $Ff:\hom_{B}(Fa,Fb)$ along $\mathsf{isotoid}(\gamma_{a})$ and $\mathsf{isotoid}(\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 $\bar{\gamma}$, if $\gamma$ were of the form $\mathsf{idtoiso}(p)$, then $\gamma_{a}$ would be equal to $\mathsf{idtoiso}(p_{a})$ (this can easily be proved by induction on $p$). Thus, $\mathsf{isotoid}(\gamma_{a})$ would be equal to $p_{a}$, and so by function extensionality we would have $\bar{\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 $\mathsf{idtoiso}(\bar{\gamma})_{a}=\gamma_{a}$. But as observed above, we have $\mathsf{idtoiso}(\bar{\gamma})_{a}=\mathsf{idtoiso}((\bar{\gamma})_{a})$, while $(\bar{\gamma})_{a}=\mathsf{isotoid}(\gamma_{a})$ by computation for function extensionality. Since $\mathsf{isotoid}$ and $\mathsf{idtoiso}$ are inverses, we have $\mathsf{idtoiso}(\bar{\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:A\to B$ and $G:B\to C$, their composite $G\circ F:A\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}):\hom_{A}(a,b)\to\hom_{C}(GFa,GFb).$

It is easy to check the axioms.

###### Definition 9.2.7.

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

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

Naturality is easy to check. Similarly, for $\gamma$ as above and $K:C\to D$, the composite $(K\gamma):KG\to KH$ is given by

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

###### Lemma 9.2.8.

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

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

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

 $\displaystyle((\delta G)(H\gamma))_{a}$ $\displaystyle\equiv(\delta G)_{a}(H\gamma)_{a}$ $\displaystyle\equiv\delta_{Ga}\circ H(\gamma_{a})$ $\displaystyle=K(\gamma_{a})\circ\delta_{Fa}{}$ (by naturality of $\delta$) $\displaystyle\equiv(K\gamma)_{a}\circ(\delta F)_{a}$ $\displaystyle\equiv((K\gamma)(\delta F))_{a}.\qed$

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(GF)=(HG)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 \autorefct: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.
\autoref

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

 $\xymatrix{&K(H(GF))\ar@{=}[dl]\ar@{=}[dr]\\ (KH)(GF)\ar@{=}[d]&&K((HG)F)\ar@{=}[d]\\ ((KH)G)F&&(K(HG))F\ar@{=}[ll]}$
###### Proof.

As in \autorefct: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 \autorefct:functor-assoc whenever necessary. We have a similar coherence result for units.

###### Lemma 9.2.11.

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

 $\xymatrix{G\circ(1_{B}\circ F)\ar@{=}[rr]\ar@{=}[dr]&&(G\circ 1_{B})\circ F\ar% @{=}[dl]\\ &G\circ F.}$

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

Title 9.2 Functors and transformations
\metatable