:: The Composition of Functors and Transformations in Alternative Categories
:: by Artur Korni{\l}owicz
::
:: Received January 21, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

registration
cluster non empty transitive strict associative with_units for AltCatStr ;
existence
 ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict )
proofend;
end;

registration
let A be non empty transitive AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict Covariant Contravariant comp-preserving comp-reversing for FunctorStr over A,B;
existence
 ex b1 being FunctorStr over A,B st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible )
proofend;
end;

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict Covariant Contravariant id-preserving comp-preserving comp-reversing for FunctorStr over A,B;
existence
 ex b1 being FunctorStr over A,B st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible & b1 is id-preserving )
proofend;
end;

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict id-preserving covariant contravariant for Functor of A,B;
existence
 ex b1 being Functor of A,B st
( b1 is strict & b1 is feasible & b1 is covariant & b1 is contravariant )
proofend;
end;

theorem :: FUNCTOR3:1
for C being category
for o1, o2, o3, o4 being object of C
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c &amp; a * (a ") = idm o2 &amp; (d ") * d = idm o4 &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; <^o2,o3^> <> {} &amp; <^o3,o4^> <> {} &amp; <^o4,o3^> <> {} holds
c * (a ") = (d ") * b
proofend;

theorem :: FUNCTOR3:2
for A being non empty transitive AltCatStr
for B, C being non empty with_units AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o),(F . o1))) * (Morph-Map (F,o,o1))
proofend;

theorem :: FUNCTOR3:3
for A being non empty transitive AltCatStr
for B, C being non empty with_units AltCatStr
for F being feasible Contravariant FunctorStr over A,B
for G being FunctorStr over B,C
for o, o1 being object of A holds Morph-Map ((G * F),o,o1) = (Morph-Map (G,(F . o1),(F . o))) * (Morph-Map (F,o,o1))
proofend;

Lm1:  for I1 being set
for I2 being non empty set
for f being Function of I1,I2
for A being ManySortedSet of I1
for B being ManySortedSet of I2
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
proofend;

theorem :: FUNCTOR3:4
for A being non empty transitive AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
proofend;

theorem :: FUNCTOR3:5
for A being non empty transitive with_units AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
proofend;

theorem Th6: :: FUNCTOR3:6
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
proofend;

theorem Th7: :: FUNCTOR3:7
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for M being feasible Contravariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
proofend;

theorem Th8: :: FUNCTOR3:8
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * F) . m = N . (F . m)
proofend;

theorem Th9: :: FUNCTOR3:9
for A being non empty AltCatStr
for C, B being non empty reflexive AltCatStr
for G being feasible Covariant FunctorStr over B,C
for M being feasible Contravariant FunctorStr over A,B
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * M) . m = G . (M . m)
proofend;

registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Covariant comp-preserving FunctorStr over A,B;
let G be feasible Covariant comp-preserving FunctorStr over B,C;
clusterG * F ->  comp-preserving ;
coherence
 G * F is comp-preserving
proofend;
end;

registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Contravariant comp-reversing FunctorStr over A,B;
let G be feasible Contravariant comp-reversing FunctorStr over B,C;
clusterG * F ->  comp-preserving ;
coherence
 G * F is comp-preserving
proofend;
end;

registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Covariant comp-preserving FunctorStr over A,B;
let G be feasible Contravariant comp-reversing FunctorStr over B,C;
clusterG * F ->  comp-reversing ;
coherence
 G * F is comp-reversing
proofend;
end;

registration
let A be non empty transitive AltCatStr ;
let B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be feasible Contravariant comp-reversing FunctorStr over A,B;
let G be feasible Covariant comp-preserving FunctorStr over B,C;
clusterG * F ->  comp-reversing ;
coherence
 G * F is comp-reversing
proofend;
end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be covariant Functor of A,B;
let G be covariant Functor of B,C;
:: original:*
redefine funcG * F ->  strict covariant Functor of A,C;
coherence
 G * F is strict covariant Functor of A,C by FUNCTOR0:def_25;
