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

Showing changes from revision #0 to #1: Added | Removed | Changed

Definition

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).

Properties

It follows that the type of natural transformations from FF to GG is a set.

See also

Category theory in HoTT functor precategory functor

References

HoTT Book

category: category theory

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