:: by Grzegorz Bancerek

::

:: Received October 24, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

theorem Th1: :: CAT_5:1

for C being Category

for D being non empty non void CatStr st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds

( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities )

for D being non empty non void CatStr st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds

( D is Category-like & D is transitive & D is associative & D is reflexive & D is with_identities )

proof end;

Lm1: for C, D being Category st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) holds

for c being Element of C

for d being Element of D st c = d holds

id c = id d

proof end;

:: deftheorem Def1 defines with_triple-like_morphisms CAT_5:def 1 :

for IT being non empty non void CatStr holds

( IT is with_triple-like_morphisms iff for f being Morphism of IT ex x being set st f = [[(dom f),(cod f)],x] );

for IT being non empty non void CatStr holds

( IT is with_triple-like_morphisms iff for f being Morphism of IT ex x being set st f = [[(dom f),(cod f)],x] );

registration

ex b_{1} being strict Category st b_{1} is with_triple-like_morphisms
end;

cluster non empty non void V63() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms for CatStr ;

existence ex b

proof end;

theorem Th2: :: CAT_5:2

for C being non empty non void with_triple-like_morphisms CatStr

for f being Morphism of C holds

( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] )

for f being Morphism of C holds

( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] )

proof end;

definition

let C be non empty non void with_triple-like_morphisms CatStr ;

let f be Morphism of C;

:: original: `11

redefine func f `11 -> Object of C;

coherence

f `11 is Object of C

redefine func f `12 -> Object of C;

coherence

f `12 is Object of C

end;
let f be Morphism of C;

:: original: `11

redefine func f `11 -> Object of C;

coherence

f `11 is Object of C

proof end;

:: original: `12redefine func f `12 -> Object of C;

coherence

