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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}$.
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 homsets.
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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}:(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{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}({\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)\text{mathrlap}\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{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}({\gamma}_{a})$. But by \autorefct:idtoisotrans, transporting $Ff:{\mathrm{hom}}_{B}(Fa,Fb)$ along $\mathrm{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}({\gamma}_{a})$ and $\mathrm{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}({\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 homsets 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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}(p)$, then ${\gamma}_{a}$ would be equal to $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({p}_{a})$ (this can easily be proved by induction on $p$). Thus, $\mathrm{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}({\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{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\overline{\gamma})}_{a}={\gamma}_{a}$. But as observed above, we have $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\overline{\gamma})}_{a}=\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}({(\overline{\gamma})}_{a})$, while ${(\overline{\gamma})}_{a}=\mathrm{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}({\gamma}_{a})$ by computation for function extensionality. Since $\mathrm{\U0001d5c2\U0001d5cc\U0001d5c8\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5bd}$ and $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}$ are inverses, we have $\mathrm{\U0001d5c2\U0001d5bd\U0001d5cd\U0001d5c8\U0001d5c2\U0001d5cc\U0001d5c8}{(\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{\u220e}$ 
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 homsets are sets, the rest of the data is automatic. ∎
The equality in \autorefct:functorassoc 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.
\autorefct:functorassoc is coherent, i.e. the following pentagon of equalities commutes:
$$\text{xymatrix}\mathrm{\&}K(H(GF))\text{ar}\mathrm{@}=[dl]\text{ar}\mathrm{@}=[dr](KH)(GF)\text{ar}\mathrm{@}=[d]\mathrm{\&}\mathrm{\&}K((HG)F)\text{ar}\mathrm{@}=[d]((KH)G)F\mathrm{\&}\mathrm{\&}(K(HG))F\text{ar}\mathrm{@}=[ll]$$ 
Proof.
As in \autorefct:functorassoc, 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:functorassoc 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.
$$\text{xymatrix}G\circ ({1}_{B}\circ F)\text{ar}\mathrm{@}=[rr]\text{ar}\mathrm{@}=[dr]\mathrm{\&}\mathrm{\&}(G\circ {1}_{B})\circ F\text{ar}\mathrm{@}=[dl]\mathrm{\&}G\circ F.$$ 
See \autorefct:pre2cat,\autorefct:2cat for further development of these ideas.
Title  9.2 Functors and transformations 

\metatable 