:: by Andrzej Trybulec

::

:: Received June 5, 1992

:: Copyright (c) 1992-2016 Association of Mizar Users

definition

let A, B, C be non empty set ;

let f be Function of A,(Funcs (B,C));

:: original: uncurry

redefine func uncurry f -> Function of [:A,B:],C;

coherence

uncurry f is Function of [:A,B:],C

end;
let f be Function of A,(Funcs (B,C));

:: original: uncurry

redefine func uncurry f -> Function of [:A,B:],C;

coherence

uncurry f is Function of [:A,B:],C

proof end;

theorem Th2: :: ISOCAT_2:2

for A, B, C being non empty set

for f being Function of A,(Funcs (B,C))

for a being Element of A

for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b

for f being Function of A,(Funcs (B,C))

for a being Element of A

for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b

proof end;

theorem Th5: :: ISOCAT_2:7

for A, B being Category

for o being set holds

( o is Object of (Functors (A,B)) iff o is Functor of A,B )

for o being set holds

( o is Object of (Functors (A,B)) iff o is Functor of A,B )

proof end;

theorem Th6: :: ISOCAT_2:8

for A, B being Category

for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st

( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] )

for f being Morphism of (Functors (A,B)) ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st

( F1 is_naturally_transformable_to F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t] )

proof end;

definition

let A, B be Category;

let a be Object of A;

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

for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b_{1} . [[F1,F2],t] = t . a

for b_{1}, b_{2} being Functor of Functors (A,B),B st ( for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b_{1} . [[F1,F2],t] = t . a ) & ( for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b_{2} . [[F1,F2],t] = t . a ) holds

b_{1} = b_{2}

end;
let a be Object of A;

func a |-> B -> Functor of Functors (A,B),B means :Def1: :: ISOCAT_2:def 1

for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

it . [[F1,F2],t] = t . a;

existence for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

it . [[F1,F2],t] = t . a;

ex b

for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b

proof end;

uniqueness for b

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b

b

proof end;

:: deftheorem Def1 defines |-> ISOCAT_2:def 1 :

for A, B being Category

for a being Object of A

for b_{4} being Functor of Functors (A,B),B holds

( b_{4} = a |-> B iff for F1, F2 being Functor of A,B

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b_{4} . [[F1,F2],t] = t . a );

for A, B being Category

for a being Object of A

for b

