let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being covariant Functor of A,B holds F is_naturally_transformable_to F
let F be covariant Functor of A,B; :: thesis: F is_naturally_transformable_to F
thus F is_transformable_to F ; :: according to FUNCTOR2:def 6 :: thesis: ex t being transformation of F,F st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a)
take idt F ; :: thesis: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
thus for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) by Lm1; :: thesis: verum