Homotopy Type Theory functor precategory > history (Rev #6)

This page is under construction. - Ali

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. \square

We define a natural isomorphism as an isomorphism in B AB^A.

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

To give an inverse to it, suppose γ:FG\gamma:F\cong G is a natural isomorphism. Then for any a:Aa:A, we have an isomorphism? γ a:FaGa\gamma_a:F 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 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)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 γ¯\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)(F=G)(F\cong G) \to (F =G). Now consider the composite

(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: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

(FG)(F=G)(FG).(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 aa we have idtoiso(γ¯) a=γ a{idtoiso(\bar\gamma)_a}={\gamma_a}. But as observed above, we have idtoiso(γ¯) a=idtoiso((γ¯) a){idtoiso(\bar\gamma)_a}={idtoiso((\bar\gamma)_a)}, while (γ¯) a=isotoid(γ a){(\bar\gamma)_a}={isotoid(\gamma_a)} by computation for function extensionality. Since isotoidisotoid and idtoisoidtoiso are inverses, we have idtoiso(γ¯) a=γ a{idtoiso(\bar\gamma)_a}={\gamma_a} as desired. \square

See also

Category theory functor category Rezk completion

References

HoTT Book

category: category theory

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