さらにcirc-Kleisli構成の副産物

入出力を持つ状態遷移機械を単に機械とか系と呼ぶとして、機械の圏の射α:A→Bは、集合圏でA×X→Pow(B×X)と解釈できるが、カリー化すると、α':X→Pow(B×X)^A、これは関手F(X) = Pow(B×X)^Aの余代数。

機械の圏でHom(A, B)を状態空間の適当な写像を射として再び圏と考える。これで機械の圏は2-圏になる。α|→α' はHome(A, B)の対象（1-セル）からF=F_A,B余代数を作る。Home(A, B)の射（2-セル）は余代数射に対応する。よって、coalg_A,B:Home(A, B)→Coalg(F_A,B)は関手。

coalg_A,Bのグローバルな（下添字を取った）定義はなんだろう？ circ-Kleisli構成をいじっているあいだにこんなもんが出来てた。他のcirc-Kleisli構成でも同じ現象が起こるのだろうか？