:: ISOCAT_2 semantic presentation

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of c₁, Funcs c₂,c₃;
redefine func uncurry as uncurry c₄ -> Function of [:a₁,a₂:],a₃;
coherence

proof end;

end;

theorem Th1: :: ISOCAT_2:1

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁, Funcs b₂,b₃ holds curry (uncurry b₄) = b₄

proof end;

theorem Th2: :: ISOCAT_2:2

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁, Funcs b₂,b₃
for b₅ being Element of b₁
for b₆ being Element of b₂ holds (uncurry b₄) . [b₅,b₆] = (b₄ . b₅) . b₆

proof end;

theorem Th3: :: ISOCAT_2:3

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of {b₁},b₂ st b₃ . b₁ = b₄ . b₁ holds
b₃ = b₄

proof end;

theorem Th4: :: ISOCAT_2:4

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Function of b₁,b₂ holds b₄ . b₃ in rng b₄

proof end;

theorem Th5: :: ISOCAT_2:5

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being Function of b₁,[:b₂,b₃:] st (pr1 b₂,b₃) * b₄ = (pr1 b₂,b₃) * b₅ & (pr2 b₂,b₃) * b₄ = (pr2 b₂,b₃) * b₅ holds
b₄ = b₅

proof end;

theorem Th6: :: ISOCAT_2:6

for b₁ being Category
for b₂ being Morphism of b₁ holds (id (cod b₂)) * b₂ = b₂

proof end;

theorem Th7: :: ISOCAT_2:7

for b₁ being Category
for b₂ being Morphism of b₁ holds b₂ * (id (dom b₂)) = b₂

proof end;

theorem Th8: :: ISOCAT_2:8

for b₁, b₂ being Category
for b₃ being set holds
( b₃ is Object of (Functors b₁,b₂) iff b₃ is Functor of b₁,b₂ )

proof end;

theorem Th9: :: ISOCAT_2:9

for b₁, b₂ being Category
for b₃ being Morphism of (Functors b₁,b₂) ex b₄, b₅ being Functor of b₁,b₂ex b₆ being natural_transformation of b₄,b₅ st
( b₄ is_naturally_transformable_to b₅ & dom b₃ = b₄ & cod b₃ = b₅ & b₃ = [[b₄,b₅],b₆] )

proof end;

definition

let c₁, c₂ be Category;
let c₃ be Object of c₁;
func c₃ |-> c₂ -> Functor of Functors a₁,a₂,a₂ means :Def1: :: ISOCAT_2:def 1
for b₁, b₂ being Functor of a₁,a₂
for b₃ being natural_transformation of b₁,b₂ st b₁ is_naturally_transformable_to b₂ holds
a₄ . [[b₁,b₂],b₃] = b₃ . a₃;
existence

proof end;

uniqueness

proof end;

end;

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

Lemma11: for b₁, b₂ being set holds
( the Objects of (1Cat b₁,b₂) = {b₁} & the Morphisms of (1Cat b₁,b₂) = {b₂} )

proof end;

theorem Th10: :: ISOCAT_2:10

canceled;

theorem Th11: :: ISOCAT_2:11

for b₁ being Category
for b₂, b₃ being set holds Functors (1Cat b₂,b₃),b₁ ~= b₁

proof end;

theorem Th12: :: ISOCAT_2:12

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁
for b₆ being Object of b₂ holds (b₄ ?- b₅) . b₆ = b₄ . [b₅,b₆]

proof end;

theorem Th13: :: ISOCAT_2:13

for b₁, b₂ being Category
for b₃, b₄ being Object of b₁
for b₅, b₆ being Object of b₂ holds
( ( Hom b₃,b₄ <> {} & Hom b₅,b₆ <> {} ) iff Hom [b₃,b₅],[b₄,b₆] <> {} )

proof end;

theorem Th14: :: ISOCAT_2:14

for b₁, b₂ being Category
for b₃, b₄ being Object of b₁
for b₅, b₆ being Object of b₂ st Hom [b₃,b₅],[b₄,b₆] <> {} holds
for b₇ being Morphism of b₁
for b₈ being Morphism of b₂ holds
( [b₇,b₈] is Morphism of [b₃,b₅],[b₄,b₆] iff ( b₇ is Morphism of b₃,b₄ & b₈ is Morphism of b₅,b₆ ) )

proof end;

