:: deftheorem Def6 defines Categorial CAT_5:def 6 :
for C being Category holds
( C is Categorial iff ( the carrier of C is categorial & ( for a being Object of C
for A being Category st a = A holds
id a = [[A,A],(id A)] ) & ( for m being Morphism of C
for A, B being Category st A = dom m & B = cod m holds
ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C
for A, B, C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds
m2 (*) m1 = [[A,C],(G * F)] ) ) );