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

Showing changes from revision #1 to #2: 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 from FF to GG is a set.

See also

Category theory in HoTT functor precategory functor


HoTT Book

category: category theory

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