:: deftheorem defines retraction ALTCAT_3:def 2 :
for C being non empty with_units AltCatStr
for o1, o2 being Object of C
for A being Morphism of o1,o2 holds
( A is retraction iff ex B being Morphism of o2,o1 st B is_right_inverse_of A );