まだ生煮えの話をします。最初に動機を書くと； 随伴系を定義する2つの方法である「ニョロニョロ関係式」と「自然なホムセット同型」が同値であることをお絵描き〈絵算 | {pictorial | graphical | diagrammatic} calculus〉で示したい！ ということです。
ニョロニョロ関係式〈snake {law | relation | equation | identity}〉を仮定して自然なホムセット同型を導くことは、過去記事「代数的な随伴系から自然なホムセット同型へ」でやっています。その過去記事において次のように書いています。
“自然なホムセット同型”から“単位と余単位を含む代数系”を作るほうは、（僕は）うまくストリング図が描けなくて毎回行き詰まります。なので、やりません（うまくいったら報告するかも）。
[追記 date="2023-07-31"]
先に自然なホムセット同型が与えられて、そこから代数的な随伴系を構成することができるのですが、うまいやり方が見つかりません。身も蓋も無いやり方は次の記事に書きました。
[/追記]
追記で参照されている別な過去記事「随伴の自然なホムセット同型から単位自然変換へ」の冒頭では：
ストリング図を使って計算する方法は思いつきません。うまくいってないです。もうしょうがないので、等式的な計算を使います。与えられた自然性を表す可換図式から要素を追いかけて等式を絞り出して。連立の等式から目的の自然性等式を得る方法です。面白くないし、絵図的直感は効かないです。ムーッ（不満）。
「ムーッ（不満）」な状態がずっと続いています。が、最近、二重圏のなかで形式圏論をすれば、「自然なホムセット同型」から「ニョロニョロ関係式」を出せるのではないか（もちろん、お絵描きで！）と思っています。細部を詰めてないので、まだ生煮えなんですがね。
動機はそういうわけなんですが、この記事では二重圏における計算方法（もちろん、お絵描きで！）を説明します。とりあえず、コーナーとキンクの計算からニョロニョロ関係式らしきものが出ることを確認します。$`\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{\twoto} {\Rightarrow }
\newcommand{\pto} {\dashrightarrow}
%\newcommand{\o}[1]{ \overline{#1} }
\newcommand{\VertL}{ { \,\mathrm{I}\, } } % Vertical Line
\newcommand{\HorizL}{ \style{display: inline-block; transform: rotate(90deg) } { \,\mathrm{I}\, } } % Horizontal Line
\require{enclose}
`$
内容：
2-圏への不満
ひとつ前の記事「二重圏のコンパニオン／コンジョイントと米田の星」も、今日の話題と関係しています。当初、「自然なホムセット同型」から「ニョロニョロ関係式」を出す問題を、2-圏 $`\mbf{Cat}`$ のなかで考えていました。これがうまくいかない。それでだんだん「2-圏でやるのはダメなんじゃないか」と考えるようになりました。
2-圏のなかでナニカをやることが、不可能ではないにしろ面倒だったり晦渋〈かいじゅう〉になってしまう事態を何度か経験しました。例えばひとつ前の記事で書いたこと：
第二種米田埋め込みを等式的に特徴付けることは、2-圏ベースの形式圏論では上手に扱えないようです。
「上手に扱えない」とは、不可能ではないにしろ面倒だったり晦渋になってしまう、ということです。
関手 $`F:\cat{C}\to \cat{D}`$ の第二種米田埋め込み（の値） $`F_{米} = \mbf{coYO}(F)`$ （「二重圏のコンパニオン／コンジョイントと米田の星」参照）を2-圏 $`\mbf{Cat}`$ 内で特徴付けるには、おそらくカン拡張を使う必要があります。
細部を確認してないので「おそらく」なんですが、次の図式で表現される問題を解く必要があります。
$`\quad \xymatrix@R+0.5pc {
\cat{C} \ar[rr]^{よ} \ar[dr]_{F}
&{} \ar@{}[d]|{?}
&{\cat{C}^\wedge}
\\
{}
&\cat{D} \ar@{.>}[ur]_{?}
&{}
}\\
\quad \text{left Kan extension? }\In \mbf{Cat}
`$
ここで：
- $`\cat{C}^\wedge`$ は、圏 $`\cat{C}`$ の前層の圏
- $`{よ}`$ は、通常の米田埋め込み
- 疑問付が付いた1-射〈関手〉と2-射〈自然変換〉は未知
- 疑問付が付いた未知部分を埋めて左カン拡張〈left Kan extension〉を作れますか？ という問題
この問題に解があったとして、それを $`(G, \alpha)`$ とします。次のような状況です。（'$`*`$' は、関手の図式順結合の中置演算子記号です。）
$`\quad \alpha :: よ \twoto F*G : \cat{C}\to \cat{C}^\wedge \In \mbf{CAT}`$
$`G`$ は、米田埋め込み $`よ`$ の $`F`$ に沿った左カン拡張〈left Kan extension of Yoned embedding along $`F`$〉です。この $`G`$ が（おそらく）$`F_{米}`$ を与えます。
と、こう言われても非常に分かりにくいですよね。そもそも、前層の圏、（通常の）米田埋め込み、カン拡張を使うので、だいぶ準備が必要。まー、それは致し方ないとしても、この構成法が自然〈オーガニック〉な気がしないのです。「気がしない」のはあくまで主観で僕の好みの問題ですが、「やりたいことが出来ない」という構造的問題に繋がっている気がします（また「気が{する | しない}」だけど）。
上の $`G`$ を少し変形して、多少は $`F_{米}`$ っぽくしましょう。$`G`$ は関手圏への関手なので、次のように書けます。
$`\quad G : \cat{D} \to [\cat{C}^\op, \mbf{Set}] \In \mbf{CAT}`$
逆カリー化〈反カリー化〉します。横着して、逆カリー化の結果も同じ名前 $`G`$ とします。
$`\quad G : \cat{C}^\op \times \cat{D} \to \mbf{Set} \In \mbf{CAT}`$
プロ関手の2-圏のなかで解釈します。横着して、プロ関手も同じ名前 $`G`$ とします。
$`\quad G : \cat{C} \to \cat{D} \In \mbf{Prof}`$
プロ関手の2-圏 $`\mbf{Prof}`$ のなかで見れば、$`G`$ と $`F_{米}`$ は、少なくともプロファイルは揃っていることが分かります。
ここまでのあやふやな議論をキッチリ正当化できたとしても、それを絵算として表現するのは難しそうです（絶対にできないとは断言しませんが）。感触としては「2-圏ではダメそう」です。
二重圏による形式圏論
二重圏を環境として使う形式圏論はけっこう多くの人がやっています。最近の人だとセレップ・ロアルド・クーデンバーグ〈Seerp Roald Koudenburg〉とか、ナタリエル・アーカーとディラン・マクダルメット〈Nathanael Arkor, Dylan McDermott〉のコンビかな*1。
形式圏論〈formal category theory | formal theory of categories〉とは、抽象化された圏論で、「圏とは何か？」には答えないで展開する圏論です。抽象的線形代数が「ベクトルとは何か？」には答えないのと同じです。「ベクトルとは、ベクトル空間の台集合の要素」という定義はありますが、これでベクトルの実体が判明するわけではないです。同様に、形式圏論における圏の定義は「圏とは、ドクトリンの対象」です。ドクトリン*2はそれ自体が圏類似代数系〈category-like algebraic system〉ですが、それが2-圏だったり二重圏だったりするわけです。
形式圏論は結局、“圏論を使って圏論をする”理論です。外側で使う圏論が、“2-圏の圏論”だったり“二重圏の圏論”だったりするので、通常の圏論より難しくなってしまいます。しかしこれは、メタ理論を展開するときの宿命なので致し方ないです。
さて、前節で述べた感触「2-圏ではダメそう」を真に受ければ、2-圏じゃない環境に以降すべきで、とりあえずの移行先は“二重圏を環境として使う形式圏論”となります。僕はそう判断したってことですね。
ただし、完全に抽象的・公理的な構造としての二重圏を使うわけではなくて（それは抽象的過ぎるので）、二重圏の一例である“関手とプロ関手の二重圏”で考えます。小さい圏*3、関手、プロ関手と、それらから定義された二重射〈double morphism〉からなる二重圏を $`\mbf{ProfDC}`$ として、$`\mbf{ProfDC}`$ 内の半形式圏論（ある程度具体化された形式圏論）が今回の話題です。二重圏 $`\mbf{ProfDC}`$ 内で絵を描くことにより、「自然なホムセット同型」から「ニョロニョロ関係式」を出せれば（当初の）目的は達成です。
動機や背景の話はここまでで、次節からは単に計算技法の話です。計算の手順やコツの話は味気ないですが、計算が出来ないと何もできないので、まずは（絵による）計算技法を開発します。
矩形からコーナーへ
二重圏の図示は、矩形をベースとしたペースティング図が主流です。ただし、以下の過去記事に書いたように縦横の方向をどのように使うかが人によりバラバラで困った状況です。
二重圏の方向（プロ方向とタイト方向）については以下の過去記事に書いています。
ここでは、プロ方向を横方向に、タイト方向を縦方向に取ります。念の為、プロ方向の矢印は破線矢印にします。二重射（二重圏の2-射）は、プロ方向に見ることもタイト方向に見ることもあるので、場合に応じて横向き（左から右）、または縦向き（上から下）の二重矢印を添えます。方向が問題にならないときは矢印は描かないときもあります。以下は二重射をタイト方向に見たときの例です。
$`\quad \xymatrix{
\cdot \ar@{-->}[r]^{M} \ar[d]_f
\ar@{}[dr]|{\Downarrow\,\alpha}
&\cdot \ar[d]^g
\\
\cdot \ar@{-->}[r]_{N}
&\cdot
}
`$
歴史的には、混乱しながらも「縦横」を使ってきましたが、今は「縦横」を使わない傾向です*4。
さて、ペースティング図をストリング図にするためにポアンカレ双対を取ります。素直に次元を反転（2次元を0次元、1次元を90度回転の1次元、2次元を0次元に）すると、以下のようなレイアウトの図になります。矢印をすべて一律に時計回りに90度回転しているわけです。
が、これだと横方向が右から左になって嫌（気分の問題）なので、左右鏡映〈ミラー反転〉して横方向のワイヤーが左から右に走るようにします。縦横のワイヤーは特に区別しない（同じ矢印）で描きます。
$`\quad \xymatrix{
{}
&{M} \ar[d]
&{}
\\
{f} \ar[r]
& *++[o][F]{\alpha} \ar[r] \ar[d]
&{g}
\\
{}
&{N}
&{}
}
`$
以下、縦横と上下左右については今決めた約束とします*6。ペースティング図でもストリング図でも不要なラベルは省略します。
次のようなペースティング図を考えましょう。
$`\quad \xymatrix{
\cdot \ar@{-->}[r] \ar[d]
\ar@{}[dr]|{\Downarrow}
&\cdot \ar@{=}[d]
\\
\cdot \ar@{=}[r]
&\cdot
}
`$
ここで、イコール記号は縦でも横でも恒等1-射を示します。横方向なら恒等プロ射、縦方向なら恒等タイト射です。これをストリング図で描くときは、恒等射を点線にします。
$`\quad \xymatrix{
{}
&{} \ar[d]
&{}
\\
{} \ar[r]
& *+[o][F]{} \ar@{.}[r] \ar@{.}[d]
&{}
\\
{}
&{}
&{}
}
`$
白丸のノードに矢印が吸い込まれているように見えますが、それは僕の「気分の問題」により恣意的に左右鏡映したからで、横方向の矢印を右から左にすれば、上からの矢印がコーナリングして左に抜けて行くように見えます。矢印があるせいで誤解をまねきそうなので、矢印は消して、イコールを表す点線も消します。すると、次のようになります。
$`\quad \xymatrix{
{}
&{} \ar@{-}[d]
&{}
\\
{} \ar@{-}[r]
& *+[o][F]{\lrcorner}
&{}
\\
{}
&{}
&{}
}
`$
この形のストリング図をコーナー〈corner〉と呼びます。コーナーのストリング図は簡潔で良いのですが、もとの意味を見失いがちです。確認のために適宜矩形ペースティング図に翻訳することをオススメします。
コーナーを組み合わせることにより、階段の一段のような形を作れます。
$`\quad \xymatrix{
{}
&{} \ar@{-}[d]
\\
*+[o][F]{\ulcorner} \ar@{-}[r] \ar@{-}[d]
& *+[o][F]{\lrcorner}
&{}
\\
{}
&{}
}
`$
この形をキンク〈kink〉と呼びます。以下のような形の関数やら図形やら現象やらをキンクと呼ぶのです。
ワイヤー・ストレッチング
我々の目標であるニョロニョロ関係式は、以下の図（「代数的な随伴系から自然なホムセット同型へ」から再掲）の右側の2つの等式です。
これは、「ストリング図のワイヤーを引き伸ばして真っ直ぐにできるよ」というタイプの等式、つまりワイヤー・ストレッチング公式です。三角恒等式〈the triangle identities〉とかジグザク等式〈the zig-zag equations〉という名前もありますが、ヘビ〈snake〉にちなんだ「ニョロニョロ」が一番わかりやすいでしょう。
目的とする（絵図的な）公式がワイヤー・ストレッチング公式であるとすれば、それを導くための前提も何かしらワイヤー・ストレッチングに近い（絵図的な）公式であるべきでしょう。
二重圏のコンパニオンとコンジョイント（今日はちゃんと説明する余裕がない）により、4種類のコーナー達と4つのキンク・ストレッチング公式〈kink stretching formula〉達が得られます。そうして得られたキンク・ストレッチング公式を組み合わせるとニョロニョロ・ストレッチング公式を導けるのです。
キンク・ストレッチング公式
4種類のコーナーは以下です。名前を付けないで象形文字で表します。ただし、象形文字は縦横上下左右に影響されてしまうので、この記事で約束した縦横上下左右の約束でないと意味がない（むしろ誤解のもと）です。象形文字の囲み丸は、MathJaxのencloseモジュールで描いています。
- $`\enclose{circle}{\ulcorner}`$
- $`\enclose{circle}{\lrcorner}`$
- $`\enclose{circle}{\llcorner}`$
- $`\enclose{circle}{\urcorner}`$
1番と2番（$`\enclose{circle}{\ulcorner}, \enclose{circle}{\lrcorner}`$ ）の組み合わせにより、二重圏のコンパニオンの定義に対応するキンク・ストレッチング公式を記述できます。3番と4番（$`\enclose{circle}{\llcorner}, \enclose{circle}{\urcorner}`$ ）の組み合わせにより、二重圏のコンジョイントの定義に対応するキンク・ストレッチング公式を記述できます。
キンク・ストレッチング公式は4つありますが、まず、そのなかのひとつを丁寧に解説します。ひとつが理解できれば、残りの3つもほぼ同様です。
ひとつのキンク・ストレッチング公式とは次のものです。
$`\quad \xymatrix{
{}
&*+[o][F]{\ulcorner} \ar@{-}[r] \ar@{-}[d]
&{}
\\
{} \ar@{-}[r]
&*+[o][F]{\lrcorner}
&{}
} \\
= \xymatrix@R+1pc{
{}\ar@{-}[rr]
&{}
&{}
}
`$
象形文字を使ったテキスト（文字と記号の列）で表現すれば：
$`\quad \enclose{circle}{\ulcorner} ; \enclose{circle}{\lrcorner} = \HorizL`$
この公式は、2つのコーナー（特殊な二重射） $`\enclose{circle}{\ulcorner}`$ と $`\enclose{circle}{\lrcorner}`$ をこの順でタイト方向に結合すると、タイト射のプロ方向恒等射になることを主張しています。そう言われてもピンとこないでしょうから、矩形ペースティング図からキンク・ストレッチングのストリング図に至る経緯を説明しましょう。
nLab項目 companion pair から、二重圏のタイト射 $`f`$ のコンパニオン（ペアのパートナー）であるプロ射が $`g`$ （$`f_*`$ とも書く）である状況のペースティング図／ペースティング図等式を引用します。
等式の素材となる2つの二重射は次のようです。
$`\quad \xymatrix{
A \ar@{=}[d] \ar@{=}[r]
\ar@{}[dr]|\psi
&A \ar[d]^f
\\
A \ar@{-->}[r]_g
&B
} \quad
\xymatrix{
A \ar[d]_f \ar@{-->}[r]^g
\ar@{}[dr]|\phi
&B \ar@{=}[d]
\\
B \ar@{=}[r]
&B
}
`$
$`g = f_*`$ （プロ射 $`g`$ はタイト射 $`f`$ のコンパニオン）であるための条件には2つの等式があります。まず一番目の等式。ラベルは省略しています。
$`\quad \xymatrix{
\cdot \ar@{=}[r] \ar@{=}[d]
\ar@{}[dr]|{\psi}
&\cdot \ar[d]
\\
\cdot \ar@{-->}[r] \ar[d]
\ar@{}[dr]|{\phi}
&\cdot \ar@{=}[d]
\\
\cdot \ar@{=}[r]
&\cdot
}\\
=
\xymatrix{
\cdot \ar@{=}[r] \ar[d]
\ar@{}[dr]|{=}
&\cdot \ar[d]
\\
\cdot \ar@{=}[r]
&\cdot
}
`$
ギリシャ文字 $`\phi`$ は二重射を識別する名前で、空集合の意味ではありません。等式右辺の二重射は、プロ方向に見てタイト射 $`f`$ の恒等2-射のことです。
次に二番目の等式。
$`\quad \xymatrix{
\cdot \ar@{=}[r] \ar@{=}[d]
\ar@{}[dr]|{\psi}
&\cdot \ar@{-->}[r] \ar@{=}[d]
\ar@{}[dr]|{\phi}
&\cdot \ar@{=}[d]
\\
\cdot \ar@{-->}[r]
&\cdot \ar@{=}[r]
&\cdot
}\\
=
\xymatrix{
\cdot \ar@{-->}[r] \ar@{=}[d]
\ar@{}[dr]|{||}
&\cdot \ar@{=}[d]
\\
\cdot \ar@{-->}[r]
&\cdot
}
`$
等式右辺の二重射は、タイト方向に見てプロ射 $`g`$ の恒等2-射のことです。
上記2つのペースティング図等式をテキスト（文字と記号の列）で表現しましょう。nLab項目 companion pair では、タイト方向の恒等2-射もプロ方向の恒等2-射も区別せずに $`\id`$ と書いてますが、分かりにくいので $`{\mrm{ID}\!\downarrow}`$ と $`\vec{\mrm{ID}}`$ とします。この象形文字的な書き方は、タイト方向を縦とするレイアウトを前提にしているので、レイアウト（描画方向の約束）に影響されます。別なレイアウトでは混乱をまねきます。
- $`\psi ; \phi = \vec{\mrm{ID}}_f`$
- $`\psi * \phi = {\mrm{ID}\!\downarrow}_g`$
'$`;`$' は二重圏のタイト方向の結合、'$`*`$' はプロ方向の結合です。今のレイアウトでは、'$`;`$' は縦結合で、'$`*`$' は横結合です。
さて次に、ポアンカレ双対によりペースティング図をストリング図に描き変えます。一番目のペースティング図等式をストリング図等式にしてみます。
$`\quad \xymatrix{
{}
&{} \ar@{.}[d]
&{}
\\
{} \ar@{.}[r]
&*+[o][F]{\psi} \ar@{-}[r] \ar@{-}[d]
&{}
\\
{} \ar@{-}[r]
&*+[o][F]{\phi} \ar@{.}[r] \ar@{.}[d]
&{}
\\
{}
&{}
&{}
}
\\ =
\quad \xymatrix{
{}
&{} \ar@{.}[d]
&{}
\\
{}\ar@{-}[r]
&*+[o][F]{=} \ar@{-}[r] \ar@{.}[d]
&{}
\\
{}
&{}
&{}
}
`$
$`\psi`$ と $`\phi`$ で形成されていたキンクがなくなって、横向きに真っ直ぐなワイヤーになる、という等式です。
さらに、ペースティング図のイコール辺であった点線を消して、ギリシャ文字 $`\psi, \phi`$ の代わりに対応する象形文字に替えて、右辺イコールは省略して一本のワイヤーにします。
$`\quad \xymatrix{
{}
&*+[o][F]{\ulcorner} \ar@{-}[r] \ar@{-}[d]
&{}
\\
{} \ar@{-}[r]
&*+[o][F]{\lrcorner}
&{}
}
\\ =
\xymatrix{
{}\ar@{-}[rr]
&{}
&{}
}
`$
これは、この節の冒頭に挙げたキンク・ストレッチング公式のストリング図です。
テキスト（象形文字使用）で書くなら、タイト方向結合の図式順演算子記号 '$`;`$' を使い、恒等2-射 $`\vec{\mrm{ID}}`$ を横棒として次の形になります。
$`\quad \enclose{circle}{\ulcorner} ; \enclose{circle}{\lrcorner} = \HorizL`$
これも冒頭に書いたものです。
上記等式の相棒となるもうひとつの等式は、プロ方向結合の図式順演算子記号 '$`*`$' を使い、恒等2-射 $`{\mrm{ID}\!\downarrow}`$ を縦棒として次のように書けます。
$`\quad \enclose{circle}{\ulcorner} * \enclose{circle}{\lrcorner} = \VertL`$
2つの等式のペアにより、コンパニオンペアが定義されます。これは、2つのニョロニョロ等式のペアにより随伴ペアが定義されるのと事情が似ています
コンジョイントペア（nLab項目 conjunction 参照、ただし現時点では間違いがあるようです*9）を定義する等式のペア（のテキスト表示）は次のようです。
- $`\quad \enclose{circle}{\urcorner} ; \enclose{circle}{\llcorner} = \HorizL`$
- $`\quad \enclose{circle}{\llcorner} * \enclose{circle}{\urcorner} = \VertL`$
このテキスト等式に至る道筋を自分でたどるのは良い練習問題です。
なお、コーナーとキンクに関連することが次の過去記事にあります。
二重圏におけストリング図の描き方は、ジャズ=メイヤーの詳しい解説があります。
- [Mye16-18]
- Title: String Diagrams For Double Categories and Equipments
- Author: David Jaz Myers
- Submitted: 8 Dec 2016 (v1), 2 Mar 2018 (v4)
- Pages: 33p
- URL: https://arxiv.org/abs/1612.02762
描画方向に関する僕のごく短いコメントは：
キンク・ストレッチングからニョロニョロ・ストレッチングへ
単に言い回しの問題ですが、キンク・ストレッチングを次のようにも言います。
- キンクの段差〈step〉を潰して平らにする。
横方向であれ縦方向であれ、キンクの段差を潰すとワイヤーはまっすぐになります。
ニョロニョロ関係式〈等式 | 恒等式 | 法則〉も2つありますが、そのうちの一方だけを見ます。次の形のニョロニョロがワイヤー・ストレッチングでまっすぐになる、というのがニョロニョロ関係式の片一方です。
$`\quad \xymatrix{
{} \ar@{-}[d]
&{}
&{}
\\
{\cdot} \ar@{-}[d]
&*+[o][F]{\ulcorner} \ar@{-}[r] \ar@{-}[d]
&*+[o][F]{\urcorner} \ar@{-}[d]
\\
*+[o][F]{\llcorner} \ar@{-}[r]
&*+[o][F]{\lrcorner}
&{\cdot} \ar@{-}[d]
\\
{}
&{}
&{}
}`$
使ってよいキンク・ストレッチング公式は次の4つでした。
- $`\enclose{circle}{\ulcorner} ; \enclose{circle}{\lrcorner} = \HorizL`$
- $`\enclose{circle}{\ulcorner} * \enclose{circle}{\lrcorner} = \VertL`$
- $`\enclose{circle}{\urcorner} ; \enclose{circle}{\llcorner} = \HorizL`$
- $`\enclose{circle}{\llcorner} * \enclose{circle}{\urcorner} = \VertL`$
手順としては、最初に1番のストレッチング公式により縦方向の段差を潰して横にまっすぐにします。次に4番のストレッチング公式により横方向の段差を潰して縦にまっすぐにします。
1番のストレッチング公式による変形は：
$`\quad
\begin{array}{lcr}
\xymatrix{
{}
&*+[o][F]{\ulcorner} \ar@{-}[r] \ar@{-}[d]
&{}
\\
{} \ar@{-}[r]
&*+[o][F]{\lrcorner}
&{}
}
&
\xymatrix{
{}
\\
{\Longrightarrow}
\\
{}
}
&
\xymatrix{
{}\ar@{-}[rr]
&{}
&{}
}
\end{array}
`$
4番のストレッチング公式による変形は：
$`\quad
\begin{array}{llr}
\xymatrix{
{} \ar@{-}[d]
&{}
\\
*+[o][F]{\llcorner} \ar@{-}[r]
&*+[o][F]{\urcorner} \ar@{-}[d]
\\
{}
&{}
}
&
\xymatrix{
{}
\\
{\Longrightarrow}
\\
{}
}
&
\xymatrix{
{}\ar@{-}[dd]
\\
{}
\\
{}
}
\end{array}
`$
これにより、ニョロニョロ・ワイヤーは縦方向にまっすぐになります。つまり、ニョロニョロ関係式の片一方が導かれます。もう一方のニョロニョロ関係式も同様にキンク・ストレッチング公式から導かれます。
そしてそれから
以上で、二重圏のなかでニョロニョロ関係式を導く方法はわかりました。が、ホムセットやホムセットの要素という概念を二重圏ベースの形式圏論において定式化しないと、ホムセット同型からキンク・ストレッチング公式に至る部分が定式化できません。具体的な圏論（形式化する前の圏論）に出てくる諸々の概念を二重圏ベースの形式圏論へと翻訳するための辞書を完備する必要がありますね。
*1:彼らの動画があります。Formalising size in formal category theory, Higher-order algebraic theories, The formal theories of presheaves and cocompletions
*2:「補足と続き： ベックの分配法則に基づく“一般化圏の製造工場” // ドクトリン」参照。
*3:サイズの問題を避けるために小さい圏としますが、実際には大きい圏も扱います。
*4:2-圏では相変わらず「縦横」を使いますが、混乱はないので問題はありません。
*5:この図はどっかで見て拾ったものですが、どこだか忘れてしまったので出典不明です。
*6:とにかく約束を決めないと、うまくコミュニケーションできません。約束の決め方の一例は「二重圏の語法・記法、ローカルルール事例」にあります。ただし、この記事ローカルの約束はまた別です。
*7:画像： https://www.researchgate.net/figure/represents-the-kink-solution-shape-for-Equation-13_fig2_377804010 より
*8:画像： https://chicodeza.com/freeitems/hebi-illust.html より
*9:$`\circ_\lambda, \circ_\tau`$ は反図式順演算子記号のはずですが、左右が逆になっています。図式順演算子記号と解釈すればあってるけど、それだと他のnLab項目と整合しないし。
