:: by Czes{\l}aw Byli\'nski

::

:: Received May 31, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: Auxiliary theorems on Functors

definition

let B, C be Category;

let c be Object of C;

coherence

the carrier' of B --> (id c) is Functor of B,C

end;
let c be Object of C;

coherence

the carrier' of B --> (id c) is Functor of B,C

proof end;

:: deftheorem defines --> CAT_2:def 1 :

for B, C being Category

for c being Object of C holds B --> c = the carrier' of B --> (id c);

for B, C being Category

for c being Object of C holds B --> c = the carrier' of B --> (id c);

theorem :: CAT_2:5

for C, B being Category

for c being Object of C

for b being Object of B holds (Obj (B --> c)) . b = c

for c being Object of C

for b being Object of B holds (Obj (B --> c)) . b = c

proof end;

definition

let C, D be Category;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Functor of C,D )

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

( x in b_{1} iff x is Functor of C,D ) ) & ( for x being set holds

( x in b_{2} iff x is Functor of C,D ) ) holds

b_{1} = b_{2}

end;
func Funct (C,D) -> set means :Def2: :: CAT_2:def 2

for x being set holds

( x in it iff x is Functor of C,D );

existence for x being set holds

( x in it iff x is Functor of C,D );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines Funct CAT_2:def 2 :

for C, D being Category

for b_{3} being set holds

( b_{3} = Funct (C,D) iff for x being set holds

( x in b_{3} iff x is Functor of C,D ) );

for C, D being Category

for b

