:: deftheorem defines Functors FUNCTOR2:def 11 :
for A, B being category
for b₃ being non empty transitive strict AltCatStr holds
( b₃ = Functors (A,B) iff ( the carrier of b₃ = Funct (A,B) & ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b₃ . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b₃ . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) );