:: FUNCTOR3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster non empty transitive strict associative with_units AltCatStr ;
existence
ex b1 being non empty AltCatStr st
( b1 is transitive & b1 is associative & b1 is with_units & b1 is strict )
proof end;
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 FunctorStr of A,B;
existence
ex b1 being FunctorStr of A,B st
( b1 is strict & b1 is comp-preserving & b1 is comp-reversing & b1 is Covariant & b1 is Contravariant & b1 is feasible )
proof end;
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 FunctorStr of A,B;
existence
ex b1 being FunctorStr of 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 )
proof end;
end;

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster feasible strict covariant contravariant 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 )
proof end;
end;

theorem :: FUNCTOR3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
proof end;

theorem :: FUNCTOR3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty transitive AltCatStr
for B, C being non empty with_units AltCatStr
for F being feasible Covariant FunctorStr of A,B
for G being FunctorStr of 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)
proof end;

theorem :: FUNCTOR3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty transitive AltCatStr
for B, C being non empty with_units AltCatStr
for F being feasible Contravariant FunctorStr of A,B
for G being FunctorStr of 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)
proof end;

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 st ( for i being set st i in I1 & A . i <> {} holds
B . (f . i) <> {} ) holds
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M
proof end;

theorem :: FUNCTOR3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty transitive AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr of A,B holds (id B) * F = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
proof end;

theorem :: FUNCTOR3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty transitive with_units AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr of A,B holds F * (id A) = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
proof end;

theorem Th6: :: FUNCTOR3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr of A,B
for G being feasible Covariant FunctorStr of 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)
proof end;

theorem Th7: :: FUNCTOR3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for M being feasible Contravariant FunctorStr of A,B
for N being feasible Contravariant FunctorStr of 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)
proof end;

theorem Th8: :: FUNCTOR3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty AltCatStr
for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr of A,B
for N being feasible Contravariant FunctorStr of 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)
proof end;

theorem Th9: :: FUNCTOR3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty AltCatStr
for C, B being non empty reflexive AltCatStr
for G being feasible Covariant FunctorStr of B,C
for M being feasible Contravariant FunctorStr of 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)
proof 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 of A,B;
let G be feasible Covariant comp-preserving FunctorStr of B,C;
cluster G * F -> comp-preserving ;
coherence
G * F is comp-preserving
proof end;
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 of A,B;
let G be feasible Contravariant comp-reversing FunctorStr of B,C;
cluster G * F -> comp-preserving ;
coherence
G * F is comp-preserving
proof end;
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 of A,B;
let G be feasible Contravariant comp-reversing FunctorStr of B,C;
cluster G * F -> comp-reversing ;
coherence
G * F is comp-reversing
proof end;
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 of A,B;
let G be feasible Covariant comp-preserving FunctorStr of B,C;
cluster G * F -> comp-reversing ;
coherence
G * F is comp-reversing
proof end;
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 func G * F -> strict covariant Functor of A,C;
coherence
G * F is strict covariant Functor of A,C
proof end;
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 func G * F -> strict covariant Functor of A,C;
coherence
G * F is strict covariant Functor of A,C
proof end;
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 func G * F -> strict contravariant Functor of A,C;
coherence
G * F is strict contravariant Functor of A,C
proof end;
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 func G * F -> strict contravariant Functor of A,C;
coherence
G * F is strict contravariant Functor of A,C
proof end;
end;

theorem Th10: :: FUNCTOR3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G1 is_transformable_to G2 holds
G1 * F1 is_transformable_to G2 * F2
proof end;

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 A1: F1 is_transformable_to F2 ;
func G * 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)
proof end;
uniqueness
for b1, b2 being transformation of G * F1,G * F2 st ( for o being object of A holds b1 . o = G . (t ! o) ) & ( for o being object of A holds b2 . o = G . (t ! o) ) holds
b1 = b2
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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 A1: G1 is_transformable_to G2 ;
func s * 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)
proof end;
uniqueness
for b1, b2 being transformation of G1 * F,G2 * F st ( for o being object of A holds b1 . o = s ! (F . o) ) & ( for o being object of A holds b2 . o = s ! (F . o) ) holds
b1 = b2
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th13: :: FUNCTOR3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
proof end;

theorem Th14: :: FUNCTOR3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
proof end;

