defpred S1[ object , object , object ] means ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( $2 = [[F,F1],t] & $1 = [[F1,F2],t1] & $3 = [[F,F2],(t1 `*` t)] );
deffunc H1( object ) -> object = ($1 `1) `1 ;
A1:
now for x, y, z1, z2 being object st x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2let x,
y,
z1,
z2 be
object ;
( x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )assume that
x in NatTrans (
A,
B)
and
y in NatTrans (
A,
B)
;
( S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )assume
S1[
x,
y,
z1]
;
( S1[x,y,z2] implies z1 = z2 )then consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A2:
y = [[F,F1],t]
and A3:
x = [[F1,F2],t1]
and A4:
z1 = [[F,F2],(t1 `*` t)]
;
assume
S1[
x,
y,
z2]
;
z1 = z2then consider F9,
F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F9,
F19,
t19 being
natural_transformation of
F19,
F29 such that A5:
y = [[F9,F19],t9]
and A6:
x = [[F19,F29],t19]
and A7:
z2 = [[F9,F29],(t19 `*` t9)]
;
A8:
t = t9
by A2, A5, XTUPLE_0:1;
[F1,F2] = [F19,F29]
by A3, A6, XTUPLE_0:1;
then A9:
F2 = F29
by XTUPLE_0:1;
A10:
t1 = t19
by A3, A6, XTUPLE_0:1;
A11:
[F,F1] = [F9,F19]
by A2, A5, XTUPLE_0:1;
then
F = F9
by XTUPLE_0:1;
hence
z1 = z2
by A4, A7, A11, A8, A10, A9, XTUPLE_0:1;
verum end;
A12:
now for x, y, z being object st x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z] holds
z in NatTrans (A,B)let x,
y,
z be
object ;
( x in NatTrans (A,B) & y in NatTrans (A,B) & S1[x,y,z] implies z in NatTrans (A,B) )assume that A13:
x in NatTrans (
A,
B)
and A14:
y in NatTrans (
A,
B)
;
( S1[x,y,z] implies z in NatTrans (A,B) )assume
S1[
x,
y,
z]
;
z in NatTrans (A,B)then consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A15:
y = [[F,F1],t]
and A16:
x = [[F1,F2],t1]
and A17:
z = [[F,F2],(t1 `*` t)]
;
A18:
F1 is_naturally_transformable_to F2
by A13, A16, Th28;
F is_naturally_transformable_to F1
by A14, A15, Th28;
hence
z in NatTrans (
A,
B)
by A17, Th28, A18, Th19;
verum end;
consider m being PartFunc of [:(NatTrans (A,B)),(NatTrans (A,B)):],(NatTrans (A,B)) such that
A19:
for x, y being object holds
( [x,y] in dom m iff ( x in NatTrans (A,B) & y in NatTrans (A,B) & ex z being object st S1[x,y,z] ) )
and
A20:
for x, y being object st [x,y] in dom m holds
S1[x,y,m . (x,y)]
from BINOP_1:sch 5(A12, A1);
A21:
now for t being Element of NatTrans (A,B) holds H1(t) in Funct (A,B)let t be
Element of
NatTrans (
A,
B);
H1(t) in Funct (A,B)consider F1,
F2 being
Functor of
A,
B,
s being
natural_transformation of
F1,
F2 such that A22:
t = [[F1,F2],s]
and
F1 is_naturally_transformable_to F2
by Def15;
(t `1) `1 =
[F1,F2] `1
by A22
.=
F1
;
hence
H1(
t)
in Funct (
A,
B)
by CAT_2:def 2;
verum end;
consider d being Function of (NatTrans (A,B)),(Funct (A,B)) such that
A23:
for t being Element of NatTrans (A,B) holds d . t = H1(t)
from FUNCT_2:sch 8(A21);
deffunc H2( set ) -> object = ($1 `1) `2 ;
A24:
now for t being Element of NatTrans (A,B) holds H2(t) in Funct (A,B)let t be
Element of
NatTrans (
A,
B);
H2(t) in Funct (A,B)consider F1,
F2 being
Functor of
A,
B,
s being
natural_transformation of
F1,
F2 such that A25:
t = [[F1,F2],s]
and
F1 is_naturally_transformable_to F2
by Def15;
(t `1) `2 =
[F1,F2] `2
by A25
.=
F2
;
hence
H2(
t)
in Funct (
A,
B)
by CAT_2:def 2;
verum end;
consider c being Function of (NatTrans (A,B)),(Funct (A,B)) such that
A26:
for t being Element of NatTrans (A,B) holds c . t = H2(t)
from FUNCT_2:sch 8(A24);
deffunc H3( Element of Funct (A,B)) -> object = [[$1,$1],(id $1)];
A27:
for F being Element of Funct (A,B) holds H3(F) in NatTrans (A,B)
by Def15;
consider i being Function of (Funct (A,B)),(NatTrans (A,B)) such that
A28:
for F being Element of Funct (A,B) holds i . F = H3(F)
from FUNCT_2:sch 8(A27);
set C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #);
A29:
now for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]let F,
F1,
F2 be
Functor of
A,
B;
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]let t be
natural_transformation of
F,
F1;
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]let t1 be
natural_transformation of
F1,
F2;
( F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 implies m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] )assume that A30:
F1 is_naturally_transformable_to F2
and A31:
F is_naturally_transformable_to F1
;
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]A32:
[[F,F1],t] in NatTrans (
A,
B)
by A31, Th28;
A33:
S1[
[[F1,F2],t1],
[[F,F1],t],
[[F,F2],(t1 `*` t)]]
;
[[F1,F2],t1] in NatTrans (
A,
B)
by A30, Th28;
then consider F9,
F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F9,
F19,
t19 being
natural_transformation of
F19,
F29 such that A34:
[[F,F1],t] = [[F9,F19],t9]
and A35:
[[F1,F2],t1] = [[F19,F29],t19]
and A36:
m . (
[[F1,F2],t1],
[[F,F1],t])
= [[F9,F29],(t19 `*` t9)]
by A20, A19, A32, A33;
A37:
t = t9
by A34, XTUPLE_0:1;
[F1,F2] = [F19,F29]
by A35, XTUPLE_0:1;
then A38:
F2 = F29
by XTUPLE_0:1;
A39:
t1 = t19
by A35, XTUPLE_0:1;
A40:
[F,F1] = [F9,F19]
by A34, XTUPLE_0:1;
then
F = F9
by XTUPLE_0:1;
hence
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
by A36, A40, A37, A39, A38, XTUPLE_0:1;
verum end;
A41:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is Category-like
proof
let f,
g be
Element of the
carrier' of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
CAT_1:def 6 ( ( not [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ) )
consider F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F19,
F29 such that A42:
f = [[F19,F29],t9]
and A43:
F19 is_naturally_transformable_to F29
by Def15;
thus
(
[g,f] in dom the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #) implies
dom g = cod f )
( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) )proof
assume
[g,f] in dom the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
;
dom g = cod f
then consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A44:
f = [[F,F1],t]
and A45:
g = [[F1,F2],t1]
and
m . (
g,
f)
= [[F,F2],(t1 `*` t)]
by A20;
thus dom g =
(g `1) `1
by A23
.=
[F1,F2] `1
by A45
.=
[F,F1] `2
.=
(f `1) `2
by A44
.=
cod f
by A26
;
verum
end;
assume A46:
dom g = cod f
;
[g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A47:
g = [[F1,F2],t]
and A48:
F1 is_naturally_transformable_to F2
by Def15;
A49:
F1 =
[F1,F2] `1
.=
(g `1) `1
by A47
.=
c . f
by A23, A46
.=
(f `1) `2
by A26
.=
[F19,F29] `2
by A42
.=
F29
;
then reconsider t =
t as
natural_transformation of
F29,
F2 ;
m . [g,f] = [[F19,F2],(t `*` t9)]
by A29, A47, A48, A42, A43, A49;
hence
[g,f] in proj1 the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
by A19, A47, A42, A49;
verum
end;
A50:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is transitive
proof
let f,
g be
Element of the
carrier' of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
CAT_1:def 7 ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
consider F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F19,
F29 such that A51:
f = [[F19,F29],t9]
and A52:
F19 is_naturally_transformable_to F29
by Def15;
assume
dom g = cod f
;
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
then A53:
[g,f] in dom m
by A41;
then consider F,
F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F,
F1,
t1 being
natural_transformation of
F1,
F2 such that A54:
f = [[F,F1],t]
and A55:
g = [[F1,F2],t1]
and A56:
m . (
g,
f)
= [[F,F2],(t1 `*` t)]
by A20;
A57:
m . (
g,
f)
= g (*) f
by A53, CAT_1:def 1;
A58:
[F,F1] = [F19,F29]
by A54, A51, XTUPLE_0:1;
then A59:
F = F19
by XTUPLE_0:1;
A60:
F1 = F29
by A58, XTUPLE_0:1;
consider F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F19,
F29 such that A61:
g = [[F19,F29],t9]
and A62:
F19 is_naturally_transformable_to F29
by Def15;
A63:
[F1,F2] = [F19,F29]
by A55, A61, XTUPLE_0:1;
then A64:
F2 = F29
by XTUPLE_0:1;
F1 = F19
by A63, XTUPLE_0:1;
then reconsider x =
[[F,F2],(t1 `*` t)] as
Element of
NatTrans (
A,
B)
by Th28, A52, A59, A60, A62, A64, Th19;
thus dom (g (*) f) =
(x `1) `1
by A23, A56, A57
.=
[F,F2] `1
.=
([[F,F1],t] `1) `1
.=
dom f
by A23, A54
;
cod (g (*) f) = cod g
thus cod (g (*) f) =
(x `1) `2
by A26, A56, A57
.=
[F,F2] `2
.=
([[F1,F2],t1] `1) `2
.=
cod g
by A26, A55
;
verum
end;
A65:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is associative
proof
A66:
for
f,
g being
Element of the
carrier' of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #) holds
(
[g,f] in dom the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #) iff
dom g = cod f )
by A41;
let f,
g,
h be
Element of the
carrier' of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
CAT_1:def 8 ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
reconsider f9 =
f,
g9 =
g,
h9 =
h as
Element of
NatTrans (
A,
B) ;
assume that A67:
dom h = cod g
and A68:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
[g9,f9] in dom m
by A41, A68;
then consider F1,
F19,
F2 being
Functor of
A,
B,
t1 being
natural_transformation of
F1,
F19,
t2 being
natural_transformation of
F19,
F2 such that A69:
f9 = [[F1,F19],t1]
and A70:
g9 = [[F19,F2],t2]
and A71:
m . (
g9,
f9)
= [[F1,F2],(t2 `*` t1)]
by A20;
[h9,g9] in dom m
by A41, A67;
then consider F29,
F3,
F39 being
Functor of
A,
B,
t29 being
natural_transformation of
F29,
F3,
t3 being
natural_transformation of
F3,
F39 such that A72:
g9 = [[F29,F3],t29]
and A73:
h9 = [[F3,F39],t3]
and
m . (
h9,
g9)
= [[F29,F39],(t3 `*` t29)]
by A20;
A74:
[F29,F3] = [F19,F2]
by A70, A72, XTUPLE_0:1;
then A75:
g9 = [[F19,F3],t2]
by A70, XTUPLE_0:1;
reconsider t2 =
t2 as
natural_transformation of
F19,
F3 by A74, XTUPLE_0:1;
A76:
F2 = F3
by A74, XTUPLE_0:1;
then A77:
F19 is_naturally_transformable_to F3
by A70, Th28;
A78:
F3 is_naturally_transformable_to F39
by A73, Th28;
then A79:
F19 is_naturally_transformable_to F39
by A77, Th19;
A80:
F1 is_naturally_transformable_to F19
by A69, Th28;
then A81:
F1 is_naturally_transformable_to F3
by A77, Th19;
A82:
h (*) g = the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
. (
h,
g)
by A66, A67, CAT_1:def 1;
A83:
dom (h (*) g) = dom g
by A50, A67;
A84:
g (*) f = the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
. (
g,
f)
by A66, A68, CAT_1:def 1;
cod (g (*) f) = cod g
by A50, A68;
hence h (*) (g (*) f) =
the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
. (
h,
( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f)))
by A84, A66, A67, CAT_1:def 1
.=
[[F1,F39],(t3 `*` (t2 `*` t1))]
by A29, A71, A73, A76, A78, A81
.=
[[F1,F39],((t3 `*` t2) `*` t1)]
by A80, A77, A78, Th22
.=
m . [[[F19,F39],(t3 `*` t2)],f9]
by A29, A69, A80, A79
.=
the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
. (
( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g)),
f)
by A29, A73, A75, A77, A78
.=
(h (*) g) (*) f
by A83, A82, A66, A68, CAT_1:def 1
;
verum
end;
A85:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is reflexive
proof
let b be
Element of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
CAT_1:def 9 not Hom (b,b) = {}
reconsider F =
b as
Functor of
A,
B by CAT_2:def 2;
reconsider s =
[[F,F],(id F)] as
Element of
NatTrans (
A,
B)
by Def15;
reconsider s =
s as
Morphism of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #) ;
A86:
dom s =
([[F,F],(id F)] `1) `1
by A23
.=
F
;
cod s =
([[F,F],(id F)] `1) `2
by A26
.=
F
;
then
s in Hom (
b,
b)
by A86;
hence
Hom (
b,
b)
<> {}
;
verum
end;
A87:
for a being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
for F being Functor of A,B st a = F holds
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
proof
let a be
Object of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
for F being Functor of A,B st a = F holds
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )let F be
Functor of
A,
B;
( a = F implies for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) )
assume A88:
a = F
;
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let ii be
Morphism of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
( ii = [[F,F],(id F)] implies for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) )
assume A89:
ii = [[F,F],(id F)]
;
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
let b be
Object of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
reconsider s =
[[F,F],(id F)] as
Element of
NatTrans (
A,
B)
by Def15;
A90:
F in Funct (
A,
B)
by CAT_2:def 2;
then A91:
i . F = [[F,F],(id F)]
by A28;
thus
(
Hom (
a,
b)
<> {} implies for
f being
Morphism of
a,
b holds
f (*) ii = f )
( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )proof
assume A92:
Hom (
a,
b)
<> {}
;
for f being Morphism of a,b holds f (*) ii = f
let f be
Morphism of
a,
b;
f (*) ii = f
reconsider f9 =
f as
Element of
NatTrans (
A,
B) ;
A93:
dom f = a
by A92, CAT_1:5;
consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A94:
f9 = [[F1,F2],t]
and
F1 is_naturally_transformable_to F2
by Def15;
A95:
F1 =
[F1,F2] `1
.=
(f9 `1) `1
by A94
.=
dom f
by A23
.=
F
by A92, A88, CAT_1:5
;
then reconsider t =
t as
natural_transformation of
F,
F2 ;
S1[
f9,
s,
[[F,F2],(t `*` (id F))]]
by A94, A95;
then consider F9,
F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F9,
F19,
t19 being
natural_transformation of
F19,
F29 such that A96:
i . F = [[F9,F19],t9]
and A97:
f9 = [[F19,F29],t19]
and A98:
m . (
f9,
(i . F))
= [[F9,F29],(t19 `*` t9)]
by A20, A91, A19;
A99:
[F9,F19] = [F,F]
by A96, A91, XTUPLE_0:1;
then A100:
F9 = F
by XTUPLE_0:1;
A101:
F19 = F
by A99, XTUPLE_0:1;
A102:
F19 is_naturally_transformable_to F29
by A97, Th28;
A103:
F29 =
([[F19,F29],t19] `1) `2
.=
([[F1,F2],t] `1) `2
by A97, A94
.=
F2
;
A104:
t19 =
[[F19,F29],t19] `2
.=
[[F1,F2],t] `2
by A97, A94
.=
t
;
A105:
t19 `*` (id F19) = t19
by Th20, A102;
cod ii =
([[F,F],(id F)] `1) `2
by A89, A26
.=
a
by A88
;
then
[f,ii] in dom the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
by A41, A93;
hence f (*) ii =
m . (
f,
ii)
by CAT_1:def 1
.=
f
by A104, A105, A95, A103, A96, A91, A100, A101, A98, A89, A94, XTUPLE_0:1
;
verum
end;
assume A106:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds ii (*) f = f
let f be
Morphism of
b,
a;
ii (*) f = f
reconsider f9 =
f as
Element of
NatTrans (
A,
B) ;
A107:
cod f = a
by A106, CAT_1:5;
consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A108:
f9 = [[F1,F2],t]
and
F1 is_naturally_transformable_to F2
by Def15;
A109:
F2 =
[F1,F2] `2
.=
(f9 `1) `2
by A108
.=
cod f
by A26
.=
F
by A106, A88, CAT_1:5
;
then reconsider t =
t as
natural_transformation of
F1,
F ;
S1[
s,
f9,
[[F1,F],((id F) `*` t)]]
by A108, A109;
then consider F9,
F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F9,
F19,
t19 being
natural_transformation of
F19,
F29 such that A110:
f9 = [[F9,F19],t9]
and A111:
i . F = [[F19,F29],t19]
and A112:
m . (
(i . F),
f9)
= [[F9,F29],(t19 `*` t9)]
by A20, A91, A19;
A113:
t19 = id F
by A111, A91, XTUPLE_0:1;
A114:
[F19,F29] = [F,F]
by A111, A91, XTUPLE_0:1;
then A115:
F19 = F
by XTUPLE_0:1;
A116:
F9 is_naturally_transformable_to F19
by A110, Th28;
A117:
F9 =
([[F9,F19],t9] `1) `1
.=
([[F1,F2],t] `1) `1
by A110, A108
.=
F1
;
A118:
t9 =
[[F9,F19],t9] `2
.=
[[F1,F2],t] `2
by A110, A108
.=
t
;
A119:
(id F19) `*` t9 = t9
by Th20, A116;
dom ii =
([[F,F],(id F)] `1) `1
by A89, A23
.=
a
by A88
;
then
[ii,f] in dom the
Comp of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #)
by A41, A107;
hence ii (*) f =
m . (
ii,
f)
by CAT_1:def 1
.=
m . (
(i . F),
f9)
by A89, A90, A28
.=
[[F9,F29],((id F19) `*` t9)]
by A113, A115, A114, A112, XTUPLE_0:1
.=
f
by A108, A118, A119, A114, A109, A117, XTUPLE_0:1
;
verum
end;
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is with_identities
proof
let a be
Element of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #);
CAT_1:def 10 ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) 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 ) )
reconsider F =
a as
Functor of
A,
B by CAT_2:def 2;
reconsider s =
[[F,F],(id F)] as
Element of
NatTrans (
A,
B)
by Def15;
reconsider s =
s as
Morphism of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #) ;
A120:
dom s =
([[F,F],(id F)] `1) `1
by A23
.=
F
;
cod s =
([[F,F],(id F)] `1) `2
by A26
.=
F
;
then
s in Hom (
a,
a)
by A120;
then reconsider s =
s as
Morphism of
a,
a by CAT_1:def 5;
take
s
;
for b1 being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) s = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds s (*) b2 = b2 ) )
thus
for
b1 being
Element of the
carrier of
CatStr(#
(Funct (A,B)),
(NatTrans (A,B)),
d,
c,
m #) holds
( (
Hom (
a,
b1)
= {} or for
b2 being
Morphism of
a,
b1 holds
b2 (*) s = b2 ) & (
Hom (
b1,
a)
= {} or for
b2 being
Morphism of
b1,
a holds
s (*) b2 = b2 ) )
by A87;
verum
end;
then reconsider C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) as strict Category by A41, A50, A65, A85;
take
C
; ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) & ( for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus
( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) )
; ( ( for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus
for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 )
by A23, A26; ( ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus
for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C
( ( for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )proof
let f,
g be
Morphism of
C;
( dom g = cod f implies [g,f] in dom the Comp of C )
assume A121:
dom g = cod f
;
[g,f] in dom the Comp of C
consider F19,
F29 being
Functor of
A,
B,
t9 being
natural_transformation of
F19,
F29 such that A122:
g = [[F19,F29],t9]
and
F19 is_naturally_transformable_to F29
by Def15;
consider F1,
F2 being
Functor of
A,
B,
t being
natural_transformation of
F1,
F2 such that A123:
f = [[F1,F2],t]
and
F1 is_naturally_transformable_to F2
by Def15;
A124:
F2 =
([[F1,F2],t] `1) `2
.=
cod f
by A26, A123
.=
([[F19,F29],t9] `1) `1
by A23, A122, A121
.=
F19
;
then reconsider t9 =
t9 as
natural_transformation of
F2,
F29 ;
S1[
g,
f,
[[F1,F29],(t9 `*` t)]]
by A123, A122, A124;
hence
[g,f] in dom the
Comp of
C
by A19;
verum
end;
thus
for f, g being Morphism of C st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] )
for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]proof
let f,
g be
Morphism of
C;
( [g,f] in dom the Comp of C implies ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) )
assume
[g,f] in dom the
Comp of
C
;
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] )
then
ex
F,
F1,
F2 being
Functor of
A,
B ex
t being
natural_transformation of
F,
F1 ex
t1 being
natural_transformation of
F1,
F2 st
(
f = [[F,F1],t] &
g = [[F1,F2],t1] & the
Comp of
C . (
g,
f)
= [[F,F2],(t1 `*` t)] )
by A20;
hence
ex
F,
F1,
F2 being
Functor of
A,
B ex
t being
natural_transformation of
F,
F1 ex
t1 being
natural_transformation of
F1,
F2 st
(
f = [[F,F1],t] &
g = [[F1,F2],t1] & the
Comp of
C . [g,f] = [[F,F2],(t1 `*` t)] )
;
verum
end;
let a be Object of C; for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
let F be Functor of A,B; ( F = a implies id a = [[F,F],(id F)] )
assume A125:
a = F
; id a = [[F,F],(id F)]
reconsider m = [[F,F],(id F)] as Element of NatTrans (A,B) by Def15;
reconsider m = m as Morphism of C ;
A126: dom m =
([[F,F],(id F)] `1) `1
by A23
.=
F
;
cod m =
([[F,F],(id F)] `1) `2
by A26
.=
F
;
then
m in Hom (a,a)
by A125, A126;
then reconsider m = m as Morphism of a,a by CAT_1:def 5;
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
by A125, A87;
hence
id a = [[F,F],(id F)]
by CAT_1:def 12; verum