thus
id A is feasible
id A is Covariant proof
let o1,
o2 be
Object of
A;
FUNCTOR0:def 11 ( <^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:87;
the
ObjectMap of
(id A) . (
o1,
o2) =
(id [: the carrier of A, the carrier of A:]) . [o1,o2]
by Def29
.=
[o1,o2]
by A1, FUNCT_1:18
;
then the
Arrows of
A . ( the ObjectMap of (id A) . (o1,o2)) =
the
Arrows of
A . (
o1,
o2)
.=
<^o1,o2^>
by ALTCAT_1:def 1
;
hence
(
<^o1,o2^> <> {} implies the
Arrows of
A . ( the ObjectMap of (id A) . (o1,o2)) <> {} )
;
verum
end;
thus
id A is Covariant
verum