( b

( x in b

definition

let C, D be Category;

ex b_{1} being non empty set st

for x being Element of b_{1} holds x is Functor of C,D

end;
mode FUNCTOR-DOMAIN of C,D -> non empty set means :Def3: :: CAT_2:def 3

for x being Element of it holds x is Functor of C,D;

existence for x being Element of it holds x is Functor of C,D;

ex b

for x being Element of b

proof end;

:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :

for C, D being Category

for b_{3} being non empty set holds

( b_{3} is FUNCTOR-DOMAIN of C,D iff for x being Element of b_{3} holds x is Functor of C,D );

for C, D being Category

for b

( b

definition

let C, D be Category;

let F be FUNCTOR-DOMAIN of C,D;

:: original: Element

redefine mode Element of F -> Functor of C,D;

coherence

for b_{1} being Element of F holds b_{1} is Functor of C,D
by Def3;

end;
let F be FUNCTOR-DOMAIN of C,D;

:: original: Element

redefine mode Element of F -> Functor of C,D;

coherence

for b

definition

let A be non empty set ;

let C, D be Category;

let F be FUNCTOR-DOMAIN of C,D;

let T be Function of A,F;

let x be Element of A;

:: original: .

redefine func T . x -> Element of F;

coherence

T . x is Element of F

end;
let C, D be Category;

let F be FUNCTOR-DOMAIN of C,D;

let T be Function of A,F;

let x be Element of A;

:: original: .

redefine func T . x -> Element of F;

coherence

T . x is Element of F

proof end;

definition

let C, D be Category;

:: original: Funct

redefine func Funct (C,D) -> FUNCTOR-DOMAIN of C,D;

coherence

Funct (C,D) is FUNCTOR-DOMAIN of C,D

end;
:: original: Funct

redefine func Funct (C,D) -> FUNCTOR-DOMAIN of C,D;

coherence

Funct (C,D) is FUNCTOR-DOMAIN of C,D

proof end;

:: Subcategory

definition

let C be Category;

ex b_{1} being Category st

( the carrier of b_{1} c= the carrier of C & ( for a, b being Object of b_{1}

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of b_{1} c= the Comp of C & ( for a being Object of b_{1}

for a9 being Object of C st a = a9 holds

id a = id a9 ) )

end;
mode Subcategory of C -> Category means :Def4: :: CAT_2:def 4

( the carrier of it c= the carrier of C & ( for a, b being Object of it

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of it c= the Comp of C & ( for a being Object of it

for a9 being Object of C st a = a9 holds

id a = id a9 ) );

existence ( the carrier of it c= the carrier of C & ( for a, b being Object of it

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of it c= the Comp of C & ( for a being Object of it

for a9 being Object of C st a = a9 holds

id a = id a9 ) );

ex b

( the carrier of b

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of b

for a9 being Object of C st a = a9 holds

id a = id a9 ) )

proof end;

:: deftheorem Def4 defines Subcategory CAT_2:def 4 :

for C, b_{2} being Category holds

( b_{2} is Subcategory of C iff ( the carrier of b_{2} c= the carrier of C & ( for a, b being Object of b_{2}

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of b_{2} c= the Comp of C & ( for a being Object of b_{2}

for a9 being Object of C st a = a9 holds

id a = id a9 ) ) );

for C, b

( b

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) c= Hom (a9,b9) ) & the Comp of b

for a9 being Object of C st a = a9 holds

id a = id a9 ) ) );

registration

let C be Category;

ex b_{1} being Subcategory of C st b_{1} is strict

end;
cluster non empty non void V55() strict Category-like transitive associative reflexive with_identities for Subcategory of C;

existence ex b

proof end;

theorem Th8: :: CAT_2:8

for C being Category

for E being Subcategory of C

for f being Morphism of E holds f is Morphism of C

for E being Subcategory of C

for f being Morphism of E holds f is Morphism of C

proof end;

theorem Th9: :: CAT_2:9

for C being Category

for E being Subcategory of C

for f being Morphism of E

for f9 being Morphism of C st f = f9 holds

( dom f = dom f9 & cod f = cod f9 )

for E being Subcategory of C

for f being Morphism of E

for f9 being Morphism of C st f = f9 holds

( dom f = dom f9 & cod f = cod f9 )

proof end;

theorem :: CAT_2:10

for C being Category

for E being Subcategory of C

for a, b being Object of E

for a9, b9 being Object of C

for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds

f is Morphism of a9,b9

for E being Subcategory of C

for a, b being Object of E

for a9, b9 being Object of C

for f being Morphism of a,b st a = a9 & b = b9 & Hom (a,b) <> {} holds

f is Morphism of a9,b9

proof end;

theorem Th11: :: CAT_2:11

for C being Category

for E being Subcategory of C

for f, g being Morphism of E

for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds

g (*) f = g9 (*) f9

for E being Subcategory of C

for f, g being Morphism of E

for f9, g9 being Morphism of C st f = f9 & g = g9 & dom g = cod f holds

g (*) f = g9 (*) f9

proof end;

definition
end;

:: deftheorem defines incl CAT_2:def 5 :

for C being Category

for E being Subcategory of C holds incl E = id E;

for C being Category

for E being Subcategory of C holds incl E = id E;

theorem Th14: :: CAT_2:14

for C being Category

for E being Subcategory of C

for a being Object of E holds (Obj (incl E)) . a = a

for E being Subcategory of C

for a being Object of E holds (Obj (incl E)) . a = a

proof end;

theorem :: CAT_2:15

theorem Th17: :: CAT_2:17

for C being Category

for E being Subcategory of C holds

( incl E is full iff for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) )

for E being Subcategory of C holds

( incl E is full iff for a, b being Object of E

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9) )

proof end;

:: deftheorem Def6 defines full CAT_2:def 6 :

for D being Category

for C being Subcategory of D holds

( C is full iff for c1, c2 being Object of C

for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds

Hom (c1,c2) = Hom (d1,d2) );

for D being Category

for C being Subcategory of D holds

( C is full iff for c1, c2 being Object of C

for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds

Hom (c1,c2) = Hom (d1,d2) );

registration

let D be Category;

ex b_{1} being Subcategory of D st b_{1} is full

end;
cluster non empty non void V55() Category-like transitive associative reflexive with_identities full for Subcategory of D;

existence ex b

proof end;

theorem Th19: :: CAT_2:19

for C being Category

for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C

for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C

proof end;

theorem Th20: :: CAT_2:20

for C being Category

for O being non empty Subset of the carrier of C

for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds

( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

for O being non empty Subset of the carrier of C

for M being non empty set st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } holds

( the Source of C | M is Function of M,O & the Target of C | M is Function of M,O & the Comp of C || M is PartFunc of [:M,M:],M )

proof end;

registration

let O, M be non empty set ;

let d, c be Function of M,O;

let p be PartFunc of [:M,M:],M;

coherence

