:: by Artur Korni{\l}owicz

::

:: Received January 21, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

registration

existence

ex b_{1} being non empty AltCatStr st

( b_{1} is transitive & b_{1} is associative & b_{1} is with_units & b_{1} is strict )

end;
ex b

( b

proof end;

registration

let A be non empty transitive AltCatStr ;

let B be non empty with_units AltCatStr ;

ex b_{1} being FunctorStr over A,B st

( b_{1} is strict & b_{1} is comp-preserving & b_{1} is comp-reversing & b_{1} is Covariant & b_{1} is Contravariant & b_{1} is feasible )

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

( b

proof end;

registration

let A be non empty transitive with_units AltCatStr ;

let B be non empty with_units AltCatStr ;

ex b_{1} being FunctorStr over A,B st

( b_{1} is strict & b_{1} is comp-preserving & b_{1} is comp-reversing & b_{1} is Covariant & b_{1} is Contravariant & b_{1} is feasible & b_{1} is id-preserving )

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

( b

proof end;

registration

let A be non empty transitive with_units AltCatStr ;

let B be non empty with_units AltCatStr ;

existence

ex b_{1} being Functor of A,B st

( b_{1} is strict & b_{1} is feasible & b_{1} is covariant & b_{1} is contravariant )

end;
let B be non empty with_units AltCatStr ;

existence

ex b

( b

proof 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

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

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

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

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

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)

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)

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)

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)

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;

coherence

G * F is comp-preserving

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

coherence

G * F is comp-preserving

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 Contravariant comp-reversing FunctorStr over A,B;

let G be feasible Contravariant comp-reversing FunctorStr over B,C;

coherence

G * F is comp-preserving

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

coherence

G * F is comp-preserving

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 Contravariant comp-reversing FunctorStr over B,C;

coherence

G * F is comp-reversing

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

coherence

G * F is comp-reversing

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 Contravariant comp-reversing FunctorStr over A,B;

let G be feasible Covariant comp-preserving FunctorStr over B,C;

coherence

G * F is comp-reversing

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

coherence

G * F is comp-reversing

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

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

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

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

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

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 ;

ex b_{1} being transformation of G * F1,G * F2 st

for o being Object of A holds b_{1} . o = G . (t ! o)

for b_{1}, b_{2} being transformation of G * F1,G * F2 st ( for o being Object of A holds b_{1} . o = G . (t ! o) ) & ( for o being Object of A holds b_{2} . o = G . (t ! o) ) holds

b_{1} = b_{2}

end;
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 for o being Object of A holds it . o = G . (t ! o);

ex b

for o being Object of A holds b

proof end;

uniqueness for b

b

proof 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_{8} being transformation of G * F1,G * F2 holds

( b_{8} = G * t iff for o being Object of A holds b_{8} . o = G . (t ! o) );

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

( b

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)

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 ;

ex b_{1} being transformation of G1 * F,G2 * F st

for o being Object of A holds b_{1} . o = s ! (F . o)

for b_{1}, b_{2} being transformation of G1 * F,G2 * F st ( for o being Object of A holds b_{1} . o = s ! (F . o) ) & ( for o being Object of A holds b_{2} . o = s ! (F . o) ) holds

b_{1} = b_{2}

end;
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 for o being Object of A holds it . o = s ! (F . o);

ex b

for o being Object of A holds b

proof end;

uniqueness for b

b

proof 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_{8} being transformation of G1 * F,G2 * F holds

( b_{8} = s * F iff for o being Object of A holds b_{8} . o = s ! (F . o) );

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

( b

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)

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)

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)

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)

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)

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)

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)

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)

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

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

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;

coherence

(s * F2) `*` (G1 * t) is transformation of G1 * F1,G2 * F2 ;

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

coherence

(s * F2) `*` (G1 * t) is transformation of G1 * F1,G2 * F2 ;

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

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)

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

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

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

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)

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)

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 )

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 ;

hence s (#) t is natural_transformation of G1 * F1,G2 * F2 by A5, FUNCTOR2:def 7; :: thesis: verum

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

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

hence s (#) t is natural_transformation of G1 * F1,G2 * F2 by A5, FUNCTOR2:def 7; :: thesis: verum

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

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

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;

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)

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

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;

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 )

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 )

end;
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 ( 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 );

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;

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

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 ;

ex b_{1} being natural_transformation of F1,F2 st

for a being Object of A holds b_{1} ! a is iso
by A1;

end;
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 for a being Object of A holds it ! a is iso ;

ex b

for a being Object of A holds b

:: 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_{5} being natural_transformation of F1,F2 holds

( b_{5} is natural_equivalence of F1,F2 iff for a being Object of A holds b_{5} ! a is iso );

for A, B being category

for F1, F2 being covariant Functor of A,B st F1,F2 are_naturally_equivalent holds

for b

( b

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

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

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 )

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 )

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 )

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 ;

ex b_{1} being natural_equivalence of F2,F1 st

for a being Object of A holds b_{1} . a = (e ! a) "

for b_{1}, b_{2} being natural_equivalence of F2,F1 st ( for a being Object of A holds b_{1} . a = (e ! a) " ) & ( for a being Object of A holds b_{2} . a = (e ! a) " ) holds

b_{1} = b_{2}

end;
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 for a being Object of A holds it . a = (e ! a) " ;

ex b

for a being Object of A holds b

proof end;

uniqueness for b

b

proof 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_{6} being natural_equivalence of F2,F1 holds

( b_{6} = e " iff for a being Object of A holds b_{6} . a = (e ! a) " );

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

( b

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

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

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

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

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

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

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

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;