:: deftheorem Def13 defines distribute ISOCAT_2:def 13 :
for A, B, C being Category
for b₄ being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] holds
( b₄ = distribute (A,B,C) iff for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds b₄ . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] );