deffunc H1( Element of the carrier' of A) -> set = [[<|(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 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;
:: thesis: ex d being Object of (Functors A,(EnsHom A)) st F . (id c) = id d
<|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 18;
take
d
;
:: thesis: F . (id c) = id d
set X =
dom <|(id c),?>;
A4:
dom <|(id c),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|c,?>)
by FUNCT_2:def 1
;
for
y being
set st
y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be
set ;
:: thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume
y in dom <|(id c),?>
;
:: thesis: <|(id c),?> . y = (id <|c,?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
<|(cod (id c)),?> is_transformable_to <|c,?>
by CAT_1:44;
then A5:
<|(cod (id c)),?> is_transformable_to <|(dom (id c)),?>
by CAT_1:44;
A6:
Hom z,
z <> {}
by CAT_1:56;
reconsider zz =
id z as
Morphism of
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))]
by CAT_1:44
.=
[[(Hom c,z),(Hom c,z)],(hom (id c),(id z))]
by CAT_1:44
.=
[[(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))]
by CAT_1:44
.=
[[(Hom c,(dom (id z))),(Hom c,(cod (id z)))],(hom c,(id z))]
by CAT_1:44
.=
<|c,?> . (id z)
by ENS_1:def 22
.=
<|c,?> . zz
by A6, NATTRA_1:def 1
.=
id (<|c,?> . z)
by NATTRA_1:15
.=
(id <|c,?>) . z
by NATTRA_1:21
.=
(id <|c,?>) . z
by NATTRA_1:def 5
;
hence
<|(id c),?> . y = (id <|c,?>) . y
by A5, NATTRA_1:def 5;
:: thesis: verum
end;
then A7:
<|(id c),?> = id <|c,?>
by A4, FUNCT_1:9;
F . (id c) =
[[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>]
by A2
.=
[[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]
by CAT_1:44
.=
[[<|c,?>,<|c,?>],(id <|c,?>)]
by A7, CAT_1:44
.=
id d
by NATTRA_1:def 18
;
hence
F . (id c) = id d
;
:: thesis: verum
end;
A8:
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;
:: thesis: ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )
set g =
F . f;
A9:
F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
by A2;
then A10:
cod (F . f) = <|(dom f),?>
by NATTRA_1:39;
A11:
dom (F . f) = <|(cod f),?>
by A9, NATTRA_1:39;
A12:
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)),?>]
by CAT_1:44
.=
[[<|(dom f),?>,<|(dom f),?>],<|(id (dom f)),?>]
by CAT_1:44
;
A13:
[[<|(dom f),?>,<|(dom f),?>],(id <|(dom f),?>)] = id (cod (F . f))
by A10, NATTRA_1:def 18;
set X =
dom <|(id (dom f)),?>;
A14:
dom <|(id (dom f)),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|(dom f),?>)
by FUNCT_2:def 1
;
A15:
for
y being
set st
y in dom <|(id (dom f)),?> holds
<|(id (dom f)),?> . y = (id <|(dom f),?>) . y
proof
let y be
set ;
:: thesis: ( y in dom <|(id (dom f)),?> implies <|(id (dom f)),?> . y = (id <|(dom f),?>) . y )
assume
y in dom <|(id (dom f)),?>
;
:: thesis: <|(id (dom f)),?> . y = (id <|(dom f),?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
<|(cod (id (dom f))),?> is_transformable_to <|(dom f),?>
by CAT_1:44;
then A16:
<|(cod (id (dom f))),?> is_transformable_to <|(dom (id (dom f))),?>
by CAT_1:44;
A17:
Hom z,
z <> {}
by CAT_1:56;
reconsider zz =
id z as
Morphism of
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))]
by CAT_1:44
.=
[[(Hom (dom f),z),(Hom (dom f),z)],(hom (id (dom f)),(id z))]
by CAT_1:44
.=
[[(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))]
by CAT_1:44
.=
[[(Hom (dom f),(dom (id z))),(Hom (dom f),(cod (id z)))],(hom (dom f),(id z))]
by CAT_1:44
.=
<|(dom f),?> . (id z)
by ENS_1:def 22
.=
<|(dom f),?> . zz
by A17, NATTRA_1:def 1
.=
id (<|(dom f),?> . z)
by NATTRA_1:15
.=
(id <|(dom f),?>) . z
by NATTRA_1:21
.=
(id <|(dom f),?>) . z
by NATTRA_1:def 5
;
hence
<|(id (dom f)),?> . y = (id <|(dom f),?>) . y
by A16, NATTRA_1:def 5;
:: thesis: verum
end;
A18:
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)),?>]
by CAT_1:44
.=
[[<|(cod f),?>,<|(cod f),?>],<|(id (cod f)),?>]
by CAT_1:44
;
set X =
dom <|(id (cod f)),?>;
A19:
dom <|(id (cod f)),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|(cod f),?>)
by FUNCT_2:def 1
;
for
y being
set st
y in dom <|(id (cod f)),?> holds
<|(id (cod f)),?> . y = (id <|(cod f),?>) . y
proof
let y be
set ;
:: thesis: ( y in dom <|(id (cod f)),?> implies <|(id (cod f)),?> . y = (id <|(cod f),?>) . y )
assume
y in dom <|(id (cod f)),?>
;
:: thesis: <|(id (cod f)),?> . y = (id <|(cod f),?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
<|(cod (id (cod f))),?> is_transformable_to <|(cod f),?>
by CAT_1:44;
then A20:
<|(cod (id (cod f))),?> is_transformable_to <|(dom (id (cod f))),?>
by CAT_1:44;
A21:
Hom z,
z <> {}
by CAT_1:56;
<|(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))]
by CAT_1:44
.=
[[(Hom (cod f),z),(Hom (cod f),z)],(hom (id (cod f)),(id z))]
by CAT_1:44
.=
[[(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))]
by CAT_1:44
.=
[[(Hom (cod f),(dom (id z))),(Hom (cod f),(cod (id z)))],(hom (cod f),(id z))]
by CAT_1:44
.=
<|(cod f),?> . (id z)
by ENS_1:def 22
.=
<|(cod f),?> . (id z)
by A21, NATTRA_1:def 1
.=
id (<|(cod f),?> . z)
by NATTRA_1:15
.=
(id <|(cod f),?>) . z
by NATTRA_1:21
.=
(id <|(cod f),?>) . z
by NATTRA_1:def 5
;
hence
<|(id (cod f)),?> . y = (id <|(cod f),?>) . y
by A20, NATTRA_1:def 5;
:: thesis: verum
end;
then
<|(id (cod f)),?> = id <|(cod f),?>
by A19, FUNCT_1:9;
hence
(
F . (id (dom f)) = id (cod (F . f)) &
F . (id (cod f)) = id (dom (F . f)) )
by A11, A12, A13, A14, A15, A18, FUNCT_1:9, NATTRA_1:def 18;
:: thesis: verum
end;
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;
:: thesis: ( dom g = cod f implies F . (g * f) = (F . f) * (F . g) )
assume A22:
dom g = cod f
;
:: thesis: F . (g * f) = (F . f) * (F . g)
then reconsider t =
<|f,?> as
natural_transformation of
<|(dom g),?>,
<|(dom f),?> ;
reconsider t1 =
<|g,?> as
natural_transformation of
<|(cod g),?>,
<|(dom g),?> ;
A23:
F . f = [[<|(dom g),?>,<|(dom f),?>],t]
by A2, A22;
A24:
F . g = [[<|(cod g),?>,<|(dom g),?>],t1]
by A2;
then A25:
[(F . f),(F . g)] in dom the
Comp of
(Functors A,(EnsHom A))
by A23, NATTRA_1:41;
then consider F',
F1',
F2' being
Functor of
A,
EnsHom A,
t' being
natural_transformation of
F',
F1',
t1' being
natural_transformation of
F1',
F2' such that A26:
(
F . g = [[F',F1'],t'] &
F . f = [[F1',F2'],t1'] )
and A27:
the
Comp of
(Functors A,(EnsHom A)) . (F . f),
(F . g) = [[F',F2'],(t1' `*` t')]
by NATTRA_1:def 18;
A28:
(
[F',F1'] = [<|(cod g),?>,<|(dom g),?>] &
[F1',F2'] = [<|(dom g),?>,<|(dom f),?>] &
<|g,?> = t' &
<|f,?> = t1' )
by A23, A24, A26, ZFMISC_1:33;
then
(
<|(cod g),?> = F' &
<|(dom g),?> = F1' &
<|(dom f),?> = F2' )
by ZFMISC_1:33;
then A29:
(F . f) * (F . g) = [[<|(cod g),?>,<|(dom f),?>],(t `*` t1)]
by A25, A27, A28, CAT_1:def 4;
A30:
(
dom (g * f) = dom f &
cod (g * f) = cod g )
by A22, CAT_1:42;
then reconsider tt =
t `*` t1 as
natural_transformation of
<|(cod (g * f)),?>,
<|(dom (g * f)),?> ;
A31:
<|(cod (g * f)),?> is_naturally_transformable_to <|(dom (g * f)),?>
by Th3;
for
o being
Object of
A holds
<|(g * f),?> . o = tt . o
proof
let o be
Object of
A;
:: thesis: <|(g * f),?> . o = tt . o
reconsider f1 =
t . o as
Morphism of
(EnsHom A) ;
reconsider f2 =
t1 . o as
Morphism of
(EnsHom A) ;
A32:
t . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
by A22, Def3;
A33:
f2 = [[(Hom (cod g),o),(Hom (dom g),o)],(hom g,(id o))]
by Def3;
A34:
<|(dom g),?> is_naturally_transformable_to <|(dom f),?>
by A22, Th3;
A35:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)),
(fId (Hom A)) #)
by ENS_1:def 14;
then reconsider f1' =
f1 as
Element of
Maps (Hom A) ;
reconsider f2' =
f2 as
Element of
Maps (Hom A) by A35;
A36:
cod f2 = dom f1
proof
A37:
dom f1 =
(fDom (Hom A)) . f1
by A35
.=
dom f1'
by ENS_1:def 10
.=
(f1 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),o),(Hom (dom f),o)] `1
by A32, MCART_1:7
.=
Hom (cod f),
o
by MCART_1:7
;
cod f2 =
(fCod (Hom A)) . f2
by A35
.=
cod f2'
by ENS_1:def 11
.=
(f2 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod g),o),(Hom (dom g),o)] `2
by A33, MCART_1:7
.=
Hom (dom g),
o
by MCART_1:7
;
hence
cod f2 = dom f1
by A22, A37;
:: thesis: verum
end;
A38:
(
dom f2 = Hom (cod g),
o &
cod f2 = Hom (dom g),
o )
proof
A39:
dom f2 =
(fDom (Hom A)) . f2
by A35
.=
dom f2'
by ENS_1:def 10
.=
(f2 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod g),o),(Hom (dom g),o)] `1
by A33, MCART_1:7
.=
Hom (cod g),
o
by MCART_1:7
;
cod f2 =
(fCod (Hom A)) . f2
by A35
.=
cod f2'
by ENS_1:def 11
.=
(f2 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod g),o),(Hom (dom g),o)] `2
by A33, MCART_1:7
.=
Hom (dom g),
o
by MCART_1:7
;
hence
(
dom f2 = Hom (cod g),
o &
cod f2 = Hom (dom g),
o )
by A39;
:: thesis: verum
end;
A40:
(
cod f1 = Hom (dom f),
o &
dom f1 = Hom (cod f),
o )
proof
A41:
cod f1 =
(fCod (Hom A)) . f1
by A35
.=
cod f1'
by ENS_1:def 11
.=
(f1 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),o),(Hom (dom f),o)] `2
by A32, MCART_1:7
.=
Hom (dom f),
o
by MCART_1:7
;
dom f1 =
(fDom (Hom A)) . f1
by A35
.=
dom f1'
by ENS_1:def 10
.=
(f1 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),o),(Hom (dom f),o)] `1
by A32, MCART_1:7
.=
Hom (cod f),
o
by MCART_1:7
;
hence
(
cod f1 = Hom (dom f),
o &
dom f1 = Hom (cod f),
o )
by A41;
:: thesis: verum
end;
A42:
<|(cod g),?> is_naturally_transformable_to <|(dom g),?>
by Th3;
set F1 =
<|(cod f),?>;
set F2 =
<|(dom f),?>;
A43:
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;
:: thesis: [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] in Hom (<|(cod f),?> . a),(<|(dom f),?> . a)
A44:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)),
(fId (Hom A)) #)
by ENS_1:def 14;
then reconsider m =
[[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] as
Morphism of
(EnsHom A) by ENS_1:48;
reconsider m' =
m as
Element of
Maps (Hom A) by ENS_1:48;
A45:
dom m =
(fDom (Hom A)) . m
by A44
.=
dom m'
by ENS_1:def 10
.=
(m `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),a),(Hom (dom f),a)] `1
by MCART_1:7
.=
Hom (cod f),
a
by MCART_1:7
.=
(Obj (hom?- (Hom A),(cod f))) . a
by ENS_1:60
.=
(hom?- (Hom A),(cod f)) . a
by CAT_1:def 20
.=
<|(cod f),?> . a
by ENS_1:def 26
;
cod m =
(fCod (Hom A)) . m
by A44
.=
cod m'
by ENS_1:def 11
.=
(m `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),a),(Hom (dom f),a)] `2
by MCART_1:7
.=
Hom (dom f),
a
by MCART_1:7
.=
(Obj (hom?- (Hom A),(dom f))) . a
by ENS_1:60
.=
(hom?- (Hom A),(dom f)) . a
by CAT_1:def 20
.=
<|(dom f),?> . a
by ENS_1:def 26
;
hence
[[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] in Hom (<|(cod f),?> . a),
(<|(dom f),?> . a)
by A45, CAT_1:18;
:: thesis: verum
end;
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;
:: thesis: [[(Hom (cod g),a),(Hom (dom g),a)],(hom g,a)] in Hom (<|(cod g),?> . a),(<|(dom g),?> . a)
A46:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)),
(fId (Hom A)) #)
by ENS_1:def 14;
then reconsider m =
[[(Hom (cod g),a),(Hom (dom g),a)],(hom g,a)] as
Morphism of
(EnsHom A) by ENS_1:48;
reconsider m' =
m as
Element of
Maps (Hom A) by ENS_1:48;
A47:
dom m =
(fDom (Hom A)) . m
by A46
.=
dom m'
by ENS_1:def 10
.=
(m `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod g),a),(Hom (dom g),a)] `1
by MCART_1:7
.=
Hom (cod g),
a
by MCART_1:7
.=
(Obj (hom?- (Hom A),(cod g))) . a
by ENS_1:60
.=
(hom?- (Hom A),(cod g)) . a
by CAT_1:def 20
.=
<|(cod g),?> . a
by ENS_1:def 26
;
cod m =
(fCod (Hom A)) . m
by A46
.=
cod m'
by ENS_1:def 11
.=
(m `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod g),a),(Hom (dom g),a)] `2
by MCART_1:7
.=
Hom (dom g),
a
by MCART_1:7
.=
(Obj (hom?- (Hom A),(dom g))) . a
by ENS_1:60
.=
(hom?- (Hom A),(dom g)) . a
by CAT_1:def 20
.=
<|(dom g),?> . a
by ENS_1:def 26
;
hence
[[(Hom (cod g),a),(Hom (dom g),a)],(hom g,a)] in Hom (<|(cod g),?> . a),
(<|(dom g),?> . a)
by A47, CAT_1:18;
:: thesis: verum
end;
then A48:
(
Hom (<|(cod f),?> . o),
(<|(dom f),?> . o) <> {} &
Hom (<|(cod g),?> . o),
(<|(dom g),?> . o) <> {} )
by A43;
A49:
tt . o =
(t . o) * (t1 . o)
by A30, A34, A42, NATTRA_1:27
.=
f1 * f2
by A22, A48, CAT_1:def 13
.=
[[(Hom (cod g),o),(Hom (dom f),o)],((hom f,(id o)) * (hom g,(id o)))]
by A32, A33, A36, A38, A40, 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 A22, ENS_1:46
;
<|(g * f),?> . o =
[[(Hom (cod g),o),(Hom (dom (g * f)),o)],(hom (g * f),(id o))]
by A30, Def3
.=
[[(Hom (cod g),o),(Hom (dom f),o)],(hom (g * f),o)]
by A30, ENS_1:53
;
hence
<|(g * f),?> . o = tt . o
by A49;
:: thesis: verum
end;
then
<|(g * f),?> = tt
by A31, ISOCAT_1:31;
hence
F . (g * f) = (F . f) * (F . g)
by A2, A29, A30;
:: thesis: verum
end;
then reconsider F = F as Contravariant_Functor of A, Functors A,(EnsHom A) by A3, A8, OPPCAT_1:def 7;
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,?>]
; :: thesis: verum