:: Categorial Categories and Slice Categories
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

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 )
proofend;

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

definition
let IT be non empty non void CatStr ;
attrIT is with_triple-like_morphisms  means :Def1: :: CAT_5:def 1
 for f being Morphism of IT ex x being set st f = [[(dom f),(cod f)],x];
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] );

registration
cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms for CatStr ;
existence
 ex b1 being strict Category st b1 is with_triple-like_morphisms
proofend;
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)] )
proofend;

definition
let C be non empty non void with_triple-like_morphisms CatStr ;
let f be Morphism of C;
:: original:`11
redefine funcf `11  ->  Object of C;
coherence
 f `11 is Object of C
proofend;
:: original:`12
redefine funcf `12  ->  Object of C;
coherence
 f `12 is Object of C
proofend;
end;

scheme :: CAT_5:sch 1
CatEx{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set , set ], F3( set , set ) ->  set } :
 ex C being strict with_triple-like_morphisms Category st
( the carrier of C = F1() & ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C ) & ( for m being Morphism of C ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) )
provided
A1: for a, b, c being Element of F1()
for f, g being Element of F2() st P1[a,b,f] & P1[b,c,g] holds
( F3(g,f) in F2() & P1[a,c,F3(g,f)] ) and
A2: for a being Element of F1() ex f being Element of F2() st
( P1[a,a,f] & ( for b being Element of F1()
for g being Element of F2() holds
( ( P1[a,b,g] implies F3(g,f) = g ) & ( P1[b,a,g] implies F3(f,g) = g ) ) ) ) and
A3: for a, b, c, d being Element of F1()
for f, g, h being Element of F2() st P1[a,b,f] & P1[b,c,g] & P1[c,d,h] holds
F3(h,F3(g,f)) = F3(F3(h,g),f)
proofend;

scheme :: CAT_5:sch 2
CatUniq{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set , set ], F3( set , set ) ->  set } :
 for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = F1() & ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C1
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) & the carrier of C2 = F1() & ( for a, b being Element of F1()
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of F1() ex f being Element of F2() st
( m = [[a,b],f] & P1[a,b,f] ) ) & ( for m1, m2 being Morphism of C2
for a1, a2, a3 being Element of F1()
for f1, f2 being Element of F2() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],F3(f2,f1)] ) holds
C1 = C2
provided
 for a being Element of F1() ex f being Element of F2() st
( P1[a,a,f] & ( for b being Element of F1()
for g being Element of F2() holds
( ( P1[a,b,g] implies F3(g,f) = g ) & ( P1[b,a,g] implies F3(f,g) = g ) ) ) )
proofend;

scheme :: CAT_5:sch 3
FunctorEx{ F1() ->  Category, F2() ->  Category, F3( set ) ->  Object of F2(), F4( set ) ->  set } :
 ex F being Functor of F1(),F2() st
for f being Morphism of F1() holds F . f = F4(f)
provided
A1: for f being Morphism of F1() holds
( F4(f) is Morphism of F2() & ( for g being Morphism of F2() st g = F4(f) holds
( dom g = F3((dom f)) & cod g = F3((cod f)) ) ) ) and
A2: for a being Object of F1() holds F4((id a)) = id F3(a) and
A3: for f1, f2 being Morphism of F1()
for g1, g2 being Morphism of F2() st g1 = F4(f1) & g2 = F4(f2) & dom f2 = cod f1 holds
F4((f2 (*) f1)) = g2 (*) g1
proofend;

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 #)
proofend;

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

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 ;
funcC1 /\ 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
 ex b1 being strict Category st
