:: CAT_5 semantic presentation

definition
let c1, c2, c3 be non empty set ;
let c4 be Element of [:[:c1,c2:],c3:];
redefine func `11 as c4 `11 -> Element of a1;
coherence
c4 `11 is Element of c1
proof end;
redefine func `12 as c4 `12 -> Element of a2;
coherence
c4 `12 is Element of c2
proof end;
end;

definition
let c1, c2 be non empty set ;
let c3 be Element of [:c1,c2:];
redefine func `2 as c3 `2 -> Element of a2;
coherence
c3 `2 is Element of c2
proof end;
end;

theorem Th1: :: CAT_5:1
for b1, b2 being CatStr st CatStr(# the Objects of b1,the Morphisms of b1,the Dom of b1,the Cod of b1,the Comp of b1,the Id of b1 #) = CatStr(# the Objects of b2,the Morphisms of b2,the Dom of b2,the Cod of b2,the Comp of b2,the Id of b2 #) & b1 is Category-like holds
b2 is Category-like
proof end;

definition
let c1 be CatStr ;
attr a1 is with_triple-like_morphisms means :Def1: :: CAT_5:def 1
for b1 being Morphism of a1 ex b2 being set st b1 = [[(dom b1),(cod b1)],b2];
end;

:: deftheorem Def1 defines with_triple-like_morphisms CAT_5:def 1 :
for b1 being CatStr holds
( b1 is with_triple-like_morphisms iff for b2 being Morphism of b1 ex b3 being set st b2 = [[(dom b2),(cod b2)],b3] );

registration
cluster strict 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 b1 being with_triple-like_morphisms CatStr
for b2 being Morphism of b1 holds
( dom b2 = b2 `11 & cod b2 = b2 `12 & b2 = [[(dom b2),(cod b2)],(b2 `2 )] )
proof end;

definition
let c1 be with_triple-like_morphisms CatStr ;
let c2 be Morphism of c1;
redefine func `11 as c2 `11 -> Object of a1;
coherence
c2 `11 is Object of c1
proof end;
redefine func `12 as c2 `12 -> Object of a1;
coherence
c2 `12 is Object of c1
proof end;
end;

scheme :: CAT_5:sch 1
s1{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ], F3( set , set ) -> set } :
ex b1 being strict with_triple-like_morphisms Category st
( the Objects of b1 = F1() & ( for b2, b3 being Element of F1()
for b4 being Element of F2() st P1[b2,b3,b4] holds
[[b2,b3],b4] is Morphism of b1 ) & ( for b2 being Morphism of b1 ex b3, b4 being Element of F1()ex b5 being Element of F2() st
( b2 = [[b3,b4],b5] & P1[b3,b4,b5] ) ) & ( for b2, b3 being Morphism of b1
for b4, b5, b6 being Element of F1()
for b7, b8 being Element of F2() st b2 = [[b4,b5],b7] & b3 = [[b5,b6],b8] holds
b3 * b2 = [[b4,b6],F3(b8,b7)] ) )
provided
E4: for b1, b2, b3 being Element of F1()
for b4, b5 being Element of F2() st P1[b1,b2,b4] & P1[b2,b3,b5] holds
( F3(b5,b4) in F2() & P1[b1,b3,F3(b5,b4)] ) and
E5: for b1 being Element of F1() ex b2 being Element of F2() st
( P1[b1,b1,b2] & ( for b3 being Element of F1()
for b4 being Element of F2() holds
( ( P1[b1,b3,b4] implies F3(b4,b2) = b4 ) & ( P1[b3,b1,b4] implies F3(b2,b4) = b4 ) ) ) ) and
E6: for b1, b2, b3, b4 being Element of F1()
for b5, b6, b7 being Element of F2() st P1[b1,b2,b5] & P1[b2,b3,b6] & P1[b3,b4,b7] holds
F3(b7,F3(b6,b5)) = F3(F3(b7,b6),b5)
proof end;

scheme :: CAT_5:sch 2
s2{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ], F3( set , set ) -> set } :
for b1, b2 being strict with_triple-like_morphisms Category st the Objects of b1 = F1() & ( for b3, b4 being Element of F1()
for b5 being Element of F2() st P1[b3,b4,b5] holds
[[b3,b4],b5] is Morphism of b1 ) & ( for b3 being Morphism of b1 ex b4, b5 being Element of F1()ex b6 being Element of F2() st
( b3 = [[b4,b5],b6] & P1[b4,b5,b6] ) ) & ( for b3, b4 being Morphism of b1
for b5, b6, b7 being Element of F1()
for b8, b9 being Element of F2() st b3 = [[b5,b6],b8] & b4 = [[b6,b7],b9] holds
b4 * b3 = [[b5,b7],F3(b9,b8)] ) & the Objects of b2 = F1() & ( for b3, b4 being Element of F1()
for b5 being Element of F2() st P1[b3,b4,b5] holds
[[b3,b4],b5] is Morphism of b2 ) & ( for b3 being Morphism of b2 ex b4, b5 being Element of F1()ex b6 being Element of F2() st
( b3 = [[b4,b5],b6] & P1[b4,b5,b6] ) ) & ( for b3, b4 being Morphism of b2
for b5, b6, b7 being Element of F1()
for b8, b9 being Element of F2() st b3 = [[b5,b6],b8] & b4 = [[b6,b7],b9] holds
b4 * b3 = [[b5,b7],F3(b9,b8)] ) holds
b1 = b2
provided
E4: for b1 being Element of F1() ex b2 being Element of F2() st
( P1[b1,b1,b2] & ( for b3 being Element of F1()
for b4 being Element of F2() holds
( ( P1[b1,b3,b4] implies F3(b4,b2) = b4 ) & ( P1[b3,b1,b4] implies F3(b2,b4) = b4 ) ) ) )
proof end;