theorem Th15: :: ISOCAT_2:15

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of [:b₁,b₂:],b₃ st b₄ is_naturally_transformable_to b₅ holds
for b₆ being natural_transformation of b₄,b₅
for b₇ being Object of b₁ holds
( b₄ ?- b₇ is_naturally_transformable_to b₅ ?- b₇ & (curry b₆) . b₇ is natural_transformation of b₄ ?- b₇,b₅ ?- b₇ )

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of [:c₁,c₂:],c₃;
let c₅ be Morphism of c₁;
func curry c₄,c₅ -> Function of the Morphisms of a₂,the Morphisms of a₃ equals :: ISOCAT_2:def 2
(curry a₄) . a₅;
coherence

proof end;

end;

:: deftheorem Def2 defines curry ISOCAT_2:def 2 :

theorem Th16: :: ISOCAT_2:16

for b₁, b₂ being Category
for b₃, b₄ being Object of b₁
for b₅, b₆ being Object of b₂
for b₇ being Morphism of b₁
for b₈ being Morphism of b₂ st b₇ in Hom b₃,b₄ & b₈ in Hom b₅,b₆ holds
[b₇,b₈] in Hom [b₃,b₅],[b₄,b₆]

proof end;

theorem Th17: :: ISOCAT_2:17

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅, b₆ being Object of b₁ st Hom b₅,b₆ <> {} holds
for b₇ being Morphism of b₅,b₆ holds
( b₄ ?- b₅ is_naturally_transformable_to b₄ ?- b₆ & (curry b₄,b₇) * the Id of b₂ is natural_transformation of b₄ ?- b₅,b₄ ?- b₆ )

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of [:c₁,c₂:],c₃;
let c₅ be Morphism of c₁;
func c₄ ?- c₅ -> natural_transformation of a₄ ?- (dom a₅),a₄ ?- (cod a₅) equals :: ISOCAT_2:def 3
(curry a₄,a₅) * the Id of a₂;
coherence

proof end;

correctness ;

end;

:: deftheorem Def3 defines ?- ISOCAT_2:def 3 :

theorem Th18: :: ISOCAT_2:18

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Morphism of b₁ holds b₄ ?- (dom b₅) is_naturally_transformable_to b₄ ?- (cod b₅)

proof end;

theorem Th19: :: ISOCAT_2:19

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Morphism of b₁
for b₆ being Object of b₂ holds (b₄ ?- b₅) . b₆ = b₄ . [b₅,(id b₆)]

proof end;

theorem Th20: :: ISOCAT_2:20

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁ holds id (b₄ ?- b₅) = b₄ ?- (id b₅)

proof end;

