添加仮想二重圏

二重圏の拡張である仮想二重圏〈virtual double category〉、添加仮想二重圏〈augmented virtual double category〉に興味がわいて、次の2つの論文をポチポチと拾い読みしています。

• [Kou19-22]
• Title: Augmented virtual double categories
• Author: Seerp Roald Koudenburg
• Submitted: 24 Oct 2019 (v1), 8 Oct 2022 (v3)
• Pages: 65p
• URL: https://arxiv.org/abs/1910.11189

---

• [AM23-]
• Title: The formal theory of relative monads
• Authors: Nathanael Arkor, Dylan McDermott
• Submitted: 27 Feb 2023 (v1), 17 May 2023 (v2)
• Pages: 85p
• URL: https://arxiv.org/abs/2302.14014

二重圏 → 仮想二重圏 → 添加仮想二重圏 と構造が複雑化しますが、それだけではなくて、一部の演算と法則は捨てられています。つまり、要求がゆるくなっているのです。捨てられた（要求されなくなった）演算・法則にも注目すべきでしょう。

この記事では仮想二重圏／添加仮想二重圏の定義を紹介するだけです。とはいえ、仮想二重圏／添加仮想二重圏は、定義・記述するだけでもけっこう大変です。$`\newcommand{\In}{\text{ in }}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\dblcat}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\proar}{\dashrightarrow }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\conc}{ \mathop{\#} }
\newcommand{\twoto}{ \Rightarrow }
\newcommand{\NFProd}[3]{ \mathop{_{#1} \!\underset{#2}{\times}\,\!_{#3} } }
`$

内容：

プロ方向とタイト方向

二重圏は、2つの方向を持ちます。多くの人が、2つの方向を縦方向と横方向と呼んでいます。しかし、「二重圏、縦横をもう一度」で述べたように、縦横の選び方は人により異なり、現状では“nLab方式”と“伝統派方式”が混在しています。なので、毎回約束を確認する必要があります。さらに悪いことには、ペースティング図の縦方向は、ストリング図では横方向になります（ディビッド・ジャズ・マイヤースのように、90度回転して揃えようとする人もいます）。

「縦横」を使い続けるのは得策じゃないな、と僕は判断しました。プロ射〈proarrow | promorphism〉という言葉は浸透していて安定しているので、縦横ではなくてプロ射の方向〈promorphism direction〉、あるいは短くプロ方向〈pro-direction〉と呼ぶことにします。

プロ射ではない1-射は、アーカー／マクダルメット [AM23-] に倣ってタイト射〈tight-morphism〉と呼ぶことにします（アーカー／マクダルメットは、プロ射をルーズ射と呼んでいます）。そして、タイト射の方向〈tight-morphism direction〉、またはタイト方向〈tight-direction〉という言葉を使います。描画のときは、プロ方向とタイト方向は直交します。

プロ射を表す矢印には、なにかしらの飾りを付けます。飾りは、短い縦棒や黒丸が多いですが、MathJax でうまく書けないので、代わりに $`\proar, \not\to, \rightsquigarrow`$ などを使います。この記事では $`\proar`$（破線矢印）とします。

モノイド圏と2-圏は、二重圏の特別なものですが、これらにおけるプロ方向とタイト方向は次のようです。

• モノイド圏のプロ方向はモノイド積の方向、タイト方向は射の方向
• 2-圏のプロ方向は1-射の方向、タイト方向は2-射の縦方向

僕の個人的なルールは：

• ペースティング図ではプロ方向を横方向にする。プロ射は左から右への矢印。
• ストリング図ではプロ方向を縦方向にする。プロ射は上から下へのワイヤー。

また、使用する演算子記号（$`;, \otimes, *, \odot`$ など）は、すべて図式順として、反図式順は使わないか、別記号を準備することにします。図式順記号と反図式順記号の混用はかなり負担・ストレスになるので（「二重圏の縦横 補遺」参照）。

添加仮想二重圏の全体構造

仮想二重圏〈virtual double category〉と添加仮想二重圏〈augmented virtual double category〉は大差ないので、添加仮想二重圏について述べます。添加仮想二重圏に少し制限を付けると仮想二重圏になります。