f `12 is Object of C

proof end;

scheme :: CAT_5:sch 1

CatEx{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set , set ], F_{3}( object , object ) -> set } :

CatEx{ F

ex C being strict with_triple-like_morphisms Category st

( the carrier of C = F_{1}() & ( for a, b being Element of F_{1}()

for f being Element of F_{2}() st P_{1}[a,b,f] holds

[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F_{1}() ex f being Element of F_{2}() st

( m = [[a,b],f] & P_{1}[a,b,f] ) ) & ( for m1, m2 being Morphism of C

for a1, a2, a3 being Element of F_{1}()

for f1, f2 being Element of F_{2}() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],F_{3}(f2,f1)] ) )

provided( the carrier of C = F

for f being Element of F

[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F

( m = [[a,b],f] & P

for a1, a2, a3 being Element of F

for f1, f2 being Element of F

m2 (*) m1 = [[a1,a3],F

A1:
for a, b, c being Element of F_{1}()

for f, g being Element of F_{2}() st P_{1}[a,b,f] & P_{1}[b,c,g] holds

( F_{3}(g,f) in F_{2}() & P_{1}[a,c,F_{3}(g,f)] )
and

A2: for a being Element of F_{1}() ex f being Element of F_{2}() st

( P_{1}[a,a,f] & ( for b being Element of F_{1}()

for g being Element of F_{2}() holds

( ( P_{1}[a,b,g] implies F_{3}(g,f) = g ) & ( P_{1}[b,a,g] implies F_{3}(f,g) = g ) ) ) )
and

A3: for a, b, c, d being Element of F_{1}()

for f, g, h being Element of F_{2}() st P_{1}[a,b,f] & P_{1}[b,c,g] & P_{1}[c,d,h] holds

F_{3}(h,F_{3}(g,f)) = F_{3}(F_{3}(h,g),f)

for f, g being Element of F

( F

A2: for a being Element of F

( P

for g being Element of F

( ( P

A3: for a, b, c, d being Element of F

for f, g, h being Element of F

F

proof end;

scheme :: CAT_5:sch 2

CatUniq{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ set , set , set ], F_{3}( set , set ) -> set } :

CatUniq{ F

for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = F_{1}() & ( for a, b being Element of F_{1}()

for f being Element of F_{2}() st P_{1}[a,b,f] holds

[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F_{1}() ex f being Element of F_{2}() st

( m = [[a,b],f] & P_{1}[a,b,f] ) ) & ( for m1, m2 being Morphism of C1

for a1, a2, a3 being Element of F_{1}()

for f1, f2 being Element of F_{2}() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],F_{3}(f2,f1)] ) & the carrier of C2 = F_{1}() & ( for a, b being Element of F_{1}()

for f being Element of F_{2}() st P_{1}[a,b,f] holds

[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F_{1}() ex f being Element of F_{2}() st

( m = [[a,b],f] & P_{1}[a,b,f] ) ) & ( for m1, m2 being Morphism of C2

for a1, a2, a3 being Element of F_{1}()

for f1, f2 being Element of F_{2}() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],F_{3}(f2,f1)] ) holds

C1 = C2

providedfor f being Element of F

[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F

( m = [[a,b],f] & P

for a1, a2, a3 being Element of F

for f1, f2 being Element of F

m2 (*) m1 = [[a1,a3],F

for f being Element of F

[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F

( m = [[a,b],f] & P

for a1, a2, a3 being Element of F

for f1, f2 being Element of F

m2 (*) m1 = [[a1,a3],F

C1 = C2

for a being Element of F_{1}() ex f being Element of F_{2}() st

( P_{1}[a,a,f] & ( for b being Element of F_{1}()

for g being Element of F_{2}() holds

( ( P_{1}[a,b,g] implies F_{3}(g,f) = g ) & ( P_{1}[b,a,g] implies F_{3}(f,g) = g ) ) ) )

( P

for g being Element of F

( ( P

proof end;

scheme :: CAT_5:sch 3

FunctorEx{ F_{1}() -> Category, F_{2}() -> Category, F_{3}( set ) -> Object of F_{2}(), F_{4}( object ) -> object } :

provided

FunctorEx{ F

provided

A1:
for f being Morphism of F_{1}() holds

( F_{4}(f) is Morphism of F_{2}() & ( for g being Morphism of F_{2}() st g = F_{4}(f) holds

( dom g = F_{3}((dom f)) & cod g = F_{3}((cod f)) ) ) )
and

A2: for a being Object of F_{1}() holds F_{4}((id a)) = id F_{3}(a)
and

A3: for f1, f2 being Morphism of F_{1}()

for g1, g2 being Morphism of F_{2}() st g1 = F_{4}(f1) & g2 = F_{4}(f2) & dom f2 = cod f1 holds

F_{4}((f2 (*) f1)) = g2 (*) g1

( F

( dom g = F

A2: for a being Object of F

A3: for f1, f2 being Morphism of F

for g1, g2 being Morphism of F

F

proof end;

theorem Th3: :: CAT_5:3

for C1 being Category

for C2 being Subcategory of C1 st C1 is Subcategory of C2 holds

CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)

for C2 being Subcategory of C1 st C1 is Subcategory of C2 holds

CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)

proof end;

theorem Th4: :: CAT_5:4

for C being Category

for D being Subcategory of C

for E being Subcategory of D holds E is Subcategory of C

for D being Subcategory of C

for E being Subcategory of D holds E is Subcategory of C

proof end;

definition

let C1, C2 be Category;

given C being Category such that A1: C1 is Subcategory of C and

A2: C2 is Subcategory of C ;

given o1 being Object of C1 such that A3: o1 is Object of C2 ;

ex b_{1} being strict Category st

( the carrier of b_{1} = the carrier of C1 /\ the carrier of C2 & the carrier' of b_{1} = the carrier' of C1 /\ the carrier' of C2 & the Source of b_{1} = the Source of C1 | the carrier' of C2 & the Target of b_{1} = the Target of C1 | the carrier' of C2 & the Comp of b_{1} = the Comp of C1 || the carrier' of C2 )

for b_{1}, b_{2} being strict Category st the carrier of b_{1} = the carrier of C1 /\ the carrier of C2 & the carrier' of b_{1} = the carrier' of C1 /\ the carrier' of C2 & the Source of b_{1} = the Source of C1 | the carrier' of C2 & the Target of b_{1} = the Target of C1 | the carrier' of C2 & the Comp of b_{1} = the Comp of C1 || the carrier' of C2 & the carrier of b_{2} = the carrier of C1 /\ the carrier of C2 & the carrier' of b_{2} = the carrier' of C1 /\ the carrier' of C2 & the Source of b_{2} = the Source of C1 | the carrier' of C2 & the Target of b_{2} = the Target of C1 | the carrier' of C2 & the Comp of b_{2} = the Comp of C1 || the carrier' of C2 holds

b_{1} = b_{2}
;

end;
given C being Category such that A1: C1 is Subcategory of C and

A2: C2 is Subcategory of C ;

given o1 being Object of C1 such that A3: o1 is Object of C2 ;

func C1 /\ C2 -> strict Category means :Def2: :: CAT_5:def 2

( the carrier of it = the carrier of C1 /\ the carrier of C2 & the carrier' of it = the carrier' of C1 /\ the carrier' of C2 & the Source of it = the Source of C1 | the carrier' of C2 & the Target of it = the Target of C1 | the carrier' of C2 & the Comp of it = the Comp of C1 || the carrier' of C2 );

existence ( the carrier of it = the carrier of C1 /\ the carrier of C2 & the carrier' of it = the carrier' of C1 /\ the carrier' of C2 & the Source of it = the Source of C1 | the carrier' of C2 & the Target of it = the Target of C1 | the carrier' of C2 & the Comp of it = the Comp of C1 || the carrier' of C2 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines /\ CAT_5:def 2 :

for C1, C2 being Category st ex C being Category st

( C1 is Subcategory of C & C2 is Subcategory of C ) & ex o1 being Object of C1 st o1 is Object of C2 holds

for b_{3} being strict Category holds

( b_{3} = C1 /\ C2 iff ( the carrier of b_{3} = the carrier of C1 /\ the carrier of C2 & the carrier' of b_{3} = the carrier' of C1 /\ the carrier' of C2 & the Source of b_{3} = the Source of C1 | the carrier' of C2 & the Target of b_{3} = the Target of C1 | the carrier' of C2 & the Comp of b_{3} = the Comp of C1 || the carrier' of C2 ) );

for C1, C2 being Category st ex C being Category st

( C1 is Subcategory of C & C2 is Subcategory of C ) & ex o1 being Object of C1 st o1 is Object of C2 holds

for b

( b

theorem Th5: :: CAT_5:5

for C being Category

for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds

C1 /\ C2 = C2 /\ C1

for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds

C1 /\ C2 = C2 /\ C1

proof end;

theorem Th6: :: CAT_5:6

for C being Category

for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds

( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )

for C1, C2 being Subcategory of C st the carrier of C1 meets the carrier of C2 holds

( C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2 )

proof end;

definition

let C, D be Category;

let F be Functor of C,D;

ex b_{1} being strict Subcategory of D st

( the carrier of b_{1} = rng (Obj F) & rng F c= the carrier' of b_{1} & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds

b_{1} is Subcategory of E ) )

for b_{1}, b_{2} being strict Subcategory of D st the carrier of b_{1} = rng (Obj F) & rng F c= the carrier' of b_{1} & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds

b_{1} is Subcategory of E ) & the carrier of b_{2} = rng (Obj F) & rng F c= the carrier' of b_{2} & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds

b_{2} is Subcategory of E ) holds

b_{1} = b_{2}

end;
let F be Functor of C,D;

func Image F -> strict Subcategory of D means :Def3: :: CAT_5:def 3

( the carrier of it = rng (Obj F) & rng F c= the carrier' of it & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds

it is Subcategory of E ) );

existence ( the carrier of it = rng (Obj F) & rng F c= the carrier' of it & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds

it is Subcategory of E ) );

ex b

( the carrier of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines Image CAT_5:def 3 :

for C, D being Category

for F being Functor of C,D

for b_{4} being strict Subcategory of D holds

( b_{4} = Image F iff ( the carrier of b_{4} = rng (Obj F) & rng F c= the carrier' of b_{4} & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds

b_{4} is Subcategory of E ) ) );

for C, D being Category

for F being Functor of C,D

for b

( b

b

theorem Th7: :: CAT_5:7

for C, D being Category

for E being Subcategory of D

for F being Functor of C,D st rng F c= the carrier' of E holds

F is Functor of C,E

for E being Subcategory of D

for F being Functor of C,D st rng F c= the carrier' of E holds

F is Functor of C,E

proof end;

theorem Th9: :: CAT_5:9

for C, D being Category

for E being Subcategory of D

for F being Functor of C,E

for G being Functor of C,D st F = G holds

Image F = Image G

for E being Subcategory of D

for F being Functor of C,E

for G being Functor of C,D st F = G holds

Image F = Image G

proof end;

:: deftheorem Def4 defines categorial CAT_5:def 4 :

for IT being set holds

( IT is categorial iff for x being set st x in IT holds

x is Category );

for IT being set holds

( IT is categorial iff for x being set st x in IT holds

x is Category );

definition

let X be non empty set ;

compatibility

( X is categorial iff for x being Element of X holds x is Category ) ;

end;
compatibility

( X is categorial iff for x being Element of X holds x is Category ) ;

:: deftheorem defines categorial CAT_5:def 5 :

for X being non empty set holds

( X is categorial iff for x being Element of X holds x is Category );

for X being non empty set holds

( X is categorial iff for x being Element of X holds x is Category );

definition

let X be non empty categorial set ;

:: original: Element

redefine mode Element of X -> Category;

coherence

for b_{1} being Element of X holds b_{1} is Category
by Def4;

end;
:: original: Element

redefine mode Element of X -> Category;

coherence

for b

definition

let C be Category;

end;
attr C is Categorial means :Def6: :: CAT_5:def 6

( the carrier of C is categorial & ( for a being Object of C

for A being Category st a = A holds

id a = [[A,A],(id A)] ) & ( for m being Morphism of C

for A, B being Category st A = dom m & B = cod m holds

ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C

for A, B, C being Category

for F being Functor of A,B

for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds

m2 (*) m1 = [[A,C],(G * F)] ) );

( the carrier of C is categorial & ( for a being Object of C

for A being Category st a = A holds

id a = [[A,A],(id A)] ) & ( for m being Morphism of C

for A, B being Category st A = dom m & B = cod m holds

ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C

for A, B, C being Category

for F being Functor of A,B

for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds

m2 (*) m1 = [[A,C],(G * F)] ) );

:: deftheorem Def6 defines Categorial CAT_5:def 6 :

for C being Category holds

( C is Categorial iff ( the carrier of C is categorial & ( for a being Object of C

for A being Category st a = A holds

id a = [[A,A],(id A)] ) & ( for m being Morphism of C

for A, B being Category st A = dom m & B = cod m holds

ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C

for A, B, C being Category

for F being Functor of A,B

for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds

m2 (*) m1 = [[A,C],(G * F)] ) ) );

for C being Category holds

( C is Categorial iff ( the carrier of C is categorial & ( for a being Object of C

for A being Category st a = A holds

id a = [[A,A],(id A)] ) & ( for m being Morphism of C

for A, B being Category st A = dom m & B = cod m holds

ex F being Functor of A,B st m = [[A,B],F] ) & ( for m1, m2 being Morphism of C

for A, B, C being Category

for F being Functor of A,B

for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G] holds

m2 (*) m1 = [[A,C],(G * F)] ) ) );

registration

for b_{1} being Category st b_{1} is Categorial holds

b_{1} is with_triple-like_morphisms
end;

cluster non empty non void Category-like transitive associative reflexive with_identities Categorial -> with_triple-like_morphisms for CatStr ;

coherence for b

b

proof end;

theorem Th10: :: CAT_5:10

for C, D being Category st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) & C is Categorial holds

D is Categorial

D is Categorial

proof end;

registration

ex b_{1} being strict Category st b_{1} is Categorial
end;

cluster non empty non void V63() strict Category-like transitive associative reflexive with_identities Categorial for CatStr ;

existence ex b

proof end;

definition

let C be Categorial Category;

let m be Morphism of C;

:: original: `11

