:: deftheorem Def28 defines Functors CAT_8:def 28 :
for C1, C2 being category
for b₃ being strict category holds
( b₃ = Functors (C1,C2) iff ( the carrier of b₃ = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b₃ = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b₃ : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) );