:: ISOCAT_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

theorem Th1: :: ISOCAT_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being non empty set
for f being Function of A, Funcs B,C holds curry (uncurry f) = f
proof end;

theorem Th2: :: ISOCAT_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th3: :: ISOCAT_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for A being non empty set
for f, g being Function of {x},A st f . x = g . x holds
f = g
proof end;

theorem Th4: :: ISOCAT_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for x being Element of A
for f being Function of A,B holds f . x in rng f
proof end;

theorem Th5: :: ISOCAT_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being non empty set
for f, g being Function of A,[:B,C:] st (pr1 B,C) * f = (pr1 B,C) * g & (pr2 B,C) * f = (pr2 B,C) * g holds
f = g
proof end;

theorem Th6: :: ISOCAT_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Category
for f being Morphism of A holds (id (cod f)) * f = f
proof end;

theorem Th7: :: ISOCAT_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Category
for f being Morphism of A holds f * (id (dom f)) = f
proof end;

theorem Th8: :: ISOCAT_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Category
for o being set holds
( o is Object of (Functors A,B) iff o is Functor of A,B )
proof end;

theorem Th9: :: ISOCAT_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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] )
proof end;

definition
let A, B be Category;
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
ex b1 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
b1 . [[F1,F2],t] = t . a
proof end;
uniqueness
for b1, b2 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
b1 . [[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
b2 . [[F1,F2],t] = t . a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines |-> ISOCAT_2:def 1 :
for A, B being Category
for a being Object of A
for b4 being Functor of Functors A,B,B holds
( b4 = 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
b4 . [[F1,F2],t] = t . a );

Lm1: for o, m being set holds
( the Objects of (1Cat o,m) = {o} & the Morphisms of (1Cat o,m) = {m} )
proof end;

theorem :: ISOCAT_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ISOCAT_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Category
for o, m being set holds Functors (1Cat o,m),A ~= A
proof end;

theorem Th12: :: ISOCAT_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th13: :: ISOCAT_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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] <> {} )
proof end;

theorem Th14: :: ISOCAT_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th15: :: ISOCAT_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let A, B, C be Category;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
func curry F,f -> Function of the Morphisms of B,the Morphisms of C equals :: ISOCAT_2:def 2
(curry F) . f;
coherence
(curry F) . f is Function of the Morphisms of B,the Morphisms of C
proof end;
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;

theorem Th16: :: ISOCAT_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th17: :: ISOCAT_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) * the Id of 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;
func F ?- f -> natural_transformation of F ?- (dom f),F ?- (cod f) equals :: ISOCAT_2:def 3
(curry F,f) * the Id of B;
coherence
(curry F,f) * the Id of B is natural_transformation of F ?- (dom f),F ?- (cod f)
proof end;
correctness
;
end;

:: 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) * the Id of B;

theorem Th18: :: ISOCAT_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th19: :: ISOCAT_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

theorem Th20: :: ISOCAT_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th21: :: ISOCAT_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let A, B, C be Category;
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
ex b1 being Functor of A, Functors B,C st
for f being Morphism of A holds b1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)]
proof end;
uniqueness
for b1, b2 being Functor of A, Functors B,C st ( for f being Morphism of A holds b1 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) & ( for f being Morphism of A holds b2 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines export ISOCAT_2:def 4 :
for A, B, C being Category
for F being Functor of [:A,B:],C
for b5 being Functor of A, Functors B,C holds
( b5 = export F iff for f being Morphism of A holds b5 . f = [[(F ?- (dom f)),(F ?- (cod f))],(F ?- f)] );

Lm2: 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 :: ISOCAT_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ISOCAT_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: ISOCAT_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th25: :: ISOCAT_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th26: :: ISOCAT_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds
F1 = F2
proof end;

theorem Th27: :: ISOCAT_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Objects of A,the Objects of B:],the Morphisms 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;
func export t -> natural_transformation of export F1, export F2 means :Def5: :: ISOCAT_2:def 5
for s being Function of [:the Objects of A,the Objects of B:],the Morphisms 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
ex b1 being natural_transformation of export F1, export F2 st
for s being Function of [:the Objects of A,the Objects of B:],the Morphisms of C st t = s holds
for a being Object of A holds b1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
by A1, Th27;
uniqueness
for b1, b2 being natural_transformation of export F1, export F2 st ( for s being Function of [:the Objects of A,the Objects of B:],the Morphisms of C st t = s holds
for a being Object of A holds b1 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) & ( for s being Function of [:the Objects of A,the Objects of B:],the Morphisms of C st t = s holds
for a being Object of A holds b2 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] ) holds
b1 = b2
proof end;
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 b7 being natural_transformation of export F1, export F2 holds
( b7 = export t iff for s being Function of [:the Objects of A,the Objects of B:],the Morphisms of C st t = s holds
for a being Object of A holds b7 . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] );

theorem Th28: :: ISOCAT_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F being Functor of [:A,B:],C holds id (export F) = export (id F)
proof end;