添加仮想二重圏を $`\dblcat{D}`$ のような白抜き黒板文字で表します。これは、二重圏に関しては比較的普及した習慣だと思います（クーデンバーグは、2-圏の習慣に従い $`\cat{K}`$ のように書いていますが）。二重圏の場合は、$`\dblcat{D}`$ を0階の構造 $`\dblcat{D}_0`$ と1階の構造 $`\dblcat{D}_1`$ に分けました。添加仮想二重圏も同様に、0階と1階に分けますが、次の記法を使います。

• 添加仮想二重圏 $`\dblcat{D}`$ の0階の構造は（通常の）圏になる。それを $`\cat{C}_\dblcat{D}`$ と書く。文脈から $`\dblcat{D}`$ が明らかなら、単に $`\cat{C}`$ と書く。
• 添加仮想二重圏 $`\dblcat{D}`$ の1階の構造はオペラッド〈複圏〉になる。それを $`\cat{D}_\dblcat{D}`$ と書く。文脈から $`\dblcat{D}`$ が明らかなら、単に $`\cat{D}`$ と書く。

二重圏とは違い、添加仮想二重圏では、0階の構造と1階の構造の種類が違います。0階の構造である圏と、1階の構造であるオペラッドでは、歴史的事情から用語法が違います。

圏の対象	オペラッドの色
圏の射	オペラッドのオペレーション

ここでは、次のように記法を揃えます。

• $`\mrm{Obj}(\cat{C}) = |\cat{C}|`$ ： 圏の対象の集合
• $`\mrm{Mor}(\cat{C})`$ ： 圏の射の集合
• $`\mrm{Obj}(\cat{D}) = |\cat{D}|`$ ： オペラッドの色の集合
• $`\mrm{Mor}(\cat{D})`$ ： オペラッドのオペレーションの集合

0階の構造である圏 $`\cat{C} = \cat{C}_\dblcat{D}`$ は次のように書きます。

$`\quad \cat{C} = (|\cat{C}|, \mrm{Mor}(\cat{C}), \mrm{dom}, \mrm{cod}, \mrm{id}, \mrm{comp})`$

結合演算 $`\mrm{comp}`$ の図式順演算子記号はセミコロン $`;`$ です。セミコロンはアーカー／マクダルメットと同じです、クーデンバーグは反図式順記号 $`\circ`$ を使っています。

1階の構造であるオペラッド〈複圏〉 $`\cat{D} = \cat{D}_\dblcat{D}`$ は次のように書きます。

$`\quad \cat{D} = (|\cat{D}|, \mrm{Mor}(\cat{D}), \mrm{src}, \mrm{trg}, \mrm{id2}, \mrm{opdcomp})`$

$`\mrm{opdcomp}`$ はオペラッド結合のつもりで、いくつかの射〈オペレーション〉のリストとひとつの射〈オペレーション〉を結合します。オペラッド結合演算 $`\mrm{opdcomp}`$ の図式順演算子記号もセミコロン $`;`$ を使います。これもアーカー／マクダルメットと同じです（クーデンバーグは反図式順の $`\circ`$）。次の書き方をします。

$`\quad (\phi_1, \cdots, \phi_n);\psi`$

$`\cat{C}, \cat{D}`$ の構成素を、添加仮想二重圏 $`\dblcat{D}`$ の構成素としては次のように呼びます。

• $`\cat{C}`$ の対象を、$`\dblcat{D}`$ の対象〈object〉と呼ぶ。
• $`\cat{C}`$ の射を、$`\dblcat{D}`$ のタイト射〈tight morphism〉と呼ぶ。
• $`\cat{C}`$ の結合を、$`\dblcat{D}`$ のタイト結合〈tight compositiont〉と呼ぶ。
• $`\cat{C}`$ の恒等射を、$`\dblcat{D}`$ のタイト恒等射〈tight identity〉と呼ぶ。
• $`\cat{D}`$ の対象〈色〉を、$`\dblcat{D}`$ のプロ射〈promorphism〉と呼ぶ。
• $`\cat{D}`$ の射〈オペレーション〉を、$`\dblcat{D}`$ の2-射〈2-morphism〉と呼ぶ。
• $`\cat{D}`$ の結合〈オペラッド結合〉を、$`\dblcat{D}`$ の2-結合〈2-composition〉と呼ぶ。
• $`\cat{D}`$ の恒等射〈恒等オペレーション〉を、$`\dblcat{D}`$ の2-恒等射〈恒等2-射〉〈2-identity〉と呼ぶ。

