:: Category of Functors between Alternative Categories
:: by Robert Nieszczerzewski
::
:: Received June 12, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster  ->  feasible id-preserving for Functor of A,B;
coherence
 for b1 being Functor of A,B holds
( b1 is feasible & b1 is id-preserving ) by FUNCTOR0:def_25;
end;

registration
let A be non empty transitive with_units AltCatStr ;
let B be non empty with_units AltCatStr ;
cluster covariant  ->  Covariant comp-preserving for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is covariant holds
( b1 is Covariant & b1 is comp-preserving ) by FUNCTOR0:def_26;
cluster Covariant comp-preserving  ->  covariant for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is Covariant & b1 is comp-preserving holds
b1 is covariant by FUNCTOR0:def_26;
cluster contravariant  ->  Contravariant comp-reversing for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is contravariant holds
( b1 is Contravariant & b1 is comp-reversing ) by FUNCTOR0:def_27;
cluster Contravariant comp-reversing  ->  contravariant for Functor of A,B;
coherence
 for b1 being Functor of A,B st b1 is Contravariant & b1 is comp-reversing holds
b1 is contravariant by FUNCTOR0:def_27;
end;

theorem Th1: :: FUNCTOR2:1
for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B
for a being object of A holds F . (idm a) = idm (F . a)
proofend;

begin

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
predF1 is_transformable_to F2 means :Def1: :: FUNCTOR2:def 1
 for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} ;
reflexivity
 for F1 being Functor of A,B
for a being object of A holds <^(F1 . a),(F1 . a)^> <> {} by ALTCAT_2:def_7;
end;

:: deftheorem Def1 defines is_transformable_to FUNCTOR2:def_1_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B holds
( F1 is_transformable_to F2 iff for a being object of A holds <^(F1 . a),(F2 . a)^> <> {} );

theorem Th2: :: FUNCTOR2:2
for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 holds
F is_transformable_to F2
proofend;

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
mode transformation of F1,F2 ->  ManySortedSet of the carrier of A means :Def2: :: FUNCTOR2:def 2
 for a being object of A holds it . a is Morphism of (F1 . a),(F2 . a);
existence
 ex b1 being ManySortedSet of the carrier of A st
for a being object of A holds b1 . a is Morphism of (F1 . a),(F2 . a)
proofend;
end;

:: deftheorem Def2 defines transformation FUNCTOR2:def_2_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for b5 being ManySortedSet of the carrier of A holds
( b5 is transformation of F1,F2 iff for a being object of A holds b5 . a is Morphism of (F1 . a),(F2 . a) );

definition
let A, B be non empty transitive with_units AltCatStr ;
let F be Functor of A,B;
func idt F ->  transformation of F,F means :Def3: :: FUNCTOR2:def 3
 for a being object of A holds it . a = idm (F . a);
existence
 ex b1 being transformation of F,F st
for a being object of A holds b1 . a = idm (F . a)
proofend;
uniqueness
 for b1, b2 being transformation of F,F st ( for a being object of A holds b1 . a = idm (F . a) ) &amp; ( for a being object of A holds b2 . a = idm (F . a) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines idt FUNCTOR2:def_3_:_
 for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for b4 being transformation of F,F holds
( b4 = idt F iff for a being object of A holds b4 . a = idm (F . a) );

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
assume A1: F1 is_transformable_to F2 ;
let t be transformation of F1,F2;
let a be object of A;
funct ! a ->  Morphism of (F1 . a),(F2 . a) means :Def4: :: FUNCTOR2:def 4
it = t . a;
existence
 ex b1 being Morphism of (F1 . a),(F2 . a) st b1 = t . a
proofend;
correctness
uniqueness
for b1, b2 being Morphism of (F1 . a),(F2 . a) st b1 = t . a &amp; b2 = t . a holds
b1 = b2;
;
end;

:: deftheorem Def4 defines ! FUNCTOR2:def_4_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being object of A
for b7 being Morphism of (F1 . a),(F2 . a) holds
( b7 = t ! a iff b7 = t . a );

definition
let A, B be non empty transitive with_units AltCatStr ;
let F, F1, F2 be Functor of A,B;
assume A1: ( F is_transformable_to F1 &amp; F1 is_transformable_to F2 ) ;
let t1 be transformation of F,F1;
let t2 be transformation of F1,F2;
funct2 `*` t1 ->  transformation of F,F2 means :Def5: :: FUNCTOR2:def 5
 for a being object of A holds it ! a = (t2 ! a) * (t1 ! a);
existence
 ex b1 being transformation of F,F2 st
for a being object of A holds b1 ! a = (t2 ! a) * (t1 ! a)
proofend;
uniqueness
 for b1, b2 being transformation of F,F2 st ( for a being object of A holds b1 ! a = (t2 ! a) * (t1 ! a) ) &amp; ( for a being object of A holds b2 ! a = (t2 ! a) * (t1 ! a) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines `*` FUNCTOR2:def_5_:_
 for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for b8 being transformation of F,F2 holds
( b8 = t2 `*` t1 iff for a being object of A holds b8 ! a = (t2 ! a) * (t1 ! a) );

theorem Th3: :: FUNCTOR2:3
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being object of A holds t1 ! a = t2 ! a ) holds
t1 = t2
proofend;

theorem Th4: :: FUNCTOR2:4
for A, B being non empty transitive with_units AltCatStr
for F being Functor of A,B
for a being object of A holds (idt F) ! a = idm (F . a)
proofend;

theorem Th5: :: FUNCTOR2:5
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2 holds
( (idt F2) `*` t = t &amp; t `*` (idt F1) = t )
proofend;

theorem Th6: :: FUNCTOR2:6
for A, B being category
for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 &amp; F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
proofend;

begin

Lm1:  for A, B being non empty transitive with_units AltCatStr
for F, G being covariant Functor of A,B
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
proofend;

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
predF1 is_naturally_transformable_to F2 means :Def6: :: FUNCTOR2:def 6
( F1 is_transformable_to F2 &amp; ex t being transformation of F1,F2 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) );
reflexivity
 for F1 being covariant Functor of A,B holds
