:: by Robert Nieszczerzewski

::

:: Received June 12, 1997

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

coherence

for b_{1} being Functor of A,B holds

( b_{1} is feasible & b_{1} is id-preserving )
by FUNCTOR0:def 25;

end;
let B be non empty with_units AltCatStr ;

coherence

for b

( b

registration

let A be non empty transitive with_units AltCatStr ;

let B be non empty with_units AltCatStr ;

coherence

for b_{1} being Functor of A,B st b_{1} is covariant holds

( b_{1} is Covariant & b_{1} is comp-preserving )
by FUNCTOR0:def 26;

coherence

for b_{1} being Functor of A,B st b_{1} is Covariant & b_{1} is comp-preserving holds

b_{1} is covariant
by FUNCTOR0:def 26;

coherence

for b_{1} being Functor of A,B st b_{1} is contravariant holds

( b_{1} is Contravariant & b_{1} is comp-reversing )
by FUNCTOR0:def 27;

coherence

for b_{1} being Functor of A,B st b_{1} is Contravariant & b_{1} is comp-reversing holds

b_{1} is contravariant
by FUNCTOR0:def 27;

end;
let B be non empty with_units AltCatStr ;

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

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)

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;

for F1 being Functor of A,B

for a being Object of A holds <^(F1 . a),(F1 . a)^> <> {} by ALTCAT_2:def 7;

end;
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 a being Object of A holds <^(F1 . a),(F2 . a)^> <> {} ;

for F1 being Functor of A,B

for a being Object of A holds <^(F1 . a),(F1 . a)^> <> {} by ALTCAT_2:def 7;

:: 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)^> <> {} );

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

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 ;

ex b_{1} being ManySortedSet of the carrier of A st

for a being Object of A holds b_{1} . a is Morphism of (F1 . a),(F2 . a)

end;
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 for a being Object of A holds it . a is Morphism of (F1 . a),(F2 . a);

ex b

for a being Object of A holds b

proof 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 b_{5} being ManySortedSet of the carrier of A holds

( b_{5} is transformation of F1,F2 iff for a being Object of A holds b_{5} . a is Morphism of (F1 . a),(F2 . a) );

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 b

