set B = EnsHom A;
deffunc H1( Element of A) -> object = [[(Hom ((cod f),$1)),(Hom ((dom f),$1))],(hom (f,(id $1)))];
set F1 = <|(cod f),?>;
set F2 = <|(dom f),?>;
A1:
for o being Object of A holds [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o))
proof
let o be
Object of
A;
[[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom ((<|(cod f),?> . o),(<|(dom f),?> . o))
A2:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)) #)
by ENS_1:def 13;
A3:
hom (
f,
(id o))
= hom (
f,
o)
by ENS_1:53;
then reconsider m =
[[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] as
Morphism of
(EnsHom A) by A2, ENS_1:48;
reconsider m9 =
m as
Element of
Maps (Hom A) by A3, ENS_1:48;
A4:
cod m =
(fCod (Hom A)) . m
by A2
.=
cod m9
by ENS_1:def 10
.=
(m `1) `2
by ENS_1:def 4
.=
[(Hom ((cod f),o)),(Hom ((dom f),o))] `2
.=
Hom (
(dom f),
o)
.=
(Obj (hom?- ((Hom A),(dom f)))) . o
by ENS_1:60
.=
(hom?- ((Hom A),(dom f))) . o
.=
<|(dom f),?> . o
by ENS_1:def 25
;
dom m =
(fDom (Hom A)) . m
by A2
.=
dom m9
by ENS_1:def 9
.=
(m `1) `1
by ENS_1:def 3
.=
[(Hom ((cod f),o)),(Hom ((dom f),o))] `1
.=
Hom (
(cod f),
o)
.=
(Obj (hom?- ((Hom A),(cod f)))) . o
by ENS_1:60
.=
(hom?- ((Hom A),(cod f))) . o
.=
<|(cod f),?> . o
by ENS_1:def 25
;
hence
[[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom (
(<|(cod f),?> . o),
(<|(dom f),?> . o))
by A4;
verum
end;
A5:
for o being Element of A holds H1(o) in the carrier' of (EnsHom A)
consider t being Function of the carrier of A, the carrier' of (EnsHom A) such that
A6:
for o being Element of A holds t . o = H1(o)
from FUNCT_2:sch 8(A5);
A7:
for o being Object of A holds t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o
proof
let o be
Object of
A;
t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o
[[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] in Hom (
(<|(cod f),?> . o),
(<|(dom f),?> . o))
by A1;
then
[[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] is
Morphism of
<|(cod f),?> . o,
<|(dom f),?> . o
by CAT_1:def 5;
hence
t . o is
Morphism of
<|(cod f),?> . o,
<|(dom f),?> . o
by A6;
verum
end;
for o being Object of A holds Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) <> {}
by A1;
then A8:
<|(cod f),?> is_transformable_to <|(dom f),?>
by NATTRA_1:def 2;
then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A7, NATTRA_1:def 3;
A9:
for a, b being Object of A st Hom (a,b) <> {} holds
for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
proof
let a,
b be
Object of
A;
( Hom (a,b) <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) )
assume A10:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
A11:
Hom (
(<|(cod f),?> . a),
(<|(cod f),?> . b))
<> {}
by A10, CAT_1:84;
let g be
Morphism of
a,
b;
(t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
A12:
dom g = a
by A10, CAT_1:5;
A13:
rng (hom ((cod f),g)) c= dom (hom (f,b))
proof
A14:
cod g = b
by A10, CAT_1:5;
per cases
( Hom ((dom f),b) = {} or Hom ((dom f),b) <> {} )
;
suppose A16:
Hom (
(dom f),
b)
<> {}
;
rng (hom ((cod f),g)) c= dom (hom (f,b))
cod g = b
by A10, CAT_1:5;
then A17:
(
rng (hom ((cod f),g)) c= Hom (
(cod f),
(cod g)) &
Hom (
(cod f),
(cod g))
= dom (hom (f,b)) )
by A16, FUNCT_2:def 1, RELAT_1:def 19;
let e be
object ;
TARSKI:def 3 ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) )assume
e in rng (hom ((cod f),g))
;
e in dom (hom (f,b))hence
e in dom (hom (f,b))
by A17;
verum end;
end;
A18:
rng (hom (f,a)) c= dom (hom ((dom f),g))
proof
A19:
dom g = a
by A10, CAT_1:5;
per cases
( Hom ((dom f),(cod g)) = {} or Hom ((dom f),(cod g)) <> {} )
;
suppose A21:
Hom (
(dom f),
(cod g))
<> {}
;
rng (hom (f,a)) c= dom (hom ((dom f),g))let e be
object ;
TARSKI:def 3 ( not e in rng (hom (f,a)) or e in dom (hom ((dom f),g)) )assume A22:
e in rng (hom (f,a))
;
e in dom (hom ((dom f),g))
(
rng (hom (f,a)) c= Hom (
(dom f),
a) &
Hom (
(dom f),
a)
= dom (hom ((dom f),g)) )
by A19, A21, FUNCT_2:def 1, RELAT_1:def 19;
hence
e in dom (hom ((dom f),g))
by A22;
verum end;
end;
A23:
dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
proof
per cases
( Hom ((cod f),(dom g)) = {} or Hom ((cod f),(dom g)) <> {} )
;
suppose A24:
Hom (
(cod f),
(dom g))
= {}
;
dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) dom ((hom (f,b)) * (hom ((cod f),g))) =
dom (hom ((cod f),g))
by A13, RELAT_1:27
.=
Hom (
(cod f),
a)
by A12, A24
.=
dom (hom (f,a))
by A12, A24
.=
dom ((hom ((dom f),g)) * (hom (f,a)))
by A18, RELAT_1:27
;
hence
dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
;
verum end; suppose A25:
Hom (
(cod f),
(dom g))
<> {}
;
dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))then A26:
Hom (
(cod f),
(cod g))
<> {}
by ENS_1:42;
A27:
Hom (
(dom f),
a)
<> {}
by A12, A25, ENS_1:42;
dom ((hom (f,b)) * (hom ((cod f),g))) =
dom (hom ((cod f),g))
by A13, RELAT_1:27
.=
Hom (
(cod f),
a)
by A12, A26, FUNCT_2:def 1
.=
dom (hom (f,a))
by A27, FUNCT_2:def 1
.=
dom ((hom ((dom f),g)) * (hom (f,a)))
by A18, RELAT_1:27
;
hence
dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
;
verum end;
end;
A28:
for
x being
object st
x in dom ((hom (f,b)) * (hom ((cod f),g))) holds
((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
proof
let x be
object ;
( x in dom ((hom (f,b)) * (hom ((cod f),g))) implies ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x )
assume A29:
x in dom ((hom (f,b)) * (hom ((cod f),g)))
;
((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
per cases
( Hom ((cod f),(dom g)) <> {} or Hom ((cod f),(dom g)) = {} )
;
suppose A30:
Hom (
(cod f),
(dom g))
<> {}
;
((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . xA31:
x in dom (hom ((cod f),g))
by A29, FUNCT_1:11;
Hom (
(cod f),
(cod g))
<> {}
by A30, ENS_1:42;
then A32:
x in Hom (
(cod f),
(dom g))
by A31, FUNCT_2:def 1;
then reconsider x =
x as
Morphism of
A ;
A33:
dom g = cod x
by A32, CAT_1:1;
cod g = b
by A10, CAT_1:5;
then A34:
cod (g (*) x) = b
by A33, CAT_1:17;
dom (g (*) x) =
dom x
by A33, CAT_1:17
.=
cod f
by A32, CAT_1:1
;
then A35:
g (*) x in Hom (
(cod f),
b)
by A34;
A36:
dom x = cod f
by A32, CAT_1:1;
then A37:
dom (x (*) f) = dom f
by CAT_1:17;
A38:
(hom (f,a)) . x = x (*) f
by A12, A32, ENS_1:def 20;
then reconsider h =
(hom (f,a)) . x as
Morphism of
A ;
A39:
(
dom g = cod x &
dom x = cod f )
by A32, CAT_1:1;
cod (x (*) f) =
cod x
by A36, CAT_1:17
.=
dom g
by A32, CAT_1:1
;
then A40:
(hom (f,a)) . x in Hom (
(dom f),
(dom g))
by A38, A37;
((hom (f,b)) * (hom ((cod f),g))) . x =
(hom (f,b)) . ((hom ((cod f),g)) . x)
by A29, FUNCT_1:12
.=
(hom (f,b)) . (g (*) x)
by A32, ENS_1:def 19
.=
(g (*) x) (*) f
by A35, ENS_1:def 20
.=
g (*) (x (*) f)
by A39, CAT_1:18
.=
g (*) h
by A12, A32, ENS_1:def 20
.=
(hom ((dom f),g)) . ((hom (f,a)) . x)
by A40, ENS_1:def 19
.=
((hom ((dom f),g)) * (hom (f,a))) . x
by A23, A29, FUNCT_1:12
;
hence
((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x
;
verum end;
end;
A42:
Hom (
(<|(dom f),?> . a),
(<|(dom f),?> . b))
<> {}
by A10, CAT_1:84;
A43:
cod g = b
by A10, CAT_1:5;
reconsider f4 =
t . a as
Morphism of
(EnsHom A) ;
A44:
t . a =
t . a
by A8, NATTRA_1:def 5
.=
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,(id a)))]
by A6
.=
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
by ENS_1:53
;
then reconsider f49 =
f4 as
Element of
Maps (Hom A) by ENS_1:48;
A45:
Hom (
(<|(cod f),?> . a),
(<|(dom f),?> . a))
<> {}
by A1;
reconsider f1 =
t . b as
Morphism of
(EnsHom A) ;
A46:
t . b =
t . b
by A8, NATTRA_1:def 5
.=
[[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,(id b)))]
by A6
.=
[[(Hom ((cod f),b)),(Hom ((dom f),b))],(hom (f,b))]
by ENS_1:53
;
then reconsider f19 =
f1 as
Element of
Maps (Hom A) by ENS_1:48;
A47:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)) #)
by ENS_1:def 13;
then A48:
cod f1 =
(fCod (Hom A)) . f1
.=
cod f19
by ENS_1:def 10
.=
(f1 `1) `2
by ENS_1:def 4
.=
[(Hom ((cod f),b)),(Hom ((dom f),b))] `2
by A46
.=
Hom (
(dom f),
b)
;
A49:
dom f4 =
(fDom (Hom A)) . f4
by A47
.=
dom f49
by ENS_1:def 9
.=
(f4 `1) `1
by ENS_1:def 3
.=
[(Hom ((cod f),a)),(Hom ((dom f),a))] `1
by A44
.=
Hom (
(cod f),
a)
;
A50:
cod f4 =
(fCod (Hom A)) . f4
by A47
.=
cod f49
by ENS_1:def 10
.=
(f4 `1) `2
by ENS_1:def 4
.=
[(Hom ((cod f),a)),(Hom ((dom f),a))] `2
by A44
.=
Hom (
(dom f),
a)
;
reconsider f2 =
<|(cod f),?> /. g as
Morphism of
(EnsHom A) ;
A51:
f2 =
(hom?- (cod f)) . g
by A10, CAT_3:def 10
.=
[[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))],(hom ((cod f),g))]
by ENS_1:def 21
;
then reconsider f29 =
f2 as
Element of
Maps (Hom A) by ENS_1:47;
A52:
dom f2 =
(fDom (Hom A)) . f2
by A47
.=
dom f29
by ENS_1:def 9
.=
(f2 `1) `1
by ENS_1:def 3
.=
[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `1
by A51
.=
Hom (
(cod f),
(dom g))
;
A53:
cod f2 =
(fCod (Hom A)) . f2
by A47
.=
cod f29
by ENS_1:def 10
.=
(f2 `1) `2
by ENS_1:def 4
.=
[(Hom ((cod f),(dom g))),(Hom ((cod f),(cod g)))] `2
by A51
.=
Hom (
(cod f),
(cod g))
;
A54:
dom f1 =
(fDom (Hom A)) . f1
by A47
.=
dom f19
by ENS_1:def 9
.=
(f1 `1) `1
by ENS_1:def 3
.=
[(Hom ((cod f),b)),(Hom ((dom f),b))] `1
by A46
.=
Hom (
(cod f),
b)
;
then A55:
cod f2 = dom f1
by A10, A53, CAT_1:5;
reconsider f3 =
<|(dom f),?> /. g as
Morphism of
(EnsHom A) ;
A56:
f3 =
(hom?- (dom f)) . g
by A10, CAT_3:def 10
.=
[[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))],(hom ((dom f),g))]
by ENS_1:def 21
;
then reconsider f39 =
f3 as
Element of
Maps (Hom A) by ENS_1:47;
A57:
cod f3 =
(fCod (Hom A)) . f3
by A47
.=
cod f39
by ENS_1:def 10
.=
(f3 `1) `2
by ENS_1:def 4
.=
[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `2
by A56
.=
Hom (
(dom f),
(cod g))
;
A58:
dom f3 =
(fDom (Hom A)) . f3
by A47
.=
dom f39
by ENS_1:def 9
.=
(f3 `1) `1
by ENS_1:def 3
.=
[(Hom ((dom f),(dom g))),(Hom ((dom f),(cod g)))] `1
by A56
.=
Hom (
(dom f),
(dom g))
;
then A59:
cod f4 = dom f3
by A10, A50, CAT_1:5;
Hom (
(<|(cod f),?> . b),
(<|(dom f),?> . b))
<> {}
by A1;
then (t . b) * (<|(cod f),?> /. g) =
f1 (*) f2
by A11, CAT_1:def 13
.=
[[(Hom ((cod f),(dom g))),(Hom ((dom f),b))],((hom (f,b)) * (hom ((cod f),g)))]
by A46, A54, A48, A51, A52, A53, A55, Th1
.=
[[(Hom ((cod f),a)),(Hom ((dom f),(cod g)))],((hom ((dom f),g)) * (hom (f,a)))]
by A12, A43, A23, A28, FUNCT_1:2
.=
f3 (*) f4
by A56, A58, A57, A44, A49, A50, A59, Th1
.=
(<|(dom f),?> /. g) * (t . a)
by A42, A45, CAT_1:def 13
;
hence
(t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)
;
verum
end;
<|(cod f),?> is_naturally_transformable_to <|(dom f),?>
by Th2;
then reconsider t = t as natural_transformation of <|(cod f),?>,<|(dom f),?> by A9, NATTRA_1:def 8;
for o being Element of A holds t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
proof
let o be
Object of
A;
t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
t . o =
t . o
by A8, NATTRA_1:def 5
.=
[[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
by A6
;
hence
t . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
;
verum
end;
hence
ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b1 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))]
; verum