end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be contravariant Functor of A,B;
let G be contravariant Functor of B,C;
:: original:*
redefine funcG * F ->  strict covariant Functor of A,C;
coherence
 G * F is strict covariant Functor of A,C by FUNCTOR0:def_25;
end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be covariant Functor of A,B;
let G be contravariant Functor of B,C;
:: original:*
redefine funcG * F ->  strict contravariant Functor of A,C;
coherence
 G * F is strict contravariant Functor of A,C by FUNCTOR0:def_25;
end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let C be non empty with_units AltCatStr ;
let F be contravariant Functor of A,B;
let G be covariant Functor of B,C;
:: original:*
redefine funcG * F ->  strict contravariant Functor of A,C;
coherence
 G * F is strict contravariant Functor of A,C by FUNCTOR0:def_25;
end;

theorem Th10: :: FUNCTOR3:10
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C st F1 is_transformable_to F2 &amp; G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
proofend;

begin

definition
let A, B, C be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
let t be transformation of F1,F2;
let G be covariant Functor of B,C;
assume B1: F1 is_transformable_to F2 ;
funcG * t ->  transformation of G * F1,G * F2 means :Def1: :: FUNCTOR3:def 1
 for o being object of A holds it . o = G . (t ! o);
existence
 ex b1 being transformation of G * F1,G * F2 st
for o being object of A holds b1 . o = G . (t ! o)
proofend;
uniqueness
 for b1, b2 being transformation of G * F1,G * F2 st ( for o being object of A holds b1 . o = G . (t ! o) ) &amp; ( for o being object of A holds b2 . o = G . (t ! o) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines * FUNCTOR3:def_1_:_
 for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for t being transformation of F1,F2
for G being covariant Functor of B,C st F1 is_transformable_to F2 holds
for b8 being transformation of G * F1,G * F2 holds
( b8 = G * t iff for o being object of A holds b8 . o = G . (t ! o) );

theorem Th11: :: FUNCTOR3:11
for C, B, A being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for o being object of A st F1 is_transformable_to F2 holds
(G1 * p) ! o = G1 . (p ! o)
proofend;

definition
let A, B, C be non empty transitive with_units AltCatStr ;
let G1, G2 be covariant Functor of B,C;
let F be covariant Functor of A,B;
let s be transformation of G1,G2;
assume B1: G1 is_transformable_to G2 ;
funcs * F ->  transformation of G1 * F,G2 * F means :Def2: :: FUNCTOR3:def 2
 for o being object of A holds it . o = s ! (F . o);
existence
 ex b1 being transformation of G1 * F,G2 * F st
for o being object of A holds b1 . o = s ! (F . o)
proofend;
uniqueness
 for b1, b2 being transformation of G1 * F,G2 * F st ( for o being object of A holds b1 . o = s ! (F . o) ) &amp; ( for o being object of A holds b2 . o = s ! (F . o) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines * FUNCTOR3:def_2_:_
 for A, B, C being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for F being covariant Functor of A,B
for s being transformation of G1,G2 st G1 is_transformable_to G2 holds
for b8 being transformation of G1 * F,G2 * F holds
( b8 = s * F iff for o being object of A holds b8 . o = s ! (F . o) );

theorem Th12: :: FUNCTOR3:12
for B, C, A being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2
for o being object of A st G1 is_transformable_to G2 holds
(q * F1) ! o = q ! (F1 . o)
proofend;

theorem Th13: :: FUNCTOR3:13
for C, A, B being non empty transitive with_units AltCatStr
for F1, F2, F3 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 &amp; F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
proofend;

theorem Th14: :: FUNCTOR3:14
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 &amp; G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
proofend;

theorem Th15: :: FUNCTOR3:15
for A, B, C, D being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
proofend;

theorem Th16: :: FUNCTOR3:16
for A, D, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
(H1 * q) * F1 = H1 * (q * F1)
proofend;

theorem Th17: :: FUNCTOR3:17
for C, D, A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1 being covariant Functor of C,D
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(H1 * G1) * p = H1 * (G1 * p)
proofend;

theorem Th18: :: FUNCTOR3:18
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)
proofend;

theorem Th19: :: FUNCTOR3:19
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1)
proofend;