redefine func m `11 -> Category;

coherence

m `11 is Category

redefine func m `12 -> Category;

coherence

m `12 is Category

end;
let m be Morphism of C;

:: original: `11

redefine func m `11 -> Category;

coherence

m `11 is Category

proof end;

:: original: `12redefine func m `12 -> Category;

coherence

m `12 is Category

proof end;

theorem Th14: :: CAT_5:14

for C1, C2 being Categorial Category st the carrier of C1 = the carrier of C2 & the carrier' of C1 = the carrier' of C2 holds

CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)

CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)

proof end;

registration

let C be Categorial Category;

coherence

for b_{1} being Subcategory of C holds b_{1} is Categorial

end;
coherence

for b

proof end;

theorem Th15: :: CAT_5:15

for C, D being Categorial Category st the carrier' of C c= the carrier' of D holds

C is Subcategory of D

C is Subcategory of D

proof end;

definition
end;

definition

let C be Categorial Category;

let m be Morphism of C;

:: original: `2

redefine func m `2 -> Functor of cat (dom m), cat (cod m);

coherence

m `2 is Functor of cat (dom m), cat (cod m)

end;
let m be Morphism of C;

:: original: `2

redefine func m `2 -> Functor of cat (dom m), cat (cod m);

coherence

m `2 is Functor of cat (dom m), cat (cod m)