( F1 is_transformable_to F1 &amp; ex t being transformation of F1,F1 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F1 . f) * (t ! a) )
proofend;
end;

:: deftheorem Def6 defines is_naturally_transformable_to FUNCTOR2:def_6_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B holds
( F1 is_naturally_transformable_to F2 iff ( F1 is_transformable_to F2 &amp; ex t being transformation of F1,F2 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ) );

theorem :: FUNCTOR2:7
for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B holds F is_naturally_transformable_to F ;

Lm2:  for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_transformable_to F1 &amp; F1 is_transformable_to F2 holds
for t1 being transformation of F,F1 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a) ) holds
for t2 being transformation of F1,F2 st ( for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a) ) holds
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
proofend;

theorem Th8: :: FUNCTOR2:8
for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2
proofend;

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
assume A1: F1 is_naturally_transformable_to F2 ;
mode natural_transformation of F1,F2 ->  transformation of F1,F2 means :Def7: :: FUNCTOR2:def 7
 for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (it ! b) * (F1 . f) = (F2 . f) * (it ! a);
existence
 ex b1 being transformation of F1,F2 st
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b1 ! b) * (F1 . f) = (F2 . f) * (b1 ! a) by A1, Def6;
end;

:: deftheorem Def7 defines natural_transformation FUNCTOR2:def_7_:_
 for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for b5 being transformation of F1,F2 holds
( b5 is natural_transformation of F1,F2 iff for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (b5 ! b) * (F1 . f) = (F2 . f) * (b5 ! a) );

definition
let A, B be non empty transitive with_units AltCatStr ;
let F be covariant Functor of A,B;
:: original:idt
redefine func idt F ->  natural_transformation of F,F;
coherence
 idt F is natural_transformation of F,F
proofend;
end;

definition
let A, B be category;
let F, F1, F2 be covariant Functor of A,B;
assume B1: ( F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 ) ;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
funct2 `*` t1 ->  natural_transformation of F,F2 means :Def8: :: FUNCTOR2:def 8
it = t2 `*` t1;
existence
 ex b1 being natural_transformation of F,F2 st b1 = t2 `*` t1
proofend;
correctness
uniqueness
for b1, b2 being natural_transformation of F,F2 st b1 = t2 `*` t1 &amp; b2 = t2 `*` t1 holds
b1 = b2;
;
end;

:: deftheorem Def8 defines `*` FUNCTOR2:def_8_:_
 for A, B being category
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for b8 being natural_transformation of F,F2 holds
( b8 = t2 `*` t1 iff b8 = t2 `*` t1 );

theorem :: FUNCTOR2:9
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds
( (idt F2) `*` t = t &amp; t `*` (idt F1) = t )
proofend;

theorem :: FUNCTOR2:10
for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
proofend;

theorem :: FUNCTOR2:11
for A, B being category
for F, F1, F2, F3 being covariant Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 &amp; F1 is_naturally_transformable_to F2 &amp; F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
proofend;

begin