theorem Th20: :: FUNCTOR3:20
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(id B) * p = p
proofend;

theorem Th21: :: FUNCTOR3:21
for C, B being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * (id B) = q
proofend;

begin

definition
let A, B, C be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
let G1, G2 be covariant Functor of B,C;
let t be transformation of F1,F2;
let s be transformation of G1,G2;
funcs (#) t ->  transformation of G1 * F1,G2 * F2 equals :: FUNCTOR3:def 3
(s * F2) `*` (G1 * t);
coherence
 (s * F2) `*` (G1 * t) is transformation of G1 * F1,G2 * F2 ;
end;

:: deftheorem  defines (#) FUNCTOR3:def_3_:_
 for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for t being transformation of F1,F2
for s being transformation of G1,G2 holds s (#) t = (s * F2) `*` (G1 * t);

theorem Th22: :: FUNCTOR3:22
for C, A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
proofend;

theorem :: FUNCTOR3:23
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
(idt (id B)) (#) p = p
proofend;

theorem :: FUNCTOR3:24
for C, B being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q
proofend;

theorem :: FUNCTOR3:25
for C, A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2 st F1 is_transformable_to F2 holds
G1 * p = (idt G1) (#) p
proofend;

theorem :: FUNCTOR3:26
for A, B, C being non empty transitive with_units AltCatStr
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q * F1 = q (#) (idt F1)
proofend;

theorem :: FUNCTOR3:27
for A, B, C, D being category
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for t being transformation of F1,F2
for s being transformation of G1,G2
for u being transformation of H1,H2 st F1 is_transformable_to F2 &amp; G1 is_transformable_to G2 &amp; H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
proofend;

Lm2: now__::_thesis:_for_A,_B,_C_being_category
for_F1,_F2_being_covariant_Functor_of_A,B
for_G1,_G2_being_covariant_Functor_of_B,C
for_s_being_natural_transformation_of_G1,G2
for_t_being_natural_transformation_of_F1,F2_st_F1_is_naturally_transformable_to_F2_&amp;_G1_is_naturally_transformable_to_G2_holds_
(_G1_*_F1_is_naturally_transformable_to_G2_*_F2_&amp;_s_(#)_t_is_natural_transformation_of_G1_*_F1,G2_*_F2_)
let A, B, C be category; ::_thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let F1, F2 be covariant Functor of A,B; ::_thesis: for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let G1, G2 be covariant Functor of B,C; ::_thesis: for s being natural_transformation of G1,G2
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let s be natural_transformation of G1,G2; ::_thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 )
let t be natural_transformation of F1,F2; ::_thesis: ( F1 is_naturally_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )
set k = s (#) t;
assume A1: F1 is_naturally_transformable_to F2 ; ::_thesis: ( G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )
then A2: F1 is_transformable_to F2 by FUNCTOR2:def_6;
assume A3: G1 is_naturally_transformable_to G2 ; ::_thesis: ( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 )
then A4: G1 is_transformable_to G2 by FUNCTOR2:def_6;
A5: now__::_thesis:_for_a,_b_being_object_of_A_st_<^a,b^>_<>_{}_holds_
for_f_being_Morphism_of_a,b_holds_((s_(#)_t)_!_b)_*_((G1_*_F1)_._f)_=_((G2_*_F2)_._f)_*_((s_(#)_t)_!_a)
let a, b be object of A; ::_thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a) )
assume A6: <^a,b^> <> {} ; ::_thesis: for f being Morphism of a,b holds ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)
A7: <^((G1 * F1) . a),((G1 * F1) . b)^> <> {} by A6, FUNCTOR0:def_18;
A8: (G2 * F2) . a = G2 . (F2 . a) by FUNCTOR0:33;
then reconsider sF2a = s ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) by FUNCTOR0:33;
A9: (G2 * F2) . b = G2 . (F2 . b) by FUNCTOR0:33;
then reconsider sF2b = s ! (F2 . b) as Morphism of ((G1 * F2) . b),((G2 * F2) . b) by FUNCTOR0:33;
 <^(G1 . (F2 . b)),(G2 . (F2 . b))^> <> {} by A4, FUNCTOR2:def_1;
then A10: <^((G1 * F2) . b),((G2 * F2) . b)^> <> {} by A9, FUNCTOR0:33;
let f be Morphism of a,b; ::_thesis: ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)
A11: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33;
then reconsider G1tbF1f = G1 . ((t ! b) * (F1 . f)) as Morphism of ((G1 * F1) . a),((G1 * F2) . b) by FUNCTOR0:33;
reconsider G1ta = G1 . (t ! a) as Morphism of ((G1 * F1) . a),((G1 * F2) . a) by A11, FUNCTOR0:33;
A12: <^(G1 . (F1 . a)),(G2 . (F1 . a))^> <> {} by A4, FUNCTOR2:def_1;
A13: (G1 * F1) . b = G1 . (F1 . b) by FUNCTOR0:33;
then reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),((G1 * F2) . b) by FUNCTOR0:33;
A14: <^(F1 . b),(F2 . b)^> <> {} by A2, FUNCTOR2:def_1;
then  <^(G1 . (F1 . b)),(G1 . (F2 . b))^> <> {} by FUNCTOR0:def_18;
then A15: <^((G1 * F1) . b),((G1 * F2) . b)^> <> {} by A13, FUNCTOR0:33;
A16: <^(F1 . a),(F1 . b)^> <> {} by A6, FUNCTOR0:def_18;
then A17: <^(F1 . a),(F2 . b)^> <> {} by A14, ALTCAT_1:def_2;
reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by A13, FUNCTOR0:33;
A18: s ! (F2 . a) = (s * F2) . a by A4, Def2;
A19: G1 . ((t ! b) * (F1 . f)) = (G1 . (t ! b)) * (G1 . (F1 . f)) by A14, A16, FUNCTOR0:def_23
.= G1tb * G1F1f by A11, A13, FUNCTOR0:33 ;
reconsider G2F2f = G2 . (F2 . f) as Morphism of ((G2 * F2) . a),((G2 * F2) . b) by A8, FUNCTOR0:33;
A20: s ! (F2 . b) = (s * F2) . b by A4, Def2;
A21: G1 * F2 is_transformable_to G2 * F2 by A4, Th10;
A22: <^(F2 . a),(F2 . b)^> <> {} by A6, FUNCTOR0:def_18;
then A23: <^(G2 . (F2 . a)),(G2 . (F2 . b))^> <> {} by FUNCTOR0:def_18;
A24: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def_1;
then A25: <^(G2 . (F1 . a)),(G2 . (F2 . a))^> <> {} by FUNCTOR0:def_18;
A26: G1 * F1 is_transformable_to G1 * F2 by A2, Th10;
hence ((s (#) t) ! b) * ((G1 * F1) . f) = (((s * F2) ! b) * ((G1 * t) ! b)) * ((G1 * F1) . f) by A21, FUNCTOR2:def_5
.= (sF2b * ((G1 * t) ! b)) * ((G1 * F1) . f) by A21, A20, FUNCTOR2:def_4
.= (sF2b * G1tb) * ((G1 * F1) . f) by A2, Th11
.= (sF2b * G1tb) * G1F1f by A6, Th6
.= sF2b * G1tbF1f by A7, A15, A10, A19, ALTCAT_1:21
.= (s ! (F2 . b)) * (G1 . ((t ! b) * (F1 . f))) by A11, A9, FUNCTOR0:33
.= (G2 . ((t ! b) * (F1 . f))) * (s ! (F1 . a)) by A3, A17, FUNCTOR2:def_7
.= (G2 . ((F2 . f) * (t ! a))) * (s ! (F1 . a)) by A1, A6, FUNCTOR2:def_7
.= ((G2 . (F2 . f)) * (G2 . (t ! a))) * (s ! (F1 . a)) by A22, A24, FUNCTOR0:def_23
.= (G2 . (F2 . f)) * ((G2 . (t ! a)) * (s ! (F1 . a))) by A12, A25, A23, ALTCAT_1:21
.= (G2 . (F2 . f)) * ((s ! (F2 . a)) * (G1 . (t ! a))) by A3, A24, FUNCTOR2:def_7
.= G2F2f * (sF2a * G1ta) by A11, A8, A9, FUNCTOR0:33
.= ((G2 * F2) . f) * (sF2a * G1ta) by A6, Th6
.= ((G2 * F2) . f) * (((s * F2) ! a) * G1ta) by A21, A18, FUNCTOR2:def_4
.= ((G2 * F2) . f) * (((s * F2) ! a) * ((G1 * t) ! a)) by A2, Th11
.= ((G2 * F2) . f) * ((s (#) t) ! a) by A21, A26, FUNCTOR2:def_5 ;
::_thesis: verum
end;
thus  G1 * F1 is_naturally_transformable_to G2 * F2 ::_thesis: s (#) t is natural_transformation of G1 * F1,G2 * F2
proof
thus  G1 * F1 is_transformable_to G2 * F2 by A2, A4, Th10; :: according toFUNCTOR2:def_6 ::_thesis: ex b1 being transformation of G1 * F1,G2 * F2 st
for b2, b3 being M2( the carrier of A) holds
( <^b2,b3^> = {} or for b4 being M2(<^b2,b3^>) holds (b1 ! b3) * ((G1 * F1) . b4) = ((G2 * F2) . b4) * (b1 ! b2) )
take  s (#) t ; ::_thesis: for b1, b2 being M2( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) )
thus  for b1, b2 being M2( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((s (#) t) ! b2) * ((G1 * F1) . b3) = ((G2 * F2) . b3) * ((s (#) t) ! b1) ) by A5; ::_thesis: verum
end;
hence  s (#) t is natural_transformation of G1 * F1,G2 * F2 by A5, FUNCTOR2:def_7; ::_thesis: verum
end;

theorem Th28: :: FUNCTOR3:28
for C, A, B being category
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
proofend;

theorem Th29: :: FUNCTOR3:29
for A, B, C being category
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
proofend;

theorem :: FUNCTOR3:30
for A, B, C being category
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for t being natural_transformation of F1,F2
for s being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 &amp; G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 &amp; s (#) t is natural_transformation of G1 * F1,G2 * F2 ) by Lm2;

theorem :: FUNCTOR3:31
for A, B, C being category
for F1, F2, F3 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for s being natural_transformation of G1,G2
for s1 being natural_transformation of G2,G3
for t being transformation of F1,F2
for t1 being transformation of F2,F3 st F1 is_naturally_transformable_to F2 &amp; F2 is_naturally_transformable_to F3 &amp; G1 is_naturally_transformable_to G2 &amp; G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
proofend;

begin

theorem Th32: :: FUNCTOR3:32
for B, A being category
for F1, F2 being covariant Functor of A,B
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 &amp; F2 is_transformable_to F1 &amp; ( for a being object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 &amp; ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " &amp; f ! a is iso ) )
proofend;

definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
predF1,F2 are_naturally_equivalent  means :Def4: :: FUNCTOR3:def 4
( F1 is_naturally_transformable_to F2 &amp; F2 is_transformable_to F1 &amp; ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso );
reflexivity
 for F1 being covariant Functor of A,B holds
( F1 is_naturally_transformable_to F1 &amp; F1 is_transformable_to F1 &amp; ex t being natural_transformation of F1,F1 st
for a being object of A holds t ! a is iso )
proofend;
symmetry
 for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 &amp; F2 is_transformable_to F1 &amp; ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso holds
( F2 is_naturally_transformable_to F1 &amp; F1 is_transformable_to F2 &amp; ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso )
proofend;
end;

:: deftheorem Def4 defines are_naturally_equivalent FUNCTOR3:def_4_:_
 for A, B being category
for F1, F2 being covariant Functor of A,B holds
( F1,F2 are_naturally_equivalent iff ( F1 is_naturally_transformable_to F2 &amp; F2 is_transformable_to F1 &amp; ex t being natural_transformation of F1,F2 st
for a being object of A holds t ! a is iso ) );

definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
assume A1: F1,F2 are_naturally_equivalent ;
mode natural_equivalence of F1,F2 ->  natural_transformation of F1,F2 means :Def5: :: FUNCTOR3:def 5
 for a being object of A holds it ! a is iso ;
existence
 ex b1 being natural_transformation of F1,F2 st
for a being object of A holds b1 ! a is iso by A1, Def4;
end;

:: deftheorem Def5 defines natural_equivalence FUNCTOR3:def_5_:_
 for A, B being category
for F1, F2 being covariant Functor of A,B st F1,F2 are_naturally_equivalent holds
for b5 being natural_transformation of F1,F2 holds
( b5 is natural_equivalence of F1,F2 iff for a being object of A holds b5 ! a is iso );

theorem Th33: :: FUNCTOR3:33
for A, B being category
for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent &amp; F2,F3 are_naturally_equivalent holds
F1,F3 are_naturally_equivalent
proofend;

theorem Th34: :: FUNCTOR3:34
for A, B being category
for F1, F2, F3 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent &amp; F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3
proofend;

theorem Th35: :: FUNCTOR3:35
for C, A, B being category
for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
( G1 * F1,G1 * F2 are_naturally_equivalent &amp; G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
proofend;

theorem Th36: :: FUNCTOR3:36
for A, B, C being category
for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for f being natural_equivalence of G1,G2 st G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F1 are_naturally_equivalent &amp; f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
proofend;

theorem :: FUNCTOR3:37
for A, B, C being category
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for e being natural_equivalence of F1,F2
for f being natural_equivalence of G1,G2 st F1,F2 are_naturally_equivalent &amp; G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent &amp; f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
proofend;

definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
let e be natural_equivalence of F1,F2;
assume B1: F1,F2 are_naturally_equivalent ;
funce "  ->  natural_equivalence of F2,F1 means :Def6: :: FUNCTOR3:def 6
 for a being object of A holds it . a = (e ! a) " ;
existence
 ex b1 being natural_equivalence of F2,F1 st
for a being object of A holds b1 . a = (e ! a) "
proofend;
uniqueness
 for b1, b2 being natural_equivalence of F2,F1 st ( for a being object of A holds b1 . a = (e ! a) " ) &amp; ( for a being object of A holds b2 . a = (e ! a) " ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines " FUNCTOR3:def_6_:_
 for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
for b6 being natural_equivalence of F2,F1 holds
( b6 = e " iff for a being object of A holds b6 . a = (e ! a) " );

theorem Th38: :: FUNCTOR3:38
for B, A being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for o being object of A st F1,F2 are_naturally_equivalent holds
(e ") ! o = (e ! o) "
proofend;

theorem Th39: :: FUNCTOR3:39
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
e `*` (e ") = idt F2
proofend;

theorem :: FUNCTOR3:40
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") `*` e = idt F1
proofend;

definition
let A, B be category;
let F be covariant Functor of A,B;
:: original:idt
redefine func idt F ->  natural_equivalence of F,F;
coherence
 idt F is natural_equivalence of F,F
proofend;
end;

theorem :: FUNCTOR3:41
for A, B being category
for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") " = e
proofend;

theorem :: FUNCTOR3:42
for A, B being category
for F1, F3, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2
for e1 being natural_equivalence of F2,F3
for k being natural_equivalence of F1,F3 st k = e1 `*` e &amp; F1,F2 are_naturally_equivalent &amp; F2,F3 are_naturally_equivalent holds
k " = (e ") `*` (e1 ")
proofend;

theorem :: FUNCTOR3:43
for A, B being category
for F1 being covariant Functor of A,B holds (idt F1) " = idt F1
proofend;