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 :
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def2 defines Funct CAT_2:def 2 :
:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :
:: deftheorem Def4 defines Subcategory CAT_2:def 4 :
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 :
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem
theorem
theorem Th25:
:: deftheorem Def6 defines is_full_subcategory_of CAT_2:def 6 :
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 ,;
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
for
M being non
empty set for
d,
c being
Function of
M,
O for
p being
PartFunc of ,
for
i being
Function of
O,
M st
M = union { (Hom a,b) where a, b is Object of : ( 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
for
M being non
empty set for
d,
c being
Function of
M,
O for
p being
PartFunc of ,
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 : ( 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 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,
c' being
Object of
for
f being
Morphism of
c,
c' for
d,
d' being
Object of
for
g being
Morphism of
d,
d' st
Hom c,
c' <> {} &
Hom d,
d' <> {} holds
[f,g] is
Morphism of
[c,d],
[c',d']
theorem Th44:
theorem Th45:
:: deftheorem defines ?- CAT_2:def 8 :
theorem
canceled;
theorem
theorem
:: deftheorem defines -? CAT_2:def 9 :
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 :
:: deftheorem defines pr2 CAT_2:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem Th62:
definition
let C,
D,
D' be
Category;
let T be
Functor of
C,
D;
let T' be
Functor of
C,
D';
<:redefine func <:T,T':> -> Functor of
C,
[:D,D':];
coherence
<:T,T':> is Functor of C,[:D,D':]
by Th62;
end;
theorem
theorem Th64:
theorem Th65:
definition
let C,
C',
D,
D' be
Category;
let T be
Functor of
C,
D;
let T' be
Functor of
C',
D';
[:redefine func [:T,T':] -> Functor of
[:C,C':],
[:D,D':];
coherence
[:T,T':] is Functor of [:C,C':],[:D,D':]
by Th65;
end;
theorem