theorem Th21: :: ISOCAT_2:21

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅, b₆ being Morphism of b₁ st dom b₅ = cod b₆ holds
for b₇ being natural_transformation of b₄ ?- (dom b₆),b₄ ?- (dom b₅) st b₇ = b₄ ?- b₆ holds
b₄ ?- (b₅ * b₆) = (b₄ ?- b₅) `*` b₇

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of [:c₁,c₂:],c₃;
func export c₄ -> Functor of a₁, Functors a₂,a₃ means :Def4: :: ISOCAT_2:def 4
for b₁ being Morphism of a₁ holds a₅ . b₁ = [[(a₄ ?- (dom b₁)),(a₄ ?- (cod b₁))],(a₄ ?- b₁)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines export ISOCAT_2:def 4 :

Lemma23: for b₁, b₂ being Category
for b₃, b₄ being Functor of b₁,b₂ st b₃ is_transformable_to b₄ holds
for b₅ being transformation of b₃,b₄
for b₆ being Object of b₁ holds b₅ . b₆ in Hom (b₃ . b₆),(b₄ . b₆)

proof end;

theorem Th22: :: ISOCAT_2:22

canceled;

theorem Th23: :: ISOCAT_2:23

canceled;

theorem Th24: :: ISOCAT_2:24

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁ holds (export b₄) . b₅ = b₄ ?- b₅

proof end;

theorem Th25: :: ISOCAT_2:25

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃
for b₅ being Object of b₁ holds (export b₄) . b₅ is Functor of b₂,b₃

proof end;

theorem Th26: :: ISOCAT_2:26

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of [:b₁,b₂:],b₃ st export b₄ = export b₅ holds
b₄ = b₅

proof end;

theorem Th27: :: ISOCAT_2:27

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of [:b₁,b₂:],b₃ st b₄ is_naturally_transformable_to b₅ holds
for b₆ being natural_transformation of b₄,b₅ holds
( export b₄ is_naturally_transformable_to export b₅ & ex b₇ being natural_transformation of export b₄, export b₅ st
for b₈ being Function of [:the Objects of b₁,the Objects of b₂:],the Morphisms of b₃ st b₆ = b₈ holds
for b₉ being Object of b₁ holds b₇ . b₉ = [[((export b₄) . b₉),((export b₅) . b₉)],((curry b₈) . b₉)] )

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of [:c₁,c₂:],c₃;
assume E28: c₄ is_naturally_transformable_to c₅ ;
let c₆ be natural_transformation of c₄,c₅;
func export c₆ -> natural_transformation of export a₄, export a₅ means :Def5: :: ISOCAT_2:def 5
for b₁ being Function of [:the Objects of a₁,the Objects of a₂:],the Morphisms of a₃ st a₆ = b₁ holds
for b₂ being Object of a₁ holds a₇ . b₂ = [[((export a₄) . b₂),((export a₅) . b₂)],((curry b₁) . b₂)];
existence by E28, Th27;
uniqueness

proof end;

end;

:: deftheorem Def5 defines export ISOCAT_2:def 5 :

theorem Th28: :: ISOCAT_2:28

for b₁, b₂, b₃ being Category
for b₄ being Functor of [:b₁,b₂:],b₃ holds id (export b₄) = export (id b₄)

proof end;

theorem Th29: :: ISOCAT_2:29

for b₁, b₂, b₃ being Category
for b₄, b₅, b₆ being Functor of [:b₁,b₂:],b₃ st b₄ is_naturally_transformable_to b₅ & b₅ is_naturally_transformable_to b₆ holds
for b₇ being natural_transformation of b₄,b₅
for b₈ being natural_transformation of b₅,b₆ holds export (b₈ `*` b₇) = (export b₈) `*` (export b₇)

proof end;

theorem Th30: :: ISOCAT_2:30

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of [:b₁,b₂:],b₃ st b₄ is_naturally_transformable_to b₅ holds
for b₆, b₇ being natural_transformation of b₄,b₅ st export b₆ = export b₇ holds
b₆ = b₇

proof end;

theorem Th31: :: ISOCAT_2:31

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁, Functors b₂,b₃ ex b₅ being Functor of [:b₁,b₂:],b₃ st b₄ = export b₅

proof end;

theorem Th32: :: ISOCAT_2:32

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of [:b₁,b₂:],b₃ st export b₄ is_naturally_transformable_to export b₅ holds
for b₆ being natural_transformation of export b₄, export b₅ holds
( b₄ is_naturally_transformable_to b₅ & ex b₇ being natural_transformation of b₄,b₅ st b₆ = export b₇ )

proof end;

definition

let c₁, c₂, c₃ be Category;
func export c₁,c₂,c₃ -> Functor of Functors [:a₁,a₂:],a₃, Functors a₁,(Functors a₂,a₃) means :Def6: :: ISOCAT_2:def 6
for b₁, b₂ being Functor of [:a₁,a₂:],a₃ st b₁ is_naturally_transformable_to b₂ holds
for b₃ being natural_transformation of b₁,b₂ holds a₄ . [[b₁,b₂],b₃] = [[(export b₁),(export b₂)],(export b₃)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines export ISOCAT_2:def 6 :

theorem Th33: :: ISOCAT_2:33

for b₁, b₂, b₃ being Category holds export b₁,b₂,b₃ is_an_isomorphism

proof end;

theorem Th34: :: ISOCAT_2:34

for b₁, b₂, b₃ being Category holds Functors [:b₁,b₂:],b₃ ~= Functors b₁,(Functors b₂,b₃)

proof end;

theorem Th35: :: ISOCAT_2:35

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆ being Functor of b₂,b₃ st b₄ is_naturally_transformable_to b₅ holds
for b₇ being natural_transformation of b₄,b₅ holds b₆ * b₇ = b₆ * b₇

proof end;

definition

let c₁, c₂ be Category;
redefine func pr1 as pr1 c₁,c₂ -> Functor of [:a₁,a₂:],a₁;
coherence ;
redefine func pr2 as pr2 c₁,c₂ -> Functor of [:a₁,a₂:],a₂;
coherence ;

end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,c₂;
let c₅ be Functor of c₁,c₃;
redefine func <: as <:c₄,c₅:> -> Functor of a₁,[:a₂,a₃:];
coherence

proof end;

end;

definition

let c₁, c₂, c₃ be Category;
let c₄ be Functor of c₁,[:c₂,c₃:];
func Pr1 c₄ -> Functor of a₁,a₂ equals :: ISOCAT_2:def 7
(pr1 a₂,a₃) * a₄;
correctness ;
func Pr2 c₄ -> Functor of a₁,a₃ equals :: ISOCAT_2:def 8
(pr2 a₂,a₃) * a₄;
correctness ;

end;

:: deftheorem Def7 defines Pr1 ISOCAT_2:def 7 :

:: deftheorem Def8 defines Pr2 ISOCAT_2:def 8 :

theorem Th36: :: ISOCAT_2:36

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃ holds
( Pr1 <:b₄,b₅:> = b₄ & Pr2 <:b₄,b₅:> = b₅ )

proof end;

theorem Th37: :: ISOCAT_2:37

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,[:b₂,b₃:] st Pr1 b₄ = Pr1 b₅ & Pr2 b₄ = Pr2 b₅ holds
b₄ = b₅

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₁,[:c₂,c₃:];
let c₆ be natural_transformation of c₄,c₅;
func Pr1 c₆ -> natural_transformation of Pr1 a₄, Pr1 a₅ equals :: ISOCAT_2:def 9
(pr1 a₂,a₃) * a₆;
coherence ;
func Pr2 c₆ -> natural_transformation of Pr2 a₄, Pr2 a₅ equals :: ISOCAT_2:def 10
(pr2 a₂,a₃) * a₆;
coherence ;

end;

:: deftheorem Def9 defines Pr1 ISOCAT_2:def 9 :

:: deftheorem Def10 defines Pr2 ISOCAT_2:def 10 :

theorem Th38: :: ISOCAT_2:38

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,[:b₂,b₃:] st b₄ is_naturally_transformable_to b₅ holds
( Pr1 b₄ is_naturally_transformable_to Pr1 b₅ & Pr2 b₄ is_naturally_transformable_to Pr2 b₅ ) by ISOCAT_1:27;

theorem Th39: :: ISOCAT_2:39

for b₁, b₂, b₃ being Category
for b₄, b₅, b₆, b₇ being Functor of b₁,[:b₂,b₃:] st b₄ is_naturally_transformable_to b₅ & b₆ is_naturally_transformable_to b₇ holds
for b₈ being natural_transformation of b₄,b₅
for b₉ being natural_transformation of b₆,b₇ st Pr1 b₈ = Pr1 b₉ & Pr2 b₈ = Pr2 b₉ holds
b₈ = b₉

proof end;

theorem Th40: :: ISOCAT_2:40

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,[:b₂,b₃:] holds
( id (Pr1 b₄) = Pr1 (id b₄) & id (Pr2 b₄) = Pr2 (id b₄) ) by ISOCAT_1:38;

theorem Th41: :: ISOCAT_2:41

for b₁, b₂, b₃ being Category
for b₄, b₅, b₆ being Functor of b₁,[:b₂,b₃:] st b₄ is_naturally_transformable_to b₅ & b₅ is_naturally_transformable_to b₆ holds
for b₇ being natural_transformation of b₄,b₅
for b₈ being natural_transformation of b₅,b₆ holds
( Pr1 (b₈ `*` b₇) = (Pr1 b₈) `*` (Pr1 b₇) & Pr2 (b₈ `*` b₇) = (Pr2 b₈) `*` (Pr2 b₇) ) by ISOCAT_1:32;

Lemma43: for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_transformable_to b₅ & b₆ is_transformable_to b₇ holds
for b₈ being transformation of b₄,b₅
for b₉ being transformation of b₆,b₇
for b₁₀ being Object of b₁ holds <:b₈,b₉:> . b₁₀ = [(b₈ . b₁₀),(b₉ . b₁₀)]

proof end;

theorem Th42: :: ISOCAT_2:42

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃
for b₆, b₇ being Object of b₁ st Hom b₆,b₇ <> {} holds
for b₈ being Morphism of b₆,b₇ holds <:b₄,b₅:> . b₈ = [(b₄ . b₈),(b₅ . b₈)]

proof end;

theorem Th43: :: ISOCAT_2:43

for b₁, b₂, b₃ being Category
for b₄ being Functor of b₁,b₂
for b₅ being Functor of b₁,b₃
for b₆ being Object of b₁ holds <:b₄,b₅:> . b₆ = [(b₄ . b₆),(b₅ . b₆)]

proof end;

Lemma46: for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_transformable_to b₅ & b₆ is_transformable_to b₇ holds
for b₈ being transformation of b₄,b₅
for b₉ being transformation of b₆,b₇
for b₁₀ being Object of b₁ holds <:b₈,b₉:> . b₁₀ in Hom (<:b₄,b₆:> . b₁₀),(<:b₅,b₇:> . b₁₀)

proof end;

theorem Th44: :: ISOCAT_2:44

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_transformable_to b₅ & b₆ is_transformable_to b₇ holds
<:b₄,b₆:> is_transformable_to <:b₅,b₇:>

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₁,c₂;
let c₆, c₇ be Functor of c₁,c₃;
assume E48: ( c₄ is_transformable_to c₅ & c₆ is_transformable_to c₇ ) ;
let c₈ be transformation of c₄,c₅;
let c₉ be transformation of c₆,c₇;
func <:c₈,c₉:> -> transformation of <:a₄,a₆:>,<:a₅,a₇:> equals :Def11: :: ISOCAT_2:def 11
<:a₈,a₉:>;
coherence

proof end;

end;

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

theorem Th45: :: ISOCAT_2:45

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_transformable_to b₅ & b₆ is_transformable_to b₇ holds
for b₈ being transformation of b₄,b₅
for b₉ being transformation of b₆,b₇
for b₁₀ being Object of b₁ holds <:b₈,b₉:> . b₁₀ = [(b₈ . b₁₀),(b₉ . b₁₀)]

proof end;

Lemma50: for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_naturally_transformable_to b₅ & b₆ is_naturally_transformable_to b₇ holds
for b₈ being natural_transformation of b₄,b₅
for b₉ being natural_transformation of b₆,b₇
for b₁₀, b₁₁ being Object of b₁ st Hom b₁₀,b₁₁ <> {} holds
for b₁₂ being Morphism of b₁₀,b₁₁ holds (<:b₈,b₉:> . b₁₁) * (<:b₄,b₆:> . b₁₂) = (<:b₅,b₇:> . b₁₂) * (<:b₈,b₉:> . b₁₀)

proof end;

theorem Th46: :: ISOCAT_2:46

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_naturally_transformable_to b₅ & b₆ is_naturally_transformable_to b₇ holds
<:b₄,b₆:> is_naturally_transformable_to <:b₅,b₇:>

proof end;

definition

let c₁, c₂, c₃ be Category;
let c₄, c₅ be Functor of c₁,c₂;
let c₆, c₇ be Functor of c₁,c₃;
assume that
E52: c₄ is_naturally_transformable_to c₅ and
E53: c₆ is_naturally_transformable_to c₇ ;
let c₈ be natural_transformation of c₄,c₅;
let c₉ be natural_transformation of c₆,c₇;
func <:c₈,c₉:> -> natural_transformation of <:a₄,a₆:>,<:a₅,a₇:> equals :Def12: :: ISOCAT_2:def 12
<:a₈,a₉:>;
coherence

proof end;

end;

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

theorem Th47: :: ISOCAT_2:47

for b₁, b₂, b₃ being Category
for b₄, b₅ being Functor of b₁,b₂
for b₆, b₇ being Functor of b₁,b₃ st b₄ is_naturally_transformable_to b₅ & b₆ is_naturally_transformable_to b₇ holds
for b₈ being natural_transformation of b₄,b₅
for b₉ being natural_transformation of b₆,b₇ holds
( Pr1 <:b₈,b₉:> = b₈ & Pr2 <:b₈,b₉:> = b₉ )

proof end;

definition

let c₁, c₂, c₃ be Category;
func distribute c₁,c₂,c₃ -> Functor of Functors a₁,[:a₂,a₃:],[:(Functors a₁,a₂),(Functors a₁,a₃):] means :Def13: :: ISOCAT_2:def 13
for b₁, b₂ being Functor of a₁,[:a₂,a₃:] st b₁ is_naturally_transformable_to b₂ holds
for b₃ being natural_transformation of b₁,b₂ holds a₄ . [[b₁,b₂],b₃] = [[[(Pr1 b₁),(Pr1 b₂)],(Pr1 b₃)],[[(Pr2 b₁),(Pr2 b₂)],(Pr2 b₃)]];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines distribute ISOCAT_2:def 13 :

theorem Th48: :: ISOCAT_2:48

for b₁, b₂, b₃ being Category holds distribute b₁,b₂,b₃ is_an_isomorphism

proof end;

theorem Th49: :: ISOCAT_2:49

for b₁, b₂, b₃ being Category holds Functors b₁,[:b₂,b₃:] ~= [:(Functors b₁,b₂),(Functors b₁,b₃):]

proof end;