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

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

Definition

For precategories A,BA,B, there is a precategory B AB^A, called the functor precategory, defined by

Proof. We define (1 F) a1 Fa(1_F)_a \equiv 1_{F a}. Naturality follows by the unit axioms of a precategory. For γ:FG\gamma : F \to G and δ:GH\delta : G \to H, we define (δγ) aδ aγ a(\delta \circ \gamma)_a \equiv \delta_a \circ \gamma_a. Naturality follows by associativity. Similarly, the unit and associativity laws for B AB^A follow from those for BB.

Properties

Lemma 9.2.4

A natural transformation γ:FG\gamma : F \to G is an isomorphism in B AB^A if and only if each γ a\gamma_a is an isomorphism in BB.

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

Conversely, suppose each γ a\gamma_a is an isomorphism?, with inverse called δ a\delta_a. We define a natural transformation δ:GF\delta : G \to F with components δ a\delta_a; for the naturality axiom we have

Ffδ a=δ bγ bFfδ a=δ bGfγ aδ a=δ bGfF 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 γδ=1 G\gamma \delta=1_G and δγ1 F.\delta \gamma 1_F.\ \square

Theorem 9.2.5

If AA is a precategory and BB is a category, then B AB^A is a category.

Proof. Let F,G:ABF,G:A\to B; we must show that idtoisoidtoiso:(idF=G)(FG) \idtoiso:(\id{F}{G}) idtoiso:({F}={G}) \to (F\cong G) is an equivalence.equivalence.

To give an inverse to it, suppose γ:FG\gamma:F\cong G is a natural isomorphism. Then for anya:Aa:Anatural isomorphism , . we Then have for an any isomorphismγ aa: Fa AGa \gamma_a:Fa a:A \cong Ga , hence we have an identityisotoid(γ a):idFaGa\isotoid(\gamma_a):\id{Fa}{Ga}isomorphism? . By function extensionality, we have an identityγ¯γ a:idF[a (A 0GaB 0)]F 0G 0 \bar{\gamma}:\id[(A_0\to \gamma_a:F B_0)]{F_0}{G_0} a \cong G a, hence an identity isotoid(γ a):Fa=Gaisotoid(\gamma_a):{F a}={G a}. By function extensionality, we have an identity γ¯:F 0= (A 0B 0)G 0\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 thatidFG\id{F}{G}functor it are will suffice to show that for anya,b:Aa,b:Amere propositions?, to show that F=G{F}={G} it will suffice to show that for any a,b:Aa,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) F a,b:hom A(a,b)hom B(Fa,Fb) F_{a,b}:hom_A(a,b) \to hom_B(F a,F b)
G a,b:hom A(a,b)hom B(Ga,Gb) 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 aa, γ¯\bar\gamma becomes equal to isotoid(γ a)\isotoid(\gamma_a). But by \cref{ct:idtoiso-trans}, transporting Ff:hom B(Fa,Fb)Ff:hom_B(Fa,Fb) along isotoid(γ a)\isotoid(\gamma_a) and isotoid(γ b)\isotoid(\gamma_b) is equal to the composite γ bFfinv(γ a)\gamma_b\circ Ff\circ \inv{(\gamma_a)}, which by naturality of γ\gamma is equal to GfGf.

become equal when transported along γ¯\bar\gamma. By computation for function extensionality, when applied to aa, γ¯\bar\gamma becomes equal to isotoid(γ a)isotoid(\gamma_a). But by \cref{ct:idtoiso-trans}, transporting Ff:hom B(Fa,Fb)F f:hom_B(F a,F b) along isotoid(γ a)isotoid(\gamma_a) and isotoid(γ b)isotoid(\gamma_b) is equal to the composite γ bFfinv(γ a)\gamma_b\circ F f\circ \inv{(\gamma_a)}, which by naturality of γ\gamma is equal to GfG f.

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

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

(1)(idFG)(FG)(idFG). (\id F G) \to (F\cong G) \to (\id F G).
(F=G)(FG)(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:idFGp,q:\id F G are equal, it suffices to show that id[idF 0G 0]pq\id[\id{F_0}{G_0}]{p}{q}. But in the definition of γ¯\bar\gamma, if γ\gamma were of the form idtoiso(p)\idtoiso(p), then γ a\gamma_a would be equal to idtoiso(p a)\idtoiso(p_a) (this can easily be proved by induction on pp). Thus, isotoid(γ a)\isotoid(\gamma_a) would be equal to p ap_a, and so by function extensionality we would have idγ¯p\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=Gp,q:F =G are equal, it suffices to show that p= F 0=G 0qp =_{{F_0}={G_0}}{q}. But in the definition of γ¯\bar\gamma, if γ\gamma were of the form idtoiso(p)idtoiso(p), then γ a\gamma_a would be equal to idtoiso(p a)idtoiso(p_a) (this can easily be proved by induction on pp). Thus, isotoid(γ a)isotoid(\gamma_a) would be equal to p ap_a, and so by function extensionality we would have γ¯=p{\bar\gamma}={p}, which is what we need.

Finally, consider the composite

(2)(FG)(F=G)(FG).(F\cong G)\to ( F = G) \to (F\cong G). (FG)(idFG)(FG).(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 eachaanatural transformations we can have be tested componentwise, it suffices to show that for eachidaidtoiso(γ¯) aγ a \id{\idtoiso(\bar\gamma)_a}{\gamma_a} a . But as observed above, we haveididtoiso(γ¯) aidtoiso(γ¯) a=idtoisoγ a((γ¯) a) \id{\idtoiso(\bar\gamma)_a}{\idtoiso((\bar\gamma)_a)} {idtoiso(\bar\gamma)_a}={\gamma_a} , . while But as observed above, we haveididtoiso(γ¯) a(γ¯) a=isotoididtoiso(γ a(γ¯) a) \id{(\bar\gamma)_a}{\isotoid(\gamma_a)} {idtoiso(\bar\gamma)_a}={idtoiso((\bar\gamma)_a)} , by while computation for function extensionality. Sinceisotoid(γ¯) a=isotoid(γ a) \isotoid {(\bar\gamma)_a}={isotoid(\gamma_a)} and by computation for function extensionality. Sinceidtoisoisotoid \idtoiso isotoid are and inverses, we haveididtoisoidtoiso(γ¯) aγ a \id{\idtoiso(\bar\gamma)_a}{\gamma_a} idtoiso are inverses, we have idtoiso(γ¯) a=γ a{idtoiso(\bar\gamma)_a}={\gamma_a} as desired.

See also

Category theory functor category Rezk completion

References

HoTT Book

category: category theory

Revision on September 5, 2018 at 13:23:49 by Ali Caglayan. See the history of this page for a list of all contributions to it.