begin
theorem Th1:
theorem Th2:
definition
let C,
D,
E be non
empty set ;
let f be
Function of
[:C,D:],
E;
curryredefine func curry f -> Function of
C,
(Funcs D,E);
coherence
curry f is Function of C,(Funcs D,E)
by Th1;
curry'redefine func curry' f -> Function of
D,
(Funcs C,E);
coherence
curry' f is Function of D,(Funcs C,E)
by Th2;
end;
theorem Th3:
theorem Th4:
:: deftheorem defines --> CAT_2:def 1 :
for B, C being Category
for c being Object of C holds B --> c = the carrier' of B --> (id c);
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def2 defines Funct CAT_2:def 2 :
for C, D being Category
for b3 being set holds
( b3 = Funct C,D iff for x being set holds
( x in b3 iff x is Functor of C,D ) );
:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :
for C, D being Category
for b3 being non empty set holds
( b3 is FUNCTOR-DOMAIN of C,D iff for x being Element of b3 holds x is Functor of C,D );
:: deftheorem Def4 defines Subcategory CAT_2:def 4 :
for C, b2 being Category holds
( b2 is Subcategory of C iff ( the carrier of b2 c= the carrier of C & ( for a, b being Object of b2
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9 ) & the Comp of b2 c= the Comp of C & ( for a being Object of b2
for a9 being Object of C st a = a9 holds
id a = id a9 ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
:: deftheorem defines incl CAT_2:def 5 :
for C being Category
for E being Subcategory of C holds incl E = id E;
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem
theorem
theorem Th25:
:: deftheorem Def6 defines is_full_subcategory_of CAT_2:def 6 :
for C being non empty non void CatStr
for D being Category holds
( C is_full_subcategory_of D iff ( C is Subcategory of D & ( for a, b being Object of C
for a9, b9 being Object of D st a = a9 & b = b9 holds
Hom a,b = Hom a9,b9 ) ) );
theorem
canceled;
theorem
theorem Th28:
theorem Th29:
registration
let O,
M be non
empty set ;
let d,
c be
Function of
M,
O;
let p be
PartFunc of
[:M,M:],
M;
let i be
Function of
O,
M;
cluster CatStr(#
O,
M,
d,
c,
p,
i #)
-> non
empty non
void ;
coherence
( not CatStr(# O,M,d,c,p,i #) is void & not CatStr(# O,M,d,c,p,i #) is empty )
;
end;
theorem
for
C being
Category for
O being non
empty Subset of the
carrier of
C for
M being non
empty set for
d,
c being
Function of
M,
O for
p being
PartFunc of
[:M,M:],
M for
i being
Function of
O,
M st
M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } &
d = the
Source of
C | M &
c = the
Target of
C | M &
p = the
Comp of
C || M &
i = the
Id of
C | O holds
CatStr(#
O,
M,
d,
c,
p,
i #)
is_full_subcategory_of C
theorem
for
C being
Category for
O being non
empty Subset of the
carrier of
C for
M being non
empty set for
d,
c being
Function of
M,
O for
p being
PartFunc of
[:M,M:],
M for
i being
Function of
O,
M st
CatStr(#
O,
M,
d,
c,
p,
i #)
is_full_subcategory_of C holds
(
M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } &
d = the
Source of
C | M &
c = the
Target of
C | M &
p = the
Comp of
C || M &
i = the
Id of
C | O )
definition
let X1,
X2,
Y1,
Y2 be non
empty set ;
let f1 be
Function of
X1,
Y1;
let f2 be
Function of
X2,
Y2;
[:redefine func [:f1,f2:] -> Function of
[:X1,X2:],
[:Y1,Y2:];
coherence
[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:]
end;
definition
let A,
B be non
empty set ;
let f be
PartFunc of
[:A,A:],
A;
let g be
PartFunc of
[:B,B:],
B;
|:redefine func |:f,g:| -> PartFunc of
[:[:A,B:],[:A,B:]:],
[:A,B:];
coherence
|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:]
by FUNCT_4:62;
end;
definition
let C,
D be
Category;
func [:C,D:] -> Category equals
CatStr(#
[:the carrier of C,the carrier of D:],
[:the carrier' of C,the carrier' of D:],
[:the Source of C,the Source of D:],
[:the Target of C,the Target of D:],
|:the Comp of C,the Comp of D:|,
[:the Id of C,the Id of D:] #);
coherence
CatStr(# [:the carrier of C,the carrier of D:],[:the carrier' of C,the carrier' of D:],[:the Source of C,the Source of D:],[:the Target of C,the Target of D:],|:the Comp of C,the Comp of D:|,[:the Id of C,the Id of D:] #) is Category
end;
:: deftheorem defines [: CAT_2:def 7 :
for C, D being Category holds [:C,D:] = CatStr(# [:the carrier of C,the carrier of D:],[:the carrier' of C,the carrier' of D:],[:the Source of C,the Source of D:],[:the Target of C,the Target of D:],|:the Comp of C,the Comp of D:|,[:the Id of C,the Id of D:] #);
theorem
canceled;
theorem
for
C,
D being
Category holds
( the
carrier of
[:C,D:] = [:the carrier of C,the carrier of D:] & the
carrier' of
[:C,D:] = [:the carrier' of C,the carrier' of D:] & the
Source of
[:C,D:] = [:the Source of C,the Source of D:] & the
Target of
[:C,D:] = [:the Target of C,the Target of D:] & the
Comp of
[:C,D:] = |:the Comp of C,the Comp of D:| & the
Id of
[:C,D:] = [:the Id of C,the Id of D:] ) ;
theorem Th34:
theorem
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem
for
C,
D being
Category for
c,
c9 being
Object of
C for
f being
Morphism of
c,
c9 for
d,
d9 being
Object of
D for
g being
Morphism of
d,
d9 st
Hom c,
c9 <> {} &
Hom d,
d9 <> {} holds
[f,g] is
Morphism of
[c,d],
[c9,d9]
theorem Th44:
theorem Th45:
:: deftheorem defines ?- CAT_2:def 8 :
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c being Object of C holds S ?- c = (curry S) . (id c);
theorem
canceled;
theorem
theorem
:: deftheorem defines -? CAT_2:def 9 :
for C, C9, D being Category
for S being Functor of [:C,C9:],D
for c9 being Object of C9 holds S -? c9 = (curry' S) . (id c9);
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th54:
theorem Th55:
definition
let C,
D be
Category;
func pr1 C,
D -> Functor of
[:C,D:],
C equals
pr1 the
carrier' of
C,the
carrier' of
D;
coherence
pr1 the carrier' of C,the carrier' of D is Functor of [:C,D:],C
by Th54;
func pr2 C,
D -> Functor of
[:C,D:],
D equals
pr2 the
carrier' of
C,the
carrier' of
D;
coherence
pr2 the carrier' of C,the carrier' of D is Functor of [:C,D:],D
by Th55;
end;
:: deftheorem defines pr1 CAT_2:def 10 :
for C, D being Category holds pr1 C,D = pr1 the carrier' of C,the carrier' of D;
:: deftheorem defines pr2 CAT_2:def 11 :
for C, D being Category holds pr2 C,D = pr2 the carrier' of C,the carrier' of D;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th62:
definition
let C,
D,
D9 be
Category;
let T be
Functor of
C,
D;
let T9 be
Functor of
C,
D9;
<:redefine func <:T,T9:> -> Functor of
C,
[:D,D9:];
coherence
<:T,T9:> is Functor of C,[:D,D9:]
by Th62;
end;
theorem
theorem Th64:
theorem Th65:
definition
let C,
C9,
D,
D9 be
Category;
let T be
Functor of
C,
D;
let T9 be
Functor of
C9,
D9;
[:redefine func [:T,T9:] -> Functor of
[:C,C9:],
[:D,D9:];
coherence
[:T,T9:] is Functor of [:C,C9:],[:D,D9:]
by Th65;
end;
theorem