:: deftheorem defines coprojection-morphisms ALTCAT_6:def 6 :
for C being category
for I being non empty set
for A being ObjectsFamily of I,C
for B being Object of C
for P being MorphismsFamily of A,B holds
( P is coprojection-morphisms iff for X being Object of C
for F being MorphismsFamily of A,X st F is feasible holds
ex f being Morphism of B,X st
( f in <^B,X^> & ( for i being Element of I holds F . i = f * (P . i) ) & ( for f1 being Morphism of B,X st ( for i being Element of I holds F . i = f1 * (P . i) ) holds
f = f1 ) ) );