:: deftheorem Def16 defines Functors NATTRA_1:def 17 :
for A, B being Category
for b₃ being strict Category holds
( b₃ = Functors (A,B) iff ( the carrier of b₃ = Funct (A,B) & the carrier' of b₃ = NatTrans (A,B) & ( for f being Morphism of b₃ holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of b₃ st dom g = cod f holds
[g,f] in dom the Comp of b₃ ) & ( for f, g being Morphism of b₃ st [g,f] in dom the Comp of b₃ holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of b₃ . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of b₃
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) ) );