( b

definition

let A, B be non empty transitive with_units AltCatStr ;

let F be Functor of A,B;

ex b_{1} being transformation of F,F st

for a being Object of A holds b_{1} . a = idm (F . a)

for b_{1}, b_{2} being transformation of F,F st ( for a being Object of A holds b_{1} . a = idm (F . a) ) & ( for a being Object of A holds b_{2} . a = idm (F . a) ) holds

b_{1} = b_{2}

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

ex b

for a being Object of A holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being transformation of F,F holds

( b_{4} = idt F iff for a being Object of A holds b_{4} . a = idm (F . a) );

for A, B being non empty transitive with_units AltCatStr

for F being Functor of A,B

for b

( b

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;

existence

ex b_{1} being Morphism of (F1 . a),(F2 . a) st b_{1} = t . a

uniqueness

for b_{1}, b_{2} being Morphism of (F1 . a),(F2 . a) st b_{1} = t . a & b_{2} = t . a holds

b_{1} = b_{2};

;

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

existence

ex b

proof end;

correctness uniqueness

for b

b

;

:: 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 b_{7} being Morphism of (F1 . a),(F2 . a) holds

( b_{7} = t ! a iff b_{7} = t . a );

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 b

( b

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;

ex b_{1} being transformation of F,F2 st

for a being Object of A holds b_{1} ! a = (t2 ! a) * (t1 ! a)

for b_{1}, b_{2} being transformation of F,F2 st ( for a being Object of A holds b_{1} ! a = (t2 ! a) * (t1 ! a) ) & ( for a being Object of A holds b_{2} ! a = (t2 ! a) * (t1 ! a) ) holds

b_{1} = b_{2}

end;
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 for a being Object of A holds it ! a = (t2 ! a) * (t1 ! a);

ex b

for a being Object of A holds b

proof end;

uniqueness for b

b

proof 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 b_{8} being transformation of F,F2 holds

( b_{8} = t2 `*` t1 iff for a being Object of A holds b_{8} ! a = (t2 ! a) * (t1 ! a) );

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 b

( b

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

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)

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 )

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)

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;

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

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

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;

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

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 ;

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

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 ;

ex b_{1} 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 (b_{1} ! b) * (F1 . f) = (F2 . f) * (b_{1} ! a)
by A1;

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

ex b

for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds (b

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

( b_{5} 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 (b_{5} ! b) * (F1 . f) = (F2 . f) * (b_{5} ! a) );

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 b

( b

for f being Morphism of a,b holds (b

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

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

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;

existence

ex b_{1} being natural_transformation of F,F2 st b_{1} = t2 `*` t1

uniqueness

for b_{1}, b_{2} being natural_transformation of F,F2 st b_{1} = t2 `*` t1 & b_{2} = t2 `*` t1 holds

b_{1} = b_{2};

;

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

existence

ex b

proof end;

correctness uniqueness

for b

b

;

:: 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 b_{8} being natural_transformation of F,F2 holds

( b_{8} = t2 `*` t1 iff b_{8} = t2 `*` t1 );

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 b

( b

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;

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;

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)

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;

( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) implies ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is ManySortedFunction of A,B ) ) & ( ex i being set st

( i in I & B . i = {} & not A . i = {} ) implies ex b_{1} being set st b_{1} = {} ) )

for b_{1}, b_{2} being set holds

( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) & ( for x being set holds

( x in b_{1} iff x is ManySortedFunction of A,B ) ) & ( for x being set holds

( x in b_{2} iff x is ManySortedFunction of A,B ) ) implies b_{1} = b_{2} ) & ( ex i being set st

( i in I & B . i = {} & not A . i = {} ) & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being set holds verum
;

end;
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 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 = {} ;

( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) implies ex b

for x being set holds

( x in b

( i in I & B . i = {} & not A . i = {} ) implies ex b

proof end;

uniqueness for b

( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) & ( for x being set holds

( x in b

( x in b

( i in I & B . i = {} & not A . i = {} ) & b

proof end;

consistency for b

:: deftheorem Def9 defines Funcs FUNCTOR2:def 9 :

for I being set

for A, B being ManySortedSet of I

for b_{4} being set holds

( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) implies ( b_{4} = Funcs (A,B) iff for x being set holds

( x in b_{4} iff x is ManySortedFunction of A,B ) ) ) & ( ex i being set st

( i in I & B . i = {} & not A . i = {} ) implies ( b_{4} = Funcs (A,B) iff b_{4} = {} ) ) );

for I being set

for A, B being ManySortedSet of I

for b

( ( ( for i being set st i in I & B . i = {} holds

A . i = {} ) implies ( b

( x in b

( i in I & B . i = {} & not A . i = {} ) implies ( b

definition

let A, B be non empty transitive with_units AltCatStr ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is strict covariant Functor of A,B )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is strict covariant Functor of A,B ) ) & ( for x being object holds

( x in b_{2} iff x is strict covariant Functor of A,B ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff x is strict covariant Functor of A,B );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def10 defines Funct FUNCTOR2:def 10 :

for A, B being non empty transitive with_units AltCatStr

for b_{3} being set holds

( b_{3} = Funct (A,B) iff for x being object holds

( x in b_{3} iff x is strict covariant Functor of A,B ) );

for A, B being non empty transitive with_units AltCatStr

for b

( b

( x in b

definition

let A, B be category;

ex b_{1} being non empty transitive strict AltCatStr st

( the carrier of b_{1} = Funct (A,B) & ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of b_{1} . (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 b_{1} . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )

for b_{1}, b_{2} being non empty transitive strict AltCatStr st the carrier of b_{1} = Funct (A,B) & ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of b_{1} . (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 b_{1} . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) & the carrier of b_{2} = Funct (A,B) & ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of b_{2} . (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 b_{2} . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for x being set holds

( x in the Arrows of b

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 b

proof end;

uniqueness for b

for x being set holds

( x in the Arrows of b

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 b

for x being set holds

( x in the Arrows of b

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 b

b

proof end;

:: deftheorem defines Functors FUNCTOR2:def 11 :

for A, B being category

for b_{3} being non empty transitive strict AltCatStr holds

( b_{3} = Functors (A,B) iff ( the carrier of b_{3} = Funct (A,B) & ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of b_{3} . (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 b_{3} . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) ) );

for A, B being category

for b

( b

for x being set holds

( x in the Arrows of b

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 b