set M = { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } ;
set a0 = the Element of F1();
consider f0 being Element of F2() such that
A4:
P1[ the Element of F1(), the Element of F1(),f0]
and
for b being Element of F1()
for g being Element of F2() holds
( ( P1[ the Element of F1(),b,g] implies F3(g,f0) = g ) & ( P1[b, the Element of F1(),g] implies F3(f0,g) = g ) )
by A2;
A5:
[[ the Element of F1(), the Element of F1()],f0] in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] }
by A4;
{ [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } c= [:[:F1(),F1():],F2():]
proof
let x be
object ;
TARSKI:def 3 ( not x in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } or x in [:[:F1(),F1():],F2():] )
assume
x in { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] }
;
x in [:[:F1(),F1():],F2():]
then
ex
a,
b being
Element of
F1() ex
f being
Element of
F2() st
(
x = [[a,b],f] &
P1[
a,
b,
f] )
;
hence
x in [:[:F1(),F1():],F2():]
;
verum
end;
then reconsider M = { [[a,b],f] where a, b is Element of F1(), f is Element of F2() : P1[a,b,f] } as non empty Subset of [:[:F1(),F1():],F2():] by A5;
A6:
now for m being Element of M holds
( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] )let m be
Element of
M;
( m = [[(m `11),(m `12)],(m `2)] & P1[m `11 ,m `12 ,m `2 ] )
m in M
;
then consider a,
b being
Element of
F1(),
f being
Element of
F2()
such that A7:
m = [[a,b],f]
and A8:
P1[
a,
b,
f]
;
A9:
m `11 = a
by A7, MCART_1:85;
m `12 = b
by A7, MCART_1:85;
hence
(
m = [[(m `11),(m `12)],(m `2)] &
P1[
m `11 ,
m `12 ,
m `2 ] )
by A7, A8, A9;
verum end;
deffunc H1( Element of M) -> Element of F1() = $1 `11 ;
consider DM being Function of M,F1() such that
A10:
for m being Element of M holds DM . m = H1(m)
from FUNCT_2:sch 4();
deffunc H2( Element of M) -> Element of F1() = $1 `12 ;
consider CM being Function of M,F1() such that
A11:
for m being Element of M holds CM . m = H2(m)
from FUNCT_2:sch 4();
deffunc H3( object , object ) -> object = [[($2 `11),($1 `12)],F3(($1 `2),($2 `2))];
defpred S1[ object , object ] means ( $1 `11 = $2 `12 & $1 in M & $2 in M );
A12:
now for x, y being object st S1[x,y] holds
H3(x,y) in Mlet x,
y be
object ;
( S1[x,y] implies H3(x,y) in M )assume A13:
S1[
x,
y]
;
H3(x,y) in Mthen consider ax,
bx being
Element of
F1(),
fx being
Element of
F2()
such that A14:
x = [[ax,bx],fx]
and A15:
P1[
ax,
bx,
fx]
;
consider ay,
b2 being
Element of
F1(),
fy being
Element of
F2()
such that A16:
y = [[ay,b2],fy]
and A17:
P1[
ay,
b2,
fy]
by A13;
A18:
x `11 = ax
by A14, MCART_1:85;
A19:
x `12 = bx
by A14, MCART_1:85;
A20:
y `11 = ay
by A16, MCART_1:85;
A21:
y `12 = b2
by A16, MCART_1:85;
A22:
x `2 = fx
by A14;
A23:
y `2 = fy
by A16;
A24:
F3(
fx,
fy)
in F2()
by A1, A13, A15, A17, A18, A21;
P1[
ay,
bx,
F3(
fx,
fy)]
by A1, A13, A15, A17, A18, A21;
hence
H3(
x,
y)
in M
by A19, A20, A22, A23, A24;
verum end;
consider CC being PartFunc of [:M,M:],M such that
A25:
for x, y being object holds
( [x,y] in dom CC iff ( x in M & y in M & S1[x,y] ) )
and
A26:
for x, y being object st [x,y] in dom CC holds
CC . (x,y) = H3(x,y)
from BINOP_1:sch 6(A12);
defpred S2[ Element of F1(), set ] means ex f being Element of F2() st
( $2 = [[$1,$1],f] & P1[$1,$1,f] & ( for b being Element of F1()
for g being Element of F2() holds
( ( P1[$1,b,g] implies F3(g,f) = g ) & ( P1[b,$1,g] implies F3(f,g) = g ) ) ) );
A27:
now for a being Element of F1() ex y being Element of M st S2[a,y]let a be
Element of
F1();
ex y being Element of M st S2[a,y]consider f being
Element of
F2()
such that A28:
P1[
a,
a,
f]
and A29:
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 ) )
by A2;
[[a,a],f] in M
by A28;
then reconsider y =
[[a,a],f] as
Element of
M ;
take y =
y;
S2[a,y]thus
S2[
a,
y]
by A28, A29;
verum end;
consider I being Function of F1(),M such that
A30:
for o being Element of F1() holds S2[o,I . o]
from FUNCT_2:sch 3(A27);
set C = CatStr(# F1(),M,DM,CM,CC #);
A31:
CatStr(# F1(),M,DM,CM,CC #) is Category-like
proof
hereby CAT_1:def 6 verum
let f,
g be
Morphism of
CatStr(#
F1(),
M,
DM,
CM,
CC #);
( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f )A32:
(
[g,f] in dom CC iff (
g in M &
f in M &
g `11 = f `12 &
g in M &
f in M ) )
by A25;
DM . g = g `11
by A10;
hence
(
[g,f] in dom the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #) iff
dom g = cod f )
by A11, A32;
verum
end;
end;
A33:
for f, g being Morphism of CatStr(# F1(),M,DM,CM,CC #) holds
( [g,f] in dom the Comp of CatStr(# F1(),M,DM,CM,CC #) iff dom g = cod f )
by A31;
A34:
CatStr(# F1(),M,DM,CM,CC #) is transitive
proof
let f,
g be
Morphism of
CatStr(#
F1(),
M,
DM,
CM,
CC #);
CAT_1:def 7 ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
A35:
the
Source of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. f = f `11
by A10;
A36:
the
Source of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. g = g `11
by A10;
A37:
the
Target of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. f = f `12
by A11;
A38:
the
Target of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. g = g `12
by A11;
assume A39:
dom g = cod f
;
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
then A40:
CC . (
g,
f)
= [[(f `11),(g `12)],F3((g `2),(f `2))]
by A26, A25, A36, A37;
A41:
(CC . [g,f]) `11 = f `11
by A40, MCART_1:85;
A42:
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
g,
f)
= g (*) f
by A39, A25, A36, A37, CAT_1:def 1;
(CC . [g,f]) `12 = g `12
by A40, MCART_1:85;
hence
(
dom (g (*) f) = dom f &
cod (g (*) f) = cod g )
by A10, A11, A35, A38, A41, A42;
verum
end;
A43:
CatStr(# F1(),M,DM,CM,CC #) is associative
proof
let f,
g,
h be
Morphism of
CatStr(#
F1(),
M,
DM,
CM,
CC #);
CAT_1:def 8 ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
A44:
the
Source of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. g = g `11
by A10;
A45:
the
Source of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. h = h `11
by A10;
A46:
the
Target of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. f = f `12
by A11;
A47:
the
Target of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. g = g `12
by A11;
assume that A48:
dom h = cod g
and A49:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
A50:
[g,f] in dom CC
by A25, A44, A46, A49;
A51:
[h,g] in dom CC
by A25, A45, A47, A48;
A52:
CC . [g,f] in rng CC
by A50, FUNCT_1:def 3;
CC . [h,g] in rng CC
by A51, FUNCT_1:def 3;
then reconsider gf =
CC . (
g,
f),
hg =
CC . (
h,
g) as
Element of
M by A52;
A53:
gf = [[(f `11),(g `12)],F3((g `2),(f `2))]
by A26, A25, A44, A46, A49;
A54:
hg = [[(g `11),(h `12)],F3((h `2),(g `2))]
by A26, A25, A45, A47, A48;
A55:
DM . gf = gf `11
by A10;
A56:
DM . hg = hg `11
by A10;
A57:
CM . gf = gf `12
by A11;
A58:
CM . hg = hg `12
by A11;
A59:
DM . gf = f `11
by A53, A55, MCART_1:85;
A60:
CM . gf = g `12
by A53, A57, MCART_1:85;
A61:
CM . hg = h `12
by A54, A58, MCART_1:85;
A62:
[h,gf] in dom CC
by A25, A45, A11, A48, A57, A60;
A63:
[hg,f] in dom CC
by A25, A44, A46, A49, A56, A54, MCART_1:85;
reconsider f9 =
f,
g9 =
g,
h9 =
h as
Element of
M ;
A64:
P1[
f9 `11 ,
f9 `12 ,
f9 `2 ]
by A6;
A65:
P1[
g9 `11 ,
g9 `12 ,
g9 `2 ]
by A6;
A66:
P1[
h9 `11 ,
h9 `12 ,
h9 `2 ]
by A6;
A67:
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
h,
g)
= h (*) g
by A33, A48, CAT_1:def 1;
A68:
dom (h (*) g) = dom g
by A34, A48;
A69:
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
g,
f)
= g (*) f
by A33, A49, CAT_1:def 1;
cod (g (*) f) = cod g
by A34, A49;
hence h (*) (g (*) f) =
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
h,
( the Comp of CatStr(# F1(),M,DM,CM,CC #) . (g,f)))
by A69, A33, A48, CAT_1:def 1
.=
[[(f `11),(h `12)],F3((h `2),(gf `2))]
by A26, A55, A59, A62
.=
[[(f `11),(h `12)],F3((h9 `2),F3((g9 `2),(f9 `2)))]
by A53
.=
[[(f `11),(h `12)],F3(F3((h9 `2),(g9 `2)),(f9 `2))]
by A3, A44, A45, A46, A47, A48, A49, A64, A65, A66
.=
[[(f `11),(h `12)],F3((hg `2),(f `2))]
by A54
.=
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
( the Comp of CatStr(# F1(),M,DM,CM,CC #) . (h,g)),
f)
by A26, A58, A61, A63
.=
(h (*) g) (*) f
by A67, A33, A49, A68, CAT_1:def 1
;
verum
end;
A70:
CatStr(# F1(),M,DM,CM,CC #) is reflexive
proof
let b be
Object of
CatStr(#
F1(),
M,
DM,
CM,
CC #);
CAT_1:def 9 not Hom (b,b) = {}
consider f being
Element of
F2()
such that A71:
I . b = [[b,b],f]
and
P1[
b,
b,
f]
and
for
c being
Element of
F1()
for
g being
Element of
F2() holds
( (
P1[
b,
c,
g] implies
F3(
g,
f)
= g ) & (
P1[
c,
b,
g] implies
F3(
f,
g)
= g ) )
by A30;
reconsider bb =
b as
Element of
F1() ;
reconsider Ib =
I . bb as
Element of
M ;
reconsider ii =
I . bb as
Morphism of
CatStr(#
F1(),
M,
DM,
CM,
CC #) ;
A72:
cod ii =
(I . b) `12
by A11
.=
b
by A71, MCART_1:85
;
dom ii =
(I . b) `11
by A10
.=
b
by A71, MCART_1:85
;
then
I . b in Hom (
b,
b)
by A72;
hence
Hom (
b,
b)
<> {}
;
verum
end;
CatStr(# F1(),M,DM,CM,CC #) is with_identities
proof
let a be
Object of
CatStr(#
F1(),
M,
DM,
CM,
CC #);
CAT_1:def 10 ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# F1(),M,DM,CM,CC #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
consider f being
Element of
F2()
such that A73:
I . a = [[a,a],f]
and
P1[
a,
a,
f]
and A74:
for
c being
Element of
F1()
for
g being
Element of
F2() holds
( (
P1[
a,
c,
g] implies
F3(
g,
f)
= g ) & (
P1[
c,
a,
g] implies
F3(
f,
g)
= g ) )
by A30;
reconsider aa =
a as
Element of
F1() ;
reconsider Ia =
I . aa as
Element of
M ;
reconsider ii =
I . aa as
Morphism of
CatStr(#
F1(),
M,
DM,
CM,
CC #) ;
A75:
cod ii =
(I . a) `12
by A11
.=
a
by A73, MCART_1:85
;
dom ii =
(I . a) `11
by A10
.=
a
by A73, MCART_1:85
;
then reconsider ii =
ii as
Morphism of
a,
a by A75, CAT_1:4;
take
ii
;
for b1 being Element of the carrier of CatStr(# F1(),M,DM,CM,CC #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be
Element of
CatStr(#
F1(),
M,
DM,
CM,
CC #);
( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
thus
(
Hom (
a,
b)
<> {} implies for
g being
Morphism of
a,
b holds
g (*) ii = g )
( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )proof
assume A76:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) ii = g
let g be
Morphism of
a,
b;
g (*) ii = g
reconsider bb =
b as
Element of
F1() ;
g in M
;
then consider a1,
b1 being
Element of
F1(),
f1 being
Element of
F2()
such that A77:
g = [[a1,b1],f1]
and A78:
P1[
a1,
b1,
f1]
;
A79:
a =
dom g
by A76, CAT_1:5
.=
DM . g
.=
[[a1,b1],f1] `11
by A77, A10
.=
a1
by MCART_1:85
;
then A80:
F3(
f1,
f)
= f1
by A74, A78;
A81:
[[a,a],f] `11 = a1
by A79, MCART_1:85;
A82:
[[a1,b1],f1] `12 = b1
by MCART_1:85;
g `11 =
[[a1,b1],f1] `11
by A77
.=
a
by A79, MCART_1:85
.=
[[a,a],f] `12
by MCART_1:85
.=
ii `12
by A73
;
then A83:
[g,ii] in dom CC
by A25;
hence g (*) ii =
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
g,
ii)
by CAT_1:def 1
.=
CC . (
g,
ii)
.=
[[(ii `11),(g `12)],F3((g `2),(ii `2))]
by A26, A83
.=
[[a1,b1],f1]
by A80, A81, A82, A77, A73
.=
g
by A77
;
verum
end;
thus
(
Hom (
b,
a)
<> {} implies for
f being
Morphism of
b,
a holds
ii (*) f = f )
verumproof
assume A84:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds ii (*) f = f
let g be
Morphism of
b,
a;
ii (*) g = g
reconsider bb =
b as
Element of
F1() ;
g in M
;
then consider b1,
a1 being
Element of
F1(),
f1 being
Element of
F2()
such that A85:
g = [[b1,a1],f1]
and A86:
P1[
b1,
a1,
f1]
;
A87:
a =
cod g
by A84, CAT_1:5
.=
CM . g
.=
[[b1,a1],f1] `12
by A85, A11
.=
a1
by MCART_1:85
;
then A88:
F3(
f,
f1)
= f1
by A74, A86;
A89:
[[a,a],f] `12 = a1
by A87, MCART_1:85;
A90:
[[b1,a1],f1] `11 = b1
by MCART_1:85;
g `12 =
[[b1,a1],f1] `12
by A85
.=
a
by A87, MCART_1:85
.=
[[a,a],f] `11
by MCART_1:85
.=
ii `11
by A73
;
then A91:
[ii,g] in dom CC
by A25;
hence ii (*) g =
the
Comp of
CatStr(#
F1(),
M,
DM,
CM,
CC #)
. (
ii,
g)
by CAT_1:def 1
.=
CC . (
ii,
g)
.=
[[(g `11),(ii `12)],F3((ii `2),(g `2))]
by A26, A91
.=
[[b1,a1],f1]
by A88, A89, A90, A85, A73
.=
g
by A85
;
verum
end;
end;
then reconsider C = CatStr(# F1(),M,DM,CM,CC #) as strict Category by A31, A34, A43, A70;
C is with_triple-like_morphisms
proof
let f be
Morphism of
C;
CAT_5:def 1 ex x being set st f = [[(dom f),(cod f)],x]
f in M
;
then consider a,
b being
Element of
F1(),
g being
Element of
F2()
such that A92:
f = [[a,b],g]
and
P1[
a,
b,
g]
;
take
g
;
f = [[(dom f),(cod f)],g]
A93:
dom f =
f `11
by A10
.=
a
by A92, MCART_1:85
;
cod f =
f `12
by A11
.=
b
by A92, MCART_1:85
;
hence
f = [[(dom f),(cod f)],g]
by A92, A93;
verum
end;
then reconsider C = C as strict with_triple-like_morphisms Category ;
take
C
; ( 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)] ) )
thus
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)] ) )
hereby ( ( 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)] ) )
let a,
b be
Element of
F1();
for f being Element of F2() st P1[a,b,f] holds
[[a,b],f] is Morphism of Clet f be
Element of
F2();
( P1[a,b,f] implies [[a,b],f] is Morphism of C )assume
P1[
a,
b,
f]
;
[[a,b],f] is Morphism of Cthen
[[a,b],f] in M
;
hence
[[a,b],f] is
Morphism of
C
;
verum
end;
hereby 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)]
let m be
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] )
m in M
;
hence
ex
a,
b being
Element of
F1() ex
f being
Element of
F2() st
(
m = [[a,b],f] &
P1[
a,
b,
f] )
;
verum
end;
let m1, m2 be 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)]
let a1, a2, a3 be 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)]
let f1, f2 be Element of F2(); ( m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] implies m2 (*) m1 = [[a1,a3],F3(f2,f1)] )
assume that
A94:
m1 = [[a1,a2],f1]
and
A95:
m2 = [[a2,a3],f2]
; m2 (*) m1 = [[a1,a3],F3(f2,f1)]
A96:
m1 `11 = a1
by A94, MCART_1:85;
A97:
m1 `12 = a2
by A94, MCART_1:85;
A98:
m2 `11 = a2
by A95, MCART_1:85;
A99:
m2 `12 = a3
by A95, MCART_1:85;
thus m2 (*) m1 =
CC . (m2,m1)
by A25, A97, A98, CAT_1:def 1
.=
[[a1,a3],F3((m2 `2),(m1 `2))]
by A26, A96, A99, A25, A97, A98
.=
[[a1,a3],F3(f2,(m1 `2))]
by A95
.=
[[a1,a3],F3(f2,f1)]
by A94
; verum