proof end;

theorem Th17: :: CAT_5:17

for X being non empty categorial set

for Y being non empty set st ( for A, B, C being Element of X

for F being Functor of A,B

for G being Functor of B,C st F in Y & G in Y holds

G * F in Y ) & ( for A being Element of X holds id A in Y ) holds

ex C being strict Categorial Category st

( the carrier of C = X & ( for A, B being Element of X

for F being Functor of A,B holds

( [[A,B],F] is Morphism of C iff F in Y ) ) )

for Y being non empty set st ( for A, B, C being Element of X

for F being Functor of A,B

for G being Functor of B,C st F in Y & G in Y holds

G * F in Y ) & ( for A being Element of X holds id A in Y ) holds

ex C being strict Categorial Category st

( the carrier of C = X & ( for A, B being Element of X

for F being Functor of A,B holds

( [[A,B],F] is Morphism of C iff F in Y ) ) )

proof end;

theorem Th18: :: CAT_5:18

for X being non empty categorial set

for Y being non empty set

for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X

for F being Functor of A,B holds

( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X

for F being Functor of A,B holds

( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds

C1 = C2

for Y being non empty set

for C1, C2 being strict Categorial Category st the carrier of C1 = X & ( for A, B being Element of X

for F being Functor of A,B holds

( [[A,B],F] is Morphism of C1 iff F in Y ) ) & the carrier of C2 = X & ( for A, B being Element of X

for F being Functor of A,B holds

( [[A,B],F] is Morphism of C2 iff F in Y ) ) holds

C1 = C2

proof end;

:: deftheorem Def8 defines full CAT_5:def 8 :

for IT being Categorial Category holds

( IT is full iff for a, b being Category st a is Object of IT & b is Object of IT holds

for F being Functor of a,b holds [[a,b],F] is Morphism of IT );

for IT being Categorial Category holds

( IT is full iff for a, b being Category st a is Object of IT & b is Object of IT holds

for F being Functor of a,b holds [[a,b],F] is Morphism of IT );

registration

ex b_{1} being strict Categorial Category st b_{1} is full
end;

cluster non empty non void V63() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms Categorial full for CatStr ;

existence ex b

proof end;

theorem :: CAT_5:19

for C1, C2 being Categorial full Category st the carrier of C1 = the carrier of C2 holds

CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)

CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)

