deffunc H1( Element of the carrier' of A) -> object = [[<|(cod $1),?>,<|(dom $1),?>],<|$1,?>];
A1:
for f being Element of the carrier' of A holds H1(f) in the carrier' of (Functors (A,(EnsHom A)))
consider F being Function of the carrier' of A, the carrier' of (Functors (A,(EnsHom A))) such that
A2:
for f being Element of the carrier' of A holds F . f = H1(f)
from FUNCT_2:sch 8(A1);
A3:
for f, g being Morphism of A st dom g = cod f holds
F . (g (*) f) = (F . f) (*) (F . g)
proof
let f,
g be
Morphism of
A;
( dom g = cod f implies F . (g (*) f) = (F . f) (*) (F . g) )
reconsider t1 =
<|g,?> as
natural_transformation of
<|(cod g),?>,
<|(dom g),?> ;
assume A4:
dom g = cod f
;
F . (g (*) f) = (F . f) (*) (F . g)
then reconsider t =
<|f,?> as
natural_transformation of
<|(dom g),?>,
<|(dom f),?> ;
A5:
F . g = [[<|(cod g),?>,<|(dom g),?>],t1]
by A2;
A6:
dom (g (*) f) = dom f
by A4, CAT_1:17;
then reconsider tt =
t `*` t1 as
natural_transformation of
<|(cod (g (*) f)),?>,
<|(dom (g (*) f)),?> by A4, CAT_1:17;
A7:
cod (g (*) f) = cod g
by A4, CAT_1:17;
for
o being
Object of
A holds
<|(g (*) f),?> . o = tt . o
proof
set F1 =
<|(cod f),?>;
set F2 =
<|(dom f),?>;
let o be
Object of
A;
<|(g (*) f),?> . o = tt . o
reconsider f1 =
t . o as
Morphism of
(EnsHom A) ;
reconsider f2 =
t1 . o as
Morphism of
(EnsHom A) ;
A8:
f2 = [[(Hom ((cod g),o)),(Hom ((dom g),o))],(hom (g,(id o)))]
by Def3;
for
a being
Object of
A holds
[[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom (
(<|(cod g),?> . a),
(<|(dom g),?> . a))
proof
let a be
Object of
A;
[[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a))
A9:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)) #)
by ENS_1:def 13;
then reconsider m =
[[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] as
Morphism of
(EnsHom A) by ENS_1:48;
reconsider m9 =
m as
Element of
Maps (Hom A) by ENS_1:48;
A10:
cod m =
(fCod (Hom A)) . m
by A9
.=
cod m9
by ENS_1:def 10
.=
(m `1) `2
by ENS_1:def 4
.=
[(Hom ((cod g),a)),(Hom ((dom g),a))] `2
.=
Hom (
(dom g),
a)
.=
(Obj (hom?- ((Hom A),(dom g)))) . a
by ENS_1:60
.=
(hom?- ((Hom A),(dom g))) . a
.=
<|(dom g),?> . a
by ENS_1:def 25
;
dom m =
(fDom (Hom A)) . m
by A9
.=
dom m9
by ENS_1:def 9
.=
(m `1) `1
by ENS_1:def 3
.=
[(Hom ((cod g),a)),(Hom ((dom g),a))] `1
.=
Hom (
(cod g),
a)
.=
(Obj (hom?- ((Hom A),(cod g)))) . a
by ENS_1:60
.=
(hom?- ((Hom A),(cod g))) . a
.=
<|(cod g),?> . a
by ENS_1:def 25
;
hence
[[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom (
(<|(cod g),?> . a),
(<|(dom g),?> . a))
by A10;
verum
end;
then A11:
Hom (
(<|(cod g),?> . o),
(<|(dom g),?> . o))
<> {}
;
for
a being
Object of
A holds
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom (
(<|(cod f),?> . a),
(<|(dom f),?> . a))
proof
let a be
Object of
A;
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a))
A12:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)) #)
by ENS_1:def 13;
then reconsider m =
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] as
Morphism of
(EnsHom A) by ENS_1:48;
reconsider m9 =
m as
Element of
Maps (Hom A) by ENS_1:48;
A13:
cod m =
(fCod (Hom A)) . m
by A12
.=
cod m9
by ENS_1:def 10
.=
(m `1) `2
by ENS_1:def 4
.=
[(Hom ((cod f),a)),(Hom ((dom f),a))] `2
.=
Hom (
(dom f),
a)
.=
(Obj (hom?- ((Hom A),(dom f)))) . a
by ENS_1:60
.=
(hom?- ((Hom A),(dom f))) . a
.=
<|(dom f),?> . a
by ENS_1:def 25
;
dom m =
(fDom (Hom A)) . m
by A12
.=
dom m9
by ENS_1:def 9
.=
(m `1) `1
by ENS_1:def 3
.=
[(Hom ((cod f),a)),(Hom ((dom f),a))] `1
.=
Hom (
(cod f),
a)
.=
(Obj (hom?- ((Hom A),(cod f)))) . a
by ENS_1:60
.=
(hom?- ((Hom A),(cod f))) . a
.=
<|(cod f),?> . a
by ENS_1:def 25
;
hence
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom (
(<|(cod f),?> . a),
(<|(dom f),?> . a))
by A13;
verum
end;
then A14:
Hom (
(<|(cod f),?> . o),
(<|(dom f),?> . o))
<> {}
;
A15:
<|(g (*) f),?> . o =
[[(Hom ((cod g),o)),(Hom ((dom (g (*) f)),o))],(hom ((g (*) f),(id o)))]
by A7, Def3
.=
[[(Hom ((cod g),o)),(Hom ((dom f),o))],(hom ((g (*) f),o))]
by A6, ENS_1:53
;
A16:
t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
by A4, Def3;
A17:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)) #)
by ENS_1:def 13;
then reconsider f19 =
f1 as
Element of
Maps (Hom A) ;
reconsider f29 =
f2 as
Element of
Maps (Hom A) by A17;
A18:
cod f2 =
(fCod (Hom A)) . f2
by A17
.=
cod f29
by ENS_1:def 10
.=
(f2 `1) `2
by ENS_1:def 4
.=
[(Hom ((cod g),o)),(Hom ((dom g),o))] `2
by A8
.=
Hom (
(dom g),
o)
;
A19:
cod f1 =
(fCod (Hom A)) . f1
by A17
.=
cod f19
by ENS_1:def 10
.=
(f1 `1) `2
by ENS_1:def 4
.=
[(Hom ((cod f),o)),(Hom ((dom f),o))] `2
by A16
.=
Hom (
(dom f),
o)
;
A20:
dom f1 =
(fDom (Hom A)) . f1
by A17
.=
dom f19
by ENS_1:def 9
.=
(f1 `1) `1
by ENS_1:def 3
.=
[(Hom ((cod f),o)),(Hom ((dom f),o))] `1
by A16
.=
Hom (
(cod f),
o)
;
A21:
dom f2 =
(fDom (Hom A)) . f2
by A17
.=
dom f29
by ENS_1:def 9
.=
(f2 `1) `1
by ENS_1:def 3
.=
[(Hom ((cod g),o)),(Hom ((dom g),o))] `1
by A8
.=
Hom (
(cod g),
o)
;
(
<|(dom g),?> is_naturally_transformable_to <|(dom f),?> &
<|(cod g),?> is_naturally_transformable_to <|(dom g),?> )
by A4, Th2;
then tt . o =
(t . o) * (t1 . o)
by A6, A7, NATTRA_1:25
.=
f1 (*) f2
by A4, A14, A11, CAT_1:def 13
.=
[[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,(id o))) * (hom (g,(id o))))]
by A4, A16, A8, A20, A18, A21, A19, Th1
.=
[[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,o)) * (hom (g,(id o))))]
by ENS_1:53
.=
[[(Hom ((cod g),o)),(Hom ((dom f),o))],((hom (f,o)) * (hom (g,o)))]
by ENS_1:53
.=
[[(Hom ((cod g),o)),(Hom ((dom f),o))],(hom ((g (*) f),o))]
by A4, ENS_1:46
;
hence
<|(g (*) f),?> . o = tt . o
by A15;
verum
end;
then A22:
<|(g (*) f),?> = tt
by Th2, ISOCAT_1:26;
A23:
F . f = [[<|(dom g),?>,<|(dom f),?>],t]
by A2, A4;
then A24:
[(F . f),(F . g)] in dom the
Comp of
(Functors (A,(EnsHom A)))
by A5, NATTRA_1:35;
then consider F9,
F19,
F29 being
Functor of
A,
EnsHom A,
t9 being
natural_transformation of
F9,
F19,
t19 being
natural_transformation of
F19,
F29 such that A25:
F . g = [[F9,F19],t9]
and A26:
F . f = [[F19,F29],t19]
and A27:
the
Comp of
(Functors (A,(EnsHom A))) . (
(F . f),
(F . g))
= [[F9,F29],(t19 `*` t9)]
by NATTRA_1:def 17;
A28:
<|f,?> = t19
by A23, A26, XTUPLE_0:1;
[F19,F29] = [<|(dom g),?>,<|(dom f),?>]
by A23, A26, XTUPLE_0:1;
then A29:
<|(dom f),?> = F29
by XTUPLE_0:1;
[F9,F19] = [<|(cod g),?>,<|(dom g),?>]
by A5, A25, XTUPLE_0:1;
then A30:
(
<|(cod g),?> = F9 &
<|(dom g),?> = F19 )
by XTUPLE_0:1;
<|g,?> = t9
by A5, A25, XTUPLE_0:1;
then
(F . f) (*) (F . g) = [[<|(cod g),?>,<|(dom f),?>],(t `*` t1)]
by A24, A27, A28, A30, A29, CAT_1:def 1;
hence
F . (g (*) f) = (F . f) (*) (F . g)
by A2, A6, A7, A22;
verum
end;
A31:
for f being Morphism of A holds
( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )
proof
let f be
Morphism of
A;
( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )
set g =
F . f;
set X =
dom <|(id (dom f)),?>;
A32:
dom <|(id (dom f)),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|(dom f),?>)
by FUNCT_2:def 1
;
A33:
F . (id (dom f)) =
[[<|(cod (id (dom f))),?>,<|(dom (id (dom f))),?>],<|(id (dom f)),?>]
by A2
.=
[[<|(dom f),?>,<|(dom (id (dom f))),?>],<|(id (dom f)),?>]
.=
[[<|(dom f),?>,<|(dom f),?>],<|(id (dom f)),?>]
;
A34:
F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
by A2;
then
cod (F . f) = <|(dom f),?>
by NATTRA_1:33;
then A35:
[[<|(dom f),?>,<|(dom f),?>],(id <|(dom f),?>)] = id (cod (F . f))
by NATTRA_1:def 17;
A36:
for
y being
object st
y in dom <|(id (dom f)),?> holds
<|(id (dom f)),?> . y = (id <|(dom f),?>) . y
proof
let y be
object ;
( y in dom <|(id (dom f)),?> implies <|(id (dom f)),?> . y = (id <|(dom f),?>) . y )
assume
y in dom <|(id (dom f)),?>
;
<|(id (dom f)),?> . y = (id <|(dom f),?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
reconsider zz =
id z as
Morphism of
z,
z ;
A37:
Hom (
z,
z)
<> {}
;
<|(id (dom f)),?> . z =
[[(Hom ((cod (id (dom f))),z)),(Hom ((dom (id (dom f))),z))],(hom ((id (dom f)),(id z)))]
by Def3
.=
[[(Hom ((dom f),z)),(Hom ((dom (id (dom f))),z))],(hom ((id (dom f)),(id z)))]
.=
[[(Hom ((dom f),z)),(Hom ((dom f),z))],(hom ((id (dom f)),(id z)))]
.=
[[(Hom ((dom f),z)),(Hom ((dom f),z))],(hom ((dom f),(id z)))]
by ENS_1:53
.=
[[(Hom ((dom f),z)),(Hom ((dom f),(cod (id z))))],(hom ((dom f),(id z)))]
.=
[[(Hom ((dom f),(dom (id z)))),(Hom ((dom f),(cod (id z))))],(hom ((dom f),(id z)))]
.=
<|(dom f),?> . (id z)
by ENS_1:def 21
.=
<|(dom f),?> /. zz
by A37, CAT_3:def 10
.=
id (<|(dom f),?> . z)
by NATTRA_1:15
.=
(id <|(dom f),?>) . z
by NATTRA_1:20
.=
(id <|(dom f),?>) . z
by NATTRA_1:def 5
;
hence
<|(id (dom f)),?> . y = (id <|(dom f),?>) . y
by NATTRA_1:def 5;
verum
end;
set X =
dom <|(id (cod f)),?>;
A38:
for
y being
object st
y in dom <|(id (cod f)),?> holds
<|(id (cod f)),?> . y = (id <|(cod f),?>) . y
proof
let y be
object ;
( y in dom <|(id (cod f)),?> implies <|(id (cod f)),?> . y = (id <|(cod f),?>) . y )
assume
y in dom <|(id (cod f)),?>
;
<|(id (cod f)),?> . y = (id <|(cod f),?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
A39:
Hom (
z,
z)
<> {}
;
<|(id (cod f)),?> . z =
[[(Hom ((cod (id (cod f))),z)),(Hom ((dom (id (cod f))),z))],(hom ((id (cod f)),(id z)))]
by Def3
.=
[[(Hom ((cod f),z)),(Hom ((dom (id (cod f))),z))],(hom ((id (cod f)),(id z)))]
.=
[[(Hom ((cod f),z)),(Hom ((cod f),z))],(hom ((id (cod f)),(id z)))]
.=
[[(Hom ((cod f),z)),(Hom ((cod f),z))],(hom ((cod f),(id z)))]
by ENS_1:53
.=
[[(Hom ((cod f),z)),(Hom ((cod f),(cod (id z))))],(hom ((cod f),(id z)))]
.=
[[(Hom ((cod f),(dom (id z)))),(Hom ((cod f),(cod (id z))))],(hom ((cod f),(id z)))]
.=
<|(cod f),?> . (id z)
by ENS_1:def 21
.=
<|(cod f),?> /. (id z)
by A39, CAT_3:def 10
.=
id (<|(cod f),?> . z)
by NATTRA_1:15
.=
(id <|(cod f),?>) . z
by NATTRA_1:20
.=
(id <|(cod f),?>) . z
by NATTRA_1:def 5
;
hence
<|(id (cod f)),?> . y = (id <|(cod f),?>) . y
by NATTRA_1:def 5;
verum
end;
dom <|(id (cod f)),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|(cod f),?>)
by FUNCT_2:def 1
;
then A40:
<|(id (cod f)),?> = id <|(cod f),?>
by A38, FUNCT_1:2;
A41:
F . (id (cod f)) =
[[<|(cod (id (cod f))),?>,<|(dom (id (cod f))),?>],<|(id (cod f)),?>]
by A2
.=
[[<|(cod f),?>,<|(dom (id (cod f))),?>],<|(id (cod f)),?>]
.=
[[<|(cod f),?>,<|(cod f),?>],<|(id (cod f)),?>]
;
dom (F . f) = <|(cod f),?>
by A34, NATTRA_1:33;
hence
(
F . (id (dom f)) = id (cod (F . f)) &
F . (id (cod f)) = id (dom (F . f)) )
by A33, A35, A32, A36, A41, A40, FUNCT_1:2, NATTRA_1:def 17;
verum
end;
for c being Object of A ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d
proof
let c be
Object of
A;
ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d
set X =
dom <|(id c),?>;
<|c,?> in Funct (
A,
(EnsHom A))
by CAT_2:def 2;
then reconsider d =
<|c,?> as
Object of
(Functors (A,(EnsHom A))) by NATTRA_1:def 17;
take
d
;
F . (id c) = id d
A42:
for
y being
object st
y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be
object ;
( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume
y in dom <|(id c),?>
;
<|(id c),?> . y = (id <|c,?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
reconsider zz =
id z as
Morphism of
z,
z ;
A43:
Hom (
z,
z)
<> {}
;
<|(id c),?> . z =
[[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]
by Def3
.=
[[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]
.=
[[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
.=
[[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))]
by ENS_1:53
.=
[[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.=
[[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.=
<|c,?> . (id z)
by ENS_1:def 21
.=
<|c,?> /. zz
by A43, CAT_3:def 10
.=
id (<|c,?> . z)
by NATTRA_1:15
.=
(id <|c,?>) . z
by NATTRA_1:20
.=
(id <|c,?>) . z
by NATTRA_1:def 5
;
hence
<|(id c),?> . y = (id <|c,?>) . y
by NATTRA_1:def 5;
verum
end;
dom <|(id c),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|c,?>)
by FUNCT_2:def 1
;
then A44:
<|(id c),?> = id <|c,?>
by A42, FUNCT_1:2;
F . (id c) =
[[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>]
by A2
.=
[[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]
.=
[[<|c,?>,<|c,?>],(id <|c,?>)]
by A44
.=
id d
by NATTRA_1:def 17
;
hence
F . (id c) = id d
;
verum
end;
then reconsider F = F as Contravariant_Functor of A, Functors (A,(EnsHom A)) by A31, A3, OPPCAT_1:def 9;
for f being Element of the carrier' of A holds F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
by A2;
hence
ex b1 being Contravariant_Functor of A, Functors (A,(EnsHom A)) st
for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
; verum