set F = Yoneda A;
for x1, x2 being object st x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 implies x1 = x2 )
assume that A1:
(
x1 in dom (Obj (Yoneda A)) &
x2 in dom (Obj (Yoneda A)) )
and A2:
(Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2
;
x1 = x2
reconsider c =
x1,
c1 =
x2 as
Object of
A by A1, FUNCT_2:def 1;
reconsider f =
id c1 as
Morphism of
c1,
c1 ;
<|c1,?> in Funct (
A,
(EnsHom A))
by CAT_2:def 2;
then reconsider d1 =
<|c1,?> as
Object of
(Functors (A,(EnsHom A))) by NATTRA_1:def 17;
<|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;
(Yoneda A) . (id c1) = id d1
proof
set X =
dom <|(id c1),?>;
A3:
for
y being
object st
y in dom <|(id c1),?> holds
<|(id c1),?> . y = (id <|c1,?>) . y
proof
let y be
object ;
( y in dom <|(id c1),?> implies <|(id c1),?> . y = (id <|c1,?>) . y )
assume
y in dom <|(id c1),?>
;
<|(id c1),?> . y = (id <|c1,?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
reconsider zz =
id z as
Morphism of
z,
z ;
A4:
Hom (
z,
z)
<> {}
;
<|(id c1),?> . z =
[[(Hom ((cod (id c1)),z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))]
by Def3
.=
[[(Hom (c1,z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))]
.=
[[(Hom (c1,z)),(Hom (c1,z))],(hom ((id c1),(id z)))]
.=
[[(Hom (c1,z)),(Hom (c1,z))],(hom (c1,(id z)))]
by ENS_1:53
.=
[[(Hom (c1,z)),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))]
.=
[[(Hom (c1,(dom (id z)))),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))]
.=
<|c1,?> . (id z)
by ENS_1:def 21
.=
<|c1,?> /. zz
by A4, CAT_3:def 10
.=
id (<|c1,?> . z)
by NATTRA_1:15
.=
(id <|c1,?>) . z
by NATTRA_1:20
.=
(id <|c1,?>) . z
by NATTRA_1:def 5
;
hence
<|(id c1),?> . y = (id <|c1,?>) . y
by NATTRA_1:def 5;
verum
end;
dom <|(id c1),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|c1,?>)
by FUNCT_2:def 1
;
then A5:
<|(id c1),?> = id <|c1,?>
by A3, FUNCT_1:2;
(Yoneda A) . (id c1) =
[[<|(cod (id c1)),?>,<|(dom (id c1)),?>],<|(id c1),?>]
by Def4
.=
[[<|c1,?>,<|(dom (id c1)),?>],<|(id c1),?>]
.=
[[<|c1,?>,<|c1,?>],(id <|c1,?>)]
by A5
.=
id d1
by NATTRA_1:def 17
;
hence
(Yoneda A) . (id c1) = id d1
;
verum
end;
then A6:
(Obj (Yoneda A)) . c1 = d1
by OPPCAT_1:30;
(Yoneda A) . (id c) = id d
proof
set X =
dom <|(id c),?>;
A7:
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 ;
A8:
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 A8, 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 A9:
<|(id c),?> = id <|c,?>
by A7, FUNCT_1:2;
(Yoneda A) . (id c) =
[[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>]
by Def4
.=
[[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]
.=
[[<|c,?>,<|c,?>],(id <|c,?>)]
by A9
.=
id d
by NATTRA_1:def 17
;
hence
(Yoneda A) . (id c) = id d
;
verum
end;
then
(Obj (Yoneda A)) . c = d
by OPPCAT_1:30;
then
[[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f
by A2, A6, ENS_1:def 21;
then
[[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))]
by ENS_1:def 21;
then
[(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))]
;
then
[(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))]
;
then
Hom (
c,
(dom f))
= Hom (
c1,
(dom f))
by XTUPLE_0:3;
then
Hom (
c,
(dom f))
= Hom (
c1,
c1)
;
then A10:
Hom (
c,
c1)
= Hom (
c1,
c1)
;
id c1 in Hom (
c1,
c1)
by CAT_1:27;
then reconsider h =
id c1 as
Morphism of
c,
c1 by A10, CAT_1:def 5;
dom h = c
by A10, CAT_1:5;
hence
x1 = x2
;
verum
end;
then
Obj (Yoneda A) is one-to-one
by FUNCT_1:def 4;
hence
Yoneda A is one-to-one
by Th5; verum