* table of contents {:toc} ## Definition ## For [[precategories]] $A,B$, there is a [[precategory]] $B^A$, called the **functor precategory**, 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_{F a}$. 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$. ## Properties ## ### Lemma 9.2.4 ### A natural transformation $\gamma : F \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$. Thus, $\delta \gamma = 1_F$ and $\gamma \delta=1_G$ imply that $\delta_a \gamma_a = 1_{F a}$ and $\gamma_a \delta_a = 1_{G a}$, so $\gamma_a$ is an isomorphism. Conversely, suppose each $\gamma_a$ is an [[isomorphism]], with inverse called $\delta_a$. We define a [[natural transformation]] $\delta : G \to F$ with components $\delta_a$; for the naturality axiom we have $$F f \circ \delta_a=\delta_b \circ \gamma_b \circ F f \circ \delta_a = \delta_b \circ G f \circ \gamma_a \circ \delta_a = \delta_b \circ G f$$ Now since composition and identity of [[natural transformations]] is determined on their components, we have $\gamma \delta=1_G$ and $\delta \gamma 1_F.\ \square$ ### 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 $\idtoiso:(\id{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 $\isotoid(\gamma_a):\id{Fa}{Ga}$. By function extensionality, we have an identity $\bar{\gamma}:\id[(A_0\to B_0)]{F_0}{G_0}$. Now since the last two axioms of a functor are mere propositions, to show that $\id{F}{G}$ it will suffice to show that for any $a,b:A$, the functions $$ F_{a,b} hom_A(a,b) \to hom_B(Fa,Fb)\mathrlap{\qquad\text{and}}\\ G_{a,b}&: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 $\isotoid(\gamma_a)$. But by \cref{ct:idtoiso-trans}, transporting $Ff:hom_B(Fa,Fb)$ along $\isotoid(\gamma_a)$ and $\isotoid(\gamma_b)$ is equal to the composite $\gamma_b\circ Ff\circ \inv{(\gamma_a)}$, which by naturality of $\gamma$ is equal to $Gf$. This completes the definition of a function $(F\cong G) \to (\id F G)$. Now consider the composite \[ (\id F G) \to (F\cong G) \to (\id F G). \] Since hom-sets are sets, their identity types are mere propositions, so to show that two identities $p,q:\id F G$ are equal, it suffices to show that $\id[\id{F_0}{G_0}]{p}{q}$. But in the definition of $\bar\gamma$, if $\gamma$ were of the form $\idtoiso(p)$, then $\gamma_a$ would be equal to $\idtoiso(p_a)$ (this can easily be proved by induction on $p$). Thus, $\isotoid(\gamma_a)$ would be equal to $p_a$, and so by function extensionality we would have $\id{\bar\gamma}{p}$, which is what we need. Finally, consider the composite \[(F\cong G)\to (\id 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 $\id{\idtoiso(\bar\gamma)_a}{\gamma_a}$. But as observed above, we have $\id{\idtoiso(\bar\gamma)_a}{\idtoiso((\bar\gamma)_a)}$, while $\id{(\bar\gamma)_a}{\isotoid(\gamma_a)}$ by computation for function extensionality. Since $\isotoid$ and $\idtoiso$ are inverses, we have $\id{\idtoiso(\bar\gamma)_a}{\gamma_a}$ as desired. ## See also ## [[Category theory]] [[functor]] [[category]] [[Rezk completion]] ## References ## [[HoTT Book]] category: category theory