( b

for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds

b

theorem Th8: :: ISOCAT_2:10

for A, B, C being Category

for F being Functor of [:A,B:],C

for a being Object of A

for b being Object of B holds (F ?- a) . b = F . [a,b]

for F being Functor of [:A,B:],C

for a being Object of A

for b being Object of B holds (F ?- a) . b = F . [a,b]

proof end;

theorem Th9: :: ISOCAT_2:11

for A, B being Category

for a1, a2 being Object of A

for b1, b2 being Object of B holds

( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )

for a1, a2 being Object of A

for b1, b2 being Object of B holds

( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )

proof end;

theorem Th10: :: ISOCAT_2:12

for A, B being Category

for a1, a2 being Object of A

for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds

for f being Morphism of A

for g being Morphism of B holds

( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )

for a1, a2 being Object of A

for b1, b2 being Object of B st Hom ([a1,b1],[a2,b2]) <> {} holds

for f being Morphism of A

for g being Morphism of B holds

( [f,g] is Morphism of [a1,b1],[a2,b2] iff ( f is Morphism of a1,a2 & g is Morphism of b1,b2 ) )

proof end;

theorem Th11: :: ISOCAT_2:13

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2

for a being Object of A holds

( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2

for a being Object of A holds

( F1 ?- a is_naturally_transformable_to F2 ?- a & (curry t) . a is natural_transformation of F1 ?- a,F2 ?- a )

proof end;

definition

let A, B, C be Category;

let F be Functor of [:A,B:],C;

let f be Morphism of A;

(curry F) . f is Function of the carrier' of B, the carrier' of C

end;
let F be Functor of [:A,B:],C;

let f be Morphism of A;

func curry (F,f) -> Function of the carrier' of B, the carrier' of C equals :: ISOCAT_2:def 2

(curry F) . f;

coherence (curry F) . f;

(curry F) . f is Function of the carrier' of B, the carrier' of C

proof end;

:: deftheorem defines curry ISOCAT_2:def 2 :

for A, B, C being Category

for F being Functor of [:A,B:],C

for f being Morphism of A holds curry (F,f) = (curry F) . f;

for A, B, C being Category

for F being Functor of [:A,B:],C

for f being Morphism of A holds curry (F,f) = (curry F) . f;

theorem Th12: :: ISOCAT_2:14

for A, B being Category

for a1, a2 being Object of A

for b1, b2 being Object of B

for f being Morphism of A

for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds

[f,g] in Hom ([a1,b1],[a2,b2])

for a1, a2 being Object of A

for b1, b2 being Object of B

for f being Morphism of A

for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds

[f,g] in Hom ([a1,b1],[a2,b2])

proof end;

theorem Th13: :: ISOCAT_2:15

for A, B, C being Category

for F being Functor of [:A,B:],C

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds

( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )

for F being Functor of [:A,B:],C

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds

( F ?- a is_naturally_transformable_to F ?- b & (curry (F,f)) * (IdMap B) is natural_transformation of F ?- a,F ?- b )

proof end;

definition

let A, B, C be Category;

let F be Functor of [:A,B:],C;

let f be Morphism of A;

(curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f)

;

end;
let F be Functor of [:A,B:],C;

let f be Morphism of A;

func F ?- f -> natural_transformation of F ?- (dom f),F ?- (cod f) equals :: ISOCAT_2:def 3

(curry (F,f)) * (IdMap B);

coherence (curry (F,f)) * (IdMap B);

(curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f)

proof end;

correctness ;

:: deftheorem defines ?- ISOCAT_2:def 3 :

for A, B, C being Category

for F being Functor of [:A,B:],C

for f being Morphism of A holds F ?- f = (curry (F,f)) * (IdMap B);

for A, B, C being Category

for F being Functor of [:A,B:],C

for f being Morphism of A holds F ?- f = (curry (F,f)) * (IdMap B);

theorem Th14: :: ISOCAT_2:16

for A, B, C being Category

for F being Functor of [:A,B:],C

for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)

for F being Functor of [:A,B:],C

for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)

proof end;

theorem Th15: :: ISOCAT_2:17

for A, B, C being Category

for F being Functor of [:A,B:],C

for f being Morphism of A

for b being Object of B holds (F ?- f) . b = F . (f,(id b))

for F being Functor of [:A,B:],C

for f being Morphism of A

for b being Object of B holds (F ?- f) . b = F . (f,(id b))

proof end;

theorem Th16: :: ISOCAT_2:18

for A, B, C being Category

for F being Functor of [:A,B:],C

for a being Object of A holds id (F ?- a) = F ?- (id a)

for F being Functor of [:A,B:],C

for a being Object of A holds id (F ?- a) = F ?- (id a)

proof end;

theorem Th17: :: ISOCAT_2:19

for A, B, C being Category

for F being Functor of [:A,B:],C

for g, f being Morphism of A st dom g = cod f holds

for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds

F ?- (g (*) f) = (F ?- g) `*` t

for F being Functor of [:A,B:],C

for g, f being Morphism of A st dom g = cod f holds

for t being natural_transformation of F ?- (dom f),F ?- (dom g) st t = F ?- f holds

F ?- (g (*) f) = (F ?- g) `*` t

proof end;

definition

let A, B, C be Category;

let F be Functor of [:A,B:],C;

ex b_{1} being Functor of A, Functors (B,C) st

for f being Morphism of A holds b_{1} . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]

for b_{1}, b_{2} being Functor of A, Functors (B,C) st ( for f being Morphism of A holds b_{1} . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds b_{2} . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) holds

b_{1} = b_{2}

end;
let F be Functor of [:A,B:],C;

func export F -> Functor of A, Functors (B,C) means :Def4: :: ISOCAT_2:def 4

for f being Morphism of A holds it . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)];

existence for f being Morphism of A holds it . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)];

ex b

for f being Morphism of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines export ISOCAT_2:def 4 :

