set o = the Object of B;
set I = A --> (idm the Object of B);
reconsider I = A --> (idm the Object of B) as Functor of A,B by FUNCTOR0:def 25;
take I ; :: thesis: ( I is strict & I is feasible & I is covariant & I is contravariant )
thus ( I is strict & I is feasible ) ; :: thesis: ( I is covariant & I is contravariant )
thus I is covariant ; :: thesis: I is contravariant
thus I is contravariant ; :: thesis: verum