proof end;

theorem Th20: :: CAT_5:20

for A being non empty categorial set ex C being strict Categorial full Category st the carrier of C = A

proof end;

theorem Th21: :: CAT_5:21

for C being Categorial Category

for D being Categorial full Category st the carrier of C c= the carrier of D holds

C is Subcategory of D

for D being Categorial full Category st the carrier of C c= the carrier of D holds

C is Subcategory of D

proof end;

theorem :: CAT_5:22

for C being Category

for D1, D2 being Categorial Category

for F1 being Functor of C,D1

for F2 being Functor of C,D2 st F1 = F2 holds

Image F1 = Image F2

for D1, D2 being Categorial Category

for F1 being Functor of C,D1

for F2 being Functor of C,D2 st F1 = F2 holds

Image F1 = Image F2

proof end;

definition

let C be Category;

let o be Object of C;

coherence

the Target of C " {o} is Subset of the carrier' of C ;

coherence

the Source of C " {o} is Subset of the carrier' of C ;

end;
let o be Object of C;

coherence

the Target of C " {o} is Subset of the carrier' of C ;

coherence

the Source of C " {o} is Subset of the carrier' of C ;

:: deftheorem defines Hom CAT_5:def 9 :

for C being Category

for o being Object of C holds Hom o = the Target of C " {o};

for C being Category

for o being Object of C holds Hom o = the Target of C " {o};

:: deftheorem defines Hom CAT_5:def 10 :

for C being Category

for o being Object of C holds o Hom = the Source of C " {o};

for C being Category

for o being Object of C holds o Hom = the Source of C " {o};

registration

let C be Category;

let o be Object of C;

coherence

not Hom o is empty

not o Hom is empty

end;
let o be Object of C;

coherence

not Hom o is empty

proof end;

coherence not o Hom is empty

proof end;

theorem Th23: :: CAT_5:23

for C being Category

for a being Object of C

for f being Morphism of C holds

( f in Hom a iff cod f = a )

for a being Object of C

for f being Morphism of C holds

( f in Hom a iff cod f = a )

proof end;

theorem Th24: :: CAT_5:24

for C being Category

for a being Object of C

for f being Morphism of C holds

( f in a Hom iff dom f = a )

for a being Object of C

for f being Morphism of C holds

( f in a Hom iff dom f = a )

proof end;

theorem :: CAT_5:26

theorem Th27: :: CAT_5:27

for C being Category

