:: deftheorem Def34 defines is_exponent_of CAT_8:def 34 :
for A, B, C being category
for E being Functor of (C [x] A),B st E is covariant holds
( C,E is_exponent_of A,B iff for D being category
for F being Functor of (D [x] A),B st F is covariant holds
ex H being Functor of D,C st
( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds
H = H1 ) ) );