let C1 be non empty category; for C2 being empty category
for E being Functor of ((OrdC 0) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 0,E is_exponent_of C1,C2
let C2 be empty category; for E being Functor of ((OrdC 0) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 0,E is_exponent_of C1,C2
let E be Functor of ((OrdC 0) [x] C1),C2; ( E = OrdC0-> C2 implies OrdC 0,E is_exponent_of C1,C2 )
assume
E = OrdC0-> C2
; OrdC 0,E is_exponent_of C1,C2
set C = OrdC 0;
reconsider E = E as Functor of ((OrdC 0) [x] C1),C2 ;
for D being category
for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
proof
let D be
category;
for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )let F be
Functor of
(D [x] C1),
C2;
( F is covariant implies ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) ) )
assume A1:
F is
covariant
;
ex H being Functor of D,(OrdC 0) st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) )
set G1 =
OrdC0-> (OrdC 0);
A2:
D is
empty
by A1, CAT_6:31;
then reconsider G1 =
OrdC0-> (OrdC 0) as
Functor of
D,
(OrdC 0) ;
take
G1
;
( G1 is covariant & F = E (*) (G1 [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
G1 = H1 ) )
thus
G1 is
covariant
by A2;
( F = E (*) (G1 [x] (id C1)) & ( for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
G1 = H1 ) )
thus
F = E (*) (G1 [x] (id C1))
;
for H1 being Functor of D,(OrdC 0) st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
G1 = H1
thus
for
G2 being
Functor of
D,
(OrdC 0) st
G2 is
covariant &
F = E (*) (G2 [x] (id C1)) holds
G1 = G2
;
verum
end;
hence
OrdC 0,E is_exponent_of C1,C2
by Def34; verum