definition
let I be set ;
let A, B be ManySortedSet of I;
func Funcs (A,B) ->  set  means :Def9: :: FUNCTOR2:def 9
 for x being set holds
( x in it iff x is ManySortedFunction of A,B ) if  for i being set st i in I &amp; B . i = {} holds
A . i = {}
otherwise it = {} ;
existence
 ( ( ( for i being set st i in I &amp; B . i = {} holds
A . i = {} ) implies ex b1 being set st
for x being set holds
( x in b1 iff x is ManySortedFunction of A,B ) ) &amp; ( ex i being set st
( i in I &amp; B . i = {} &amp; not A . i = {} ) implies ex b1 being set st b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( ( for i being set st i in I &amp; B . i = {} holds
A . i = {} ) &amp; ( for x being set holds
( x in b1 iff x is ManySortedFunction of A,B ) ) &amp; ( for x being set holds
( x in b2 iff x is ManySortedFunction of A,B ) ) implies b1 = b2 ) &amp; ( ex i being set st
( i in I &amp; B . i = {} &amp; not A . i = {} ) &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) )
proofend;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def9 defines Funcs FUNCTOR2:def_9_:_
 for I being set
for A, B being ManySortedSet of I
for b4 being set holds
( ( ( for i being set st i in I &amp; B . i = {} holds
A . i = {} ) implies ( b4 = Funcs (A,B) iff for x being set holds
( x in b4 iff x is ManySortedFunction of A,B ) ) ) &amp; ( ex i being set st
( i in I &amp; B . i = {} &amp; not A . i = {} ) implies ( b4 = Funcs (A,B) iff b4 = {} ) ) );

definition
let A, B be non empty transitive with_units AltCatStr ;
func Funct (A,B) ->  set  means :Def10: :: FUNCTOR2:def 10
 for x being set holds
( x in it iff x is strict covariant Functor of A,B );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is strict covariant Functor of A,B )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict covariant Functor of A,B ) ) &amp; ( for x being set holds
( x in b2 iff x is strict covariant Functor of A,B ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines Funct FUNCTOR2:def_10_:_
 for A, B being non empty transitive with_units AltCatStr
for b3 being set holds
( b3 = Funct (A,B) iff for x being set holds
( x in b3 iff x is strict covariant Functor of A,B ) );

definition
let A, B be category;
func Functors (A,B) ->  non empty transitive strict AltCatStr  means :: FUNCTOR2:def 11
( the carrier of it = Funct (A,B) &amp; ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of it . (F,G) iff ( F is_naturally_transformable_to G &amp; x is natural_transformation of F,G ) ) ) &amp; ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G &amp; G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of it . (F,G,H) &amp; f . (t2,t1) = t2 `*` t1 ) ) );
existence
 ex b1 being non empty transitive strict AltCatStr st
( the carrier of b1 = Funct (A,B) &amp; ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b1 . (F,G) iff ( F is_naturally_transformable_to G &amp; x is natural_transformation of F,G ) ) ) &amp; ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G &amp; G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b1 . (F,G,H) &amp; f . (t2,t1) = t2 `*` t1 ) ) )
proofend;
uniqueness
 for b1, b2 being non empty transitive strict AltCatStr st the carrier of b1 = Funct (A,B) &amp; ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b1 . (F,G) iff ( F is_naturally_transformable_to G &amp; x is natural_transformation of F,G ) ) ) &amp; ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G &amp; G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b1 . (F,G,H) &amp; f . (t2,t1) = t2 `*` t1 ) ) &amp; the carrier of b2 = Funct (A,B) &amp; ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b2 . (F,G) iff ( F is_naturally_transformable_to G &amp; x is natural_transformation of F,G ) ) ) &amp; ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G &amp; G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b2 . (F,G,H) &amp; f . (t2,t1) = t2 `*` t1 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines Functors FUNCTOR2:def_11_:_
 for A, B being category
for b3 being non empty transitive strict AltCatStr holds
( b3 = Functors (A,B) iff ( the carrier of b3 = Funct (A,B) &amp; ( for F, G being strict covariant Functor of A,B
for x being set holds
( x in the Arrows of b3 . (F,G) iff ( F is_naturally_transformable_to G &amp; x is natural_transformation of F,G ) ) ) &amp; ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G &amp; G is_naturally_transformable_to H holds
for t1 being natural_transformation of F,G
for t2 being natural_transformation of G,H ex f being Function st
( f = the Comp of b3 . (F,G,H) &amp; f . (t2,t1) = t2 `*` t1 ) ) ) );