theorem Th29: :: ISOCAT_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th30: :: ISOCAT_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th31: :: ISOCAT_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th32: :: ISOCAT_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let A, B, C be Category;
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
ex b1 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 b1 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)]
proof end;
uniqueness
for b1, b2 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 b1 . [[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 b2 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines export ISOCAT_2:def 6 :
for A, B, C being Category
for b4 being Functor of Functors [:A,B:],C, Functors A,(Functors B,C) holds
( b4 = 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 b4 . [[F1,F2],t] = [[(export F1),(export F2)],(export t)] );

theorem Th33: :: ISOCAT_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category holds export A,B,C is_an_isomorphism
proof end;

theorem :: ISOCAT_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category holds Functors [:A,B:],C ~= Functors A,(Functors B,C)
proof end;

theorem Th35: :: ISOCAT_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let A, B be Category;
:: original: pr1
redefine func pr1 A,B -> Functor of [:A,B:],A;
coherence
pr1 A,B is Functor of [:A,B:],A
;
:: original: pr2
redefine func pr2 A,B -> Functor of [:A,B:],B;
coherence
pr2 A,B is Functor of [:A,B:],B
;
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:]
proof end;
end;

definition
let A, B, C be Category;
let F be Functor of A,[:B,C:];
func Pr1 F -> Functor of A,B equals :: ISOCAT_2:def 7
(pr1 B,C) * F;
correctness
coherence
(pr1 B,C) * F is Functor of A,B
;
;
func Pr2 F -> Functor of A,C equals :: ISOCAT_2:def 8
(pr2 B,C) * F;
correctness
coherence
(pr2 B,C) * F is Functor of A,C
;
;
end;

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

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

theorem Th36: :: ISOCAT_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F being Functor of A,B
for G being Functor of A,C holds
( Pr1 <:F,G:> = F & Pr2 <:F,G:> = G )
proof end;

theorem Th37: :: ISOCAT_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F, G being Functor of A,[:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G holds
F = G
proof end;

definition
let A, B, C be Category;
let F1, F2 be Functor of A,[:B,C:];
let t be natural_transformation of F1,F2;
func Pr1 t -> natural_transformation of Pr1 F1, Pr1 F2 equals :: ISOCAT_2:def 9
(pr1 B,C) * t;
coherence
(pr1 B,C) * t is natural_transformation of Pr1 F1, Pr1 F2
;
func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals :: ISOCAT_2:def 10
(pr2 B,C) * t;
coherence
(pr2 B,C) * t is natural_transformation of Pr2 F1, Pr2 F2
;
end;

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

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

theorem Th38: :: ISOCAT_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F, G being Functor of A,[:B,C:] st F is_naturally_transformable_to G holds
( Pr1 F is_naturally_transformable_to Pr1 G & Pr2 F is_naturally_transformable_to Pr2 G ) by ISOCAT_1:27;

theorem Th39: :: ISOCAT_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th40: :: ISOCAT_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F being Functor of A,[:B,C:] holds
( id (Pr1 F) = Pr1 (id F) & id (Pr2 F) = Pr2 (id F) ) by ISOCAT_1:38;

theorem Th41: :: ISOCAT_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F, G, H being Functor of A,[:B,C:] st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds
for s being natural_transformation of F,G
for t being natural_transformation of G,H holds
( Pr1 (t `*` s) = (Pr1 t) `*` (Pr1 s) & Pr2 (t `*` s) = (Pr2 t) `*` (Pr2 s) ) by ISOCAT_1:32;

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 = [(t1 . a),(t2 . a)]
proof end;

theorem Th42: :: ISOCAT_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category
for F being Functor of A,B
for G being Functor of A,C
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)]
proof end;

theorem Th43: :: ISOCAT_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
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_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 Th44: :: ISOCAT_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:>
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_transformable_to G1 & F2 is_transformable_to G2 ) ;
let t1 be transformation of F1,G1;
let t2 be transformation of F2,G2;
func <:t1,t2:> -> transformation of <:F1,F2:>,<:G1,G2:> equals :Def11: :: ISOCAT_2:def 11
<:t1,t2:>;
coherence
<:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:>
proof end;
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:>;

theorem Th45: :: ISOCAT_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm5: 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 Th46: :: ISOCAT_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:>
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 that
A1: F1 is_naturally_transformable_to G1 and
A2: 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:> is natural_transformation of <:F1,F2:>,<:G1,G2:>
proof end;
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:>;

theorem Th47: :: ISOCAT_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let A, B, C be Category;
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
ex b1 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 b1 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
proof end;
uniqueness
for b1, b2 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 b1 . [[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 b2 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines distribute ISOCAT_2:def 13 :
for A, B, C being Category
for b4 being Functor of Functors A,[:B,C:],[:(Functors A,B),(Functors A,C):] holds
( b4 = 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 b4 . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] );

theorem Th48: :: ISOCAT_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category holds distribute A,B,C is_an_isomorphism
proof end;

theorem :: ISOCAT_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Category holds Functors A,[:B,C:] ~= [:(Functors A,B),(Functors A,C):]
proof end;