是的，事实上任何函子都会以这种方式产生一个独特的共单子，除非 f==0。
让 F 成为 Hask 上的内函子。让
W(a) = ∀r.F(a->r)->r
W(f) = F(f∗)∗
where g∗(h) = h∘g
一旦你意识到以下同构，这个谜题本质上就变成了几何/组合：
定理 1。
假设两个类型 (∀r.r->F(r)) (∀r.F(r)->r) 都不为空。则有类型 W(a) ≃ (∀r.F(r)->r, a) 的同构。
证明：
class Functor f => Fibration f where
projection :: ∀r. f(r)->r
some_section :: ∀r. r->f(r) -- _any_ section will work
to :: forall f a. Fibration f
=> (∀r.f(a->r) -> r)
-> (∀r.f(r)->r, a)
to(f) = ( f . fmap const
, f(some_section(id)))
from :: forall f a. Fibration f
=> (∀r.f(r)->r, a)
-> (∀r.f(a->r) -> r)
from (π,η) = ev(η) . π
ev :: a -> (a->b) -> b
ev x f = f x
填写详细信息（我可以根据要求发布）将需要
一点参数化和米田引理。当 F 不是 Fibration（如我在上面定义的）时，W 如您所见是微不足道的。
如果投影是唯一的，我们将纤维化称为覆盖（尽管我不确定这种用法是否合适）。
承认这个定理，你可以看到 W(a) 是由_所有可能的纤维 ∀r.F(r)->r 索引的 a 的余积，即
W(a) ≃ ∐a
π::∀f.F(r)->r
换句话说，函子 W（作为 Func(Hask) 上的预层）接受一个纤维化并从中构造一个规范的平凡覆盖空间。
例如，令 F(a)=(Int,a,a,a)。然后我们有三个明显的自然纤维 F(a)->a。用 + 来写联积，下图连同上面的定理应该足以具体描述共单子：
a
^
| ε
|
a+a+a
^ | ^
Wε | |δ | εW
| v |
(a+a+a)+(a+a+a)+(a+a+a)
因此，counit 是独一无二的。使用联积的明显索引，Wε 将 (i,j) 映射到 j，εW 将 (i,j) 映射到 i。所以δ一定是唯一的“对角线”映射，即δ(i) == (i,i)！
定理 2。
令 F 为 Fibration，令 ΩW 为所有带有底层函子 W 的共单子的集合。然后 ΩW≃1。
（对不起，我没有正式证明。）
单子集 ΜW 的类似组合论证也会很有趣，但在这种情况下 ΜW 可能不是单例。 （取一些常数 c 并设置 η:1->c 和 μ(i,j)=i+j-c。）
请注意，这样构造的单子/单子通常不是原始单子/单子的对偶。例如让 M 是一个单子
(F(a)=(Int,a), η(x) = (0,x), μ(n,(m,x)) = (n+m,x))，即 aWriter。自然投影是唯一的，因此由定理 W(a)≃a，没有办法尊重原始代数。
还要注意，除非Void，否则comonad 是微不足道的Fibration（可能有很多不同的方式），这就是为什么您从Comonad 得到Monad 的原因（但这不一定是唯一的！）。
关于您的观察的一些信息：
-
Dual IO a 本质上是无效的
据我所知，在 Haskell 中，IO 定义如下：
-- ghc/libraries/ghc-prim/GHC/Types.hs
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
这意味着仅从类型论来看，相应的覆盖是_由所有State# RealWorlds 索引的唯一规范覆盖空间。您是否可以（或应该）拒绝这可能是一个哲学问题，而不是一个技术问题。
-
MonadPlus m => Dual m a 无效
是的，但请注意，如果 F(a)=0 则 W(a)=1 并且它不是共单胞（因为否则该共单将暗示 W(0)->0 ≃ 1->0 类型） .这是给定任意函子 W 甚至不能是普通共单子的唯一情况。
Dual Reader 是..
这些陈述有时是正确的，有时不是。取决于感兴趣的（共）代数是否与覆盖的（双）代数一致。
所以我很惊讶几何 Haskell 真的很有趣！我想可能有很多类似的几何结构。例如，对此的自然概括是考虑某些协变函子 F,G 的 F->G 的“规范平凡化”。那么基空间的自同构群将不再是微不足道的，因此需要更多的理论来正确理解这一点。
最后，这是一个概念验证代码。感谢您提供了一个令人耳目一新的拼图，祝您圣诞节快乐 ;-)
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Control.Comonad
class Functor f => Fibration f where
x0 :: f ()
x0 = some_section ()
some_section :: forall r. r -> f(r)
some_section x = fmap (const x) x0
projection :: forall r. f(r) -> r
newtype W f a = W { un_w :: forall r. f(a->r)->r }
instance Functor f => Functor (W f) where
fmap f (W c) = W $ c . fmap (. f)
instance Fibration f => Comonad (W f) where
extract = ε
duplicate = δ
-- The counit is determined uniquely, independently of the choice of a particular section.
ε :: forall f a. Fibration f => W f a -> a
ε (W f) = f (some_section id)
-- The comultiplication is unique too.
δ :: forall f a. Fibration f => W f a -> W f (W f a)
δ f = W $ ev(f) . un_w f . fmap const
ev :: forall a b. a -> (a->b)->b
ev x f = f x
-- An Example
data Pair a = P {p1 ::a
,p2 :: a
}
deriving (Eq,Show)
instance Functor Pair where
fmap f (P x y) = P (f x) (f y)
instance Fibration Pair where
x0 = P () ()
projection = p1
type PairCover a = W Pair a
-- How to construct a cover (you will need unsafePerformIO if you want W IO.)
cover :: a -> W Pair a
cover x = W $ ev(x) . p1