( the carrier of b1 = the carrier of C1 /\ the carrier of C2 & the carrier' of b1 = the carrier' of C1 /\ the carrier' of C2 & the Source of b1 = the Source of C1 | the carrier' of C2 & the Target of b1 = the Target of C1 | the carrier' of C2 & the Comp of b1 = the Comp of C1 || the carrier' of C2 )
proofend;
uniqueness
 for b1, b2 being strict Category st the carrier of b1 = the carrier of C1 /\ the carrier of C2 & the carrier' of b1 = the carrier' of C1 /\ the carrier' of C2 & the Source of b1 = the Source of C1 | the carrier' of C2 & the Target of b1 = the Target of C1 | the carrier' of C2 & the Comp of b1 = the Comp of C1 || the carrier' of C2 & the carrier of b2 = the carrier of C1 /\ the carrier of C2 & the carrier' of b2 = the carrier' of C1 /\ the carrier' of C2 & the Source of b2 = the Source of C1 | the carrier' of C2 & the Target of b2 = the Target of C1 | the carrier' of C2 & the Comp of b2 = the Comp of C1 || the carrier' of C2 holds
b1 = b2 ;
end;

:: 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 b3 being strict Category holds
( b3 = C1 /\ C2 iff ( the carrier of b3 = the carrier of C1 /\ the carrier of C2 & the carrier' of b3 = the carrier' of C1 /\ the carrier' of C2 & the Source of b3 = the Source of C1 | the carrier' of C2 & the Target of b3 = the Target of C1 | the carrier' of C2 & the Comp of b3 = the Comp of C1 || the carrier' of C2 ) );

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

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 )
proofend;

definition
let C, D be Category;
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
 ex b1 being strict Subcategory of D st
( the carrier of b1 = rng (Obj F) & rng F c= the carrier' of b1 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
b1 is Subcategory of E ) )
proofend;
uniqueness
 for b1, b2 being strict Subcategory of D st the carrier of b1 = rng (Obj F) & rng F c= the carrier' of b1 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
b1 is Subcategory of E ) & the carrier of b2 = rng (Obj F) & rng F c= the carrier' of b2 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
b2 is Subcategory of E ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Image CAT_5:def_3_:_
 for C, D being Category
for F being Functor of C,D
for b4 being strict Subcategory of D holds
( b4 = Image F iff ( the carrier of b4 = rng (Obj F) & rng F c= the carrier' of b4 & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
b4 is Subcategory of E ) ) );

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

theorem :: CAT_5:8
for C, D being Category
for F being Functor of C,D holds F is Functor of C, Image F
proofend;

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

begin

definition
let IT be set ;
attrIT is categorial  means :Def4: :: CAT_5:def 4
 for x being set st x in IT holds
x is Category;
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 );

definition
let X be non empty set ;
redefine attr X is categorial  means :Def5: :: CAT_5:def 5
 for x being Element of X holds x is Category;
compatibility
 ( X is categorial iff for x being Element of X holds x is Category )
proofend;
end;

:: deftheorem Def5 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 );

registration
cluster non empty categorial for set ;
existence
 ex b1 being non empty set st b1 is categorial
proofend;
end;

definition
let X be non empty categorial set ;
:: original:Element
redefine mode Element of X ->  Category;
coherence
 for b1 being Element of X holds b1 is Category by Def4;
end;

definition
let C be Category;
attrC 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)] ) );
end;

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

registration
cluster non empty non void Category-like transitive associative reflexive with_identities Categorial  ->  with_triple-like_morphisms for CatStr ;
coherence
 for b1 being Category st b1 is Categorial holds
b1 is with_triple-like_morphisms
proofend;
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
proofend;

theorem Th11: :: CAT_5:11
for C being Category holds 1Cat (C,[[C,C],(id C)]) is Categorial
proofend;

registration
cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities Categorial for CatStr ;
existence
 ex b1 being strict Category st b1 is Categorial
proofend;
end;

theorem Th12: :: CAT_5:12
for C being Categorial Category
for a being Object of C holds a is Category
proofend;

theorem Th13: :: CAT_5:13
for C being Categorial Category
for f being Morphism of C holds
( dom f = f `11 & cod f = f `12 )
proofend;

