https://m-hiyama.hatenablog.com/entry/2025/04/07/132836

形式圏論を考える舞台として2-圏より二重圏のほうが良さそうな気がします。ちょっとした状況証拠をひとつ挙げます。

“二重圏を使った圏論”について考えているわけです。「コーナー、キンク、ニョロニョロ」に書いたように、完全に形式的な圏論じゃないですけど：

ただし、完全に抽象的・公理的な構造としての二重圏を使うわけではなくて（それは抽象的過ぎるので）、二重圏の一例である“関手とプロ関手の二重圏”で考えます。小さい圏、関手、プロ関手と、それらから定義された二重射〈double morphism〉からなる二重圏を $`\mathbf{ProfDC}`$ として、$`\mathbf{ProfDC}`$ 内の半形式圏論（ある程度具体化された形式圏論）が今回の話題です。

二重圏 $`\mathbf{ProfDC}`$ と、圏・関手・自然変換の2-圏 $`\mathbf{Cat}`$ との関係が問題になります。この記事の話題は、その関係を述べる準備です。通常の自然変換を、二重圏の二重射へと変換します。またその逆変換も調べます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
%\newcommand{\Imp}{\Longrightarrow} % for meta prop
\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\pto} {\not\to }
%%
\newcommand{\DM}[4]{ #1 \underset{#4}{\overset{#3}{\Box}} #2} % Double Morphism
\newcommand{\DO}[4]{ {^{#1}_{#3}\Box^{#2}_{#4}} } % Double Objects
`$

内容：

動機：圏達の2-圏と二重圏

$`\mbf{Cat}`$ は次のような2-圏です。

対象：小さい圏
射〈1-射〉：関手
2-射：自然変換

$`\mbf{Prof}`$ は次のような2-圏です。

対象：小さい圏
射〈1-射〉：プロ関手
2-射：プロ関手のあいだの自然変換

$`\mbf{ProfDC}`$ は次のような二重圏です。

対象：小さい圏
タイト射：関手
プロ射：プロ関手
二重射〈2-射〉：以下に説明

$`\mbf{ProfDC}`$ の二重射〈double morphism〉について説明します。以下のような四辺形（内部は持たないフレーム〈境界〉）を考えます。

$`\quad \xymatrix{
\cat{A} \ar[d]_F \ar[r]|{/}^P
& \cat{C} \ar[d]^G
\\
\cat{B} \ar[r]|{/}_Q
& \cat{D}
}`$

ここで、$`F, G`$ は関手で $`P, Q`$ はプロ関手（矢印は '$`\pto`$'）です。プロ関手は次のような関手です。

$`\quad P :\cat{A}^\op \times \cat{C} \to \mbf{Set} \In \mbf{CAT}\\
\quad Q :\cat{B}^\op \times \cat{D} \to \mbf{Set} \In \mbf{CAT}
`$

$`Q(F^\op, G)`$ は次の意味です。アスタリスクは、関手の図式順結合演算子記号です。

$`\quad Q(F^\op, G) := (F^\op \times G)* Q : \cat{A}^\op \times \cat{C} \to \mbf{Set}
\In \mbf{CAT}`$

関手 $`F^\op`$ は、$`F`$ と同じ対象パート写像／射パート写像を持ちますが $`F^\op : \cat{C}^\op \to \cat{D}^\op`$ というプロファイルの関手です。

プロ関手としてのプロファイルは次のようになります。

$`\quad Q(F^\op, G) : \cat{A} \to \cat{D} \In \mbf{Prof}`$

二重圏 $`\mbf{ProfDC}`$ におけるプロファイルは次です。

$`\quad Q(F^\op, G) : \cat{A} \pto \cat{D} \In \mbf{ProfDC}`$

$`Q(F^\op, G)`$ は、$`F^\op \times G`$ によるプレ結合引き戻しですが、$`Q`$ の（$`F, G`$ による）制限〈restriction〉と呼ぶこともあります。$`F, G`$ が埋め込みの場合は制限がふさわしいですが、一般的には「制限」の語感とは違った状況になります。

プロ関手 $`P`$ から制限 $`Q(F^\op, G)`$ への自然変換が、上記のフレームを埋める二重射です。

$`\qquad \alpha :: P \twoto Q(F^\op, G) : \cat{A}^\op \times \cat{C} \to \mbf{Set}\In \mbf{CAT}\\
\Longleftrightarrow \alpha :: \DM{F}{G}{P}{Q} : \DO{\cat{A}} {\cat{C}} {\cat{B}} {\cat{D}} \In \mbf{ProfDC}
`$

二行目は、以下の図式のテキスト表現です（「構造を持つ概念的事物の記述と参照：コンパニオンを例に // コンパニオン系の記述」）。

$`\quad \xymatrix{
\cat{A} \ar[d]_F \ar[r]|{/}^P
\ar@{}[dr]|{\alpha}
& \cat{C} \ar[d]^G
\\
\cat{B} \ar[r]|{/}_Q
& \cat{D}
} \\
\quad \In \mbf{ProfDC}
`$

以上で、二重圏 $`\mbf{ProfDC}`$ の二重射は説明できました。

さて、2-圏 $`\mbf{Cat}`$ を、二重圏 $`\mbf{ProfDC}`$ のなかに埋め込むことが出来ます。その埋め込みの構成のときに必要な、自然変換達の集合のあいだの同型が今回の話題です。

自然変換達の集合のあいだの同型

$`F, G:\cat{A}\to\cat{X}`$ を関手として、これらのあいだの自然変換の集合を $`\mrm{Nat}(F, G: \cat{A} \to \cat{X})`$ と書きます。$`\cat{A}, \cat{X}`$ が了解済みなら省略してもかまいません。

$`\quad \mrm{Nat}(F, G) = \mrm{Nat}(F, G: \cat{A}\to\cat{X}) = \mbf{Cat}(\cat{A}, \cat{X})(F, G)`$

圏 $`\cat{A}`$ のホム双関手〈ホム二項関手〉は次のような書き方をします。

$`\mrm{Hom}_\cat{A} : \cat{A}^\op \times \cat{A}\to \mbf{Set}`$
$`\cat{A}(\hyp, \hyp) : \cat{A}^\op \times \cat{A}\to \mbf{Set}`$
$`\cat{A}(\mrm{Id}_{\cat{A}^\op}, \mrm{Id}_\cat{A}) : \cat{A}^\op \times \cat{A}\to \mbf{Set}`$
$`\cat{A}({\mrm{Id}_{\cat{A}}}^\op, \mrm{Id}_\cat{A}) : \cat{A}^\op \times \cat{A}\to \mbf{Set}`$

プロ関手の制限と書き方を揃えるため、主に最後の書き方を使いますが、下付きの $`\cat{A}`$ は省略して、$`\cat{A}(\mrm{Id}^\op, \mrm{Id})`$ とします。

次の同型があります。

$`\quad \mrm{Nat}(F, G:\cat{A}\to\cat{X}) \cong \mrm{Nat}(\cat{A}(\mrm{Id}^\op, \mrm{Id}), \cat{X}(F^\op, G) : \cat{A}^\op \times \cat{A} \to \mbf{Set})`$

この同型を構成することがこの記事の目的です。

記法の約束

圏は、カリグラフィー体ラテン大文字で書きます。$`\cat{A}, \cat{X}`$ など。
圏の対象は、ラテンアルファベット前半の小文字とします。前半は 'p' より前とします。'p' からは後半です。$`f, g, h`$ なども前半ですから対象を表します（紛らわしいから今回は使いませんけど）。
圏の射は、ラテン小文字後半の小文字とします。$`p, q, u, v, w`$ など。
関手は、ラテンアルファベット前半の大文字とします。$`A, B, F, G`$ など。
プロ関手は、ラテンアルファベット後半の大文字とします。$`P, Q`$ など。
自然変換は、ギリシャ文字小文字とします。$`\alpha, \varphi`$ など。

$`u: a \to b \In \cat{A}`$ に対して、対応する反対圏の射を $`\o{u}: \o{b} \to \o{a} \In \cat{A}^\op`$ と書きます。対象集合／射集合の要素としては、$`\o{a} = a, \o{b} = b, \o{u} = u`$ なので、$`u: b \to a \In \cat{A}^\op`$ でも間違いではありませんが、反対圏と反変関手（「イイカゲンとインチキを悔い改めるためのコスト」参照）について明確に意識するためにこの記法を使います。

上線〈オーバーライン〉を引いた変数は、反対圏の対象集合／射集合上を走る変数として扱います*1。$`F:\cat{A} \to \cat{X}`$ に対する $`F^\op : \cat{A}^\op\to \cat{X}^\op`$ に引数を渡した形式は
$`\quad F^\op(\o{a}), F^\op(\o{u})`$
です。これは、ラムダ記法で書けば次のようです。

$`\quad {F^\op}_\mrm{obj} = \lambda\, \o{a}\in |\cat{A}^\op|.\, F^\op(\o{a})\\
\quad {F^\op}_\mrm{mor} = \lambda\, \o{u}\in \mrm{Mor}(\cat{A}^\op).\, F^\op(\o{u})
`$

しかし、次のような解釈も可能です。

$`\quad {\o{F}}_\mrm{obj} = \lambda\, a\in |\cat{A}|.\, F^\op(\o{a})\\
\quad {\o{F}}_\mrm{mor} = \lambda\, u\in \mrm{Mor}(\cat{A}).\, F^\op(\o{u})
`$

ここで、$`\o{F}(a) = \o{F(a)} = F^\op(\o{a})`$ です。上線〈オーバーライン〉は、
「層化ストリング図 // 裏返し反変関手」で導入した裏返し関手〈reversing functor〉の略記です。次の可換図式があります。

$`\quad \xymatrix{
\cat{A} \ar[r]^F \ar[d]_{\mrm{Rev}_\cat{A}}
\ar[dr]|{\o{F}}
& \cat{X} \ar[d]^{\mrm{Rev}_\cat{X}}
\\
\cat{A}^\op \ar[r]_{F^\op}
& \cat{X}^\op
}\\
\quad \text{commutative}
`$

対象 $`a\in |\cat{A}|`$ を追跡すれば事情が分かるでしょう。

$`\quad \xymatrix{
a \ar@{|->}[r]^F \ar@{|->}[dd]_{ \mrm{Rev}_\cat{A} } \ar@{|->}[dr]|{\o{F}}
&F(a) \ar@{|->}[d]|{\mrm{Rev}_\cat{X} }
\\
{}
&{\o{F(a)}} \ar@{=}[d]
\\
\o{a} \ar@{|->}[r]_{F^\op}
& {F^\op(\o{a})}
}
`$

$`F^\op(\o{a})`$ が、下側横向きの矢印を表すか、斜め矢印を表すかは文脈依存です。が、次の等式は常に成立します。

$`\quad \o{F}(a) = \o{F(a)} = F^\op(\o{a})`$

割と広く使われている習慣として、ホム双関手〈ホム二項関手〉の2つの引数に対象と射が入ったときは、対象を恒等射と解釈します。

$`\quad \cat{A}(\o{a}, v) = \cat{A}(a, v) = \cat{A}(\id_a, v)`$

自然変換の変換と逆変換の定義

自然変換 $`\alpha \in \mrm{Nat}(F, G: \cat{A}\to \cat{X})`$ に対して、別な形の自然変換 $`\widetilde{\alpha}`$ を定義します*2。

$`\quad \widetilde{\alpha}\in \mrm{Nat}(\cat{A}(\mrm{Id}^\op, \mrm{Id}), \cat{X}(F^\op, G) : \cat{A}^\op\times \cat{A} \to \mbf{Set})`$

$`\alpha`$ も $`\widetilde{\alpha}`$ も自然変換なので、次のような射の族で自然性を満たすものです。

$`\quad (\alpha_a: F(a) \to G(a) )_{a\in |\cat{A}|}\\
\quad (\widetilde{\alpha}_{\o{a}, b} : \cat{A}(\o{a}, b)\to \cat{X}(F^\op(\o{a}), G(b)) )_{(\o{a}, b)\in |\cat{A}^\op \times \cat{A}|}
`$

$`\widetilde{\alpha}`$ の成分は次のように定義します。

$`\text{For }a\in |\cat{A}| \:\text{ i.e. } \o{a}\in |\cat{A}^\op|\\
\text{For }b\in |\cat{A}|\\
\text{For }(p : a\to b) \in \cat{C}(\o{a}, b)\\
\quad \widetilde{\alpha}_{\o{a}, b}(p) := (F(p); \alpha_b : F(a) \to B(b))
\:\text{or-also } (\alpha_a ; G(p) : F(a) \to G(b) )
`$

ここで $`\text{or-also}`$ は、「どちらで定義してもいい」ということです。次の2つの定義があり、どちらでも同じです。

$`\widetilde{\alpha}_{\o{a}, b}(p) := (F(p); \alpha_b : F(a) \to G(b))`$
$`\widetilde{\alpha}_{\o{a}, b}(p) := (\alpha_a ; G(p) : F(a) \to G(b) )`$

同じである理由は、次の自然性があるからです。

$`\text{For }p:a \to b \In \cat{A} \:\text{ i.e. }p \in \cat{A}(\o{a}, b)\\
\quad \xymatrix{
F(a) \ar[r]^{\alpha_a} \ar[d]_{F(p)}
\ar[dr]|{\widetilde{\alpha}_{\o{a}, b}(p) }
&G(b) \ar[d]^{G(p)}
\\
F(b) \ar[r]_{\alpha_b}
&G(b)
}\\
\text{commutative }\In \cat{X}
`$

こうして定義された射の族 $`(\widetilde{\alpha}_{\o{a}, b} )_{(\o{a}, b)\in |\cat{A}^\op\times \cat{A}|}`$ が実際に自然変換になっているかどうかは後で考えます。

さて、今度は $`\varphi \in \mrm{Nat}(\cat{A}(\mrm{Id}^\op, \mrm{Id}), \cat{X}(F^\op, G))`$ に対して、別な自然変換 $`\check{\varphi}`$ を定義します*3。$`\alpha \mapsto \widetilde{\alpha}`$ と $`\varphi \mapsto \check{\varphi}`$ は互いに逆写像となりますが、それは次節で示します。

$`\text{For }\varphi :: \cat{A}(\mrm{Id}^\op, \mrm{Id})\twoto \cat{X}(F^\op, G):\cat{A}^\op \times \cat{A} \to \mbf{Set}\In \mbf{CAT}\\
\text{For }a\in |\cat{A}|\\
\quad \check{\varphi}_a := (\varphi_{\o{a}, a}(\id_a) : F(a) \to G(a) )
`$

互いに逆写像であること

前節で定義した $`\alpha \mapsto \widetilde{\alpha}`$ と $`\varphi \mapsto \check{\varphi}`$ は互いに逆写像であることを示します。そのためには、次の等式が必要です。

$`\check{\widetilde{\alpha}} =\alpha`$
$`\widetilde{\check{\varphi}} =\varphi`$

成分を計算して示しましょう。

$`\text{For } a \in |\cat{A}|\\
\quad \check{\widetilde{\alpha}}_a \\
= \widetilde{\alpha}_{\o{a}, a}(\id_a)\\
= F(\id_a) ; \alpha_a\\
= \id_{F(a)} ; \alpha_a \\
= \alpha_a
`$

これで一番目は示せました。次は二番目です。

$`\text{For }\o{a}\in |\cat{A}^\op|, b\in |\cat{A}|\\
\text{For }p : a\to b \In \cat{A}\\
\quad \widetilde{\check{\varphi}}_{\o{a}, b}(p)\\
= \check{\varphi}_a ; G(p)\\
= \varphi_{\o{a}, a}(\id_a) ; G(p)\\
= \varphi_{\o{a}, b}(p)
`$

ここで、次の等式を使っています。

$`\quad \varphi_{\o{a}, a}(\id_a) ; G(p) = \varphi_{\o{a}, b}(p)`$

これは、次の $`\varphi`$ の自然性から出ます。

$`\text{For }p : a \to b \In \cat{A}\\
\quad \xymatrix{
{\cat{A}(\o{a}, a)} \ar[r]^-{\varphi_{\o{a}, a}}
\ar[d]_{\cat{A}(\o{a}, p) }
&{\cat{X}(F^\op(\o{a}), G(a) )} \ar[d]^{\cat{X}(F^\op(\o{a}), G(p) ) }
\\
{\cat{A}(\o{a}, b)} \ar[r]_-{\varphi_{\o{a}, b}}
&{\cat{X}(F^\op(\o{a}), G(b) ) }
}\\
\quad \text{commutative }\In \mbf{Set}
`$

集合の要素を追いかけます。

$`\quad \xymatrix{
(\id_a : a\to a) \ar[r]^-{\varphi_{\o{a}, a} }
\ar[dd]_{\hyp ; p}
&(\varphi_{\o{a}, a}(\id_a) : F^\op(\o{a}) \to G(a)) \ar[d]^{\hyp; G(p)}
\\
{}
&(\varphi_{\o{a}, a}(\id_a); G(p) : F^\op(\o{a}) \to G(b) ) \ar@{=}[d]
\\
(\id_a ; p : a \to b) \ar[r]_-{\varphi_{\o{a}, b}}
&(\varphi_{\o{a}, b}(p) : F^\op(\o{a}) \to G(b) )
}
`$

この図式のなかに等式 $`\varphi_{\o{a}, a}(\id_a) ; G(p) = \varphi_{\o{a}, b}(p)`$ が含まれます。

自然変換の変換が自然変換であること

自然変換 $`\alpha : F \to G`$ に対する $`\widetilde{\alpha}`$ が“自然変換”だと言いましたが、それは後知恵であって、現時点では $`\widetilde{\alpha}`$ が自然変換かどうかは分かっていません。自然性を確認する必要があります。$`\widetilde{\alpha}`$ の自然性は次のように書けます。

$`\text{For }u: c \to a \In \cat{A} \:\text{ i.e. }\o{u}: \o{a}\to \o{c}\In \cat{A}^\op\\
\text{For }v: b \to d \In \cat{A} \\
\quad \xymatrix{
{ \cat{A}(\o{a}, b) } \ar[r]^-{ \widetilde{\alpha}_{\o{a}, b} }
\ar[d]_{\cat{A}(\o{u}, v)}
&{ \cat{X}(F^\op(\o{a}), G(b)) }
\ar[d]^{\cat{X}(F^\op(\o{u}), G(v))}
\\
{\cat{A}(\o{c}, d)} \ar[r]_-{\widetilde{\alpha}_{\o{c}, d}}
&{\cat{X}(F^\op(\o{c}), G(d)) }
}\\
\quad \text{commutative }\In \mbf{Set}
`$

要素を追いかけると次のようです。

$`\quad \xymatrix{
(p: a \to b) \ar[r]^-{\widetilde{\alpha}_{\o{a}, b} }
\ar[dd]_{u;\hyp; v}
&(\widetilde{\alpha}_{\o{a}, b}(p) : F^\op(\o{a}) \to G(b))
\ar[d]^{F(u) ; \hyp ; G(v)}
\\
{}
&(F(u); \widetilde{\alpha}_{\o{a}, b}(p) ; G(v) : F^\op(\o{c}) \to G(d) )
\ar@{=}[d]
\\
(u;p;v : c \to d) \ar[r]_-{\widetilde{\alpha}_{\o{c}, d} }
&(\widetilde{\alpha}_{\o{c}, d}(u;p;v) : F^\op(\o{c}) \to G(d) )
}
`$

要求される等式は次のものです。

$`\quad
F(u); \widetilde{\alpha}_{\o{a}, b}(p) ; G(v) = \widetilde{\alpha}_{\o{c}, d}(u;p;v)
\; : F(c) \to G(d) \In \cat{X}
`$

左辺・右辺を $`\widetilde{\alpha}`$ の定義により展開してみます。

$`\quad F(u); \widetilde{\alpha}_{\o{a}, b}(p) ; G(v)\\
= F(u) ; (F(p); \alpha_b ) ; G(v)\\
= (F(u) ; F(p) ) ; (\alpha_b ; G(v) )
`$

$`\quad \widetilde{\alpha}_{\o{c}, d}(u;p;v) \\
= F(u;p;v) ; \alpha_d \\
= ( F(u); F(p); F(v) ) ; \alpha_d \\
= ( F(u); F(p) );( F(v) ; \alpha_d )
`$

等式 $`\alpha_b ; G(v) = F(v) ; \alpha_d`$ が示せれば、目的の等式も言えます。当該等式は次の $`\alpha`$ の自然性から出ます。

$`\text{For }v : b \to d \In \cat{A}\\
\quad \xymatrix{
F(b) \ar[r]^{\alpha_b} \ar[d]_{F(v)}
&G(b) \ar[d]^{G(v)}
\\
F(d) \ar[r]_{\alpha_d}
&G(d)
}\\
\quad \text{commutative }\In \cat{X}
`$

つまり、$`\alpha`$ が自然変換であるという仮定のもとで、変換した $`\widetilde{\alpha}`$ も自然変換だと言えました。

自然変換の逆変換が自然変換であること

前節で、$`\alpha`$ に対する $`\widetilde{\alpha}`$ が自然性を持つことを示しました。今度は、$`\varphi`$ に対する $`\check{\varphi}`$ が自然性を持つことを示しましょう。

$`\check{\varphi}`$ の自然性は次の可換図式で表されます。

$`\text{For }w: a \to b \In \cat{A}\\
\quad \xymatrix{
F(a) \ar[r]^{\check{\varphi}_a} \ar[d]_{F(w)}
&G(a) \ar[d]^{G(w)}
\\
F(b) \ar[r]_{\check{\varphi}_b}
&G(b)
}\\
\quad \text{commutative }\In \cat{X}
`$

等式で書けば：

$`\quad \check{\varphi}_a; G(w) = F(w); \check{\varphi}_b \; : F(a) \to G(b) \In \cat{X}`$

$`\check{\varphi}`$ の定義により展開すると：

$`\quad {\varphi}_{\o{a}, a}(\id_a); G(w) = F(w); {\varphi}_{\o{b},b}(\id_b) \; : F(a) \to G(b) \In \cat{X}`$

これが示すべき等式です。

もし、以下の2つの等式が成立するなら、目的の等式は言えます。

$`{\varphi}_{\o{a}, a}(\id_a); G(w) = \varphi_{\o{a}, b}(w)`$
$`F(w); {\varphi}_{\o{b},b}(\id_b) = \varphi_{\o{a}, b}(w)`$

よって、この2つの等式をターゲット命題に設定します。どちらも、$`\varphi`$ の自然性から導出します。

$`\varphi`$ の自然性から次の可換図式があります。

$`\text{For }w: a \to b\In \cat{A}\\
\quad \xymatrix{
\cat{A}(\o{a}, a) \ar[r]^-{\varphi_{\o{a}, a}}
\ar[d]_{\cat{A}(\o{a}, w)}
&{\cat{X}(F^\op(\o{a}), G(a))}
\ar[d]^{\cat{X}(F^\op(\o{a}), G(w) )}
\\
\cat{A}(\o{a}, b) \ar[r]_-{\varphi_{\o{a}, b}}
&{\cat{X}(F^\op(\o{a}), G(b) )}
}\\
\quad \text{commutative }\In \cat{X}
`$

要素を追いかけます。

$`\quad \xymatrix{
(\id_a :a \to a) \ar@{|->}[r]^-{\varphi_{\o{a}, a}} \ar@{|->}[dd]_{\hyp; w}
&(\varphi_{\o{a}, a}(\id_a) : F^\op(\o{a}) \to G(a)) \ar@{|->}[d]^{\hyp; G(w)}
\\
{}
&(\varphi_{\o{a}, a}(\id_a) ; G(w) : F^\op(\o{a}) \to G(b)) \ar@{=}[d]
\\
(\id_a; w : a\to b) \ar@{|->}[r]_-{\varphi_{\o{a}, b}}
&(\varphi_{\o{a}, b}(w) : F^\op(\o{a}) \to G(b))
}`$

これから一番目のターゲット命題（等式）が言えます。

$`\quad {\varphi}_{\o{a}, a}(\id_a); G(w) = \varphi_{\o{a}, b}(w)`$

$`\varphi`$ の自然性から次の可換図式もあります。

$`\text{For }w: a \to b\In \cat{A}\:\text{ i.e. }\o{w}: \o{b}\to \o{a}\In \cat{A}^\op\\
\quad \xymatrix{
\cat{A}(\o{b}, b) \ar[r]^-{\varphi_{\o{b}, b}}
\ar[d]_{\cat{A}(\o{w}, b)}
&{\cat{X}(F^\op(\o{w}), G(b))}
\ar[d]^{\cat{X}(F^\op(\o{w}), G(b) )}
\\
\cat{A}(\o{a}, b) \ar[r]_-{\varphi_{\o{a}, b}}
&{\cat{X}(F^\op(\o{a}), G(b) )}
}\\
\quad \text{commutative }\In \cat{X}
`$

同様に要素を追いかけると（割愛）、二番目のターゲット命題（等式）が言えます。

$`\quad F(w); {\varphi}_{\o{b},b}(\id_b) = \varphi_{\o{a}, b}(w)`$

以上により、$`\varphi`$ が自然変換であるという仮定のもとで、逆変換した $`\check{\varphi}`$ も自然変換だと言えました。

まとめ

$`\alpha \mapsto \widetilde{\alpha}`$ が自然変換を自然変換に移すことから、次の写像が確かに定義されています。

$`\quad \widetilde{\hyp} : \mrm{Nat}(F, G: \cat{A}\to \cat{X})\to \mrm{Nat}(\cat{A}(\mrm{Id}^\op, \mrm{Id}), \cat{X}(F^\op, G) : \cat{A}^\op\times \cat{A} \to \mbf{Set} )`$

$`\varphi \mapsto \check{\varphi}`$ が自然変換を自然変換に移すことから、次の写像が確かに定義されています。

$`\quad \check{\hyp} : \mrm{Nat}(\cat{A}(\mrm{Id}^\op, \mrm{Id}), \cat{X}(F^\op, G) : \cat{A}^\op\times \cat{A} \to \mbf{Set} ) \to \mrm{Nat}(F, G: \cat{A}\to \cat{X})
`$

これら2つの写像は互いに逆で、一対一対応を与えます。よって、2つの集合は同型です。

$`\quad \mrm{Nat}(F, G: \cat{A}\to \cat{X}) \cong \mrm{Nat}(\cat{A}(\mrm{Id}^\op, \mrm{Id}), \cat{X}(F^\op, G) : \cat{A}^\op\times \cat{A} \to \mbf{Set} )`$

冒頭でも触れたように、この同型は、2-圏 $`\mbf{Cat}`$ と二重圏 $`\mbf{ProfDC}`$ の関係を考える上で基本的な事実となります。

*1:「状態遷移系としての前層・余前層・プロ関手」参照。使用例は例えば "(Co)ends for representations of tensor categories" by Noelia Bortolussi, Martín Mombelli など。

*2:定義した段階では、自然変換かどうかは分かりません。

*3:定義した段階では、自然変換かどうかは分かりません。

動機： 圏達の2-圏と二重圏