:: FUNCTOR2 semantic presentation

registration
let c1 be non empty transitive with_units AltCatStr ;
let c2 be non empty with_units AltCatStr ;
cluster -> feasible id-preserving Functor of a1,a2;
coherence
for b1 being Functor of c1,c2 holds
( b1 is feasible & b1 is id-preserving ) by FUNCTOR0:def 26;
end;

registration
let c1 be non empty transitive with_units AltCatStr ;
let c2 be non empty with_units AltCatStr ;
cluster covariant -> feasible Covariant id-preserving comp-preserving Functor of a1,a2;
coherence
for b1 being Functor of c1,c2 st b1 is covariant holds
( b1 is Covariant & b1 is comp-preserving ) by FUNCTOR0:def 27;
cluster Covariant comp-preserving -> feasible id-preserving covariant Functor of a1,a2;
coherence
for b1 being Functor of c1,c2 st b1 is Covariant & b1 is comp-preserving holds
b1 is covariant by FUNCTOR0:def 27;
cluster contravariant -> feasible Contravariant id-preserving comp-reversing Functor of a1,a2;
coherence
for b1 being Functor of c1,c2 st b1 is contravariant holds
( b1 is Contravariant & b1 is comp-reversing ) by FUNCTOR0:def 28;
cluster Contravariant comp-reversing -> feasible id-preserving contravariant Functor of a1,a2;
coherence
for b1 being Functor of c1,c2 st b1 is Contravariant & b1 is comp-reversing holds
b1 is contravariant by FUNCTOR0:def 28;
end;

theorem Th1: :: FUNCTOR2:1
canceled;

theorem Th2: :: FUNCTOR2:2
for b1, b2 being non empty transitive with_units AltCatStr
for b3 being covariant Functor of b1,b2
for b4 being object of b1 holds b3 . (idm b4) = idm (b3 . b4)
proof end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3, c4 be covariant Functor of c1,c2;
pred c3 is_transformable_to c4 means :Def1: :: FUNCTOR2:def 1
for b1 being object of a1 holds <^(a3 . b1),(a4 . b1)^> <> {} ;
reflexivity
for b1 being covariant Functor of c1,c2
for b2 being object of c1 holds <^(b1 . b2),(b1 . b2)^> <> {} by ALTCAT_2:def 7;
end;

:: deftheorem Def1 defines is_transformable_to FUNCTOR2:def 1 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 holds
( b3 is_transformable_to b4 iff for b5 being object of b1 holds <^(b3 . b5),(b4 . b5)^> <> {} );

theorem Th3: :: FUNCTOR2:3
canceled;

theorem Th4: :: FUNCTOR2:4
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4, b5 being covariant Functor of b1,b2 st b3 is_transformable_to b4 & b4 is_transformable_to b5 holds
b3 is_transformable_to b5
proof end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3, c4 be covariant Functor of c1,c2;
assume E4: c3 is_transformable_to c4 ;
mode transformation of c3,c4 -> ManySortedSet of the carrier of a1 means :Def2: :: FUNCTOR2:def 2
for b1 being object of a1 holds a5 . b1 is Morphism of (a3 . b1),(a4 . b1);
existence
ex b1 being ManySortedSet of the carrier of c1 st
for b2 being object of c1 holds b1 . b2 is Morphism of (c3 . b2),(c4 . b2)
proof end;
end;