for f being Morphism of C

for g being Element of Hom (dom f) holds f (*) g in Hom (cod f)

for f being Morphism of C

for g being Element of Hom (dom f) holds f (*) g in Hom (cod f)

proof end;

theorem Th28: :: CAT_5:28

for C being Category

for f being Morphism of C

for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom

for f being Morphism of C

for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom

proof end;

definition

let C be Category;

let o be Object of C;

set A = Hom o;

set B = the carrier' of C;

defpred S_{1}[ Element of Hom o, Element of Hom o, Element of the carrier' of C] means ( dom $2 = cod $3 & $1 = $2 (*) $3 );

deffunc H_{1}( Morphism of C, Morphism of C) -> Element of the carrier' of C = $1 (*) $2;

A1: for a, b, c being Element of Hom o

for f, g being Element of the carrier' of C st S_{1}[a,b,f] & S_{1}[b,c,g] holds

( H_{1}(g,f) in the carrier' of C & S_{1}[a,c,H_{1}(g,f)] )

( S_{1}[a,a,f] & ( for b being Element of Hom o

for g being Element of the carrier' of C holds

( ( S_{1}[a,b,g] implies H_{1}(g,f) = g ) & ( S_{1}[b,a,g] implies H_{1}(f,g) = g ) ) ) )

for f, g, h being Element of the carrier' of C st S_{1}[a,b,f] & S_{1}[b,c,g] & S_{1}[c,d,h] holds

H_{1}(h,H_{1}(g,f)) = H_{1}(H_{1}(h,g),f)

ex b_{1} being strict with_triple-like_morphisms Category st

( the carrier of b_{1} = Hom o & ( for a, b being Element of Hom o

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b_{1} ) & ( for m being Morphism of b_{1} ex a, b being Element of Hom o ex f being Morphism of C st

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b_{1}

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) )

for b_{1}, b_{2} being strict with_triple-like_morphisms Category st the carrier of b_{1} = Hom o & ( for a, b being Element of Hom o

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b_{1} ) & ( for m being Morphism of b_{1} ex a, b being Element of Hom o ex f being Morphism of C st

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b_{1}

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) & the carrier of b_{2} = Hom o & ( for a, b being Element of Hom o

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b_{2} ) & ( for m being Morphism of b_{2} ex a, b being Element of Hom o ex f being Morphism of C st

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b_{2}

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) holds

b_{1} = b_{2}

defpred S_{2}[ Element of o Hom , Element of o Hom , Element of the carrier' of C] means ( dom $3 = cod $1 & $2 = $3 (*) $1 );

A16: for a, b, c being Element of o Hom

for f, g being Element of the carrier' of C st S_{2}[a,b,f] & S_{2}[b,c,g] holds

( H_{1}(g,f) in the carrier' of C & S_{2}[a,c,H_{1}(g,f)] )

( S_{2}[a,a,f] & ( for b being Element of o Hom

for g being Element of the carrier' of C holds

( ( S_{2}[a,b,g] implies H_{1}(g,f) = g ) & ( S_{2}[b,a,g] implies H_{1}(f,g) = g ) ) ) )

for f, g, h being Element of the carrier' of C st S_{2}[a,b,f] & S_{2}[b,c,g] & S_{2}[c,d,h] holds

H_{1}(h,H_{1}(g,f)) = H_{1}(H_{1}(h,g),f)

ex b_{1} being strict with_triple-like_morphisms Category st

( the carrier of b_{1} = o Hom & ( for a, b being Element of o Hom

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b_{1} ) & ( for m being Morphism of b_{1} ex a, b being Element of o Hom ex f being Morphism of C st

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b_{1}

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) )

for b_{1}, b_{2} being strict with_triple-like_morphisms Category st the carrier of b_{1} = o Hom & ( for a, b being Element of o Hom

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b_{1} ) & ( for m being Morphism of b_{1} ex a, b being Element of o Hom ex f being Morphism of C st

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b_{1}

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) & the carrier of b_{2} = o Hom & ( for a, b being Element of o Hom

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b_{2} ) & ( for m being Morphism of b_{2} ex a, b being Element of o Hom ex f being Morphism of C st

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b_{2}

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) holds

b_{1} = b_{2}

end;
let o be Object of C;

set A = Hom o;

set B = the carrier' of C;

defpred S

deffunc H

A1: for a, b, c being Element of Hom o

for f, g being Element of the carrier' of C st S

( H

proof end;

A6:
for a being Element of Hom o ex f being Element of the carrier' of C st ( S

for g being Element of the carrier' of C holds

( ( S

proof end;

A9:
for a, b, c, d being Element of Hom ofor f, g, h being Element of the carrier' of C st S

H

proof end;

func C -SliceCat o -> strict with_triple-like_morphisms Category means :Def11: :: CAT_5:def 11

( the carrier of it = Hom o & ( for a, b being Element of Hom o

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of Hom o ex f being Morphism of C st

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of it

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) );

existence ( the carrier of it = Hom o & ( for a, b being Element of Hom o

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of Hom o ex f being Morphism of C st

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of it

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) );

ex b

( the carrier of b

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) )

proof end;

uniqueness for b

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) & the carrier of b

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) holds

b

proof end;

set X = o Hom ;defpred S

A16: for a, b, c being Element of o Hom

for f, g being Element of the carrier' of C st S

( H

proof end;

A21:
for a being Element of o Hom ex f being Element of the carrier' of C st ( S

for g being Element of the carrier' of C holds

( ( S

proof end;

A24:
for a, b, c, d being Element of o Hom for f, g, h being Element of the carrier' of C st S

H

proof end;

func o -SliceCat C -> strict with_triple-like_morphisms Category means :Def12: :: CAT_5:def 12

( the carrier of it = o Hom & ( for a, b being Element of o Hom

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of o Hom ex f being Morphism of C st

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of it

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) );

existence ( the carrier of it = o Hom & ( for a, b being Element of o Hom

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of it ) & ( for m being Morphism of it ex a, b being Element of o Hom ex f being Morphism of C st

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of it

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) );

ex b

( the carrier of b

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) )

proof end;

uniqueness for b

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) & the carrier of b

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) holds

b

proof end;

:: deftheorem Def11 defines -SliceCat CAT_5:def 11 :

for C being Category

for o being Object of C

for b_{3} being strict with_triple-like_morphisms Category holds

( b_{3} = C -SliceCat o iff ( the carrier of b_{3} = Hom o & ( for a, b being Element of Hom o

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b_{3} ) & ( for m being Morphism of b_{3} ex a, b being Element of Hom o ex f being Morphism of C st

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b_{3}

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) );

for C being Category

for o being Object of C

for b

( b

for f being Morphism of C st dom b = cod f & a = b (*) f holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom b = cod f & a = b (*) f ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of Hom o

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) );

:: deftheorem Def12 defines -SliceCat CAT_5:def 12 :

for C being Category

for o being Object of C

for b_{3} being strict with_triple-like_morphisms Category holds

( b_{3} = o -SliceCat C iff ( the carrier of b_{3} = o Hom & ( for a, b being Element of o Hom

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b_{3} ) & ( for m being Morphism of b_{3} ex a, b being Element of o Hom ex f being Morphism of C st

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b_{3}

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) );

for C being Category

for o being Object of C

for b

( b

for f being Morphism of C st dom f = cod a & f (*) a = b holds

[[a,b],f] is Morphism of b

( m = [[a,b],f] & dom f = cod a & f (*) a = b ) ) & ( for m1, m2 being Morphism of b

for a1, a2, a3 being Element of o Hom

for f1, f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds

m2 (*) m1 = [[a1,a3],(f2 (*) f1)] ) ) );

definition

let C be Category;

let o be Object of C;

let m be Morphism of (C -SliceCat o);

:: original: `2

redefine func m `2 -> Morphism of C;

coherence

m `2 is Morphism of C

redefine func m `11 -> Element of Hom o;

coherence

m `11 is Element of Hom o

redefine func m `12 -> Element of Hom o;

coherence

m `12 is Element of Hom o

end;
let o be Object of C;

let m be Morphism of (C -SliceCat o);

:: original: `2

redefine func m `2 -> Morphism of C;

coherence

m `2 is Morphism of C

proof end;

:: original: `11redefine func m `11 -> Element of Hom o;

coherence

m `11 is Element of Hom o

proof end;

:: original: `12redefine func m `12 -> Element of Hom o;

coherence

m `12 is Element of Hom o

proof end;

theorem Th29: :: CAT_5:29

for C being Category

for a being Object of C

for m being Morphism of (C -SliceCat a) holds

( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 )

for a being Object of C

for m being Morphism of (C -SliceCat a) holds

( m = [[(m `11),(m `12)],(m `2)] & dom (m `12) = cod (m `2) & m `11 = (m `12) (*) (m `2) & dom m = m `11 & cod m = m `12 )

proof end;

theorem Th30: :: CAT_5:30

for C being Category

for o being Object of C

for f being Element of Hom o

for a being Object of (C -SliceCat o) st a = f holds

id a = [[a,a],(id (dom f))]

for o being Object of C

for f being Element of Hom o

for a being Object of (C -SliceCat o) st a = f holds

id a = [[a,a],(id (dom f))]

proof end;

definition

let C be Category;

let o be Object of C;

let m be Morphism of (o -SliceCat C);

:: original: `2

redefine func m `2 -> Morphism of C;

coherence

m `2 is Morphism of C

redefine func m `11 -> Element of o Hom ;

coherence

m `11 is Element of o Hom

redefine func m `12 -> Element of o Hom ;

coherence

m `12 is Element of o Hom

end;
let o be Object of C;

let m be Morphism of (o -SliceCat C);

:: original: `2

redefine func m `2 -> Morphism of C;

coherence

m `2 is Morphism of C

proof end;

:: original: `11redefine func m `11 -> Element of o Hom ;

coherence

m `11 is Element of o Hom

proof end;

:: original: `12redefine func m `12 -> Element of o Hom ;

coherence

m `12 is Element of o Hom

proof end;

theorem Th31: :: CAT_5:31

for C being Category

for a being Object of C

for m being Morphism of (a -SliceCat C) holds

( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 )

for a being Object of C

for m being Morphism of (a -SliceCat C) holds

( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 )

proof end;

theorem Th32: :: CAT_5:32

for C being Category

for o being Object of C

for f being Element of o Hom

for a being Object of (o -SliceCat C) st a = f holds

id a = [[a,a],(id (cod f))]

for o being Object of C

for f being Element of o Hom

for a being Object of (o -SliceCat C) st a = f holds

id a = [[a,a],(id (cod f))]

proof end;

definition

let C be Category;

let f be Morphism of C;

ex b_{1} being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st

for m being Morphism of (C -SliceCat (dom f)) holds b_{1} . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)]

for b_{1}, b_{2} being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st ( for m being Morphism of (C -SliceCat (dom f)) holds b_{1} . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) & ( for m being Morphism of (C -SliceCat (dom f)) holds b_{2} . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) holds

b_{1} = b_{2}

ex b_{1} being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st

for m being Morphism of ((cod f) -SliceCat C) holds b_{1} . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)]

for b_{1}, b_{2} being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st ( for m being Morphism of ((cod f) -SliceCat C) holds b_{1} . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) & ( for m being Morphism of ((cod f) -SliceCat C) holds b_{2} . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) holds

b_{1} = b_{2}

end;
let f be Morphism of C;

func SliceFunctor f -> Functor of C -SliceCat (dom f),C -SliceCat (cod f) means :Def13: :: CAT_5:def 13

for m being Morphism of (C -SliceCat (dom f)) holds it . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)];