プロ射とプロ射のあいだの結合が定義されてないことに注意してください。これは、二重圏との大きな差です。2-射のオペラッド結合はあっても、プロ射の結合はないのです。（にも関わらず、後述の“プロ射の結合”が出てくるところがややこしいのですが。）

添加仮想二重圏 $`\dblcat{D}`$ の構成素を表す文字は、次のように約束します。

• $`\dblcat{D}`$ の対象は、ラテン文字大文字 $`A, B`$ などで表す。（クーデンバーグに従う*1。）
• $`\dblcat{D}`$ のタイト射は、ラテン文字小文字 $`f, g`$ などで表す。
• $`\dblcat{D}`$ のプロ射は、ラテン文字小文字 $`p, q`$ などで表す。（アーカー／マクダルメットに従う*2。）
• $`\dblcat{D}`$ の2-射は、ギリシャ文字小文字 $`\phi, \psi`$ などで表す。
• $`\dblcat{D}`$ の対象 $`A`$ に対するタイト恒等射は $`\mrm{id}_A`$ と書く。
• $`\dblcat{D}`$ のプロ射 $`p`$ に対する2-恒等射は $`\mrm{id2}_p`$ と書く。

2-射をペースティング図で描くと次の形です。

$`\quad \xymatrix@R+1pc{
A_0 \ar@{-->}[r]^{p_1} \ar[d]_{f} \ar@{}[rrrrd]|{\phi}
& A_1 \ar@{..}[r]
& {} \ar@{..}[r]
& A_{n - 1}\ar@{-->}[r]^{p_n}
& A_n \ar[d]^{g}
\\
B_0 \ar@{-->}[rrrr]_{q}
&{}
&{}
&{}
& B_1
}`$

プロ射のパス

添加仮想二重圏 $`\dblcat{D}`$ の構造の一部として、対象を頂点としてプロ射を辺とする有向グラフ構造があります。その有向グラフ（以下、単にグラフ）構造を次のように表します。（start, goal を使ったのは、後述のオペラッド〈複圏〉の下部構造である複グラフの src, trg と区別するためです。）

$`\quad \xymatrix@C+1pc{
|\cat{D}_\dblcat{D}| \ar@/^1pc/[r]^-{\mrm{start}} \ar@/_1pc/[r]_-{\mrm{goal}}
& |\cat{C}_\dblcat{D}|
}\\
\quad \In {\bf SET}
`$

$`\dblcat{D}`$ のプロ射とは、オペラッド $`\cat{D} = \cat{D}_\dblcat{D}`$ の対象〈色〉でした。$`\dblcat{D}`$ の対象とは、圏 $`\cat{C} = \cat{C}_\dblcat{D}`$ の対象でした。これらから構成されるグラフをプロ射のグラフ〈graph of promorphisms〉と呼ぶことにします。

辺であるプロ射 $`p \in |\cat{D}|`$ に対して、$`\mrm{start}(p)`$ が始点で、$`\mrm{goal}(p)`$ が終点です。二重圏では、プロ射のグラフの上に圏の構造が事前に載っていたのですが、添加仮想二重圏では、そのような圏構造を前提にはしません。プロ射達と対象達は、単にグラフ構造を形成するだけです。

添加仮想二重圏 $`\dblcat{D}`$ のプロ射のグラフを $`G = G_\cat{D}`$ と書くことにします。$`G`$ は圏ではありませんが、圏の記法を流用すると：

• $`|G|`$ ： $`G`$ の頂点の集合
• $`\mrm{Mor}(G)`$ ： $`G`$ の辺の集合

次が成立します。（$`|\dblcat{D}|`$ は $`\dblcat{D}`$ の対象の集合です。）

