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


begin

definition
let D1, D2, D be non empty set ;
let x be Element of [:[:D1,D2:],D:];
:: original: `11
redefine func x `11 -> Element of D1;
coherence
x `11 is Element of D1
proof end;
:: original: `12
redefine func x `12 -> Element of D2;
coherence
x `12 is Element of D2
proof end;
end;

definition
let D1, D2 be non empty set ;
let x be Element of [:D1,D2:];
:: original: `2
redefine func x `2 -> Element of D2;
coherence
x `2 is Element of D2
proof end;
end;

theorem Th1: :: CAT_5:1
for C, D being CatStr st CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C, the Id of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D, the Id of D #) & C is Category-like holds
D is Category-like
proof end;

definition
let IT be non empty non void CatStr ;
attr IT 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 strict Category-like with_triple-like_morphisms CatStr ;
existence
ex b1 being strict Category st b1 is with_triple-like_morphisms
proof end;
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)] )
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
proof end;
:: original: `12
redefine func f `12 -> Object of C;
coherence
f `12 is Object of C
proof end;
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)
proof end;

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
A1: 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 ) ) ) )
proof end;

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
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, the Id of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2, the Id 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
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 ;
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 & the Id of it = the Id 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 & the Id of b1 = the Id of C1 | the carrier of C2 )
proof end;
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 Id of b1 = the Id 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 & the Id of b2 = the Id 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 & the Id of b3 = the Id 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
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 )
proof end;

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

theorem :: CAT_5:8
for C, D being Category
for F being Functor of C,D holds F is Functor of C, Image F
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
proof end;

begin

definition
let IT be set ;
attr IT 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 )
proof end;
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 set ;
existence
ex b1 being non empty set st b1 is categorial
proof end;
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;
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)] ) );
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 Categorial -> with_triple-like_morphisms CatStr ;
coherence
for b1 being Category st b1 is Categorial holds
b1 is with_triple-like_morphisms
proof end;
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, the Id of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D, the Id of D #) & C is Categorial holds
D is Categorial
proof end;

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

registration
cluster non empty non void strict Category-like Categorial CatStr ;
existence
ex b1 being strict Category st b1 is Categorial
proof end;
end;

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

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 )
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
proof end;
:: original: `12
redefine func m `12 -> Category;
coherence
m `12 is Category
proof end;
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, the Id of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2, the Id of C2 #)
proof end;

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

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

definition
let IT be Categorial Category;
attr IT 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 strict Category-like with_triple-like_morphisms Categorial full CatStr ;
existence
ex b1 being strict Categorial Category st b1 is full
proof end;
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, the Id of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2, the Id 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
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
proof end;

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 ;
func o 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
proof end;
cluster o Hom -> non empty ;
coherence
not o Hom is empty
proof end;
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 )
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 )
proof end;

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

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

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)] )
proof end;
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 ) ) ) )
proof end;
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)
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
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)] ) )
proof end;
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
proof end;
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)] )
proof end;
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 ) ) ) )
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 S2[a,b,f] & S2[b,c,g] & S2[c,d,h] holds
H1(h,H1(g,f)) = H1(H1(h,g),f)
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
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)] ) )
proof end;
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
proof end;
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 func m `2 -> Morphism of C;
coherence
m `2 is Morphism of C
proof end;
:: original: `11
redefine func m `11 -> Element of Hom o;
coherence
m `11 is Element of Hom o
proof end;
:: original: `12
redefine func m `12 -> Element of Hom o;
coherence
m `12 is Element of Hom o
proof end;
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 )
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))]
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
proof end;
:: original: `11
redefine func m `11 -> Element of o Hom ;
coherence
m `11 is Element of o Hom
proof end;
:: original: `12
redefine func m `12 -> Element of o Hom ;
coherence
m `12 is Element of o Hom
proof end;
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 )
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))]
proof end;

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