existence for m being Morphism of (C -SliceCat (dom f)) holds it . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)];

ex b

for m being Morphism of (C -SliceCat (dom f)) holds b

proof end;

uniqueness for b

b

proof end;

func SliceContraFunctor f -> Functor of (cod f) -SliceCat C,(dom f) -SliceCat C means :Def14: :: CAT_5:def 14

for m being Morphism of ((cod f) -SliceCat C) holds it . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)];

existence for m being Morphism of ((cod f) -SliceCat C) holds it . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)];

ex b

for m being Morphism of ((cod f) -SliceCat C) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines SliceFunctor CAT_5:def 13 :

for C being Category

for f being Morphism of C

for b_{3} being Functor of C -SliceCat (dom f),C -SliceCat (cod f) holds

( b_{3} = SliceFunctor f iff for m being Morphism of (C -SliceCat (dom f)) holds b_{3} . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] );

for C being Category

for f being Morphism of C

for b

( b

:: deftheorem Def14 defines SliceContraFunctor CAT_5:def 14 :

for C being Category

for f being Morphism of C

for b_{3} being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C holds

( b_{3} = SliceContraFunctor f iff for m being Morphism of ((cod f) -SliceCat C) holds b_{3} . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] );

for C being Category

for f being Morphism of C

for b

( b

theorem :: CAT_5:33

for C being Category

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

SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f)

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

SliceFunctor (g (*) f) = (SliceFunctor g) * (SliceFunctor f)

proof end;

theorem :: CAT_5:34

for C being Category

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

SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g)

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

SliceContraFunctor (g (*) f) = (SliceContraFunctor f) * (SliceContraFunctor g)

proof end;