Does a natural monoidal structure on copoints of a Functor induce a Comonad?

Question

The situation is as follows (I changed to more standard-ish Haskell notation):

class Functor f => MonoidallyCopointed f where
    copointAppend ::  (∀r.f(r)->r) -> (∀r.f(r)->r) -> (∀r.f(r)->r)
    copointEmpty  ::  ∀r.f(r)->r

such that for all instance F of MonoidallyCopointed and for all

x,y,z::∀r.F(r)->r

The following holds:

x `copointAppend` copointEmpty == copointEmpty `copointAppend` x == x
x `copointAppend` (y `copointAppend` z) == (x `copointAppend` y) `copointAppend` z

Then is it true that F has a natural Comonad instance defined from copointAppend and copointEmpty?

N.B. The converse holds (with copointEmpty = extract and copointAppend f g = f . g . duplicate.)

EDIT

As Bartosz pointed out in the comment, this is mostly the definition of comonads using the co-Kleisli adjunction. So the question is really about the constructivity of this notion. Accordingly, the following question is probably more interesting in terms of real-world applications:

Does there exist a constructive isomorphism between the set of possible Comonad instances of f and the set of possible MonoidallyCopointed instances of f?

This can be useful in practice because a direct definition of Comonad instance can involve a bit of technical, hard-to-read code that cannot be verified by the type checker. For example,

data W a = W (Maybe a) (Int -> a) (Either (String -> a) (a,a,a,a))

has a Comonad instance but the direct definition (with the proof that it's indeed a Comonad!) may not be so easy. On the other hand, providing a MonoidallyCopointed instance may be a little easier (but I'm not perfectly sure of this point).