$`\quad |G| = |\cat{C}| = |\dblcat{D}| \In {\bf SET}\\
\quad \mrm{Mor}(G) = |\cat{D}| \In {\bf SET}
`$

$`G = G_\dblcat{D}`$ はグラフなので、パスの集合を定義できます。それを次のように書きます。

$`\quad \mrm{Path}(G)`$

長さが $`n`$ のパスは次の形に書きます。

$`\quad (A_0 \overset{p_1}{\proar} A_1 \;\cdots\; A_{n - 1} \overset{p_n}{\proar} A_n)`$

「二重圏の縦横 補遺」で述べたように、このときの番号の付け方が色々あります。ここでは、図でもテキストでも、左から右に番号が増えると決めます。対象の番号は0始まり、プロ射の番号は1始まりです。対象は(n + 1)個あり、プロ射はn本あります。

特別な場合として、長さ0、長さ1のパスは次の形です。

$`\quad (A_0)\\
\quad (A_0 \overset{p_1}{\proar} A_1)
`$

パスの頂点を省略する場合は次の形にします。

$`\quad (\underset{\proar}{p_1}, \cdots, \underset{\proar}{p_n})`$

長さ0のパスでは頂点を省略できません。長さ1のパスの省略形は次の形です。

$`\quad (\underset{\proar}{p_1})`$

対象とプロ射は大文字・小文字で書き分ける規約のもとでは、長さ0のパスと長さ1のパスを次のように書いても混乱は起きません。

$`\quad (A)\\
\quad (p)
`$

さらに、長さ0のパスと対象、長さ1のパスとプロ射をしばしば同一視します。

$`\quad (A) = A \:\text{ where } A \in |\cat{C}|\\
\quad (p) = p \:\text{ where } p \in |\cat{D}|
`$

次の同型があるからです。

$`\quad \mrm{Path}_0 (G) \cong |G| = |\cat{C}| \In {\bf SET}\\
\quad \mrm{Path}_1 (G) \cong \mrm{Mor}(G) = |\cat{D}| \In {\bf SET}
`$

プロ射のパスを、 $`\vec{p}`$ のようにベクトル風に書きます。

$`\quad \vec{p} = (A_0 \overset{p_1}{\proar} A_1 \cdots A_{n - 1} \overset{p_n}{\proar} A_n)`$

$`\vec{p}`$ が長さ0のパスを表す可能性もあります。注意してください。

辺（プロ射）に対して定義されていた $`\mrm{start}, \mrm{goal}`$ をパスに拡張して、同じ記号を使い回します（オーバーロード）。

$`\quad \mrm{start} : \mrm{Path}(G) \to |G| = |\cat{C}| \In {\bf SET}\\
\quad \mrm{goal} : \mrm{Path}(G) \to |G| = |\cat{C}| \In {\bf SET}
`$

$`\mrm{start}(\vec{p})`$ はパスの始点、$`\mrm{goal}(\vec{p})`$ はパスの終点です。

$`\vec{p}, \vec{q}`$ が2つのパスだとして、その連接〈concatenation〉は次のように書きます*3。

$`\quad \vec{p}\conc \vec{q}`$

連接は、$`\mrm{goal}(\vec{p}) = \mrm{start}(\vec{q})`$ でないと定義できません。$`(\conc)`$ はファイバー積の上で定義されています。

$`\quad (\conc) : \mrm{Path}(G) \NFProd{\mrm{goal}}{|G|}{\mrm{start}} \mrm{Path}(G) \to \mrm{Path}(G) \In {\bf SET}`$

グラフのパスの全体は、自由圏（「モノイドと有向グラフから圏を構成する」参照）の構造を持つので圏となります。しかし、パスの連接をプロ射の結合とは考えません。繰り返し言いますが、プロ射とプロ射のあいだの結合は、添加仮想二重圏の構造としては定義されていません。

添加仮想二重圏の2-射のフレーム

添加仮想二重圏 $`\dblcat{D}`$ の1階の構造であるオペラッド〈複圏〉 $`\cat{D} = \cat{D}_\dblcat{D}`$ は次のようでした。

