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

Definition

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

  • (B A) 0(B^A)_0 is the type of functors from AA to BB.
  • hom B A(F,G)hom_{B^A}(F,G) is the type of natural transformations from FF to GG. 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.

See also

Category theory functor category Rezk completion

References

HoTT Book

category: category theory

Revision on September 4, 2018 at 19:30:07 by Ali Caglayan. See the history of this page for a list of all contributions to it.