let C, D, C9 be Category; for S being Functor of [:C,C9:],D
for c being Object of C holds (curry S) . (id c) is Functor of C9,D
let S be Functor of [:C,C9:],D; for c being Object of C holds (curry S) . (id c) is Functor of C9,D
let c be Object of C; (curry S) . (id c) is Functor of C9,D
reconsider S9 = S as Function of [: the carrier' of C, the carrier' of C9:], the carrier' of D ;
reconsider T = (curry S9) . (id c) as Function of the carrier' of C9, the carrier' of D ;
now ( ( for c9 being Object of C9 ex d being Object of D st T . (id c9) = id d ) & ( for f being Morphism of C9 holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C9 st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )thus
for
c9 being
Object of
C9 ex
d being
Object of
D st
T . (id c9) = id d
( ( for f being Morphism of C9 holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C9 st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )A2:
(
dom (id c) = c &
cod (id c) = c )
;
thus
for
f being
Morphism of
C9 holds
(
T . (id (dom f)) = id (dom (T . f)) &
T . (id (cod f)) = id (cod (T . f)) )
for f, g being Morphism of C9 st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)proof
let f be
Morphism of
C9;
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
thus T . (id (dom f)) =
S . (
(id c),
(id (dom f)))
by FUNCT_5:69
.=
S . (id [c,(dom f)])
by Th25
.=
S . (id [(dom (id c)),(dom f)])
.=
S . (id (dom [(id c),f]))
by Th22
.=
id (dom (S . ((id c),f)))
by CAT_1:63
.=
id (dom (T . f))
by FUNCT_5:69
;
T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) =
S . (
(id c),
(id (cod f)))
by FUNCT_5:69
.=
S . (id [c,(cod f)])
by Th25
.=
S . (id [(cod (id c)),(cod f)])
.=
S . (id (cod [(id c),f]))
by Th22
.=
id (cod (S . ((id c),f)))
by CAT_1:63
.=
id (cod (T . f))
by FUNCT_5:69
;
verum
end; let f,
g be
Morphism of
C9;
( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )assume A3:
dom g = cod f
;
T . (g (*) f) = (T . g) (*) (T . f)
Hom (
c,
c)
<> {}
;
then A4:
(id c) * (id c) = (id c) (*) (id c)
by CAT_1:def 13;
A5:
(
dom [(id c),g] = [(dom (id c)),(dom g)] &
cod [(id c),f] = [(cod (id c)),(cod f)] )
by Th22;
thus T . (g (*) f) =
S . (
((id c) * (id c)),
(g (*) f))
by FUNCT_5:69
.=
S . ([(id c),g] (*) [(id c),f])
by A3, A2, A4, Th23
.=
(S . ((id c),g)) (*) (S . ((id c),f))
by A3, A5, CAT_1:64
.=
(T . g) (*) (S . ((id c),f))
by FUNCT_5:69
.=
(T . g) (*) (T . f)
by FUNCT_5:69
;
verum end;
hence
(curry S) . (id c) is Functor of C9,D
by CAT_1:61; verum