:: deftheorem defines -CatCoproduct-like ALTCAT_6:def 8 :
for C being category
for I being set
for A being ObjectsFamily of I,C
for B being Object of C holds
( B is A -CatCoproduct-like iff ex P being MorphismsFamily of A,B st
( P is feasible & P is coprojection-morphisms ) );