thus id A is feasible :: thesis: id A is Covariant

proof

let o1, o2 be object of A; :: according to FUNCTOR0:def 12 :: thesis: ( <^o1,o2^> <> {} implies the Arrows of A . (the ObjectMap of (id A) . o1,o2) <> {} )
A1: [o1,o2] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
the ObjectMap of (id A) . o1,o2 = (id [:the carrier of A,the carrier of A:]) . [o1,o2] by Def30
.= [o1,o2] by A1, FUNCT_1:35 ;
then the Arrows of A . (the ObjectMap of (id A) . o1,o2) = the Arrows of A . o1,o2
.= <^o1,o2^> by ALTCAT_1:def 2 ;
hence ( <^o1,o2^> <> {} implies the Arrows of A . (the ObjectMap of (id A) . o1,o2) <> {} ) ; :: thesis: verum

end;

thus id A is Covariant :: thesis: verum

proof

take I = id the carrier of A; :: according to FUNCTOR0:def 2,FUNCTOR0:def 13 :: thesis: the ObjectMap of (id A) = [:I,I:]
thus the ObjectMap of (id A) = id [:the carrier of A,the carrier of A:] by Def30
.= [:I,I:] by FUNCT_3:90 ; :: thesis: verum

end;