形式圏論を考える舞台として2-圏より二重圏のほうが良さそうな気がします。ちょっとした状況証拠をひとつ挙げます。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
%\newcommand{\mfk}[1]{\mathfrak{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\id}{ \mathrm{id}}
\newcommand{\op}{ \mathrm{op}}
\newcommand{\In}{ \text{ in }}
\newcommand{\hyp}{\text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\pto} {\dashrightarrow}
%\newcommand{\o}[1]{ \overline{#1} }
`$
内容：
第二種米田埋め込み
「米田テンソル計算 4： 米田埋め込み」において、第一種米田埋め込みと第二種米田埋め込みを定義しています。
小さい圏 $`\cat{C}`$ の前層の圏を $`\cat{C}^\wedge`$ 、余前層の圏を $`\cat{C}^\vee`$ とします。第一種米田埋め込み（通常の米田埋め込み）の共変版・反変版、第ニ種米田埋め込みの共変版・反変版*1の4つのプロファイルを列挙すると：
$`\quad \mbf{Yo}_\cat{C} : \cat{C} \to \cat{C}^\wedge \In \mbf{CAT}\\
\quad \mbf{coYo}_\cat{C} : \cat{C}^\op \to \cat{C}^\vee \In \mbf{CAT}\\
\quad \mbf{YO}_{\cat{C},\cat{D}} : \mbf{Cat}(\cat{C}, \cat{D})\to \mbf{Prof}(\cat{D}, \cat{C}) \In \mbf{CAT}\\
\quad \mbf{coYO}_{\cat{C},\cat{D}} : \mbf{Cat}(\cat{C}, \cat{D})\to \mbf{Prof}(\cat{C}, \cat{D}) \In \mbf{CAT}
`$
これらの定義を簡略に（かつ一部省略して）書けば：
$`\quad \mbf{Yo}_\cat{C}(A) := \cat{C}(\hyp, A)\\
\quad \mbf{coYo}_\cat{C}(A) : \cat{C}(A, \hyp)\\
\quad \mbf{YO}_{\cat{C},\cat{D}}(F) := \cat{D}(\hyp, F(\hyp) )\\
\quad \mbf{coYO}_{\cat{C},\cat{D}}(F) := \cat{D}(F(\hyp),\hyp)
`$
詳細は「米田テンソル計算 4： 米田埋め込み」を見てください。
第二種米田埋め込みは、関手をプロ関手として埋め込むものです。第一種米田埋め込みは、第二種米田埋め込みに包摂されます。
具体的な定義を書いて第二種米田埋め込みを定義できるのですが、第二種米田埋め込みを等式的に特徴付けることは、2-圏ベースの形式圏論では上手に扱えないようです。
二重圏のコンパニオン／コンジョイント
二重圏のコンパニオン〈companion〉とコンジョイント〈conjoint〉については、ロバート・パレ〈Robert Pare〉のスライド "The horizontal/vertical synergy of double categories" の7ページから先に手短に書いてあります。nLab項目もあります。
パレはタイト射を横方向に描き、nLabは縦方向なので注意してください。
タイト射 $`f:A\to B`$ が与えられたとき、プロ射〈ルーズ射〉$`v:A \pto B`$ とのコンパニオン・ペア〈companion pair〉$`(f, w)`$ が、等式的条件により定義できます。また双対的に、プロ射〈ルーズ射〉$`w:B \pto A`$ とのコンジョイント・ペア〈conjoint pair〉$`(f , w)`$ も、等式的条件により定義できます。
パレに従い、タイト射 $`f`$ に対するコンパニオン（コンパニオン・ペアのパートナー）を $`f_*`$ 、$`f`$ に対するコンジョイント（コンジョイント・ペアのパートナー）を $`f^*`$ と書くことにします。
タイト射を縦方向に描くなら、$`f, f_*, f^*`$ の配置は以下のようになります。
$`\quad \xymatrix{
B \ar@{-->}[r]^{f^*}
&A \ar@{-->}[r]^{f_*} \ar[d]|f
&B
\\
{}
&B
{}
}`$
このレイアウトに限った話ですが、$`f`$ を反時計回りに90度回転すると $`f_*`$ になります。そして、$`f`$ を時計回りに90度回転させて、さらに矢印の向きを逆にすると $`f^*`$ になります。
米田の星で書く
タイト射を関手、プロ射をプロ関手とする二重圏を考えると、関手 $`F:\cat{C}\to\cat{D}`$ のコンパニオンは $`\mbf{coYO}(F)`$ となり、コンジョイントは $`\mbf{YO}(F)`$ となります。パレのアスタリスクを使う記法だと：
$`\quad F_* := \mbf{coYO}(F)\\
\quad F^* := \mbf{YO}(F)
`$
しかし、アスタリスクは色々な場面で使われすぎです。アスタリスクではなくて、「米」を使いましょう。「困った時の米田頼み、ご利益ツールズ」より：
さて、A∈|C| で定義される反変関手をA米で表すことにします。つまり：
- A米 := λx.C(x, A) : Cop→Set
上付きの文字はアスタリスクではなくて漢字の「米」です。米田の米〈よね〉からです。下付きの米は次のように定義します。
- A米 := λy.C(A, y) : C→Set
こちらは共変関手（opが付いてない）です。
$`\quad F_{米} := \mbf{coYO}(F)\\
\quad F^{米} := \mbf{YO}(F)
`$
第ニ種米田埋め込み（第一種も）は、二重圏のなかでコンパニオン／コンジョイントにより等式的に特徴付けられて、米田の星で簡潔に書けます。
*1:どちらを共変（あるいは反変）と呼ぶかはかなりややこしいです！
