情况如下（我改为更标准的Haskell表示法）：
class Functor f => MonoidallyCopointed f where
copointAppend :: (∀r.f(r)->r) -> (∀r.f(r)->r) -> (∀r.f(r)->r)
copointEmpty :: ∀r.f(r)->r
对于 MonoidallyCopointed 的所有实例F和所有实例
x,y,z::∀r.F(r)->r
以下是：
x `copointAppend` copointEmpty == copointEmpty `copointAppend` x == x
x `copointAppend` (y `copointAppend` z) == (x `copointAppend` y) `copointAppend` z
那么F是否具有从 copointAppend 和 copointEmpty 定义的自然 Comonad 实例？
注：反之亦然（ copointEmpty = extract 和 copointAppend f g = f . g . duplicate . ）
编辑
正如Bartosz在评论中指出的那样，这主要是使用co-Kleisli附加的comonads的定义 . 所以问题实际上是关于这个概念的构造性 . 因此，就实际应用而言，以下问题可能更有趣：
在f的可能 Comonad 实例集和f的可能 MonoidallyCopointed 实例集之间是否存在建设性同构？
这在实践中很有用，因为 Comonad 实例的直接定义可能涉及一些技术难以阅读的代码，这些代码无法通过类型检查器进行验证 . 例如，
data W a = W (Maybe a) (Int -> a) (Either (String -> a) (a,a,a,a))
有一个Comonad实例，但直接定义（证明它确实是Comonad！）可能不那么容易 . 另一方面，提供一个 MonoidallyCopointed 实例可能会更容易一点（但我不完全确定这一点） .