:: deftheorem Def1 defines Covariant FUNCTOR0:def 1 :
for A, B being set
for f being bifunction of A,B holds
( f is Covariant iff ex g being Function of A,B st f = [:g,g:] );