thus
Functors (B,A) is quasi-discrete
NATTRA_1:def 20 Functors (B,A) is pseudo-discrete proof
let a,
b be
Element of
(Functors (B,A));
NATTRA_1:def 18 ( Hom (a,b) <> {} implies a = b )
assume
Hom (
a,
b)
<> {}
;
a = b
then consider f being
Morphism of
a,
b such that A1:
f in Hom (
a,
b)
by CAT_1:91;
f in the
carrier' of
(Functors (B,A))
;
then
f in NatTrans (
B,
A)
by Def16;
then consider F1,
F2 being
Functor of
B,
A,
t being
natural_transformation of
F1,
F2 such that A2:
f = [[F1,F2],t]
and A3:
F1 is_naturally_transformable_to F2
by Def15;
A4:
F1 =
dom f
by A2, Th29
.=
a
by A1, CAT_1:1
;
F2 =
cod f
by A2, Th29
.=
b
by A1, CAT_1:1
;
hence
a = b
by A4, Th34, A3;
verum
end;
let a be Element of (Functors (B,A)); NATTRA_1:def 19 Hom (a,a) is trivial
A5:
now for f being set st f in Hom (a,a) holds
f = id alet f be
set ;
( f in Hom (a,a) implies f = id a )assume A6:
f in Hom (
a,
a)
;
f = id a
f in the
carrier' of
(Functors (B,A))
by A6;
then
f in NatTrans (
B,
A)
by Def16;
then consider F1,
F2 being
Functor of
B,
A,
t being
natural_transformation of
F1,
F2 such that A7:
f = [[F1,F2],t]
and A8:
F1 is_naturally_transformable_to F2
by Def15;
reconsider ff =
f as
Morphism of
(Functors (B,A)) by A6;
A9:
F1 =
dom ff
by A7, Th29
.=
a
by A6, CAT_1:1
;
A10:
F1 = F2
by Th34, A8;
then
t = id F1
by Th35;
hence
f = id a
by A9, Def16, A7, A10;
verum end;
let x, y be object ; ZFMISC_1:def 10 ( not x in Hom (a,a) or not y in Hom (a,a) or x = y )
assume
( x in Hom (a,a) & y in Hom (a,a) )
; x = y
then
( x = id a & y = id a )
by A5;
hence
x = y
; verum