( not CatStr(# O,M,d,c,p #) is void & not CatStr(# O,M,d,c,p #) is empty ) ;

end;
let d, c be Function of M,O;

let p be PartFunc of [:M,M:],M;

coherence

( not CatStr(# O,M,d,c,p #) is void & not CatStr(# O,M,d,c,p #) is empty ) ;

Lm1: for C being Category

for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Category

proof end;

Lm2: for C being Category

for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is Subcategory of C

proof end;

theorem :: CAT_2:21

for C being Category

for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is full Subcategory of C

for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M

for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds

CatStr(# O,M,d,c,p #) is full Subcategory of C

proof end;

theorem :: CAT_2:22

for C being Category

for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds

( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )

for O being non empty Subset of the carrier of C

for M being non empty set

for d, c being Function of M,O

for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) is full Subcategory of C holds

( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )

proof end;

:: Product of Categories

definition

let X1, X2, Y1, Y2 be non empty set ;

let f1 be Function of X1,Y1;

let f2 be Function of X2,Y2;

:: original: [:

redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];

coherence

[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]

end;
let f1 be Function of X1,Y1;

let f2 be Function of X2,Y2;

:: original: [:

redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];

coherence

[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]

proof end;

definition

let A, B be non empty set ;

let f be PartFunc of [:A,A:],A;

let g be PartFunc of [:B,B:],B;

:: original: |:

redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];

coherence

|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:] by FUNCT_4:59;

end;
let f be PartFunc of [:A,A:],A;

let g be PartFunc of [:B,B:],B;

:: original: |:

redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];

coherence

|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:] by FUNCT_4:59;

definition

let C, D be Category;

CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category

end;
func [:C,D:] -> Category equals :: CAT_2:def 7

CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);

coherence CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);

CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #) is Category

proof end;

:: deftheorem defines [: CAT_2:def 7 :

for C, D being Category holds [:C,D:] = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);

for C, D being Category holds [:C,D:] = CatStr(# [: the carrier of C, the carrier of D:],[: the carrier' of C, the carrier' of D:],[: the Source of C, the Source of D:],[: the Target of C, the Target of D:],|: the Comp of C, the Comp of D:| #);

theorem :: CAT_2:23

for C, D being Category holds

( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] & the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] & the Source of [:C,D:] = [: the Source of C, the Source of D:] & the Target of [:C,D:] = [: the Target of C, the Target of D:] & the Comp of [:C,D:] = |: the Comp of C, the Comp of D:| ) ;