$`\quad \cat{D} = (|\cat{D}|, \mrm{Mor}(\cat{D}), \mrm{src}, \mrm{trg}, \mrm{id2}, \mrm{opdcomp})`$

オペラッド〈複圏〉の対象〈色〉の集合 $`|\cat{D}|`$ は、プロ射のグラフ $`G = G_\dblcat{D}`$ の辺の集合 $`\mrm{Mor}(G)`$ でした。オペラッド〈複圏〉の射〈複射 | オペレーション〉のソース〈域〉とターゲット〈余域〉は次のような写像です。

$`\quad \mrm{src} : \mrm{Mor}(\cat{D}) \to \mrm{Path}(G) \In {\bf SET}\\
\quad \mrm{trg} : \mrm{Mor}(\cat{D}) \to \mrm{Path}_{\le 1}(G) \In {\bf SET}
`$

ここで、$`\mrm{Path}_{\le 1}(G) `$ は、長さが1以下のパスの集合です。つまり、オペラッド $`\cat{D}`$ の射〈複射 | オペレーション〉のソースは任意の長さのプロ射のパス、ターゲットは長さ1か長さ0のプロ射のパスとなります。

オペラッド $`\cat{D}`$ の射とは添加仮想二重圏 $`\dblcat{D}`$ の2-射のことですから、$`\dblcat{D}`$ の2-射は、以下のどちらかの形をしています。

$`\quad \xymatrix@R+1pc{
A_0 \ar@{-->}[r]^{p_1} \ar[d]_{f} \ar@{}[rrrrd]|{\phi}
& A_1 \ar@{..}[r]
& {} \ar@{..}[r]
& A_{n - 1}\ar@{-->}[r]^{p_n}
& A_n \ar[d]^{g}
\\
B_0 \ar@{-->}[rrrr]_{q}
&{}
&{}
&{}
& B_1
}`$

$`\quad \xymatrix@R+1pc{
A_0 \ar@{-->}[r]^{p_1} \ar[drr]_{f}
& A_1 \ar@{..}[r]
& {} \ar@{..}[r] \ar@{}[d]|{\phi}
& A_{n - 1}\ar@{-->}[r]^{p_n}
& A_n \ar[dll]^{g}
\\
{}
&{}
& B
&{}
&{}
}`$

仮想二重圏〈virtual double category〉では、ニ番目の形状の2-射を許していません。それが、仮想二重圏と添加仮想二重圏の違いです。場合により、ソースにも長さ0のパスを許してない仮想二重圏の定義もあります。いずれにしても、添加仮想二重圏は、仮想二重圏の2-射の形状を少し一般化したものです。

添加仮想二重圏 $`\dblcat{D}`$ の2-射 $`\phi`$ の境界の情報を次のように書きます。

$`\quad \phi :: f[\vec{p} \twoto \vec{q}]g \In \dblcat{D}`$

$`\vec{p},\vec{q}`$ はプロ射のパスですが、$`\vec{q}`$ は長さ1か長さ0なので、次のように書けます。

$`\quad \phi :: f[\vec{p} \twoto q]g \In \dblcat{D}\\
\quad \phi :: f[\vec{p} \twoto B]g \In \dblcat{D}
`$

$`f[\vec{p} \twoto \vec{q}]g`$ を2-射 $`\phi`$ のフレーム〈frame〉と呼びます。

プロ射を横方向に描くペースティング図で見るなら：

• フレーム $`f[\vec{p} \twoto \vec{q}]g`$ の $`f`$ は、左側のタイト射
• フレーム $`f[\vec{p} \twoto \vec{q}]g`$ の $`\vec{p}`$ は、上側のプロ射のパス
• フレーム $`f[\vec{p} \twoto \vec{q}]g`$ の $`\vec{q}`$ は、下側のプロ射のパス（長さ1、または長さ0）
• フレーム $`f[\vec{p} \twoto \vec{q}]g`$ の $`g`$ は、右側のタイト射

$`f, \vec{p}, \vec{q}, g`$ は次の条件を満たします。

