>>168
何らかの多相型をMとおいたとき、f : a -> bなる関数をmapで持ち上げたmap f : M a -> M bというと、
多相性を持ったまま何らかの操作を行う関数tx : forall a. M a -> M aは可換である、ということはなんとなく分かる。
多分、証明もできる。

もっと緩い条件もあるかもしれないけど、型レベルだとこの程度しか言えないんじゃないか？