definition
let C be Categorial Category;
let m be Morphism of C;
:: original:`11
redefine funcm `11  ->  Category;
coherence
 m `11 is Category
proofend;
:: original:`12
redefine funcm `12  ->  Category;
coherence
 m `12 is Category
proofend;
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 #)
proofend;

registration
let C be Categorial Category;
cluster  ->  Categorial for Subcategory of C;
coherence
 for b1 being Subcategory of C holds b1 is Categorial
proofend;
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
proofend;

definition
let a be set ;
assume A1: a is Category ;
func cat a ->  Category equals :Def7: :: CAT_5:def 7
a;
correctness
coherence
a is Category;
by A1;
end;

:: deftheorem Def7 defines cat CAT_5:def_7_:_
 for a being set st a is Category holds
cat a = a;

theorem Th16: :: CAT_5:16
for C being Categorial Category
for c being Object of C holds cat c = c
proofend;

definition
let C be Categorial Category;
let m be Morphism of C;
:: original:`2
redefine funcm `2  ->  Functor of cat (dom m), cat (cod m);
coherence
 m `2 is Functor of cat (dom m), cat (cod m)
proofend;
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 ) ) )
proofend;

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

definition
let IT be Categorial Category;
attrIT is full  means :Def8: :: CAT_5:def 8
 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;
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 );

registration
cluster non empty non void V58() strict Category-like transitive associative reflexive with_identities with_triple-like_morphisms Categorial full for CatStr ;
existence
 ex b1 being strict Categorial Category st b1 is full
proofend;
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 #)
proofend;

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

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

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

begin

definition
let C be Category;
let o be Object of C;
func Hom o ->  Subset of the carrier' of C equals :: CAT_5:def 9
 the Target of C " {o};
coherence
 the Target of C " {o} is Subset of the carrier' of C ;
funco Hom  ->  Subset of the carrier' of C equals :: CAT_5:def 10
 the Source of C " {o};
coherence
 the Source of C " {o} is Subset of the carrier' of C ;
end;

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

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

registration
let C be Category;
let o be Object of C;
cluster Hom o ->  non empty ;
coherence
 not Hom o is empty
proofend;
clustero Hom  ->  non empty ;
coherence
 not o Hom is empty
proofend;
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 )
proofend;

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 )
proofend;

theorem :: CAT_5:25
for C being Category
for a, b being Object of C holds Hom (a,b) = (a Hom) /\ (Hom b)
proofend;

theorem :: CAT_5:26
for C being Category
for f being Morphism of C holds
( f in (dom f) Hom & f in Hom (cod f) ) by Th23, Th24;

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)
proofend;

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

definition
let C be Category;
let o be Object of C;
set A = Hom o;
set B = the carrier' of C;
defpred S1[ Element of Hom o, Element of Hom o, Element of the carrier' of C] means ( dom $2 = cod $3 & $1 = $2 (*) $3 );
deffunc H1( 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 S1[a,b,f] & S1[b,c,g] holds
( H1(g,f) in the carrier' of C & S1[a,c,H1(g,f)] )
proofend;
A6: for a being Element of Hom o ex f being Element of the carrier' of C st
( S1[a,a,f] & ( for b being Element of Hom o
for g being Element of the carrier' of C holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
proofend;
A9: for a, b, c, d being Element of Hom o
for f, g, h being Element of the carrier' of C st S1[a,b,f] & S1[b,c,g] & S1[c,d,h] holds
H1(h,H1(g,f)) = H1(H1(h,g),f)
proofend;
funcC -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
 ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = 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 b1 ) & ( for m being Morphism of b1 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 b1
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)] ) )
proofend;
uniqueness
 for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = 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 b1 ) & ( for m being Morphism of b1 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 b1
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 b2 = 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 b2 ) & ( for m being Morphism of b2 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 b2
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
b1 = b2
proofend;
set X = o Hom ;
defpred S2[ 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 S2[a,b,f] & S2[b,c,g] holds
( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] )
proofend;
A21: for a being Element of o Hom ex f being Element of the carrier' of C st
( S2[a,a,f] & ( for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) ) )
proofend;
A24: for a, b, c, d being Element of o Hom
for f, g, h being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] & S2[c,d,h] holds
H1(h,H1(g,f)) = H1(H1(h,g),f)
proofend;
funco -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
 ex b1 being strict with_triple-like_morphisms Category st
( the carrier of b1 = 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 b1 ) & ( for m being Morphism of b1 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 b1
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)] ) )
proofend;
uniqueness
 for b1, b2 being strict with_triple-like_morphisms Category st the carrier of b1 = 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 b1 ) & ( for m being Morphism of b1 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 b1
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 b2 = 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 b2 ) & ( for m being Morphism of b2 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 b2
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
b1 = b2
proofend;
end;

:: deftheorem Def11 defines -SliceCat CAT_5:def_11_:_
 for C being Category
for o being Object of C
for b3 being strict with_triple-like_morphisms Category holds
( b3 = C -SliceCat o iff ( the carrier of b3 = 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 b3 ) & ( for m being Morphism of b3 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 b3
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 b3 being strict with_triple-like_morphisms Category holds
( b3 = o -SliceCat C iff ( the carrier of b3 = 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 b3 ) & ( for m being Morphism of b3 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 b3
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 funcm `2  ->  Morphism of C;
coherence
 m `2 is Morphism of C
proofend;
:: original:`11
redefine funcm `11  ->  Element of Hom o;
coherence
 m `11 is Element of Hom o
