:: Category of Functors between Alternative Categories
:: by Robert Nieszczerzewski
::
:: Copyright (c) 1997-2021 Association of Mizar Users

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 ;
coherence
for b1 being Functor of A,B st b1 is covariant holds
( b1 is Covariant & b1 is comp-preserving )
by FUNCTOR0:def 26;
coherence
for b1 being Functor of A,B st b1 is Covariant & b1 is comp-preserving holds
b1 is covariant
by FUNCTOR0:def 26;
coherence
for b1 being Functor of A,B st b1 is contravariant holds
( b1 is Contravariant & b1 is comp-reversing )
by FUNCTOR0:def 27;
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)
proof end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be Functor of A,B;
pred F1 is_transformable_to F2 means :: 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 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 & F1 is_transformable_to F2 holds
F is_transformable_to F2
proof end;

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)
proof end;
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)
proof end;
uniqueness
for b1, b2 being transformation of F,F st ( for a being Object of A holds b1 . a = idm (F . a) ) & ( for a being Object of A holds b2 . a = idm (F . a) ) holds
b1 = b2
proof end;
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;
func t ! 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
proof end;
correctness
uniqueness
for b1, b2 being Morphism of (F1 . a),(F2 . a) st b1 = t . a & 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 & F1 is_transformable_to F2 ) ;
let t1 be transformation of F,F1;
let t2 be transformation of F1,F2;
func t2 * 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)
proof end;
uniqueness
for b1, b2 being transformation of F,F2 st ( for a being Object of A holds b1 ! a = (t2 ! a) * (t1 ! a) ) & ( for a being Object of A holds b2 ! a = (t2 ! a) * (t1 ! a) ) holds
b1 = b2
proof end;
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 & 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
proof end;

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

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 & t * (idt F1) = t )
proof end;

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 & F1 is_transformable_to F2 & 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)
proof end;

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)

proof end;

definition
let A, B be non empty transitive with_units AltCatStr ;
let F1, F2 be covariant Functor of A,B;
pred F1 is_naturally_transformable_to F2 means :: FUNCTOR2:def 6
( F1 is_transformable_to F2 & 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 & 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) )
proof end;
end;

:: deftheorem 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 & 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 & 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)

proof end;

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 & F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2
proof end;

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

definition
let A, B be category;
let F, F1, F2 be covariant Functor of A,B;
assume A1: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 ) ;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
func t2 * 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
proof end;
correctness
uniqueness
for b1, b2 being natural_transformation of F,F2 st b1 = t2 * t1 & 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 & 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 & t * (idt F1) = t ) by Th5;

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 & 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) by Def5;

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 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
for t3 being natural_transformation of F2,F3 holds (t3 * t1) * t = t3 * (t1 * t)
proof end;

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 & B . i = {} holds
A . i = {}
otherwise it = {} ;
existence
( ( ( for i being set st i in I & 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 ) ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ex b1 being set st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) & ( for x being set holds
( x in b1 iff x is ManySortedFunction of A,B ) ) & ( for x being set holds
( x in b2 iff x is ManySortedFunction of A,B ) ) implies b1 = b2 ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
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 & 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 ) ) ) & ( ex i being set st
( i in I & B . i = {} & 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 object holds
( x in it iff x is strict covariant Functor of A,B );
existence
ex b1 being set st
for x being object holds
( x in b1 iff x is strict covariant Functor of A,B )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff x is strict covariant Functor of A,B ) ) & ( for x being object holds
( x in b2 iff x is strict covariant Functor of A,B ) ) holds
b1 = b2
proof end;
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 object 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) & ( 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 & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & 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) & f . (t2,t1) = t2 * t1 ) ) );
existence
ex b1 being non empty transitive strict AltCatStr st
( the carrier of b1 = Funct (A,B) & ( 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 & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & 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) & f . (t2,t1) = t2 * t1 ) ) )
proof end;
uniqueness
for b1, b2 being non empty transitive strict AltCatStr st the carrier of b1 = Funct (A,B) & ( 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 & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & 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) & f . (t2,t1) = t2 * t1 ) ) & the carrier of b2 = Funct (A,B) & ( 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 & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & 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) & f . (t2,t1) = t2 * t1 ) ) holds
b1 = b2
proof end;
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) & ( 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 & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & 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) & f . (t2,t1) = t2 * t1 ) ) ) );