for A, B, C being Category

for F being Functor of [:A,B:],C

for b_{5} being Functor of A, Functors (B,C) holds

( b_{5} = export F iff for f being Morphism of A holds b_{5} . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] );

for A, B, C being Category

for F being Functor of [:A,B:],C

for b

( b

Lm1: for A, B being Category

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 holds t . a in Hom ((F1 . a),(F2 . a))

proof end;

theorem Th18: :: ISOCAT_2:20

for A, B, C being Category

for F being Functor of [:A,B:],C

for a being Object of A holds (export F) . a = F ?- a

for F being Functor of [:A,B:],C

for a being Object of A holds (export F) . a = F ?- a

proof end;

theorem Th19: :: ISOCAT_2:21

for A, B, C being Category

for F being Functor of [:A,B:],C

for a being Object of A holds (export F) . a is Functor of B,C

for F being Functor of [:A,B:],C

for a being Object of A holds (export F) . a is Functor of B,C

proof end;

theorem Th20: :: ISOCAT_2:22

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds

F1 = F2

for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds

F1 = F2

proof end;

theorem Th21: :: ISOCAT_2:23

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds

( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st

for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds

( export F1 is_naturally_transformable_to export F2 & ex G being natural_transformation of export F1, export F2 st

for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds G . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )

proof end;

definition

let A, B, C be Category;

let F1, F2 be Functor of [:A,B:],C;

assume A1: F1 is_naturally_transformable_to F2 ;

let t be natural_transformation of F1,F2;

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

for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds b_{1} . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
by A1, Th21;

uniqueness

for b_{1}, b_{2} being natural_transformation of export F1, export F2 st ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds b_{1} . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds b_{2} . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) holds

b_{1} = b_{2}

end;
let F1, F2 be Functor of [:A,B:],C;

assume A1: F1 is_naturally_transformable_to F2 ;

let t be natural_transformation of F1,F2;

func export t -> natural_transformation of export F1, export F2 means :Def5: :: ISOCAT_2:def 5

for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds it . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)];

existence for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds it . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)];

ex b

for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds b

uniqueness

for b

for a being Object of A holds b

for a being Object of A holds b

b

proof end;

:: deftheorem Def5 defines export ISOCAT_2:def 5 :

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2

for b_{7} being natural_transformation of export F1, export F2 holds

( b_{7} = export t iff for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st t = s holds

for a being Object of A holds b_{7} . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] );

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2

for b

( b

for a being Object of A holds b

theorem Th23: :: ISOCAT_2:25

for A, B, C being Category

for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t1 being natural_transformation of F1,F2

for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)

for F1, F2, F3 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t1 being natural_transformation of F1,F2

for t2 being natural_transformation of F2,F3 holds export (t2 `*` t1) = (export t2) `*` (export t1)

proof end;

theorem Th24: :: ISOCAT_2:26

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds

t1 = t2

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t1, t2 being natural_transformation of F1,F2 st export t1 = export t2 holds

t1 = t2

proof end;

theorem Th25: :: ISOCAT_2:27

for A, B, C being Category

for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F

for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F

proof end;

theorem Th26: :: ISOCAT_2:28

for A, B, C being Category

for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds

for t being natural_transformation of export F1, export F2 holds

( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )

for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds

for t being natural_transformation of export F1, export F2 holds

( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )

proof end;

definition

let A, B, C be Category;

ex b_{1} being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) st

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{1} . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]

for b_{1}, b_{2} being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) st ( for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{1} . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) & ( for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{2} . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) holds

b_{1} = b_{2}

end;
func export (A,B,C) -> Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) means :Def6: :: ISOCAT_2:def 6

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds it . [[F1,F2],t] = [[(export F1),(export F2)],(export t)];

existence for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds it . [[F1,F2],t] = [[(export F1),(export F2)],(export t)];

ex b

for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b

proof end;

uniqueness for b

for t being natural_transformation of F1,F2 holds b

for t being natural_transformation of F1,F2 holds b

b

proof end;

:: deftheorem Def6 defines export ISOCAT_2:def 6 :