proofend;
:: original:`12
redefine funcm `12  ->  Element of Hom o;
coherence
 m `12 is Element of Hom o
proofend;
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 )
proofend;

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))]
proofend;

definition
let C be Category;
let o be Object of C;
let m be Morphism of (o -SliceCat C);
:: original:`2
redefine funcm `2  ->  Morphism of C;
coherence
 m `2 is Morphism of C
proofend;
:: original:`11
redefine funcm `11  ->  Element of o Hom ;
coherence
 m `11 is Element of o Hom
proofend;
:: original:`12
redefine funcm `12  ->  Element of o Hom ;
coherence
 m `12 is Element of o Hom
proofend;
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 )
proofend;

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))]
proofend;

begin

definition
let C be Category;
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
 ex b1 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st
for m being Morphism of (C -SliceCat (dom f)) holds b1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)]
proofend;
uniqueness
 for b1, b2 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) st ( for m being Morphism of (C -SliceCat (dom f)) holds b1 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) & ( for m being Morphism of (C -SliceCat (dom f)) holds b2 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] ) holds
b1 = b2
proofend;
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
 ex b1 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st
for m being Morphism of ((cod f) -SliceCat C) holds b1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)]
proofend;
uniqueness
 for b1, b2 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C st ( for m being Morphism of ((cod f) -SliceCat C) holds b1 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) & ( for m being Morphism of ((cod f) -SliceCat C) holds b2 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines SliceFunctor CAT_5:def_13_:_
 for C being Category
for f being Morphism of C
for b3 being Functor of C -SliceCat (dom f),C -SliceCat (cod f) holds
( b3 = SliceFunctor f iff for m being Morphism of (C -SliceCat (dom f)) holds b3 . m = [[(f (*) (m `11)),(f (*) (m `12))],(m `2)] );

:: deftheorem Def14 defines SliceContraFunctor CAT_5:def_14_:_
 for C being Category
for f being Morphism of C
for b3 being Functor of (cod f) -SliceCat C,(dom f) -SliceCat C holds
( b3 = SliceContraFunctor f iff for m being Morphism of ((cod f) -SliceCat C) holds b3 . m = [[((m `11) (*) f),((m `12) (*) f)],(m `2)] );

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)
proofend;

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)
proofend;