Homotopy Type Theory
natural transformation



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


It follows that the type of natural transformations from FF 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

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

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