for A, B, C being Category

for b_{4} being Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C))) holds

( b_{4} = export (A,B,C) iff for F1, F2 being Functor of [:A,B:],C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{4} . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] );

for A, B, C being Category

for b

( b

for t being natural_transformation of F1,F2 holds b

theorem Th28: :: ISOCAT_2:30

for A, B, C being Category

for F1, F2 being Functor of A,B

for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds G * t = G * t

for F1, F2 being Functor of A,B

for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds G * t = G * t

proof end;

definition

let A, B, C be Category;

let F be Functor of A,B;

let G be Functor of A,C;

:: original: <:

redefine func <:F,G:> -> Functor of A,[:B,C:];

coherence

<:F,G:> is Functor of A,[:B,C:]

end;
let F be Functor of A,B;

let G be Functor of A,C;

:: original: <:

redefine func <:F,G:> -> Functor of A,[:B,C:];

coherence

<:F,G:> is Functor of A,[:B,C:]

proof end;

definition

let A, B, C be Category;

let F be Functor of A,[:B,C:];

correctness

coherence

(pr1 (B,C)) * F is Functor of A,B;

;

correctness

coherence

(pr2 (B,C)) * F is Functor of A,C;

;

end;
let F be Functor of A,[:B,C:];

correctness

coherence

(pr1 (B,C)) * F is Functor of A,B;

;

correctness

coherence

(pr2 (B,C)) * F is Functor of A,C;

;

:: deftheorem defines Pr1 ISOCAT_2:def 7 :

for A, B, C being Category

for F being Functor of A,[:B,C:] holds Pr1 F = (pr1 (B,C)) * F;

for A, B, C being Category

for F being Functor of A,[:B,C:] holds Pr1 F = (pr1 (B,C)) * F;

:: deftheorem defines Pr2 ISOCAT_2:def 8 :

for A, B, C being Category

for F being Functor of A,[:B,C:] holds Pr2 F = (pr2 (B,C)) * F;

for A, B, C being Category

for F being Functor of A,[:B,C:] holds Pr2 F = (pr2 (B,C)) * F;

definition

let A, B, C be Category;

let F1, F2 be Functor of A,[:B,C:];

let t be natural_transformation of F1,F2;

coherence

(pr1 (B,C)) * t is natural_transformation of Pr1 F1, Pr1 F2 ;

coherence

(pr2 (B,C)) * t is natural_transformation of Pr2 F1, Pr2 F2 ;

end;
let F1, F2 be Functor of A,[:B,C:];

let t be natural_transformation of F1,F2;

coherence

(pr1 (B,C)) * t is natural_transformation of Pr1 F1, Pr1 F2 ;

coherence

(pr2 (B,C)) * t is natural_transformation of Pr2 F1, Pr2 F2 ;

:: deftheorem defines Pr1 ISOCAT_2:def 9 :

for A, B, C being Category

for F1, F2 being Functor of A,[:B,C:]

for t being natural_transformation of F1,F2 holds Pr1 t = (pr1 (B,C)) * t;

for A, B, C being Category

for F1, F2 being Functor of A,[:B,C:]

for t being natural_transformation of F1,F2 holds Pr1 t = (pr1 (B,C)) * t;

:: deftheorem defines Pr2 ISOCAT_2:def 10 :

for A, B, C being Category

for F1, F2 being Functor of A,[:B,C:]

for t being natural_transformation of F1,F2 holds Pr2 t = (pr2 (B,C)) * t;

for A, B, C being Category

for F1, F2 being Functor of A,[:B,C:]

for t being natural_transformation of F1,F2 holds Pr2 t = (pr2 (B,C)) * t;

theorem Th31: :: ISOCAT_2:33

for A, B, C being Category

for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds

for s being natural_transformation of F1,F2

for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds

s = t

for F1, F2, G1, G2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds

for s being natural_transformation of F1,F2

for t being natural_transformation of G1,G2 st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds

s = t

proof end;

Lm2: for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

for t1 being transformation of F1,G1

for t2 being transformation of F2,G2

for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]

proof end;

theorem Th33: :: ISOCAT_2:35

for A, B, C being Category

