:: deftheorem Def1 defines |-> ISOCAT_2:def 1 :
for A, B being Category
for a being Object of A
for b₄ being Functor of Functors (A,B),B holds
( b₄ = a |-> B iff for F1, F2 being Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
b₄ . [[F1,F2],t] = t . a );