諸々の事情から、不調っぽいよー。
……
…
それはさておき、圏Cが完備または余完備性を持つとき、その完備／余完備性（特に有限余完備性）を、適当なモナドLによりKleisli圏に持ち上げられないだろうか？ 「モナドLがこれこれの条件を満たせば、LのKleisli圏も余完備になる」という結果があるとすごくうれしい!。
具体的には、インスティチューション(Sign, Sen, Mod, |=)の指標圏Signが有限余完備な状況を考える。Maude（http://maude.cs.uiuc.edu/）やCASL（http://www.cofi.info/CASL.html）でも、この状況は仮定している。
この状況で、Signがプアなとき、Sign上のモナドLを使ってSignを拡張したいことがあるのだ。そもそもインスティチューション自体をKleisli圏まで持ち上げなくてはならないのだが、それはいいとして（よくないかも知れないが）、新しい指標圏NewSign=Kleisli(Sign, L)が有限余完備でないと困ってしまう。
ところで、指標圏の拡張に使いたいモナドLだが、これはだいたいプログラミング言語ってことになる。普通の代数的または余代数的指標は、それによって1つの型（余代数なら、ほぼオブジェクト指向のクラスに対応）を定める。が、指標（関数やメソッドだね）だけではプログラミングができない。if, while, caseなどが必要。指標Σをベースにしたコード集合をL(Σ)だとして、L(Σ)は“構成に関して閉じている”とすれば、L(L(Σ)) = L(Σ) だし、ΣはL(Σ)に自然に埋め込めるだろうからモナドになる。
Kleisli射Σ→L(Γ)ってのは、だいたいは、なんつうか、まーマクロ展開（のコード）みたいなもんでしょう。オブジェクト指向風の言葉でいえば、Σはインターフェースで、Γが別なインターフェースだから、Kleisli射Σ→L(Γ)は、“Γを仮定したコードによる、インターフェースΣの実装（マクロ展開定義）”ということになる。あるいは、“Γがあれば言語LでΣアダプター（インターフェース変換）が書けるよ”ってことでもある。
もとの指標圏Signがソート／プロファイルのレベルでの射（あまり面白くない単純対応）で構成されるのに対して、プログラミング（マクロ）言語Lを使って拡張したNewSignはずっと自由度が高くなっている。だけど、余完備性を失っていれば全然うれしくない。有限余完備ってのは、モジュラリティのことだから、もしNewSigが有限余完備なら、対象が“インターフェース”、射が“インターフェースのエミュレーションコード”で、完全にモジュール構成がサポートされた圏がKleisli構成でできあがる。
面白いのは、ここまでの構成では意味論が全然出てこないってことだ。いま、「マクロ」って言葉を使ったのは、射が、（記号じゃなくてほんとの）関数やメソッドのようなdenotationalな対象ではなくて、コード（プログラム字面）そのもの、構文的な対象が射であって“コンパイルも解釈もされてない”ことを強調したいからだ。
もちろん、インスティチューション全体を考えると、Mod関手と充足関係があるから、意味論もからんでくるのは当然だが、指標圏がプログラムコードでできてる、という状況はなんか楽しい。 -- 楽しいのは僕だけかなー？ 楽しいのにぃ。
