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

registration

cluster non empty transitive strict associative with_units for AltCatStr ;

existence
ex b₁ being non empty AltCatStr st
( b₁ is transitive & b₁ is associative & b₁ is with_units & b₁ 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 for FunctorStr over A,B;

existence
ex b₁ being FunctorStr over A,B st
( b₁ is strict & b₁ is comp-preserving & b₁ is comp-reversing & b₁ is Covariant & b₁ is Contravariant & b₁ 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 for FunctorStr over A,B;

existence
ex b₁ being FunctorStr over A,B st
( b₁ is strict & b₁ is comp-preserving & b₁ is comp-reversing & b₁ is Covariant & b₁ is Contravariant & b₁ is feasible & b₁ 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 id-preserving covariant contravariant for Functor of A,B;

existence
ex b₁ being Functor of A,B st
( b₁ is strict & b₁ is feasible & b₁ is covariant & b₁ is contravariant )

proof end;

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 & 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

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))

proof end;

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))

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
for M being ManySortedFunction of A,B * f holds ((id B) * f) ** M = M

proof end;

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 #)

proof end;

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 #)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

theorem Th9: :: FUNCTOR3:9

for A being non empty AltCatStr
for B, C 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)

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 over A,B;
let G be feasible Covariant comp-preserving FunctorStr over 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 over A,B;
let G be feasible Contravariant comp-reversing FunctorStr over 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 over A,B;
let G be feasible Contravariant comp-reversing FunctorStr over 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 over A,B;
let G be feasible Covariant comp-preserving FunctorStr over 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 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 func G * 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 func G * 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 func G * 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 & 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 b₁ being transformation of G * F1,G * F2 st
for o being Object of A holds b₁ . o = G . (t ! o)

proof end;

uniqueness
for b₁, b₂ being transformation of G * F1,G * F2 st ( for o being Object of A holds b₁ . o = G . (t ! o) ) & ( for o being Object of A holds b₂ . o = G . (t ! o) ) holds
b₁ = b₂

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 b₈ being transformation of G * F1,G * F2 holds
( b₈ = G * t iff for o being Object of A holds b₈ . o = G . (t ! o) );

theorem Th11: :: FUNCTOR3:11

for A, B, C 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 b₁ being transformation of G1 * F,G2 * F st
for o being Object of A holds b₁ . o = s ! (F . o)

proof end;

uniqueness
for b₁, b₂ being transformation of G1 * F,G2 * F st ( for o being Object of A holds b₁ . o = s ! (F . o) ) & ( for o being Object of A holds b₂ . o = s ! (F . o) ) holds
b₁ = b₂

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 b₈ being transformation of G1 * F,G2 * F holds
( b₈ = s * F iff for o being Object of A holds b₈ . o = s ! (F . o) );

theorem Th12: :: FUNCTOR3:12

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
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

for A, B, C 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

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

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

for A, B, C, D 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

for A, B, C, D 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

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

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

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

for B, C 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

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 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

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

for B, C 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

for A, B, C 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

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

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 :: 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 & 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 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 & 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 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 & 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 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 & 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 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 ) )
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 & s (#) t is natural_transformation of G1 * F1,G2 * F2 ) )
then A2: F1 is_transformable_to F2 ;
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 ;

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;
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;
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;
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;
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 by A2, A4, Th10, A5; :: thesis: s (#) t is natural_transformation of G1 * F1,G2 * F2
hence s (#) t is natural_transformation of G1 * F1,G2 * F2 by A5, FUNCTOR2:def 7; :: thesis: verum

end;

theorem Th28: :: FUNCTOR3:28

for A, B, C 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

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

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

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

for A, B 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 b₁ being natural_transformation of F1,F2 st
for a being Object of A holds b₁ ! a is iso by A1;

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 b₅ being natural_transformation of F1,F2 holds
( b₅ is natural_equivalence of F1,F2 iff for a being Object of A holds b₅ ! 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 & F2,F3 are_naturally_equivalent holds
F1,F3 are_naturally_equivalent

proof end;

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 & F2,F3 are_naturally_equivalent holds
e1 `*` e is natural_equivalence of F1,F3

proof end;

theorem Th35: :: FUNCTOR3:35

for A, B, C 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

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

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 b₁ being natural_equivalence of F2,F1 st
for a being Object of A holds b₁ . a = (e ! a) "

proof end;

uniqueness
for b₁, b₂ being natural_equivalence of F2,F1 st ( for a being Object of A holds b₁ . a = (e ! a) " ) & ( for a being Object of A holds b₂ . a = (e ! a) " ) holds
b₁ = b₂

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 b₆ being natural_equivalence of F2,F1 holds
( b₆ = e " iff for a being Object of A holds b₆ . a = (e ! a) " );

theorem Th38: :: FUNCTOR3:38

for A, B 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

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

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

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

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
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

for A, B being category
for F1 being covariant Functor of A,B holds (idt F1) " = idt F1

proof end;