1. $`f, g\in \mrm{Mor}(\cat{C}_\dblcat{D})`$
2. $`\vec{p}, \vec{q} \in \mrm{Path}(G_\dblcat{D})`$
3. $`\mrm{length}(\vec{q}) \le 1`$
4. $`\mrm{start}(\vec{p}) = \mrm{dom}(f)`$
5. $`\mrm{goal}(\vec{p}) = \mrm{dom}(g)`$
6. $`\mrm{start}(\vec{q}) = \mrm{cod}(f)`$
7. $`\mrm{goal}(\vec{q}) = \mrm{cod}(g)`$

フレームが $`f[\vec{p} \twoto \vec{q}]g`$ である $`\dblcat{D}`$ の2-射の全体を次のように書きます。

$`\quad \dblcat{D}(f[\vec{p} \twoto \vec{q}]g)`$

当然に次が成立します。

$`\quad \phi \in \dblcat{D}(f[\vec{p} \twoto \vec{q}]g) \iff (\phi :: f[\vec{p} \twoto \vec{q}]g \In \dblcat{D})`$

$`\dblcat{D}(f[\vec{p} \twoto \vec{q}]g)`$ は、2-射達のホムセットです。

階数0の構造と階数1の構造の関係性

添加仮想二重圏 $`\dblcat{D}`$ の階数0の構造は圏 $`\cat{C} = \cat{C}_\dblcat{D}`$ 、階数1の構造はオペラッド〈複圏〉 $`\cat{D} = \cat{D}_\dblcat{D}`$ でした。それらのあいだを中継するのがグラフ $`G = G_\dblcat{D}`$ です。

二重圏の場合と同様に、$`\cat{C}`$ と $`\cat{D}`$ のあいだは“関手”で結ばれます。ただし、$`\cat{D}`$ は圏ではなくてオペラッド〈複圏〉なので、オペラッドと圏を繋ぐ関手類似準同型射〈functor-like homomorphism〉です。二重圏の場合と違うのは、2階の構造による結合〈外部結合〉が無いことです。プロ方向へのプロ射の結合と、プロ方向への2-射の結合は定義されていません。プロ射パスの連接は、プロ方向への結合ではありません。

$`\cat{C}`$ と $`\cat{D}`$ を関係付ける“関手”を次のように命名します。

$`\quad \xymatrix@C+2pc{
\cat{D} \ar@/^1pc/[r]^{\mrm{Start}} \ar@/_1pc/[r]_{\mrm{Goal}}
& \cat{C} \ar[l]|{\mrm{Id}}
}\\
\quad \In {\bf CATLIKE}
`$

$`{\bf CATLIKE}`$ は、圏類似代数系〈category-like algebraic {system | structure}〉が何でも入っているような圏のつもりですが、今ここで正確な定義は述べません*4。

$`\mrm{Start}`$ は次のように定義します。

• プロ射のパス $`\vec{p}`$ に、$`\mrm{start}(\vec{p}) \in |\cat{C}|`$ を割り当てる。
• 2-射（$`\cat{D}`$ の射〈複射 | オペレーション〉） $`\phi :: f[\vec{p} \twoto \vec{q}]g`$ に、$`f : \mrm{start}(\vec{p}) \to \mrm{start}(\vec{q}) \In \cat{C}`$ を割り当てる。

$`\mrm{Goal}`$ は次のように定義します。

• プロ射のパス $`\vec{p}`$ に、$`\mrm{goal}(\vec{p}) \in |\cat{C}|`$ を割り当てる。
• 2-射（$`\cat{D}`$ の射〈複射 | オペレーション〉） $`\phi :: f[\vec{p} \twoto \vec{q}]g`$ に、$`g : \mrm{goal}(\vec{p}) \to \mrm{goal}(\vec{q}) \In \cat{C}`$ を割り当てる。

$`\mrm{Id}`$ は、その存在を添加仮想二重圏の公理として要請します。$`\mrm{Id}`$ の法則はすぐ後で述べます。

• $`A\in |\cat{C}|`$ に、$`\mrm{Id}(A) \in |\cat{D}| = \mrm{Mor}(G)`$ を割り当てる。
• $`f:A \to B \In \cat{C}`$ に、$`\mrm{Id}(f) \in \mrm{Mor}(\cat{D})`$ を割り当てる。

