本日さきほど上げた記事「二重圏化と米田モナド」にて：
最近、思っていることなんだけど； 通常の圏〈1-圏〉や2-圏でやっていたことを、二重圏でやってみると割といいことあるよね。たまに“すごくいいこと”もあります。
うまいこと、二重圏／三重圏（一般には多重圏）が見つかると、いいことあります。
二重圏でやってみて実際にいいことありました。いいこと一つ目は、長年の懸案であった「『自然なホムセット同型』で与えられる随伴系〈adjunction | adjoint system〉から、『ニョロニョロ関係式』をお絵描きで導出する」に目星が付きました。
「コーナー、キンク、ニョロニョロ」にて：
まだ生煮えの話をします。最初に動機を書くと； 随伴系を定義する2つの方法である「ニョロニョロ関係式」と「自然なホムセット同型」が同値であることをお絵描き〈絵算 | {pictorial | graphical | diagrammatic} calculus〉で示したい！ ということです。
最近、二重圏のなかで形式圏論をすれば、「自然なホムセット同型」から「ニョロニョロ関係式」を出せるのではないか（もちろん、お絵描きで！）と思っています。
2025年2月の時点では生煮えだったのですが、それから少し煮込んで、だいぶ良い感じになってきました。キンク・ストレッチング公式からニョロニョロ公式〈ベント・ストレッチング公式〉は出そうです（ほぼ確実）。
いいこと二つ目も長年の懸案だったことで、一般化したオートマトンの順次結合〈sequential composition〉が定義できたことです。オートマトン（の遷移系部分）を、状態空間にモノイドが作用すると考えていてはウマくなくて、圏が作用していると考えます。この発想は二重圏 $`\mathbf{ProfDC}`$ の変種（三重圏になる）のなかで定式化できます。
いいこと三つ目、「二重圏化と米田モナド」の最後のほうに書いたことですが、「関数：関係：包含 ＝ 関手：プロ関手：制限自然変換」という“比例式”がより鮮明になってきました。圏論の進んだ概念を、馴染み深く初等的な、関数、関係（あるいは述語）、部分集合の包含などとのアナロジーで考えることが正当化されます。
ハイパードクトリンの二重圏ベースでの再定式化とか、関係データベースの二重圏（むしろ多重圏）による数理モデリングとかも（ひょっとして）出来るかも。