:: deftheorem Def2 defines transformation FUNCTOR2:def 2 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 st b3 is_transformable_to b4 holds
for b5 being ManySortedSet of the carrier of b1 holds
( b5 is transformation of b3,b4 iff for b6 being object of b1 holds b5 . b6 is Morphism of (b3 . b6),(b4 . b6) );

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3 be covariant Functor of c1,c2;
func idt c3 -> transformation of a3,a3 means :Def3: :: FUNCTOR2:def 3
for b1 being object of a1 holds a4 . b1 = idm (a3 . b1);
existence
ex b1 being transformation of c3,c3 st
for b2 being object of c1 holds b1 . b2 = idm (c3 . b2)
proof end;
uniqueness
for b1, b2 being transformation of c3,c3 st ( for b3 being object of c1 holds b1 . b3 = idm (c3 . b3) ) & ( for b3 being object of c1 holds b2 . b3 = idm (c3 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines idt FUNCTOR2:def 3 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3 being covariant Functor of b1,b2
for b4 being transformation of b3,b3 holds
( b4 = idt b3 iff for b5 being object of b1 holds b4 . b5 = idm (b3 . b5) );

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3, c4 be covariant Functor of c1,c2;
assume E6: c3 is_transformable_to c4 ;
let c5 be transformation of c3,c4;
let c6 be object of c1;
func c5 ! c6 -> Morphism of (a3 . a6),(a4 . a6) means :Def4: :: FUNCTOR2:def 4
a7 = a5 . a6;
existence
ex b1 being Morphism of (c3 . c6),(c4 . c6) st b1 = c5 . c6
proof end;
correctness
uniqueness
for b1, b2 being Morphism of (c3 . c6),(c4 . c6) st b1 = c5 . c6 & b2 = c5 . c6 holds
b1 = b2;
;
end;

:: deftheorem Def4 defines ! FUNCTOR2:def 4 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 st b3 is_transformable_to b4 holds
for b5 being transformation of b3,b4
for b6 being object of b1
for b7 being Morphism of (b3 . b6),(b4 . b6) holds
( b7 = b5 ! b6 iff b7 = b5 . b6 );

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3, c4, c5 be covariant Functor of c1,c2;
assume that
E7: c3 is_transformable_to c4 and
E8: c4 is_transformable_to c5 ;
let c6 be transformation of c3,c4;
let c7 be transformation of c4,c5;
func c7 `*` c6 -> transformation of a3,a5 means :Def5: :: FUNCTOR2:def 5
for b1 being object of a1 holds a8 ! b1 = (a7 ! b1) * (a6 ! b1);
existence
ex b1 being transformation of c3,c5 st
for b2 being object of c1 holds b1 ! b2 = (c7 ! b2) * (c6 ! b2)
proof end;
uniqueness
for b1, b2 being transformation of c3,c5 st ( for b3 being object of c1 holds b1 ! b3 = (c7 ! b3) * (c6 ! b3) ) & ( for b3 being object of c1 holds b2 ! b3 = (c7 ! b3) * (c6 ! b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines `*` FUNCTOR2:def 5 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4, b5 being covariant Functor of b1,b2 st b3 is_transformable_to b4 & b4 is_transformable_to b5 holds
for b6 being transformation of b3,b4
for b7 being transformation of b4,b5
for b8 being transformation of b3,b5 holds
( b8 = b7 `*` b6 iff for b9 being object of b1 holds b8 ! b9 = (b7 ! b9) * (b6 ! b9) );

theorem Th5: :: FUNCTOR2:5
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 st b3 is_transformable_to b4 holds
for b5, b6 being transformation of b3,b4 st ( for b7 being object of b1 holds b5 ! b7 = b6 ! b7 ) holds
b5 = b6
proof end;

theorem Th6: :: FUNCTOR2:6
for b1, b2 being non empty transitive with_units AltCatStr
for b3 being covariant Functor of b1,b2
for b4 being object of b1 holds (idt b3) ! b4 = idm (b3 . b4)
proof end;

theorem Th7: :: FUNCTOR2:7
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 st b3 is_transformable_to b4 holds
for b5 being transformation of b3,b4 holds
( (idt b4) `*` b5 = b5 & b5 `*` (idt b3) = b5 )
proof end;

theorem Th8: :: FUNCTOR2:8
for b1, b2 being category
for b3, b4, b5, b6 being covariant Functor of b1,b2 st b3 is_transformable_to b4 & b4 is_transformable_to b5 & b5 is_transformable_to b6 holds
for b7 being transformation of b3,b4
for b8 being transformation of b4,b5
for b9 being transformation of b5,b6 holds (b9 `*` b8) `*` b7 = b9 `*` (b8 `*` b7)
proof end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3, c4 be covariant Functor of c1,c2;
pred c3 is_naturally_transformable_to c4 means :Def6: :: FUNCTOR2:def 6
( a3 is_transformable_to a4 & ex b1 being transformation of a3,a4 st
for b2, b3 being object of a1 st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds (b1 ! b3) * (a3 . b4) = (a4 . b4) * (b1 ! b2) );
end;

:: deftheorem Def6 defines is_naturally_transformable_to FUNCTOR2:def 6 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 holds
( b3 is_naturally_transformable_to b4 iff ( b3 is_transformable_to b4 & ex b5 being transformation of b3,b4 st
for b6, b7 being object of b1 st <^b6,b7^> <> {} holds
for b8 being Morphism of b6,b7 holds (b5 ! b7) * (b3 . b8) = (b4 . b8) * (b5 ! b6) ) );

Lemma13: for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2
for b5, b6 being object of b1 st <^b5,b6^> <> {} holds
for b7 being Morphism of b5,b6 holds ((idt b3) ! b6) * (b3 . b7) = (b3 . b7) * ((idt b3) ! b5)
proof end;

theorem Th9: :: FUNCTOR2:9
for b1, b2 being non empty transitive with_units AltCatStr
for b3 being covariant Functor of b1,b2 holds b3 is_naturally_transformable_to b3
proof end;

Lemma15: for b1, b2 being category
for b3, b4, b5 being covariant Functor of b1,b2 st b3 is_transformable_to b4 & b4 is_transformable_to b5 holds
for b6 being transformation of b3,b4 st ( for b7, b8 being object of b1 st <^b7,b8^> <> {} holds
for b9 being Morphism of b7,b8 holds (b6 ! b8) * (b3 . b9) = (b4 . b9) * (b6 ! b7) ) holds
for b7 being transformation of b4,b5 st ( for b8, b9 being object of b1 st <^b8,b9^> <> {} holds
for b10 being Morphism of b8,b9 holds (b7 ! b9) * (b4 . b10) = (b5 . b10) * (b7 ! b8) ) holds
for b8, b9 being object of b1 st <^b8,b9^> <> {} holds
for b10 being Morphism of b8,b9 holds ((b7 `*` b6) ! b9) * (b3 . b10) = (b5 . b10) * ((b7 `*` b6) ! b8)
proof end;

theorem Th10: :: FUNCTOR2:10
for b1, b2 being category
for b3, b4, b5 being covariant Functor of b1,b2 st b3 is_naturally_transformable_to b4 & b4 is_naturally_transformable_to b5 holds
b3 is_naturally_transformable_to b5
proof end;

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3, c4 be covariant Functor of c1,c2;
assume E17: c3 is_naturally_transformable_to c4 ;
mode natural_transformation of c3,c4 -> transformation of a3,a4 means :Def7: :: FUNCTOR2:def 7
for b1, b2 being object of a1 st <^b1,b2^> <> {} holds
for b3 being Morphism of b1,b2 holds (a5 ! b2) * (a3 . b3) = (a4 . b3) * (a5 ! b1);
existence
ex b1 being transformation of c3,c4 st
for b2, b3 being object of c1 st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3 holds (b1 ! b3) * (c3 . b4) = (c4 . b4) * (b1 ! b2) by E17, Def6;
end;

:: deftheorem Def7 defines natural_transformation FUNCTOR2:def 7 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 st b3 is_naturally_transformable_to b4 holds
for b5 being transformation of b3,b4 holds
( b5 is natural_transformation of b3,b4 iff for b6, b7 being object of b1 st <^b6,b7^> <> {} holds
for b8 being Morphism of b6,b7 holds (b5 ! b7) * (b3 . b8) = (b4 . b8) * (b5 ! b6) );

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
let c3 be covariant Functor of c1,c2;
redefine func idt as idt c3 -> natural_transformation of a3,a3;
coherence
idt c3 is natural_transformation of c3,c3
proof end;
end;

definition
let c1, c2 be category;
let c3, c4, c5 be covariant Functor of c1,c2;
assume that
E18: c3 is_naturally_transformable_to c4 and
E19: c4 is_naturally_transformable_to c5 ;
let c6 be natural_transformation of c3,c4;
let c7 be natural_transformation of c4,c5;
func c7 `*` c6 -> natural_transformation of a3,a5 means :Def8: :: FUNCTOR2:def 8
a8 = a7 `*` a6;
existence
ex b1 being natural_transformation of c3,c5 st b1 = c7 `*` c6
proof end;
correctness
uniqueness
for b1, b2 being natural_transformation of c3,c5 st b1 = c7 `*` c6 & b2 = c7 `*` c6 holds
b1 = b2;
;
end;

:: deftheorem Def8 defines `*` FUNCTOR2:def 8 :
for b1, b2 being category
for b3, b4, b5 being covariant Functor of b1,b2 st b3 is_naturally_transformable_to b4 & b4 is_naturally_transformable_to b5 holds
for b6 being natural_transformation of b3,b4
for b7 being natural_transformation of b4,b5
for b8 being natural_transformation of b3,b5 holds
( b8 = b7 `*` b6 iff b8 = b7 `*` b6 );

theorem Th11: :: FUNCTOR2:11
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4 being covariant Functor of b1,b2 st b3 is_naturally_transformable_to b4 holds
for b5 being natural_transformation of b3,b4 holds
( (idt b4) `*` b5 = b5 & b5 `*` (idt b3) = b5 )
proof end;

theorem Th12: :: FUNCTOR2:12
for b1, b2 being non empty transitive with_units AltCatStr
for b3, b4, b5 being covariant Functor of b1,b2 st b3 is_naturally_transformable_to b4 & b4 is_naturally_transformable_to b5 holds
for b6 being natural_transformation of b3,b4
for b7 being natural_transformation of b4,b5
for b8 being object of b1 holds (b7 `*` b6) ! b8 = (b7 ! b8) * (b6 ! b8)
proof end;

theorem Th13: :: FUNCTOR2:13
for b1, b2 being category
for b3, b4, b5, b6 being covariant Functor of b1,b2
for b7 being natural_transformation of b3,b4
for b8 being natural_transformation of b4,b5 st b3 is_naturally_transformable_to b4 & b4 is_naturally_transformable_to b5 & b5 is_naturally_transformable_to b6 holds
for b9 being natural_transformation of b5,b6 holds (b9 `*` b8) `*` b7 = b9 `*` (b8 `*` b7)
proof end;

definition
let c1 be set ;
let c2, c3 be ManySortedSet of c1;
func Funcs c2,c3 -> set means :Def9: :: FUNCTOR2:def 9
for b1 being set holds
( b1 in a4 iff b1 is ManySortedFunction of a2,a3 ) if for b1 being set st b1 in a1 & a3 . b1 = {} holds
a2 . b1 = {}
otherwise a4 = {} ;
existence
( ( ( for b1 being set st b1 in c1 & c3 . b1 = {} holds
c2 . b1 = {} ) implies ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is ManySortedFunction of c2,c3 ) ) & ( ex b1 being set st
( b1 in c1 & c3 . b1 = {} & not c2 . b1 = {} ) implies ex b1 being set st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( ( for b3 being set st b3 in c1 & c3 . b3 = {} holds
c2 . b3 = {} ) & ( for b3 being set holds
( b3 in b1 iff b3 is ManySortedFunction of c2,c3 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is ManySortedFunction of c2,c3 ) ) implies b1 = b2 ) & ( ex b3 being set st
( b3 in c1 & c3 . b3 = {} & not c2 . b3 = {} ) & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
consistency
for b1 being set holds verum ;
end;

:: deftheorem Def9 defines Funcs FUNCTOR2:def 9 :
for b1 being set
for b2, b3 being ManySortedSet of b1
for b4 being set holds
( ( ( for b5 being set st b5 in b1 & b3 . b5 = {} holds
b2 . b5 = {} ) implies ( b4 = Funcs b2,b3 iff for b5 being set holds
( b5 in b4 iff b5 is ManySortedFunction of b2,b3 ) ) ) & ( ex b5 being set st
( b5 in b1 & b3 . b5 = {} & not b2 . b5 = {} ) implies ( b4 = Funcs b2,b3 iff b4 = {} ) ) );

definition
let c1, c2 be non empty transitive with_units AltCatStr ;
func Funct c1,c2 -> set means :Def10: :: FUNCTOR2:def 10
for b1 being set holds
( b1 in a3 iff b1 is strict covariant Functor of a1,a2 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is strict covariant Functor of c1,c2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is strict covariant Functor of c1,c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is strict covariant Functor of c1,c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines Funct FUNCTOR2:def 10 :
for b1, b2 being non empty transitive with_units AltCatStr
for b3 being set holds
( b3 = Funct b1,b2 iff for b4 being set holds
( b4 in b3 iff b4 is strict covariant Functor of b1,b2 ) );

definition
let c1, c2 be category;
func Functors c1,c2 -> non empty transitive strict AltCatStr means :: FUNCTOR2:def 11
( the carrier of a3 = Funct a1,a2 & ( for b1, b2 being strict covariant Functor of a1,a2
for b3 being set holds
( b3 in the Arrows of a3 . b1,b2 iff ( b1 is_naturally_transformable_to b2 & b3 is natural_transformation of b1,b2 ) ) ) & ( for b1, b2, b3 being strict covariant Functor of a1,a2 st b1 is_naturally_transformable_to b2 & b2 is_naturally_transformable_to b3 holds
for b4 being natural_transformation of b1,b2
for b5 being natural_transformation of b2,b3 ex b6 being Function st
( b6 = the Comp of a3 . b1,b2,b3 & b6 . b5,b4 = b5 `*` b4 ) ) );
existence
ex b1 being non empty transitive strict AltCatStr st
( the carrier of b1 = Funct c1,c2 & ( for b2, b3 being strict covariant Functor of c1,c2
for b4 being set holds
( b4 in the Arrows of b1 . b2,b3 iff ( b2 is_naturally_transformable_to b3 & b4 is natural_transformation of b2,b3 ) ) ) & ( for b2, b3, b4 being strict covariant Functor of c1,c2 st b2 is_naturally_transformable_to b3 & b3 is_naturally_transformable_to b4 holds
for b5 being natural_transformation of b2,b3
for b6 being natural_transformation of b3,b4 ex b7 being Function st
( b7 = the Comp of b1 . b2,b3,b4 & b7 . b6,b5 = b6 `*` b5 ) ) )
proof end;
uniqueness
for b1, b2 being non empty transitive strict AltCatStr st the carrier of b1 = Funct c1,c2 & ( for b3, b4 being strict covariant Functor of c1,c2
for b5 being set holds
( b5 in the Arrows of b1 . b3,b4 iff ( b3 is_naturally_transformable_to b4 & b5 is natural_transformation of b3,b4 ) ) ) & ( for b3, b4, b5 being strict covariant Functor of c1,c2 st b3 is_naturally_transformable_to b4 & b4 is_naturally_transformable_to b5 holds
for b6 being natural_transformation of b3,b4
for b7 being natural_transformation of b4,b5 ex b8 being Function st
( b8 = the Comp of b1 . b3,b4,b5 & b8 . b7,b6 = b7 `*` b6 ) ) & the carrier of b2 = Funct c1,c2 & ( for b3, b4 being strict covariant Functor of c1,c2
for b5 being set holds
( b5 in the Arrows of b2 . b3,b4 iff ( b3 is_naturally_transformable_to b4 & b5 is natural_transformation of b3,b4 ) ) ) & ( for b3, b4, b5 being strict covariant Functor of c1,c2 st b3 is_naturally_transformable_to b4 & b4 is_naturally_transformable_to b5 holds
for b6 being natural_transformation of b3,b4
for b7 being natural_transformation of b4,b5 ex b8 being Function st
( b8 = the Comp of b2 . b3,b4,b5 & b8 . b7,b6 = b7 `*` b6 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines Functors FUNCTOR2:def 11 :
for b1, b2 being category
for b3 being non empty transitive strict AltCatStr holds
( b3 = Functors b1,b2 iff ( the carrier of b3 = Funct b1,b2 & ( for b4, b5 being strict covariant Functor of b1,b2
for b6 being set holds
( b6 in the Arrows of b3 . b4,b5 iff ( b4 is_naturally_transformable_to b5 & b6 is natural_transformation of b4,b5 ) ) ) & ( for b4, b5, b6 being strict covariant Functor of b1,b2 st b4 is_naturally_transformable_to b5 & b5 is_naturally_transformable_to b6 holds
for b7 being natural_transformation of b4,b5
for b8 being natural_transformation of b5,b6 ex b9 being Function st
( b9 = the Comp of b3 . b4,b5,b6 & b9 . b8,b7 = b8 `*` b7 ) ) ) );