ここで、オペラッド〈複圏〉 $`\cat{D}`$ の構成素に $`\mrm{id2}`$ があったことを思い出しましょう。

$`\quad \mrm{id2} : |\cat{C}| + |\cat{D}| \to \mrm{Mor}(\cat{D}) \In {\bf SET}`$

$`\mrm{id2}`$ は、$`|\cat{C}| + |\cat{D}|`$ の要素、つまり対象またはプロ射に、2-射 $`\mrm{id2}_A`$ または $`\mrm{id2}_p`$ を割り当てます。$`\mrm{id2}_A`$ 、 $`\mrm{id2}_p`$ は、オペラッドとしての恒等射〈恒等オペレーション〉となります。

$`\mrm{Id}`$ の公理〈法則 | 条件〉として、2つの方法で得られる恒等2-射が一致することを要請します。

$`\quad \mrm{Id}(\mrm{id}_A) = \mrm{id2}_A`$

次は定義から言えます

$`\quad \mrm{Start}(\mrm{Id}(\mrm{id}_A) ) = A\\
\quad \mrm{Goal}(\mrm{Id}(\mrm{id}_A) ) = A
`$

$`\mrm{Id}`$ は $`\cat{C}`$ の射、つまりタイト射に対しても定義されていて、関手性を満たします（それを要請する）。

$`\text{For } f: A \to B, g:B \to C \In \cat{C}\\
\quad \mrm{src}(\mrm{Id}(f)) = \mrm{Id}( \mrm{dom}(f) )\\
\quad \mrm{trg}(\mrm{Id}(f)) = \mrm{Id}( \mrm{cod}(f) )\\
\quad \mrm{Id}(f;g) = (\mrm{Id}(f) ); \mrm{Id}(g)\\
\quad \mrm{Id}(\mrm{id}_A) = \mrm{id2}_{\mrm{Id}(A)}
`$

ここで：

• $`(\hyp); \hyp`$ は、2-射のオペラッド結合
• $`\mrm{Id}(A) = A`$ と定義している。$`A\in |\cat{C}|`$ に対する $`\mrm{id2}_A`$ は定義されている。

プロ射の結合と単位プロ射

プロ射の結合は定義されないと言いました。しかし、アーカー／マクダルメット論文にもクーデンバーグ論文にも“プロ射の結合”が出てきます。どちらも演算子記号には $`\odot`$ を使っています。これはいったいどういうことかと言うと、特別な性質を持つ2-射（{反 | 余}デカルト2-射）が在る場合、そのソースとターゲットのあいだにも特別な関係があり、その特別な関係を演算子記号 $`\odot`$ で表現しているのです。添加仮想二重圏の構造として、二項演算 $`\odot`$ を持っているわけではありません。

ちなみに、「二重圏の縦横 補遺」に書いたように、アーカー／マクダルメットは反図式順、クーデンバーグ（パトリック・シュルツも）は図式順で使っています。僕は図式順で使います。

プロ射の結合に関連して、アーカー／マクダルメットではルーズ恒等射〈loose-identity〉$`A(1, 1)`$ 、クーデンバーグでは水平単位〈horizontal unit〉 $`I_A`$ が出てきます。これは、プロ射の結合に対して単位として振る舞うようなプロ射（あるいは長さ1のパス）です。これも、添加仮想二重圏の構造として与えられるものではありません。

プロ射の結合は、他の結合演算とは違うので、プロ積〈pro-product〉、その単位はプロ単位〈pro-unit〉と呼んだほうが誤解を減らせると思います。プロ積は常に定義できるわけではないし、プロ単位が常に存在するわけでもありません。

おわりに

これで、添加仮想二重圏の定義は述べたので、添加仮想二重圏の事例やより詳しい性質、添加仮想二重圏の使い方などの話もできるでしょう。

*1:アーカー／マクダルメットは、対象には大文字・小文字を混合使用しています。

*2:クーデンバーグは、$`J`$ 以降の大文字でプロ射を表しています。

*3:クーデンバーグは、連接の演算子記号に $`\smallfrown`$ を使っています。

*4:ハッキリとした定義はわかってないです。