theorem Th15: :: FUNCTOR3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th16: :: FUNCTOR3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th17: :: FUNCTOR3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th18: :: FUNCTOR3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th19: :: FUNCTOR3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th20: :: FUNCTOR3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th21: :: FUNCTOR3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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;
func s (#) 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
proof end;

theorem :: FUNCTOR3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCTOR3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCTOR3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCTOR3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: FUNCTOR3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G1 is_transformable_to G2 & H1 is_transformable_to H2 holds
(u (#) s) (#) t = u (#) (s (#) t)
proof end;

Lm2: now
let A, B, C be category;
let F1, F2 be covariant Functor of A,B;
let G1, G2 be covariant Functor of B,C;
let s be natural_transformation of G1,G2; :: thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & 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 & G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: ( G1 is_naturally_transformable_to G2 implies ( G1 * F1 is_naturally_transformable_to G2 * F2 & 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 & s (#) t is natural_transformation of G1 * F1,G2 * F2 )
then A4: G1 is_transformable_to G2 by FUNCTOR2:def 6;
set k = s (#) t;
A5: now
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)
let f be Morphism of a,b; :: thesis: ((s (#) t) ! b) * ((G1 * F1) . f) = ((G2 * F2) . f) * ((s (#) t) ! a)
A7: ( (G1 * F1) . a = G1 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by FUNCTOR0:34;
A8: ( (G1 * F1) . b = G1 . (F1 . b) & (G2 * F2) . b = G2 . (F2 . b) ) by FUNCTOR0:34;
A9: <^(F1 . b),(F2 . b)^> <> {} by A2, FUNCTOR2:def 1;
A10: <^(F1 . a),(F1 . b)^> <> {} by A6, FUNCTOR0:def 19;
then A11: <^(F1 . a),(F2 . b)^> <> {} by A9, ALTCAT_1:def 4;
A12: <^(F2 . a),(F2 . b)^> <> {} by A6, FUNCTOR0:def 19;
A13: <^(F1 . a),(F2 . a)^> <> {} by A2, FUNCTOR2:def 1;
A14: <^(G1 . (F1 . a)),(G2 . (F1 . a))^> <> {} by A4, FUNCTOR2:def 1;
A15: <^(G2 . (F1 . a)),(G2 . (F2 . a))^> <> {} by A13, FUNCTOR0:def 19;
A16: <^(G2 . (F2 . a)),(G2 . (F2 . b))^> <> {} by A12, FUNCTOR0:def 19;
A17: <^((G1 * F1) . a),((G1 * F1) . b)^> <> {} by A6, FUNCTOR0:def 19;
<^(G1 . (F1 . b)),(G1 . (F2 . b))^> <> {} by A9, FUNCTOR0:def 19;
then A18: <^((G1 * F1) . b),((G1 * F2) . b)^> <> {} by A8, FUNCTOR0:34;
<^(G1 . (F2 . b)),(G2 . (F2 . b))^> <> {} by A4, FUNCTOR2:def 1;
then A19: <^((G1 * F2) . b),((G2 * F2) . b)^> <> {} by A8, FUNCTOR0:34;
A20: G1 * F2 is_transformable_to G2 * F2 by A4, Th10;
A21: G1 * F1 is_transformable_to G1 * F2 by A2, Th10;
A22: s ! (F2 . b) = (s * F2) . b by A4, Def2;
A23: s ! (F2 . a) = (s * F2) . a by A4, Def2;
reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),((G1 * F2) . b) by A8, FUNCTOR0:34;
reconsider sF2b = s ! (F2 . b) as Morphism of ((G1 * F2) . b),((G2 * F2) . b) by A8, FUNCTOR0:34;
reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by A8, FUNCTOR0:34;
reconsider G1tbF1f = G1 . ((t ! b) * (F1 . f)) as Morphism of ((G1 * F1) . a),((G1 * F2) . b) by A7, FUNCTOR0:34;
reconsider G1ta = G1 . (t ! a) as Morphism of ((G1 * F1) . a),((G1 * F2) . a) by A7, FUNCTOR0:34;
reconsider sF2a = s ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) by A7, FUNCTOR0:34;
reconsider G2F2f = G2 . (F2 . f) as Morphism of ((G2 * F2) . a),((G2 * F2) . b) by A7, FUNCTOR0:34;
A24: G1 . ((t ! b) * (F1 . f)) = (G1 . (t ! b)) * (G1 . (F1 . f)) by A9, A10, FUNCTOR0:def 24
.= G1tb * G1F1f by A7, A8, FUNCTOR0:34 ;
thus ((s (#) t) ! b) * ((G1 * F1) . f) = (((s * F2) ! b) * ((G1 * t) ! b)) * ((G1 * F1) . f) by A20, A21, FUNCTOR2:def 5
.= (sF2b * ((G1 * t) ! b)) * ((G1 * F1) . f) by A20, A22, FUNCTOR2:def 4
.= (sF2b * G1tb) * ((G1 * F1) . f) by A2, Th11
.= (sF2b * G1tb) * G1F1f by A6, Th6
.= sF2b * G1tbF1f by A17, A18, A19, A24, ALTCAT_1:25
.= (s ! (F2 . b)) * (G1 . ((t ! b) * (F1 . f))) by A7, A8, FUNCTOR0:34
.= (G2 . ((t ! b) * (F1 . f))) * (s ! (F1 . a)) by A3, A11, 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 A12, A13, FUNCTOR0:def 24
.= (G2 . (F2 . f)) * ((G2 . (t ! a)) * (s ! (F1 . a))) by A14, A15, A16, ALTCAT_1:25
.= (G2 . (F2 . f)) * ((s ! (F2 . a)) * (G1 . (t ! a))) by A3, A13, FUNCTOR2:def 7
.= G2F2f * (sF2a * G1ta) by A7, A8, FUNCTOR0:34
.= ((G2 * F2) . f) * (sF2a * G1ta) by A6, Th6
.= ((G2 * F2) . f) * (((s * F2) ! a) * G1ta) by A20, A23, FUNCTOR2:def 4
.= ((G2 * F2) . f) * (((s * F2) ! a) * ((G1 * t) ! a)) by A2, Th11
.= ((G2 * F2) . f) * ((s (#) t) ! a) by A20, A21, FUNCTOR2:def 5 ; :: thesis: verum
end;
thus A25: 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 to FUNCTOR2: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;
thus s (#) t is natural_transformation of G1 * F1,G2 * F2 :: thesis: verum
proof
thus G1 * F1 is_naturally_transformable_to G2 * F2 by A25; :: according to FUNCTOR2:def 7 :: 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;
end;

theorem Th28: :: FUNCTOR3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th29: :: FUNCTOR3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCTOR3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G1 is_naturally_transformable_to G2 holds
( G1 * F1 is_naturally_transformable_to G2 * F2 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) by Lm2;

theorem :: FUNCTOR3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & F2 is_naturally_transformable_to F3 & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(s1 `*` s) (#) (t1 `*` t) = (s1 (#) t1) `*` (s (#) t)
proof end;

theorem Th32: :: FUNCTOR3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & F2 is_transformable_to F1 & ( for a being object of A holds t ! a is iso ) holds
( F2 is_naturally_transformable_to F1 & ex f being natural_transformation of F2,F1 st
for a being object of A holds
( f . a = (t ! a) " & f ! a is iso ) )
proof end;

definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
pred F1,F2 are_naturally_equivalent means :Def4: :: FUNCTOR3:def 4
( F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & 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 & F1 is_transformable_to F1 & ex t being natural_transformation of F1,F1 st
for a being object of A holds t ! a is iso )
proof end;
symmetry
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & 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 & F1 is_transformable_to F2 & ex t being natural_transformation of F2,F1 st
for a being object of A holds t ! a is iso )
proof end;
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 & F2 is_transformable_to F1 & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category
for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
F1,F3 are_naturally_equivalent
proof end;

theorem Th34: :: FUNCTOR3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3
proof end;

theorem Th35: :: FUNCTOR3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G1 * e is natural_equivalence of G1 * F1,G1 * F2 )
proof end;

theorem Th36: :: FUNCTOR3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & f * F1 is natural_equivalence of G1 * F1,G2 * F1 )
proof end;

theorem :: FUNCTOR3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & G1,G2 are_naturally_equivalent holds
( G1 * F1,G2 * F2 are_naturally_equivalent & f (#) e is natural_equivalence of G1 * F1,G2 * F2 )
proof end;

definition
let A, B be category;
let F1, F2 be covariant Functor of A,B;
let e be natural_equivalence of F1,F2;
assume A1: F1,F2 are_naturally_equivalent ;
func e " -> 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) "
proof end;
uniqueness
for b1, b2 being natural_equivalence of F2,F1 st ( for a being object of A holds b1 . a = (e ! a) " ) & ( for a being object of A holds b2 . a = (e ! a) " ) holds
b1 = b2
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) "
proof end;

theorem Th39: :: FUNCTOR3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCTOR3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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
proof end;
end;

theorem :: FUNCTOR3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: FUNCTOR3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
k " = (e " ) `*` (e1 " )
proof end;

theorem :: FUNCTOR3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being category
for F1 being covariant Functor of A,B holds (idt F1) " = idt F1
proof end;