for F being Functor of A,B

for G being Functor of A,C

for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]

for F being Functor of A,B

for G being Functor of A,C

for a being Object of A holds <:F,G:> . a = [(F . a),(G . a)]

proof end;

Lm3: for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

for t1 being transformation of F1,G1

for t2 being transformation of F2,G2

for a being Object of A holds <:t1,t2:> . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a))

proof end;

theorem Th34: :: ISOCAT_2:36

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

<:F1,F2:> is_transformable_to <:G1,G2:> by Lm3;

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

<:F1,F2:> is_transformable_to <:G1,G2:> by Lm3;

definition

let A, B, C be Category;

let F1, G1 be Functor of A,B;

let F2, G2 be Functor of A,C;

assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ;

let t1 be transformation of F1,G1;

let t2 be transformation of F2,G2;

coherence

<:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:>

end;
let F1, G1 be Functor of A,B;

let F2, G2 be Functor of A,C;

assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ;

let t1 be transformation of F1,G1;

let t2 be transformation of F2,G2;

coherence

<:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:>

proof end;

:: deftheorem Def11 defines <: ISOCAT_2:def 11 :

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

for t1 being transformation of F1,G1

for t2 being transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

for t1 being transformation of F1,G1

for t2 being transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;

theorem Th35: :: ISOCAT_2:37

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

for t1 being transformation of F1,G1

for t2 being transformation of F2,G2

for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds

for t1 being transformation of F1,G1

for t2 being transformation of F2,G2

for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]

proof end;

Lm4: for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

for t1 being natural_transformation of F1,G1

for t2 being natural_transformation of F2,G2

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a)

proof end;

theorem Th36: :: ISOCAT_2:38

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

<:F1,F2:> is_naturally_transformable_to <:G1,G2:>

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

<:F1,F2:> is_naturally_transformable_to <:G1,G2:>

proof end;

definition

let A, B, C be Category;

let F1, G1 be Functor of A,B;

let F2, G2 be Functor of A,C;

assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ;

let t1 be natural_transformation of F1,G1;

let t2 be natural_transformation of F2,G2;

<:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:>

end;
let F1, G1 be Functor of A,B;

let F2, G2 be Functor of A,C;

assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ;

let t1 be natural_transformation of F1,G1;

let t2 be natural_transformation of F2,G2;

func <:t1,t2:> -> natural_transformation of <:F1,F2:>,<:G1,G2:> equals :Def12: :: ISOCAT_2:def 12

<:t1,t2:>;

coherence <:t1,t2:>;

<:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:>

proof end;

:: deftheorem Def12 defines <: ISOCAT_2:def 12 :

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

for t1 being natural_transformation of F1,G1

for t2 being natural_transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

for t1 being natural_transformation of F1,G1

for t2 being natural_transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;

theorem Th37: :: ISOCAT_2:39

for A, B, C being Category

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

for t1 being natural_transformation of F1,G1

for t2 being natural_transformation of F2,G2 holds

( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )

for F1, G1 being Functor of A,B

for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds

for t1 being natural_transformation of F1,G1

for t2 being natural_transformation of F2,G2 holds

( Pr1 <:t1,t2:> = t1 & Pr2 <:t1,t2:> = t2 )

proof end;

definition

let A, B, C be Category;

ex b_{1} being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] st

for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{1} . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]

for b_{1}, b_{2} being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] st ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{1} . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) & ( for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{2} . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) holds

b_{1} = b_{2}

end;
func distribute (A,B,C) -> Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] means :Def13: :: ISOCAT_2:def 13

for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds it . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]];

existence for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds it . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]];

ex b

for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b

proof end;

uniqueness for b

for t being natural_transformation of F1,F2 holds b

for t being natural_transformation of F1,F2 holds b

b

proof end;

:: deftheorem Def13 defines distribute ISOCAT_2:def 13 :

for A, B, C being Category

for b_{4} being Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] holds

( b_{4} = distribute (A,B,C) iff for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds

for t being natural_transformation of F1,F2 holds b_{4} . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] );

for A, B, C being Category

for b

( b

for t being natural_transformation of F1,F2 holds b