scheme :: CAT_5:sch 3
s3{ F1() -> Category, F2() -> Category, F3( set ) -> Object of F2(), F4( set ) -> set } :
ex b1 being Functor of F1(),F2() st
for b2 being Morphism of F1() holds b1 . b2 = F4(b2)
provided
E4: for b1 being Morphism of F1() holds
( F4(b1) is Morphism of F2() & ( for b2 being Morphism of F2() st b2 = F4(b1) holds
( dom b2 = F3((dom b1)) & cod b2 = F3((cod b1)) ) ) ) and
E5: for b1 being Object of F1() holds F4((id b1)) = id F3(b1) and
E6: for b1, b2 being Morphism of F1()
for b3, b4 being Morphism of F2() st b3 = F4(b1) & b4 = F4(b2) & dom b2 = cod b1 holds
F4((b2 * b1)) = b4 * b3
proof end;

theorem Th3: :: CAT_5:3
for b1 being Category
for b2 being Subcategory of b1 st b1 is Subcategory of b2 holds
CatStr(# the Objects of b1,the Morphisms of b1,the Dom of b1,the Cod of b1,the Comp of b1,the Id of b1 #) = CatStr(# the Objects of b2,the Morphisms of b2,the Dom of b2,the Cod of b2,the Comp of b2,the Id of b2 #)
proof end;

theorem Th4: :: CAT_5:4
for b1 being Category
for b2 being Subcategory of b1
for b3 being Subcategory of b2 holds b3 is Subcategory of b1
proof end;

definition
let c1, c2 be Category;
given c3 being Category such that E6: ( c1 is Subcategory of c3 & c2 is Subcategory of c3 ) ;
given c4 being Object of c1 such that E7: c4 is Object of c2 ;
func c1 /\ c2 -> strict Category means :Def2: :: CAT_5:def 2
( the Objects of a3 = the Objects of a1 /\ the Objects of a2 & the Morphisms of a3 = the Morphisms of a1 /\ the Morphisms of a2 & the Dom of a3 = the Dom of a1 | the Morphisms of a2 & the Cod of a3 = the Cod of a1 | the Morphisms of a2 & the Comp of a3 = the Comp of a1 || the Morphisms of a2 & the Id of a3 = the Id of a1 | the Objects of a2 );
existence
ex b1 being strict Category st
( the Objects of b1 = the Objects of c1 /\ the Objects of c2 & the Morphisms of b1 = the Morphisms of c1 /\ the Morphisms of c2 & the Dom of b1 = the Dom of c1 | the Morphisms of c2 & the Cod of b1 = the Cod of c1 | the Morphisms of c2 & the Comp of b1 = the Comp of c1 || the Morphisms of c2 & the Id of b1 = the Id of c1 | the Objects of c2 )
proof end;
uniqueness
for b1, b2 being strict Category st the Objects of b1 = the Objects of c1 /\ the Objects of c2 & the Morphisms of b1 = the Morphisms of c1 /\ the Morphisms of c2 & the Dom of b1 = the Dom of c1 | the Morphisms of c2 & the Cod of b1 = the Cod of c1 | the Morphisms of c2 & the Comp of b1 = the Comp of c1 || the Morphisms of c2 & the Id of b1 = the Id of c1 | the Objects of c2 & the Objects of b2 = the Objects of c1 /\ the Objects of c2 & the Morphisms of b2 = the Morphisms of c1 /\ the Morphisms of c2 & the Dom of b2 = the Dom of c1 | the Morphisms of c2 & the Cod of b2 = the Cod of c1 | the Morphisms of c2 & the Comp of b2 = the Comp of c1 || the Morphisms of c2 & the Id of b2 = the Id of c1 | the Objects of c2 holds
b1 = b2 ;
end;

:: deftheorem Def2 defines /\ CAT_5:def 2 :
for b1, b2 being Category st ex b3 being Category st
( b1 is Subcategory of b3 & b2 is Subcategory of b3 ) & ex b3 being Object of b1 st b3 is Object of b2 holds
for b3 being strict Category holds
( b3 = b1 /\ b2 iff ( the Objects of b3 = the Objects of b1 /\ the Objects of b2 & the Morphisms of b3 = the Morphisms of b1 /\ the Morphisms of b2 & the Dom of b3 = the Dom of b1 | the Morphisms of b2 & the Cod of b3 = the Cod of b1 | the Morphisms of b2 & the Comp of b3 = the Comp of b1 || the Morphisms of b2 & the Id of b3 = the Id of b1 | the Objects of b2 ) );

theorem Th5: :: CAT_5:5
for b1 being Category
for b2, b3 being Subcategory of b1 st the Objects of b2 meets the Objects of b3 holds
b2 /\ b3 = b3 /\ b2
proof end;

theorem Th6: :: CAT_5:6
for b1 being Category
for b2, b3 being Subcategory of b1 st the Objects of b2 meets the Objects of b3 holds
( b2 /\ b3 is Subcategory of b2 & b2 /\ b3 is Subcategory of b3 )
proof end;

definition
let c1, c2 be Category;
let c3 be Functor of c1,c2;
func Image c3 -> strict Subcategory of a2 means :Def3: :: CAT_5:def 3
( the Objects of a4 = rng (Obj a3) & rng a3 c= the Morphisms of a4 & ( for b1 being Subcategory of a2 st the Objects of b1 = rng (Obj a3) & rng a3 c= the Morphisms of b1 holds
a4 is Subcategory of b1 ) );
existence
ex b1 being strict Subcategory of c2 st
( the Objects of b1 = rng (Obj c3) & rng c3 c= the Morphisms of b1 & ( for b2 being Subcategory of c2 st the Objects of b2 = rng (Obj c3) & rng c3 c= the Morphisms of b2 holds
b1 is Subcategory of b2 ) )
proof end;
uniqueness
for b1, b2 being strict Subcategory of c2 st the Objects of b1 = rng (Obj c3) & rng c3 c= the Morphisms of b1 & ( for b3 being Subcategory of c2 st the Objects of b3 = rng (Obj c3) & rng c3 c= the Morphisms of b3 holds
b1 is Subcategory of b3 ) & the Objects of b2 = rng (Obj c3) & rng c3 c= the Morphisms of b2 & ( for b3 being Subcategory of c2 st the Objects of b3 = rng (Obj c3) & rng c3 c= the Morphisms of b3 holds
b2 is Subcategory of b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Image CAT_5:def 3 :
for b1, b2 being Category
for b3 being Functor of b1,b2
for b4 being strict Subcategory of b2 holds
( b4 = Image b3 iff ( the Objects of b4 = rng (Obj b3) & rng b3 c= the Morphisms of b4 & ( for b5 being Subcategory of b2 st the Objects of b5 = rng (Obj b3) & rng b3 c= the Morphisms of b5 holds
b4 is Subcategory of b5 ) ) );

theorem Th7: :: CAT_5:7
for b1, b2 being Category
for b3 being Subcategory of b2
for b4 being Functor of b1,b2 st rng b4 c= the Morphisms of b3 holds
b4 is Functor of b1,b3
proof end;

theorem Th8: :: CAT_5:8
for b1, b2 being Category
for b3 being Functor of b1,b2 holds b3 is Functor of b1, Image b3
proof end;

theorem Th9: :: CAT_5:9
for b1, b2 being Category
for b3 being Subcategory of b2
for b4 being Functor of b1,b3
for b5 being Functor of b1,b2 st b4 = b5 holds
Image b4 = Image b5
proof end;

definition
let c1 be set ;
attr a1 is categorial means :Def4: :: CAT_5:def 4
for b1 being set st b1 in a1 holds
b1 is Category;
end;

:: deftheorem Def4 defines categorial CAT_5:def 4 :
for b1 being set holds
( b1 is categorial iff for b2 being set st b2 in b1 holds
b2 is Category );

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

:: deftheorem Def5 defines categorial CAT_5:def 5 :
for b1 being non empty set holds
( b1 is categorial iff for b2 being Element of b1 holds b2 is Category );

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

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

definition
let c1 be Category;
attr a1 is Categorial means :Def6: :: CAT_5:def 6
( the Objects of a1 is categorial & ( for b1 being Object of a1
for b2 being Category st b1 = b2 holds
id b1 = [[b2,b2],(id b2)] ) & ( for b1 being Morphism of a1
for b2, b3 being Category st b2 = dom b1 & b3 = cod b1 holds
ex b4 being Functor of b2,b3 st b1 = [[b2,b3],b4] ) & ( for b1, b2 being Morphism of a1
for b3, b4, b5 being Category
for b6 being Functor of b3,b4
for b7 being Functor of b4,b5 st b1 = [[b3,b4],b6] & b2 = [[b4,b5],b7] holds
b2 * b1 = [[b3,b5],(b7 * b6)] ) );
end;

:: deftheorem Def6 defines Categorial CAT_5:def 6 :
for b1 being Category holds
( b1 is Categorial iff ( the Objects of b1 is categorial & ( for b2 being Object of b1
for b3 being Category st b2 = b3 holds
id b2 = [[b3,b3],(id b3)] ) & ( for b2 being Morphism of b1
for b3, b4 being Category st b3 = dom b2 & b4 = cod b2 holds
ex b5 being Functor of b3,b4 st b2 = [[b3,b4],b5] ) & ( for b2, b3 being Morphism of b1
for b4, b5, b6 being Category
for b7 being Functor of b4,b5
for b8 being Functor of b5,b6 st b2 = [[b4,b5],b7] & b3 = [[b5,b6],b8] holds
b3 * b2 = [[b4,b6],(b8 * b7)] ) ) );

registration
cluster 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 b1, b2 being Category st CatStr(# the Objects of b1,the Morphisms of b1,the Dom of b1,the Cod of b1,the Comp of b1,the Id of b1 #) = CatStr(# the Objects of b2,the Morphisms of b2,the Dom of b2,the Cod of b2,the Comp of b2,the Id of b2 #) & b1 is Categorial holds
b2 is Categorial
proof end;

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

registration
cluster strict with_triple-like_morphisms Categorial CatStr ;
existence
ex b1 being strict Category st b1 is Categorial
proof end;
end;

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

theorem Th13: :: CAT_5:13
for b1 being Categorial Category
for b2 being Morphism of b1 holds
( dom b2 = b2 `11 & cod b2 = b2 `12 )
proof end;

definition
let c1 be Categorial Category;
let c2 be Morphism of c1;
redefine func `11 as c2 `11 -> Category;
coherence
c2 `11 is Category
proof end;
redefine func `12 as c2 `12 -> Category;
coherence
c2 `12 is Category
proof end;
end;

theorem Th14: :: CAT_5:14
for b1, b2 being Categorial Category st the Objects of b1 = the Objects of b2 & the Morphisms of b1 = the Morphisms of b2 holds
CatStr(# the Objects of b1,the Morphisms of b1,the Dom of b1,the Cod of b1,the Comp of b1,the Id of b1 #) = CatStr(# the Objects of b2,the Morphisms of b2,the Dom of b2,the Cod of b2,the Comp of b2,the Id of b2 #)
proof end;

registration
let c1 be Categorial Category;
cluster -> Categorial Subcategory of a1;
coherence
for b1 being Subcategory of c1 holds b1 is Categorial
proof end;
end;

theorem Th15: :: CAT_5:15
for b1, b2 being Categorial Category st the Morphisms of b1 c= the Morphisms of b2 holds
b1 is Subcategory of b2
proof end;

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

:: deftheorem Def7 defines cat CAT_5:def 7 :
for b1 being set st b1 is Category holds
cat b1 = b1;

theorem Th16: :: CAT_5:16
for b1 being Categorial Category
for b2 being Object of b1 holds cat b2 = b2
proof end;

definition
let c1 be Categorial Category;
let c2 be Morphism of c1;
redefine func `2 as c2 `2 -> Functor of cat (dom a2), cat (cod a2);
coherence
c2 `2 is Functor of cat (dom c2), cat (cod c2)
proof end;
end;

theorem Th17: :: CAT_5:17
for b1 being non empty categorial set
for b2 being non empty set st ( for b3, b4, b5 being Element of b1
for b6 being Functor of b3,b4
for b7 being Functor of b4,b5 st b6 in b2 & b7 in b2 holds
b7 * b6 in b2 ) & ( for b3 being Element of b1 holds id b3 in b2 ) holds
ex b3 being strict Categorial Category st
( the Objects of b3 = b1 & ( for b4, b5 being Element of b1
for b6 being Functor of b4,b5 holds
( [[b4,b5],b6] is Morphism of b3 iff b6 in b2 ) ) )
proof end;

theorem Th18: :: CAT_5:18
for b1 being non empty categorial set
for b2 being non empty set
for b3, b4 being strict Categorial Category st the Objects of b3 = b1 & ( for b5, b6 being Element of b1
for b7 being Functor of b5,b6 holds
( [[b5,b6],b7] is Morphism of b3 iff b7 in b2 ) ) & the Objects of b4 = b1 & ( for b5, b6 being Element of b1
for b7 being Functor of b5,b6 holds
( [[b5,b6],b7] is Morphism of b4 iff b7 in b2 ) ) holds
b3 = b4
proof end;

definition
let c1 be Categorial Category;
attr a1 is full means :Def8: :: CAT_5:def 8
for b1, b2 being Category st b1 is Object of a1 & b2 is Object of a1 holds
for b3 being Functor of b1,b2 holds [[b1,b2],b3] is Morphism of a1;
end;

:: deftheorem Def8 defines full CAT_5:def 8 :
for b1 being Categorial Category holds
( b1 is full iff for b2, b3 being Category st b2 is Object of b1 & b3 is Object of b1 holds
for b4 being Functor of b2,b3 holds [[b2,b3],b4] is Morphism of b1 );

registration
cluster strict with_triple-like_morphisms Categorial full CatStr ;
existence
ex b1 being strict Categorial Category st b1 is full
proof end;
end;

theorem Th19: :: CAT_5:19
for b1, b2 being Categorial full Category st the Objects of b1 = the Objects of b2 holds
CatStr(# the Objects of b1,the Morphisms of b1,the Dom of b1,the Cod of b1,the Comp of b1,the Id of b1 #) = CatStr(# the Objects of b2,the Morphisms of b2,the Dom of b2,the Cod of b2,the Comp of b2,the Id of b2 #)
proof end;

theorem Th20: :: CAT_5:20
for b1 being non empty categorial set ex b2 being strict Categorial full Category st the Objects of b2 = b1
proof end;

theorem Th21: :: CAT_5:21
for b1 being Categorial Category
for b2 being Categorial full Category st the Objects of b1 c= the Objects of b2 holds
b1 is Subcategory of b2
proof end;

theorem Th22: :: CAT_5:22
for b1 being Category
for b2, b3 being Categorial Category
for b4 being Functor of b1,b2
for b5 being Functor of b1,b3 st b4 = b5 holds
Image b4 = Image b5
proof end;

definition
let c1 be Category;
let c2 be Object of c1;
func Hom c2 -> Subset of the Morphisms of a1 equals :: CAT_5:def 9
the Cod of a1 " {a2};
coherence
the Cod of c1 " {c2} is Subset of the Morphisms of c1 ;
func c2 Hom -> Subset of the Morphisms of a1 equals :: CAT_5:def 10
the Dom of a1 " {a2};
coherence
the Dom of c1 " {c2} is Subset of the Morphisms of c1 ;
end;

:: deftheorem Def9 defines Hom CAT_5:def 9 :
for b1 being Category
for b2 being Object of b1 holds Hom b2 = the Cod of b1 " {b2};

:: deftheorem Def10 defines Hom CAT_5:def 10 :
for b1 being Category
for b2 being Object of b1 holds b2 Hom = the Dom of b1 " {b2};

registration
let c1 be Category;
let c2 be Object of c1;
cluster Hom a2 -> non empty ;
coherence
not Hom c2 is empty
proof end;
cluster a2 Hom -> non empty ;
coherence
not c2 Hom is empty
proof end;
end;

theorem Th23: :: CAT_5:23
for b1 being Category
for b2 being Object of b1
for b3 being Morphism of b1 holds
( b3 in Hom b2 iff cod b3 = b2 )
proof end;

theorem Th24: :: CAT_5:24
for b1 being Category
for b2 being Object of b1
for b3 being Morphism of b1 holds
( b3 in b2 Hom iff dom b3 = b2 )
proof end;

theorem Th25: :: CAT_5:25
for b1 being Category
for b2, b3 being Object of b1 holds Hom b2,b3 = (b2 Hom ) /\ (Hom b3)
proof end;

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

theorem Th27: :: CAT_5:27
for b1 being Category
for b2 being Morphism of b1
for b3 being Element of Hom (dom b2) holds b2 * b3 in Hom (cod b2)
proof end;

theorem Th28: :: CAT_5:28
for b1 being Category
for b2 being Morphism of b1
for b3 being Element of (cod b2) Hom holds b3 * b2 in (dom b2) Hom
proof end;

definition
let c1 be Category;
let c2 be Object of c1;
set c3 = Hom c2;
set c4 = the Morphisms of c1;
defpred S1[ Element of Hom c2, Element of Hom c2, Element of the Morphisms of c1] means ( dom a2 = cod a3 & a1 = a2 * a3 );
deffunc H1( Morphism of c1, Morphism of c1) -> Element of the Morphisms of c1 = a1 * a2;
E32: for b1, b2, b3 being Element of Hom c2
for b4, b5 being Element of the Morphisms of c1 st S1[b1,b2,b4] & S1[b2,b3,b5] holds
( H1(b5,b4) in the Morphisms of c1 & S1[b1,b3,H1(b5,b4)] )
proof end;
E33: for b1 being Element of Hom c2 ex b2 being Element of the Morphisms of c1 st
( S1[b1,b1,b2] & ( for b3 being Element of Hom c2
for b4 being Element of the Morphisms of c1 holds
( ( S1[b1,b3,b4] implies H1(b4,b2) = b4 ) & ( S1[b3,b1,b4] implies H1(b2,b4) = b4 ) ) ) )
proof end;
E34: for b1, b2, b3, b4 being Element of Hom c2
for b5, b6, b7 being Element of the Morphisms of c1 st S1[b1,b2,b5] & S1[b2,b3,b6] & S1[b3,b4,b7] holds
H1(b7,H1(b6,b5)) = H1(H1(b7,b6),b5)
proof end;
func c1 -SliceCat c2 -> strict with_triple-like_morphisms Category means :Def11: :: CAT_5:def 11
( the Objects of a3 = Hom a2 & ( for b1, b2 being Element of Hom a2
for b3 being Morphism of a1 st dom b2 = cod b3 & b1 = b2 * b3 holds
[[b1,b2],b3] is Morphism of a3 ) & ( for b1 being Morphism of a3 ex b2, b3 being Element of Hom a2ex b4 being Morphism of a1 st
( b1 = [[b2,b3],b4] & dom b3 = cod b4 & b2 = b3 * b4 ) ) & ( for b1, b2 being Morphism of a3
for b3, b4, b5 being Element of Hom a2
for b6, b7 being Morphism of a1 st b1 = [[b3,b4],b6] & b2 = [[b4,b5],b7] holds
b2 * b1 = [[b3,b5],(b7 * b6)] ) );
existence
ex b1 being strict with_triple-like_morphisms Category st
( the Objects of b1 = Hom c2 & ( for b2, b3 being Element of Hom c2
for b4 being Morphism of c1 st dom b3 = cod b4 & b2 = b3 * b4 holds
[[b2,b3],b4] is Morphism of b1 ) & ( for b2 being Morphism of b1 ex b3, b4 being Element of Hom c2ex b5 being Morphism of c1 st
( b2 = [[b3,b4],b5] & dom b4 = cod b5 & b3 = b4 * b5 ) ) & ( for b2, b3 being Morphism of b1
for b4, b5, b6 being Element of Hom c2
for b7, b8 being Morphism of c1 st b2 = [[b4,b5],b7] & b3 = [[b5,b6],b8] holds
b3 * b2 = [[b4,b6],(b8 * b7)] ) )
proof end;
uniqueness
for b1, b2 being strict with_triple-like_morphisms Category st the Objects of b1 = Hom c2 & ( for b3, b4 being Element of Hom c2
for b5 being Morphism of c1 st dom b4 = cod b5 & b3 = b4 * b5 holds
[[b3,b4],b5] is Morphism of b1 ) & ( for b3 being Morphism of b1 ex b4, b5 being Element of Hom c2ex b6 being Morphism of c1 st
( b3 = [[b4,b5],b6] & dom b5 = cod b6 & b4 = b5 * b6 ) ) & ( for b3, b4 being Morphism of b1
for b5, b6, b7 being Element of Hom c2
for b8, b9 being Morphism of c1 st b3 = [[b5,b6],b8] & b4 = [[b6,b7],b9] holds
b4 * b3 = [[b5,b7],(b9 * b8)] ) & the Objects of b2 = Hom c2 & ( for b3, b4 being Element of Hom c2
for b5 being Morphism of c1 st dom b4 = cod b5 & b3 = b4 * b5 holds
[[b3,b4],b5] is Morphism of b2 ) & ( for b3 being Morphism of b2 ex b4, b5 being Element of Hom c2ex b6 being Morphism of c1 st
( b3 = [[b4,b5],b6] & dom b5 = cod b6 & b4 = b5 * b6 ) ) & ( for b3, b4 being Morphism of b2
for b5, b6, b7 being Element of Hom c2
for b8, b9 being Morphism of c1 st b3 = [[b5,b6],b8] & b4 = [[b6,b7],b9] holds
b4 * b3 = [[b5,b7],(b9 * b8)] ) holds
b1 = b2
proof end;
set c5 = c2 Hom ;
defpred S2[ Element of c2 Hom , Element of c2 Hom , Element of the Morphisms of c1] means ( dom a3 = cod a1 & a2 = a3 * a1 );
E35: for b1, b2, b3 being Element of c2 Hom
for b4, b5 being Element of the Morphisms of c1 st S2[b1,b2,b4] & S2[b2,b3,b5] holds
( H1(b5,b4) in the Morphisms of c1 & S2[b1,b3,H1(b5,b4)] )
proof end;
E36: for b1 being Element of c2 Hom ex b2 being Element of the Morphisms of c1 st
( S2[b1,b1,b2] & ( for b3 being Element of c2 Hom
for b4 being Element of the Morphisms of c1 holds
( ( S2[b1,b3,b4] implies H1(b4,b2) = b4 ) & ( S2[b3,b1,b4] implies H1(b2,b4) = b4 ) ) ) )
proof end;
E37: for b1, b2, b3, b4 being Element of c2 Hom
for b5, b6, b7 being Element of the Morphisms of c1 st S2[b1,b2,b5] & S2[b2,b3,b6] & S2[b3,b4,b7] holds
H1(b7,H1(b6,b5)) = H1(H1(b7,b6),b5)
proof end;
func c2 -SliceCat c1 -> strict with_triple-like_morphisms Category means :Def12: :: CAT_5:def 12
( the Objects of a3 = a2 Hom & ( for b1, b2 being Element of a2 Hom
for b3 being Morphism of a1 st dom b3 = cod b1 & b3 * b1 = b2 holds
[[b1,b2],b3] is Morphism of a3 ) & ( for b1 being Morphism of a3 ex b2, b3 being Element of a2 Hom ex b4 being Morphism of a1 st
( b1 = [[b2,b3],b4] & dom b4 = cod b2 & b4 * b2 = b3 ) ) & ( for b1, b2 being Morphism of a3
for b3, b4, b5 being Element of a2 Hom
for b6, b7 being Morphism of a1 st b1 = [[b3,b4],b6] & b2 = [[b4,b5],b7] holds
b2 * b1 = [[b3,b5],(b7 * b6)] ) );
existence
ex b1 being strict with_triple-like_morphisms Category st
( the Objects of b1 = c2 Hom & ( for b2, b3 being Element of c2 Hom
for b4 being Morphism of c1 st dom b4 = cod b2 & b4 * b2 = b3 holds
[[b2,b3],b4] is Morphism of b1 ) & ( for b2 being Morphism of b1 ex b3, b4 being Element of c2 Hom ex b5 being Morphism of c1 st
( b2 = [[b3,b4],b5] & dom b5 = cod b3 & b5 * b3 = b4 ) ) & ( for b2, b3 being Morphism of b1
for b4, b5, b6 being Element of c2 Hom
for b7, b8 being Morphism of c1 st b2 = [[b4,b5],b7] & b3 = [[b5,b6],b8] holds
b3 * b2 = [[b4,b6],(b8 * b7)] ) )
proof end;
uniqueness
for b1, b2 being strict with_triple-like_morphisms Category st the Objects of b1 = c2 Hom & ( for b3, b4 being Element of c2 Hom
for b5 being Morphism of c1 st dom b5 = cod b3 & b5 * b3 = b4 holds
[[b3,b4],b5] is Morphism of b1 ) & ( for b3 being Morphism of b1 ex b4, b5 being Element of c2 Hom ex b6 being Morphism of c1 st
( b3 = [[b4,b5],b6] & dom b6 = cod b4 & b6 * b4 = b5 ) ) & ( for b3, b4 being Morphism of b1
for b5, b6, b7 being Element of c2 Hom
for b8, b9 being Morphism of c1 st b3 = [[b5,b6],b8] & b4 = [[b6,b7],b9] holds
b4 * b3 = [[b5,b7],(b9 * b8)] ) & the Objects of b2 = c2 Hom & ( for b3, b4 being Element of c2 Hom
for b5 being Morphism of c1 st dom b5 = cod b3 & b5 * b3 = b4 holds
[[b3,b4],b5] is Morphism of b2 ) & ( for b3 being Morphism of b2 ex b4, b5 being Element of c2 Hom ex b6 being Morphism of c1 st
( b3 = [[b4,b5],b6] & dom b6 = cod b4 & b6 * b4 = b5 ) ) & ( for b3, b4 being Morphism of b2
for b5, b6, b7 being Element of c2 Hom
for b8, b9 being Morphism of c1 st b3 = [[b5,b6],b8] & b4 = [[b6,b7],b9] holds
b4 * b3 = [[b5,b7],(b9 * b8)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines -SliceCat CAT_5:def 11 :
for b1 being Category
for b2 being Object of b1
for b3 being strict with_triple-like_morphisms Category holds
( b3 = b1 -SliceCat b2 iff ( the Objects of b3 = Hom b2 & ( for b4, b5 being Element of Hom b2
for b6 being Morphism of b1 st dom b5 = cod b6 & b4 = b5 * b6 holds
[[b4,b5],b6] is Morphism of b3 ) & ( for b4 being Morphism of b3 ex b5, b6 being Element of Hom b2ex b7 being Morphism of b1 st
( b4 = [[b5,b6],b7] & dom b6 = cod b7 & b5 = b6 * b7 ) ) & ( for b4, b5 being Morphism of b3
for b6, b7, b8 being Element of Hom b2
for b9, b10 being Morphism of b1 st b4 = [[b6,b7],b9] & b5 = [[b7,b8],b10] holds
b5 * b4 = [[b6,b8],(b10 * b9)] ) ) );

:: deftheorem Def12 defines -SliceCat CAT_5:def 12 :
for b1 being Category
for b2 being Object of b1
for b3 being strict with_triple-like_morphisms Category holds
( b3 = b2 -SliceCat b1 iff ( the Objects of b3 = b2 Hom & ( for b4, b5 being Element of b2 Hom
for b6 being Morphism of b1 st dom b6 = cod b4 & b6 * b4 = b5 holds
[[b4,b5],b6] is Morphism of b3 ) & ( for b4 being Morphism of b3 ex b5, b6 being Element of b2 Hom ex b7 being Morphism of b1 st
( b4 = [[b5,b6],b7] & dom b7 = cod b5 & b7 * b5 = b6 ) ) & ( for b4, b5 being Morphism of b3
for b6, b7, b8 being Element of b2 Hom
for b9, b10 being Morphism of b1 st b4 = [[b6,b7],b9] & b5 = [[b7,b8],b10] holds
b5 * b4 = [[b6,b8],(b10 * b9)] ) ) );

definition
let c1 be Category;
let c2 be Object of c1;
let c3 be Morphism of (c1 -SliceCat c2);
redefine func `2 as c3 `2 -> Morphism of a1;
coherence
c3 `2 is Morphism of c1
proof end;
redefine func `11 as c3 `11 -> Element of Hom a2;
coherence
c3 `11 is Element of Hom c2
proof end;
redefine func `12 as c3 `12 -> Element of Hom a2;
coherence
c3 `12 is Element of Hom c2
proof end;
end;

theorem Th29: :: CAT_5:29
for b1 being Category
for b2 being Object of b1
for b3 being Morphism of (b1 -SliceCat b2) holds
( b3 = [[(b3 `11 ),(b3 `12 )],(b3 `2 )] & dom (b3 `12 ) = cod (b3 `2 ) & b3 `11 = (b3 `12 ) * (b3 `2 ) & dom b3 = b3 `11 & cod b3 = b3 `12 )
proof end;

theorem Th30: :: CAT_5:30
for b1 being Category
for b2 being Object of b1
for b3 being Element of Hom b2
for b4 being Object of (b1 -SliceCat b2) st b4 = b3 holds
id b4 = [[b4,b4],(id (dom b3))]
proof end;

definition
let c1 be Category;
let c2 be Object of c1;
let c3 be Morphism of (c2 -SliceCat c1);
redefine func `2 as c3 `2 -> Morphism of a1;
coherence
c3 `2 is Morphism of c1
proof end;
redefine func `11 as c3 `11 -> Element of a2 Hom ;
coherence
c3 `11 is Element of c2 Hom
proof end;
redefine func `12 as c3 `12 -> Element of a2 Hom ;
coherence
c3 `12 is Element of c2 Hom
proof end;
end;

theorem Th31: :: CAT_5:31
for b1 being Category
for b2 being Object of b1
for b3 being Morphism of (b2 -SliceCat b1) holds
( b3 = [[(b3 `11 ),(b3 `12 )],(b3 `2 )] & dom (b3 `2 ) = cod (b3 `11 ) & (b3 `2 ) * (b3 `11 ) = b3 `12 & dom b3 = b3 `11 & cod b3 = b3 `12 )
proof end;

theorem Th32: :: CAT_5:32
for b1 being Category
for b2 being Object of b1
for b3 being Element of b2 Hom
for b4 being Object of (b2 -SliceCat b1) st b4 = b3 holds
id b4 = [[b4,b4],(id (cod b3))]
proof end;

definition
let c1 be Category;
let c2 be Morphism of c1;
func SliceFunctor c2 -> Functor of a1 -SliceCat (dom a2),a1 -SliceCat (cod a2) means :Def13: :: CAT_5:def 13
for b1 being Morphism of (a1 -SliceCat (dom a2)) holds a3 . b1 = [[(a2 * (b1 `11 )),(a2 * (b1 `12 ))],(b1 `2 )];
existence
ex b1 being Functor of c1 -SliceCat (dom c2),c1 -SliceCat (cod c2) st
for b2 being Morphism of (c1 -SliceCat (dom c2)) holds b1 . b2 = [[(c2 * (b2 `11 )),(c2 * (b2 `12 ))],(b2 `2 )]
proof end;
uniqueness
for b1, b2 being Functor of c1 -SliceCat (dom c2),c1 -SliceCat (cod c2) st ( for b3 being Morphism of (c1 -SliceCat (dom c2)) holds b1 . b3 = [[(c2 * (b3 `11 )),(c2 * (b3 `12 ))],(b3 `2 )] ) & ( for b3 being Morphism of (c1 -SliceCat (dom c2)) holds b2 . b3 = [[(c2 * (b3 `11 )),(c2 * (b3 `12 ))],(b3 `2 )] ) holds
b1 = b2
proof end;
func SliceContraFunctor c2 -> Functor of (cod a2) -SliceCat a1,(dom a2) -SliceCat a1 means :Def14: :: CAT_5:def 14
for b1 being Morphism of ((cod a2) -SliceCat a1) holds a3 . b1 = [[((b1 `11 ) * a2),((b1 `12 ) * a2)],(b1 `2 )];
existence
ex b1 being Functor of (cod c2) -SliceCat c1,(dom c2) -SliceCat c1 st
for b2 being Morphism of ((cod c2) -SliceCat c1) holds b1 . b2 = [[((b2 `11 ) * c2),((b2 `12 ) * c2)],(b2 `2 )]
proof end;
uniqueness
for b1, b2 being Functor of (cod c2) -SliceCat c1,(dom c2) -SliceCat c1 st ( for b3 being Morphism of ((cod c2) -SliceCat c1) holds b1 . b3 = [[((b3 `11 ) * c2),((b3 `12 ) * c2)],(b3 `2 )] ) & ( for b3 being Morphism of ((cod c2) -SliceCat c1) holds b2 . b3 = [[((b3 `11 ) * c2),((b3 `12 ) * c2)],(b3 `2 )] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines SliceFunctor CAT_5:def 13 :
for b1 being Category
for b2 being Morphism of b1
for b3 being Functor of b1 -SliceCat (dom b2),b1 -SliceCat (cod b2) holds
( b3 = SliceFunctor b2 iff for b4 being Morphism of (b1 -SliceCat (dom b2)) holds b3 . b4 = [[(b2 * (b4 `11 )),(b2 * (b4 `12 ))],(b4 `2 )] );

:: deftheorem Def14 defines SliceContraFunctor CAT_5:def 14 :
for b1 being Category
for b2 being Morphism of b1
for b3 being Functor of (cod b2) -SliceCat b1,(dom b2) -SliceCat b1 holds
( b3 = SliceContraFunctor b2 iff for b4 being Morphism of ((cod b2) -SliceCat b1) holds b3 . b4 = [[((b4 `11 ) * b2),((b4 `12 ) * b2)],(b4 `2 )] );

theorem Th33: :: CAT_5:33
for b1 being Category
for b2, b3 being Morphism of b1 st dom b3 = cod b2 holds
SliceFunctor (b3 * b2) = (SliceFunctor b3) * (SliceFunctor b2)
proof end;

theorem Th34: :: CAT_5:34
for b1 being Category
for b2, b3 being Morphism of b1 st dom b3 = cod b2 holds
SliceContraFunctor (b3 * b2) = (SliceContraFunctor b2) * (SliceContraFunctor b3)
proof end;