( the carrier of [:C,D:] = [: the carrier of C, the carrier of D:] & the carrier' of [:C,D:] = [: the carrier' of C, the carrier' of D:] & the Source of [:C,D:] = [: the Source of C, the Source of D:] & the Target of [:C,D:] = [: the Target of C, the Target of D:] & the Comp of [:C,D:] = |: the Comp of C, the Comp of D:| ) ;

definition

let C, D be Category;

let c be Object of C;

let d be Object of D;

:: original: [

redefine func [c,d] -> Object of [:C,D:];

coherence

[c,d] is Object of [:C,D:]

end;
let c be Object of C;

let d be Object of D;

:: original: [

redefine func [c,d] -> Object of [:C,D:];

coherence

[c,d] is Object of [:C,D:]

proof end;

theorem :: CAT_2:25

definition

let C, D be Category;

let f be Morphism of C;

let g be Morphism of D;

:: original: [

redefine func [f,g] -> Morphism of [:C,D:];

coherence

[f,g] is Morphism of [:C,D:]

end;
let f be Morphism of C;

let g be Morphism of D;

:: original: [

redefine func [f,g] -> Morphism of [:C,D:];

coherence

[f,g] is Morphism of [:C,D:]

proof end;

theorem :: CAT_2:27

theorem Th28: :: CAT_2:28

for C, D being Category

for f being Morphism of C

for g being Morphism of D holds

( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )

for f being Morphism of C

for g being Morphism of D holds

( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )

proof end;

theorem Th29: :: CAT_2:29

for C, D being Category

for f, f9 being Morphism of C

for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds

[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]

for f, f9 being Morphism of C

for g, g9 being Morphism of D st dom f9 = cod f & dom g9 = cod g holds

[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]

proof end;

theorem Th30: :: CAT_2:30

for C, D being Category

for f, f9 being Morphism of C

for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds

[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]

for f, f9 being Morphism of C

for g, g9 being Morphism of D st dom [f9,g9] = cod [f,g] holds

[f9,g9] (*) [f,g] = [(f9 (*) f),(g9 (*) g)]

proof end;

theorem Th31: :: CAT_2:31

for C, D being Category

for c being Object of C

for d being Object of D holds id [c,d] = [(id c),(id d)]

for c being Object of C

for d being Object of D holds id [c,d] = [(id c),(id d)]

proof end;

theorem :: CAT_2:32

for C, D being Category

for c, c9 being Object of C

for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]

for c, c9 being Object of C

for d, d9 being Object of D holds Hom ([c,d],[c9,d9]) = [:(Hom (c,c9)),(Hom (d,d9)):]

proof end;

theorem :: CAT_2:33

for C, D being Category

for c, c9 being Object of C

for f being Morphism of c,c9

for d, d9 being Object of D

for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds

[f,g] is Morphism of [c,d],[c9,d9]

for c, c9 being Object of C

for f being Morphism of c,c9

for d, d9 being Object of D

for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds

[f,g] is Morphism of [c,d],[c9,d9]

proof end;

:: Bifunctors

definition

let C, C9, D be Category;

let S be Functor of [:C,C9:],D;

let m be Morphism of C;

let m9 be Morphism of C9;

:: original: .

redefine func S . (m,m9) -> Morphism of D;

coherence

S . (m,m9) is Morphism of D

end;
let S be Functor of [:C,C9:],D;

let m be Morphism of C;

let m9 be Morphism of C9;

:: original: .

redefine func S . (m,m9) -> Morphism of D;

coherence

S . (m,m9) is Morphism of D

proof end;

theorem Th34: :: CAT_2:34

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c being Object of C holds (curry S) . (id c) is Functor of C9,D

for S being Functor of [:C,C9:],D

for c being Object of C holds (curry S) . (id c) is Functor of C9,D

proof end;

theorem Th35: :: CAT_2:35

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D

for S being Functor of [:C,C9:],D

for c9 being Object of C9 holds (curry' S) . (id c9) is Functor of C,D

proof end;

:: Partial Functors

definition

let C, C9, D be Category;

let S be Functor of [:C,C9:],D;

let c be Object of C;

coherence

(curry S) . (id c) is Functor of C9,D by Th34;

end;
let S be Functor of [:C,C9:],D;

let c be Object of C;

coherence

(curry S) . (id c) is Functor of C9,D by Th34;

:: deftheorem defines ?- CAT_2:def 8 :

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c being Object of C holds S ?- c = (curry S) . (id c);

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c being Object of C holds S ?- c = (curry S) . (id c);

theorem :: CAT_2:36

theorem :: CAT_2:37

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c being Object of C

for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)

for S being Functor of [:C,C9:],D

for c being Object of C

for c9 being Object of C9 holds (Obj (S ?- c)) . c9 = (Obj S) . (c,c9)

proof end;

definition

let C, C9, D be Category;

let S be Functor of [:C,C9:],D;

let c9 be Object of C9;

coherence

(curry' S) . (id c9) is Functor of C,D by Th35;

end;
let S be Functor of [:C,C9:],D;

let c9 be Object of C9;

coherence

(curry' S) . (id c9) is Functor of C,D by Th35;

:: deftheorem defines -? CAT_2:def 9 :

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c9 being Object of C9 holds S -? c9 = (curry' S) . (id c9);

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c9 being Object of C9 holds S -? c9 = (curry' S) . (id c9);

theorem :: CAT_2:38

theorem :: CAT_2:39

for C, C9, D being Category

for S being Functor of [:C,C9:],D

for c being Object of C

for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)

for S being Functor of [:C,C9:],D

for c being Object of C

for c9 being Object of C9 holds (Obj (S -? c9)) . c = (Obj S) . (c,c9)

proof end;

theorem :: CAT_2:40

for C, B, D being Category

for L being Function of the carrier of C,(Funct (B,D))

for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds

ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

for L being Function of the carrier of C,(Funct (B,D))

for M being Function of the carrier of B,(Funct (C,D)) st ( for c being Object of C

for b being Object of B holds (M . b) . (id c) = (L . c) . (id b) ) & ( for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g) ) holds

ex S being Functor of [:B,C:],D st

for f being Morphism of B

for g being Morphism of C holds S . (f,g) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

proof end;

theorem :: CAT_2:41

for C, B, D being Category

for L being Function of the carrier of C,(Funct (B,D))

for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) holds

for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

for L being Function of the carrier of C,(Funct (B,D))

for M being Function of the carrier of B,(Funct (C,D)) st ex S being Functor of [:B,C:],D st

for c being Object of C

for b being Object of B holds

( S -? c = L . c & S ?- b = M . b ) holds

for f being Morphism of B

for g being Morphism of C holds ((M . (cod f)) . g) (*) ((L . (dom g)) . f) = ((L . (cod g)) . f) (*) ((M . (dom f)) . g)

proof end;

definition

let C, D be Category;

pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C

pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D

end;
func pr1 (C,D) -> Functor of [:C,D:],C equals :: CAT_2:def 10

pr1 ( the carrier' of C, the carrier' of D);

coherence pr1 ( the carrier' of C, the carrier' of D);

pr1 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],C

proof end;

func pr2 (C,D) -> Functor of [:C,D:],D equals :: CAT_2:def 11

pr2 ( the carrier' of C, the carrier' of D);

coherence pr2 ( the carrier' of C, the carrier' of D);

pr2 ( the carrier' of C, the carrier' of D) is Functor of [:C,D:],D

proof end;

:: deftheorem defines pr1 CAT_2:def 10 :

for C, D being Category holds pr1 (C,D) = pr1 ( the carrier' of C, the carrier' of D);

for C, D being Category holds pr1 (C,D) = pr1 ( the carrier' of C, the carrier' of D);

:: deftheorem defines pr2 CAT_2:def 11 :

for C, D being Category holds pr2 (C,D) = pr2 ( the carrier' of C, the carrier' of D);

for C, D being Category holds pr2 (C,D) = pr2 ( the carrier' of C, the carrier' of D);

theorem :: CAT_2:44

for C, D being Category

for c being Object of C

for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c

for c being Object of C

for d being Object of D holds (Obj (pr1 (C,D))) . (c,d) = c

proof end;

theorem :: CAT_2:45

for C, D being Category

for c being Object of C

for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d

for c being Object of C

for d being Object of D holds (Obj (pr2 (C,D))) . (c,d) = d

proof end;

definition

let C, D, D9 be Category;

let T be Functor of C,D;

let T9 be Functor of C,D9;

:: original: <:

redefine func <:T,T9:> -> Functor of C,[:D,D9:];

coherence

<:T,T9:> is Functor of C,[:D,D9:]

end;
let T be Functor of C,D;

let T9 be Functor of C,D9;

:: original: <:

redefine func <:T,T9:> -> Functor of C,[:D,D9:];

coherence

<:T,T9:> is Functor of C,[:D,D9:]

proof end;

theorem :: CAT_2:47

for C, D, D9 being Category

for T being Functor of C,D

for T9 being Functor of C,D9

for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]

for T being Functor of C,D

for T9 being Functor of C,D9

for c being Object of C holds (Obj <:T,T9:>) . c = [((Obj T) . c),((Obj T9) . c)]

proof end;

theorem Th48: :: CAT_2:48

for C, D, C9, D9 being Category

for T being Functor of C,D

for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>

for T being Functor of C,D

for T9 being Functor of C9,D9 holds [:T,T9:] = <:(T * (pr1 (C,C9))),(T9 * (pr2 (C,C9))):>

proof end;

definition

let C, C9, D, D9 be Category;

let T be Functor of C,D;

let T9 be Functor of C9,D9;

:: original: [:

redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:];

coherence

[:T,T9:] is Functor of [:C,C9:],[:D,D9:]

end;
let T be Functor of C,D;

let T9 be Functor of C9,D9;

:: original: [:

redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:];

coherence

[:T,T9:] is Functor of [:C,C9:],[:D,D9:]

proof end;

theorem :: CAT_2:50

for C, D, C9, D9 being Category

for T being Functor of C,D

for T9 being Functor of C9,D9

for c being Object of C

for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]

for T being Functor of C,D

for T9 being Functor of C9,D9

for c being Object of C

for c9 being Object of C9 holds (Obj [:T,T9:]) . (c,c9) = [((Obj T) . c),((Obj T9) . c9)]

proof end;