Homotopy Type Theory functor precategory > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

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

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\mathrm{idtoiso}:(idF=G)\to (F\cong G)$ \idtoiso:(\id{F}{G}) idtoiso:({F}={G}) \to (F\cong G) is an equivalence.equivalence.

To give an inverse to it, suppose $\gamma:F\cong G$ is a natural isomorphism. Then for any$a:A$natural isomorphism , . we Then have for an any isomorphism${\gamma }_{a}a:\mathrm{<span><del\; class="diffmod">\; Fa</del><ins\; class="diffmod">\; A</ins></span>}\cong \mathrm{Ga}$ \gamma_a:Fa a:A \cong Ga , hence we have an identity$\isotoid(\gamma_a):\id{Fa}{Ga}$isomorphism? . By function extensionality, we have an identity$\overline{\gamma }{\gamma }_a:idF[a<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; \cong </ins></span>A_{0}G\to a{B}_0)]F_0{G}_0$ \bar{\gamma}:\id[(A_0\to \gamma_a:F B_0)]{F_0}{G_0} a \cong G a, hence an identity $isotoid(\gamma_a):{F a}={G a}$. 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$\id{F}{G}$functor it are will suffice to show that for any$a,b:A$mere propositions?, to show that ${F}={G}$ it will suffice to show that for any $a,b:A$, the functions

$$G_{a,b}:hom_A(a,b) \to hom_B(G a,G b)$$

become equal when transported along $F_{a,b} hom_A(a,b) \to hom_B(Fa,Fb)\mathrlap{\qquad\text{and}}\\\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$.

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 $F f:hom_B(F a,F b)$ along $isotoid(\gamma_a)$ and $isotoid(\gamma_b)$ is equal to the composite $\gamma_b\circ F f\circ \inv{(\gamma_a)}$, which by naturality of $\gamma$ is equal to $G f$.

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

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

(1)$$(\id F G) \to (F\cong G) \to (\id F G).$$

$$(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:\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.

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 $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 ${\bar\gamma}={p}$, which is what we need.

Finally, consider the composite

Since identity of natural transformations can be tested componentwise, it suffices to show that for each$a$natural transformations we can have be tested componentwise, it suffices to show that for each$idaidtoiso(\overline{\gamma }{)}_a{\gamma }_a$ \id{\idtoiso(\bar\gamma)_a}{\gamma_a} a . But as observed above, we have$id\mathrm{idtoiso}(\overline{\gamma }{)}_{a}idtoiso(\overline{\gamma }{)}_a=idtoiso{\gamma }_a((\overline{\gamma }{)}_a)$ \id{\idtoiso(\bar\gamma)_a}{\idtoiso((\bar\gamma)_a)} {idtoiso(\bar\gamma)_a}={\gamma_a} , . while But as observed above, we have$id\mathrm{idtoiso}(\overline{\gamma }{)}_a(\overline{\gamma }{)}_a=isotoid\mathrm{idtoiso}({\gamma }_a(\overline{\gamma }{)}_a)$ \id{(\bar\gamma)_a}{\isotoid(\gamma_a)} {idtoiso(\bar\gamma)_a}={idtoiso((\bar\gamma)_a)} , by while computation for function extensionality. Since$isotoid(\overline{\gamma }{)}_a=\mathrm{isotoid}({\gamma }_a)$ \isotoid {(\bar\gamma)_a}={isotoid(\gamma_a)} and by computation for function extensionality. Since$idtoiso\mathrm{isotoid}$ \idtoiso isotoid are and inverses, we have$id\mathrm{idtoiso}idtoiso(\overline{\gamma }{)}_a{\gamma }_a$ \id{\idtoiso(\bar\gamma)_a}{\gamma_a} idtoiso are inverses, we have ${idtoiso(\bar\gamma)_a}={\gamma_a}$ as desired.

See also

Category theory functor category Rezk completion

References

HoTT Book