:: deftheorem Def11 defines -functor INDEX_1:def 11 :
for C being Category
for I being Indexing of C
for T being TargetCat of I
for b₄ being Functor of C,T holds
( b₄ = I -functor (C,T) iff for f being Morphism of C holds b₄ . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] );