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

Showing changes from revision #2 to #3: 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 idtoiso:(idFG)(FG)\idtoiso:(\id{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:Fa \cong Ga, hence an identity isotoid(γ a):idFaGa\isotoid(\gamma_a):\id{Fa}{Ga}. By function extensionality, we have an identity γ¯:id[(A 0B 0)]F 0G 0\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 idFG\id{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)

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.

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

(1)(idFG)(FG)(idFG). (\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: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.

Finally, consider the composite

(2)(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 each aa we have ididtoiso(γ¯) aγ a\id{\idtoiso(\bar\gamma)_a}{\gamma_a}. But as observed above, we have ididtoiso(γ¯) aidtoiso((γ¯) a)\id{\idtoiso(\bar\gamma)_a}{\idtoiso((\bar\gamma)_a)}, while id(γ¯) aisotoid(γ a)\id{(\bar\gamma)_a}{\isotoid(\gamma_a)} by computation for function extensionality. Since isotoid\isotoid and idtoiso\idtoiso are inverses, we have ididtoiso(γ¯) aγ a\id{\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 10:26:18 by Ali Caglayan. See the history of this page for a list of all contributions to it.