Homotopy Type Theory
natural transformation (Rev #3, changes)

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


For functors F,G:ABF,G: A \to B, a natural transformation γ:FG\gamma : F \to G consists of

  • For each a:Aa : A, a morphism γ a:hom B(Fa,Ga)\gamma_a: hom_B(F a,G a) called the components of γ\gamma at aa.
  • For each a,b:Aa,b:A and f:hom A(a,b)f:hom_A(a,b), we have Gfγ a=γ bFfG f \circ \gamma_a= \gamma_b \circ F f (the naturality axiom).


It follows that the type of natural transformations fromFFnatural transformations to from G F G F to GG is a set.

Composites with functors

For functors F:ABF : A \to B and G,H:BCG,H : B \to C and a natural transformation γ:GH\gamma : G \to H, the composite (γF):GFHF(\gamma F) : G F \to H F is given by

  • For each a:Aa:A, the component γ Fa\gamma_{F a}.

Naturality is easy to check. Similarly, for γ\gamma as above and K:CDK : C \to D, the composite (Kγ):KGKH(K \gamma): K G \to K H is given by

  • For each b:Bb: B, the component K(γ b)K(\gamma_b).

Lemma 9.2.8

For functors F,G:ABF,G: A\to B and H,K:BCH,K: B \to C and natural transformations γ:FG\gamma : F \to G and δ:HK\delta : H \to K, we have

(δG)(Hγ)=(Kγ)(δF).(\delta G)(H \gamma) = (K \gamma) (\delta F).

Proof. It suffices to check componentwise: at a:Aa:A we have

((δG)(Hγ)) a (δG) a(Hγ) a δ GaH(γ a) =K(γ a)δ Fa(bynaturalityofδ) (Kγ) a(δF) a ((Kγ)(δF)) a. \begin{aligned} ((\delta G)(H \gamma))_a &\equiv (\delta G)_a (H \gamma)_a \\ &\equiv \delta_{G a} \circ H(\gamma_a)\\ &= K(\gamma_a) \circ \delta_{F a} \qquad (by\ naturality\ of\ \delta) \\ &\equiv (K \gamma)_a \circ (\delta F)_a\\ &\equiv ((K \gamma)(\delta F))_a.\ \square \end{aligned}

See also

Category theory functor precategory functor


HoTT Book

category: category theory

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