両クライスリ圏が構成できた

「コモナドは何の役に立つ」にて：

実例を調べると、単なるコモナド／モナド・ペアがあるだけでは不十分で、コモナドとモナドが一定の法則を満たす必要があります。僕は、その「法則」の形がハッキリとはわかんなかったのですが、ここ2,3日当たりを付けていたらだいたい予想できました。予想が事実だとわかったら、また報告することにします。

この話、うまくいきました。モナドのクライスリ圏とコモナドの余クライスリ圏を同時に含むような一般化が構成可能です。圏C上の余モナドFとモナドGに対して、両クライスリ圏（と呼ぶことにした圏）DiKl(F, G; C)が定義できて、

1. FがI（恒等関手）とき、DiKl(I, G; C) = Kl(G; C)（モナドGのクライスリ圏）、
2. GがI（恒等関手）とき、DiKl(F, I; C) = CoKl(F; C)（コモナドFの余クライスリ圏）。

どこかの誰かが同じ計算をしているでしょうが、山勘の予想がバッチリ当たったので、昨日はムヒヒヒ、ニヤニヤしてました。

興味を持つ人がいそうにないけど、メモ編に書いた記録：

1. 両代数と両クライスリ圏
   圏論的次元解析をもとにして、両クライスリ結合を定義してみた。関手の順序交換が出てくるので、ひょっとしてベックの法則（distributive law in the sense of Beck）かも？ と思って絵算を使って法則をでっち上げてみる。この時点ではイイカゲンな山勘なので、自信はなし。
2. 両クライスリ圏構成の準備
   とりあえず必要そうな等式を全部列挙。計算の準備をする。
3. 両クライスリ圏、ひょとすると、、
   DOTNを使って計算開始。単位律を確認。これでいけそうだと、ほぼ確信した。
4. 両クライスリ圏、出来た！
   やたっ、結合律が成立することが分かった。
5. 両モナドと両クライスリ圏
   忘れないうちに計算手順をメモ。