HeftierEquiv.txt

括弧が見づらいので()に加えて[],{}も括弧の代わりに使います
つまり[]はいわゆるHaskellのリストの型ではないので注意してください

まず前提として
Hefty h a = Return a | Op [h (Hefty h) (Hefty h a)]
Coyoneda f a = ∀b. (b -> a,  f b)
です
(cf. https://twitter.com/ymdfield/status/1743235218847465546)

ここでCoyonedaの高階版を定義します
HCoyoneda h f a := Coyoneda (h f) a = ∀b. (b -> a,  h f b)

そしてHeftyとHCoyonedaを合成して新たに
Heftier h a := Hefty (HCoyoneda h) a
と定義します

展開すると
Heftier h a
= Return a | Op {HCoyoneda h [Hefty (HCoyoneda h)] [Hefty (HCoyoneda h) a]}
= Return a | Op [HCoyoneda h (Heftier h) (Heftier h a)]
= Return a | Op {Coyoneda [h (Heftier h)] (Heftier h a)} -- (1)

次にFreerから定義したバージョンです
まず
Free f a = Pure a | Free [f (Free f a)]
（https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html#t:Free より）
そして
Freer f a = Free (Coyoneda f) a
です

展開すると
Freer f a
= Pure a | Free {Coyoneda f [Free (Coyoneda f) a]}
= Pure a | Free {Coyoneda f (Freer f a)}

最後に、Freerに基づき再帰型的に定義したバージョンのHeftier'を
Heftier' h a := Freer [h (Heftier' h)] a
で定義します
( cf. https://twitter.com/Kory__3/status/1733437962787189064
    Heftier' h a = (fix α. Freer (h α)) a
)

展開すると
Heftier' h a
= Pure a | Free {Coyoneda [h (Heftier' h)] {Freer [h (Heftier' h)] a}}
Heftier'の定義より
= Pure a | Free {Coyoneda [h (Heftier' h)] (Heftier' h a)}

ところで(1)より
Heftier h a = Return a | Op {Coyoneda [h (Heftier h)] (Heftier h a)}
です

Heftier, Return, OpがそれぞれHeftier', Pure, Freeに対応してます

よって
Heftier ≅ Heftier' ■

Effectが実は多項式Functor

自分はたまたま多項式Functorに馴染みがあったので自然に流してしまいましたが、結構面白いことですよね
「Effectは任意の多項式Functorを記述している」という目でEffect^Hを見ると、「Effect^Hはh :: * -> *とx :: *からなる"多項式"を記述している」という雰囲気があります。