for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )