カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッド（「コンテキスタッド、包括圏、ハイパードクトリン」参照）は、型理論と思いのほか相性がいいようです。ちょっと驚いています。
型理論的概念である包括圏を、テレスコープ構成により加工するとコンテキスタッドを作れます。しかし、型理論が想定している典型例／メンタルモデルは、カプチ／マイヤースが想定している典型例／メンタルモデルとだいぶ違うので次のようなことになっています。
「コンテキスタッドかぁ、ウーム‥‥」より：
カプチ／マイヤースのテーマは、コンテキストフルな計算です。ここでのコンテキストは、明示的な入力と出力以外で計算に影響を与える要因のことです -- この意味で用語「コンテキスト」を使う時点で嫌な予感はしましたが、案の定、型理論とはひどく食い違った（真逆とも言える）用語法になってしまいました。
ここらへんの食い違いを埋める算段をしながら、カプチ／マイヤースのコンテキストフル構成を、型理論の観点から見てみます。焦点〈ハイライト〉はコンテキストフル射です。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\ot}{\leftarrow }
\newcommand{\thot}{\twoheadleftarrow}
\newcommand{\thto}{\twoheadrightarrow}
%\newcommand{\parto}{ \supset\!\to }
\newcommand{\In}{\text{ in }}
\newcommand{\op}{\mathrm{op}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
\newcommand{\mappedfrom}{ \mathrel{\style{display: inline-block; transform: rotate(180deg)} {\mapsto} } }
\newcommand{\vmapsto}{\style{display: inline-block; transform: rotate(90deg)} {\mapsto} }
\newcommand{\ctxpair}[2]{ \begin{pmatrix}#1 \\ #2\end{pmatrix} }
\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\newcommand{\lift}{ \mathop{\Uparrow} }
\newcommand{\hto}{\rightharpoonup}
\newcommand{\cohto}{\rightharpoondown}
\newcommand{\conc}{\mathop{\#}}
`$
内容：
- 厳密コンテキスタッド
- 厳密コンテキスタッドの台スパン
- 依存ペアと作用演算
- トータル射
- 自己スパンの結合平方
- コンテキスタッドの乗法と単位
- 計算のための具体的な表示
- コンテキストフル射
- 余ハープーン射の結合
- そしてそれから
追記：
ハブ記事：
厳密コンテキスタッド
コンテキスタッドの定義は複雑です。
「コンテキスタッドかぁ、ウーム‥‥」より：
コンテキスタッド全体は複雑で大規模な構造です。上記論文 [CM24-] の Definition3.17. がコンテキスタッドの定義ですが、形式的定義だけで3ページを費やしています。
例えば、群の定義を形式的に書けば数行で終わるでしょう。それに対して丸々3ページです。
- [CM24-]
- Title: Contextads as Wreaths; Kleisli, Para, and Span Constructions as Wreath Products
- Authors: Matteo Capucci, David Jaz Myers
- Submitted: 29 Oct 2024
- Pages: 84p
- URL: https://arxiv.org/abs/2410.21889
最初から一般的なコンテキスタッドを扱うのは荷が重いので、簡略化した厳密コンテキスタッド〈strict contextad〉を考えます。「厳密」の意味は、スード／ラックス／反ラックスなどの弱い法則性をすべて等式的法則にして考える、ということです。これにより、高次の一貫性〈coherence〉を考える必要がなくなり、議論は極端に単純化されます。
より具体的には：
- ファイブレーション〈ファイバー付き圏 | グロタンディーク・ファイブレーション〉は分裂ファイブレーション〈split fibration〉だけを考える。
- 2-圏内のスパンの結合は厳密プルバック四角形により構成する。
- 2-圏内のスパンのあいだの射は、左四角形も右四角形も厳密可換四角形とする。
分裂ファイブレーションに関しては、
を参照してください。ベース射（ベース圏の射）のデカルト持ち上げ〈Cartesian lift〉として、厳密関手性を持つ亀裂（それが分裂）が指定されたファイブレーションが分裂ファイブレーションです。
2-圏内のスパンとスパンのあいだの射については、
を参照してください。一般には、2-圏内のスパン、スパンの結合、スパンのあいだの射は難しい概念になります。が、すべて厳密に〈等式的に〉考えれば、1-圏の場合と同じことで、2-圏内であることは忘れても大丈夫です。
型理論的圏について考える場合は、厳密コンテキスタッドでも十分に実用になります。ファイブレーションに基づく型理論的圏については以下の過去記事を参照してください。
厳密コンテキスタッドの台スパン
コンテキスタッドは高次の〈higher dimensional〉ゆるい〈lax または oplax〉モナドです。一般的な2-圏のなかに棲息するコンテキスタッドも考えられます*1が、ここでは、コンテキスタッドの居場所は2-圏 $`\mbf{CAT}`$ に限りましょう。
コンテキスタッドの台〈underlying thing | carrier〉は $`\mbf{CAT}`$ 内のスパンです。それを次のように書きます。
$`\quad \cat{C} \overset{\pi}{\thot} \cat{E} \overset{\alpha}{\to} \cat{C}\In \mbf{CAT}`$
ここで、矢印 $`\thto`$ は圏のファイブレーション（ファイバー付き圏の射影）を表します。前節で述べたように、今回は特に分裂ファイブレーション〈split fibration〉だけを考えます。すべての分裂ファイブレーション達は、$`\mbf{CAT}`$ の射クラス〈class of morphisms | morphism class〉（1-射達の集合）になります。分裂ファイブレーション達の射クラス $`\cat{SplFib}`$ は、公理的な意味でファイブレーションクラス（「クラン、ファイブレーション、スパン // ファイブレーションクラス付き圏」参照）になります。それは次を満たすことです。
- $`\cat{SplFib}`$ はファイバー引き戻しに関して閉じている。
- $`\mbf{CAT}`$ の同型射（圏同型を与える関手）は $`\cat{SplFib}`$ に所属する。
- $`\cat{SplFib}`$ は結合に関して閉じている。
「ファイバー引き戻しに関して閉じている」「結合に関して閉じている」については「クラン、ファイブレーション、スパン // ファイブレーションクラス付き圏」を参照してください。
また、脚に条件を付けたスパンと、そのようなスパンの結合に関しては以下の過去記事に書いています。
今回のスパンは、左脚が分裂ファイブレーションで、右脚は条件なしです。
上記のスパン（コンテキスタッドの台）を $`(\cat{C}, \cat{E}, \pi, \alpha)`$ とも書きます。構成素の呼び名〈構成素役割り名〉は次のようです。
- $`\cat{C}`$ は、スパンの足（左足と右足は同じ）、コンテキスタッドの基礎圏〈ground category〉またはルート圏〈root category〉
- $`\cat{E}`$ は、スパンのボディ〈body〉、コンテキスタッドの構成素としてもボディ〈body〉と呼ぶ。
- $`\pi`$ は、スパンの左脚、分裂ファイバー付き圏の射影、コンテキスタッドの射影〈projection〉と呼ぶ。
- $`\alpha`$ は、スパンの右脚、コンテキスタッドの作用〈action〉と呼ぶ（アクテゴリーに由来する呼び名）。
依存ペアと作用演算
コンテキスタッドの台であるスパンの左脚はファイバー付き圏〈ファイブレーション | グロタンディーク・ファイブレーション〉です。ファイバー付き圏に関しては次の用語を使います。
- 圏 $`\cat{C}`$ をベース圏〈base category〉、$`\cat{C}`$ の対象と射はベース対象〈base object〉、ベース射〈base morphism〉と呼ぶ。
- 圏 $`\cat{E}`$ をトータル圏〈total category〉、$`\cat{E}`$ の対象と射はトータル対象〈total object〉、トータル射〈total morphism〉と呼ぶ。
- 射影 $`\pi`$ の逆像 $`\pi^{-1}(X)\text{ for }X\in |\cat{C}|`$ はトータル圏の部分圏となる。この部分圏を $`X`$ 上のファイバー〈fiber〉または局所圏〈local category〉と呼び、$`\cat{E}_X`$ または $`\cat{E}_{@X}`$ と書く。ファイバー内の射は垂直射〈vertical morphism〉と呼ぶ。
- ベース射 $`f:X\to Y\In \cat{C}`$ と、$`Y`$ 上のファイバー内の対象 $`B\in |\cat{E}_Y|`$ に対して、分裂子〈splitting〉（「ファイブレーションの亀裂と分裂」参照）によりデカルト持ち上げ〈Cartesian lift〉が一意的に決まるので、そのデカルト持ち上げを $`f\lift B`$ と書く。記号 '$`\lift`$' が分裂子の中置演算子記号。比喩的に言えば、$`f\lift B`$ は、$`B`$ へと向かう“$`f`$ に平行な水平方向のトータル射”。
任意のトータル対象 $`A`$ は、どれかのファイバー内の対象です。$`A\in |\cat{E}_X|`$ のとき、$`A`$ を、ベース対象 $`X`$ とファイバー内の対象 $`A`$ のペアとして $`(X, A)`$ と書きます。この状況でのペア $`(X, A)`$ を依存ペア〈dependent pair〉と呼びます。依存ペア $`(X, A)`$ は、$`X`$ の情報は余分という意味で冗長記法です。
$`\quad A = (X, A)`$
しかし、「ベース対象 $`X`$ を先に決めて、$`X`$ 上のファイバー内で $`A`$ を決める」と考えると $`(X, A)`$ と書く意味もあります。依存ペアの書き方は色々あります。
- $`(X, A)`$
- $`A @ X`$
- $`(X \mappedfrom A)`$
- $`(A \mapsto X)`$
- $`(X \vdash A)`$
- $`{_X A}`$
- $`\begin{pmatrix}A \\ \vmapsto \\ X\end{pmatrix}`$
- $`\begin{pmatrix}A \\ X\end{pmatrix}`$
カプチ／マイヤースは、最後の縦に並べる記法を使っているので、ここでも縦ベクトル記法を使います。射影との関係は次のように書けます。
$`\text{For }A \in |\cat{E}|\\
\quad \pi(A) = \pi( \begin{pmatrix}A \\ X\end{pmatrix} ) = X`$
コンテキスタッドの作用（スパンの右脚）による値は次のように書きます。
$`\text{For }A \in |\cat{E}|\\
\quad \alpha(A) = \alpha( \begin{pmatrix}A \\ X\end{pmatrix} ) = X\cdot A`$
依存ペアに対する作用の中置演算子記号がナカグロ〈centerdot〉です。カプチ／マイヤースは $`\odot`$ を使っています。ナカグロは、型理論のコンテキスト拡張の演算子と合わせた記法です。
デカルト持ち上げを $`f\lift B`$ としましたが、余デカルト持ち上げ〈{coCartesian | opCartesian} lift〉も考えると、別な記法のほうが良かったと思います。例えば：
- デカルト持ち上げ $`f^{\Uparrow B}`$
- 余デカルト持ち上げ $`{^{A \Uparrow}f}`$
「コンテキスタッド、包括圏、ハイパードクトリン // 包括圏とテレスコープ構成」では、包括圏のコンテキスト拡張演算に '$`\cdot`$' 、テレスコープ〈依存リスト〉によるコンテキスト拡張に '$`\odot`$' を使っています。この記事では、テレスコープが最初から組み込まれた状況を考えています。この記事の $`\cat{E}`$ は過去記事の $`\vec{\cat{E}}`$ です。よって、この記事の '$`\cdot`$' はテレスコープによるコンテキスト拡張の意味です。
単純なコンテキスト拡張と、テレスコープによるコンテキスト拡張を区別するなら、$`\cdot`$ と $`\odot`$ より、$`\cdot`$ と $`\bullet`$ がよさそうです。対象にも射にも同じ記号 $`\bullet`$ を使うと間違いが少ないでしょう。
- 対象 $`(X, A)\mapsto (\bullet)( (X, A)) = X\mathop{\bullet} A`$
- 射 $`F \mapsto (\bullet)( F ) = F^{\bullet}`$
[/補足 追記]
トータル射
2-圏 $`\mbf{CAT}`$ 内の自己スパン〈endo-span〉（右足と左足が同じスパン） $`(\cat{C}, \cat{E}, \pi, \alpha)`$ のボディ $`\cat{E}`$ の射がトータル射でした。トータル射はラテン文字大文字で書くことにします。
$`\text{For }A, B \in |\cat{E}|\\
\quad F: A \to B \In \cat{E}
`$
トータル対象 $`A, B`$ を依存ペアで表記すれば：
$`\quad F: \ctxpair{A}{X} \to \ctxpair{B}{Y} \In \cat{E}`$
ファイバー付き圏〈ファイブレーション〉のトータル射については、次のような概念があります。
- ベースパート
- リダクト関手
- ファイバーパート
ベースパート〈base part〉は簡単で、トータル射を射影でベース圏に落としたものです。$`F`$ のベースパートは $`\base{F}`$ と書くことにします。
$`\text{For }F: A\to B \In \cat{E}\\
\quad \base{F}:= \pi(F) : \pi(A) \to \pi(B) \In \cat{C}
`$
トータル対象 $`A, B`$ を依存ペアで表記すれば：
$`\text{For }F: \ctxpair{A}{X}\to \ctxpair{B}{Y} \In \cat{E}\\
\quad \base{F}:= \pi(F) : X \to Y \In \cat{C}
`$
ベースパートはベース射です。一般に、ベース射 $`f:X\to Y\In \mbf{C}`$ には、次のような関手が伴います。
$`\quad f^* : \cat{E}_Y \to \cat{E}_X \In \mbf{CAT}`$
$`f^*`$ は、ファイバー〈局所圏〉からファイバーへの関手です。$`f`$ に対して $`f^*`$ は逆方向ですが、それと、関手 $`f^*`$ が反変か共変かは何の関係もありません（実際は共変）。ファイバー〈局所圏〉間の関手 $`f^*`$ をリダクト関手〈reduct functor〉またはリインデキシング関手〈reindexing functor〉と呼びます。「リダクト関手」はインスティチューション理論で使われる言葉です。
「$`\cat{C}`$ の対象 $`\mapsto`$ ファイバー〈局所圏〉」「$`\cat{C}`$ の射 $`\mapsto`$ リダクト関手」という対応は反変関手ですが、この反変関手は、ファイブレーション〈ファイバー付き圏〉 $`\pi: \cat{E}\thto \cat{C}`$ から逆グロタンディーク構成（「グロタンディーク構成・逆構成と同値対応」参照）で得られたインデキシング〈インデックス付き圏〉です。
- グロタンディーク構成 : インデキシング〈インデックス付き圏〉→ ファイブレーション〈ファイバー付き圏〉
- 逆グロタンディーク構成 : ファイブレーション〈ファイバー付き圏〉→ インデキシング〈インデックス付き圏〉
トータル射 $`F`$ のファイバーパート〈fiber part〉は $`F^\flat`$ と書くことにします。ファイバーパートは次のような垂直射（ファイバー内の射）です。
$`\quad F^\flat : A \to \base{F}^*(B) \In \cat{E}_X`$
今回は次の記法を採用しました。
- ベースパート： $`\base{F}`$
- リダクト関手： $`\base{F}^*`$
- ファイバーパート： $`F^\flat`$
他に、各パートを示すために $`\u{(\hyp)}\;, (\hyp)^\#, (\hyp)^\diamond`$ などの飾りが使われることがあります。
「コンテキスタッド、包括圏、ハイパードクトリン // グロタンディーク構成とデカルト圏に関する準備」では、「$`F`$ のベースパートが $`\u{F}`$ 、ファイバーバートが $`F^\#`$」としています。
「関係とファミリーのあいだの関係 // ファミリー達の圏」では、「$`\varphi`$ のベースパートが $`\base{\varphi}`$ 、ファイバーバートが $`\varphi^\#`$」としています。
[/補足 追記]
トータル射 $`F`$ をベースパートとファイバーパートのペアで表示するときは、次の書き方（単なるペア）を使います。特別な括弧や区切り記号は使いません。
$`\quad F = (\base{F}, F^\flat)\\
\text{Where}\\
\quad \base{F} : X \to Y \In \cat{C}\\
\quad F^\flat : A \to \base{F}^*(B) \In \cat{E}_X
`$
ベース射 $`f:X \to Y\In \cat{C}`$ のデカルト持ち上げ $`f\lift B`$ は次のようなトータル射です。
$`\quad f\lift B : \ctxpair{f^*(B)}{X} \to \ctxpair{B}{Y} \In \cat{E}`$
これを、ベースパート・ファイバーパートのペアで書くと次のようになります。
$`\quad f\lift B = (f, \id_{f^*(B)})\\
\text{Where}\\
\quad f : X \to Y \In \cat{C}\\
\quad \id_{f^*(B)} : f^*(B) \to f^*(B) \In \cat{E}_X
`$
トータル射 $`F`$ に対する作用（スパンの右脚）による値は次のように書きます。
$`\quad \alpha(F) =: {F}^\bullet`$
トータル対象を依存ペアで書けば次のようです。
$`\text{For }F : \ctxpair{A}{X} \to \ctxpair{B}{Y} \In \cat{E}\\
\quad \alpha(F) = {F}^\bullet \;: X\cdot A \to Y\cdot B \In \cat{C}
`$
型理論の包括圏では、トータル射 $`F`$ の情報が、ベース圏 $`\cat{C}`$ 内の標準プルバック四角形（下図）にエンコードされます。
$`\quad \xymatrix{
{X\cdot A} \ar[r]^{{F}^\bullet} \ar[d]_{\rho^{X, A}}
\ar@{}[dr]|{\text{p.b.} }
&{Y\cdot B} \ar[d]^{\rho^{Y, B}}
\\
{X} \ar[r]_{\base{F}}
&{Y}
}\\
\quad \In \cat{C}
`$
これは、以下のようなデカルト自然変換（自然性可換四角形がプルバック四角形である自然変換） $`\rho`$ が在ることを意味します。
$`\quad \rho :: \alpha \twoto \pi : \cat{E} \to \cat{C} \In \mbf{CAT}`$
あるいは：
$`\quad \xymatrix{
\cat{E} \ar@/^/[r]^{\alpha} \ar@/_/[r]_{\pi}
\ar@{}[r]|{\Downarrow\rho}
&\cat{C}
}\\
\quad \In \mbf{CAT}
`$
上の標準プルバック四角形は、以下のような、自然変換 $`\rho`$ の自然性可換四角形です。$`\rho`$ の成分の添字は上付きです。
$`\quad \xymatrix{
{ \alpha(\ctxpair{A}{X}) } \ar[r]^{\alpha(F) } \ar[d]_{\rho^{\ctxpair{A}{X}}}
&{\alpha(\ctxpair{B}{Y}) } \ar[d]^{\rho^{\ctxpair{B}{Y}}}
\\
{\pi(\ctxpair{A}{X}) } \ar[r]_{\pi(F) }
&{\pi(\ctxpair{B}{Y})}
}\\
\quad \text{commutative }\In \cat{C}
`$
$`\rho`$ はデカルト自然変換なので、自然性可換四角形は単なる可換四角形ではなくてプルバック四角形です。
自己スパンの結合平方
記号の乱用として、スパン全体をスパンのボディで表すことにします。
$`\quad \cat{E} = (\cat{C} \overset{\pi}{\thot} \cat{E} \overset{\alpha}{\to} \cat{C}) \In \mbf{CAT}`$
あるいは：
$`\quad \cat{E} = (\cat{C}, \cat{E}, \pi, \alpha)`$
スパン $`\cat{E}`$ は自己スパン〈endo-span〉なので、自分自身と結合できます。スパンの結合を併置（演算子記号なし）で表すと、自分自身との結合、つまり結合平方は $`\cat{E E}`$ と書けます。より詳しく描けば以下のようです。
$`\quad \xymatrix{
{}
&{}
&{\cat{E E} } \ar@{->>}[dl]_{\pi'} \ar[dr]^{\alpha'}
\ar@{->>}@/_1.8pc/[ddll]_{\pi\pi}
\ar@/^1.8pc/[ddrr]^{\alpha\alpha}
\ar@{}[dd]|{\text{p.b.}}
&{}
&{}
\\
{}
&{\cat{E} } \ar@{->>}[dl]_\pi \ar[dr]^\alpha
&{}
&{\cat{E} } \ar@{->>}[dl]_\pi \ar[dr]^\alpha
&{}
\\
{\cat{C}}
&{}
&{\cat{C}}
&{}
&{\cat{C}}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
ここで、$`\pi\pi`$ や $`\alpha\alpha`$ はオフィシャルには二文字からなる名前で、積・結合の意味はありません。が、気持ちとしては射影の繰り返し、作用の繰り返しを表現しています。
スパン $`\cat{E}`$ の平方 $`\cat{E E}`$ の記号の乱用による表示は：
$`\quad \cat{E E} = (\cat{C} \overset{\pi\pi}{\thot} \cat{E E} \overset{\alpha\alpha}{\to} \cat{C} \In \mbf{CAT})`$
あるいは：
$`\quad \cat{E E} = (\cat{C}, \cat{E E}, \pi\pi, \alpha\alpha)`$
コンテキスタッドの乗法と単位
コンテキスタッドは、スパン $`\cat{E}`$ を台とするモナドなので、モナド乗法とモナド単位を持ちます。それらを次のように書きます。
- モナド乗法： $`\gamma : \cat{E E} \to \cat{E}`$
- モナド単位： $`\iota : \mrm{Id}_\cat{C} \to \cat{E}`$
モナドの乗法と単位に $`\gamma, \iota`$ を使いましたが、習慣としては $`\mu, \eta`$ が多いです。が、習慣を守らないと殺されるわけでもないんで、気にしてません。
「コンテキスタッド、包括圏、ハイパードクトリン // 包括圏とテレスコープ構成」では、$`\gamma`$ を包括圏の包括関手〈comprehension functor〉の意味で使ってましたが、これは単なるコンフリクト〈偶発的かち合い〉です。包括関手とモナド乗法は直接的な関係はありません。
包括関手に対応する概念は、スパンの左右の脚をつなぐ自然変換 $`\rho`$ です。その意味では、包括関手に $`\rho`$ を使っていればオーバーロード（意図的に同じ名前）として説明できました。今度からはそうするかも。
[/補足 追記]
$`\mbf{CAT}`$ 内の図式に展開して描くと次のようです。
$`\quad \xymatrix{
{\cat{C}} \ar@{=}[d]
&{\cat{EE}} \ar@{->>}[l]_{\pi\pi} \ar[r]^{\alpha\alpha}
\ar[d]^\gamma
&{\cat{C}} \ar@{=}[d]
\\
{\cat{C}}
&{\cat{E}} \ar@{->>}[l]_{\pi} \ar[r]^{\alpha}
&{\cat{C}}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
$`\quad \xymatrix{
{\cat{C}} \ar@{=}[d]
&{\cat{C}} \ar@{=}[l] \ar@{=}[r]
\ar[d]^\iota
&{\cat{C}} \ar@{=}[d]
\\
{\cat{C}}
&{\cat{E}} \ar@{->>}[l]_{\pi} \ar[r]^{\alpha}
&{\cat{C}}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
2-圏内のスパンの一般論は「2-圏のなかのスパンのあいだの射」に書いています。スパンのあいだの射には左右の四角形（イコールを縮約すると三角形／二角系）があり、一般的には面倒な計算になります。しかし今ここでは、左右の四角形はどちらも厳密可換です。したがって、次のような等式による記述が可能です。アスタリスクは関手の図式順結合記号です。
- $`\pi\pi = \gamma * \pi`$ （乗法による射影の保存）
- $`\gamma * \alpha = \alpha\alpha`$ （乗法による作用の保存）
- $`\mrm{Id}_\cat{C} = \iota*\pi`$ （単位のセクション性）
- $`\iota;\alpha = \mrm{Id}_\cat{C}`$ （単位の作用に対する中立性〈neutrality〉）
以上はスパンのあいだの射（乗法と単位）が満たすべき等式であって、モナドの法則ではありません。モナドの法則は、モノイド構造の法則でした。
モノイド構造を記述するには、（モナド／モノイドの）乗法 $`\gamma`$ と単位 $`\iota`$ をストリング図で描いてみるのが良い方法です。
$`\quad \xymatrix{
{\cat{E}} \ar@{-}@/_/[dr]
\ar@{}@/_1pc/[rr]|{\cat{C}}
&{}
&{\cat{E}} \ar@{-}@/^/[dl]
\\
{\cat{C}}
&*+[o][F]{\gamma} \ar@{-}[d]
&{\cat{C}}
\\
{}
&{\cat{E}}
&{}
}
`$
$`\quad \xymatrix{
{}
&{\mrm{Id}_\cat{C}} \ar@{.}[d]
&{}
\\
{\cat{C}}
&*+[o][F]{\iota} \ar@{-}[d]
&{\cat{C}}
\\
{}
&{\cat{E}}
&{}
}`$
このレイアウトでは、ストリング図の横方向は、スパンの結合／可換四角形の横結合の方向になります。ストリング図の縦方向は、関手結合／可換四角形の縦結合の方向になります。
モノイド構造の法則を表すストリング図は、「依存アクテゴリーが面白い // 二重圏内のモノイドと2-圏内のモナド」にあります。
ペースティング図は以下の過去記事の2つの節にあります。
[/補足 追記]
横方向の結合を併置、縦方向の結合をアスタリスクで表し、対象（ストリング図のワイヤー）と恒等（ストリング図のダミーのノード）を同一視した記法でテキスト表示するなら、モノイド構造の結合法則と左右の単位法則は次のようになります。
- $`\gamma\cat{E} * \gamma = \cat{E}\gamma * \gamma`$ （結合法則）
- $`\iota\cat{E} * \gamma = \cat{E}`$ （左単位法則）
- $`\cat{E}\iota* \gamma = \cat{E}`$ （右単位法則）
単純な等式で書けました。が、これは記号の乱用と略記と同一視を重ねて得られた単純さであることに注意してください。アンパックして具体的に書き下せばそれなりに複雑になります。
そもそも、高次のモナドの法則は等式で書けるとは限りません。今回は厳密コンテキスタッドに制限することにより、等式による記述を可能にしています。
計算のための具体的な表示
圏 $`\cat{E E}`$（スパン $`\cat{E E}`$ のボディ）の対象を次の形に書くことにします。
$`\quad (X, A, B) \text{ where }\pi(B) = X\cdot A`$
縦ベクトル記法ならば：
$`\quad \ctxpair{A, B}{X} \text{ where } B = \ctxpair{B}{X\cdot A}`$
この書き方が許されることは確認が必要ですが、プルバック四角形の定義をもとに各自確認してみてください。
入れ子の依存ペアに関しては次の等式を仮定します。
$`\quad (X, A, B) = ( (X, A), B) = (X, (X\cdot A, B))`$
縦ベクトル記法ならば次のようです。
$`\quad \ctxpair{A, B}{X} = \ctxpair{B}{ \ctxpair{A}{X} } = \ctxpair{\ctxpair{B}{X\cdot A} }{X}`$
一般論では、これも等式とは限らず結合律子〈unitor〉で記述することになりますが、今回は等式だとします。
コンテキスタッドのモナド乗法 $`\gamma`$ の中置演算子記号として $`\conc`$ を使うことにして（カプチ／マイヤースは $`\otimes`$）、圏 $`\cat{E E}`$ の対象（被演算子＝オペランド）に対する各種演算の結果は次のように表します。
$`\quad \pi\pi( (X, A, B) ) = \pi\pi( X, A, B ) = X`$
$`\quad \alpha\alpha( (X, A, B) ) = (X\cdot A)\cdot B = X\cdot A\cdot B`$
$`\quad \gamma( (X, A, B) ) = \gamma( X, A, B ) = (X, A\conc B)`$
縦ベクトル記法ならば：
$`\quad \pi\pi( \ctxpair{A, B}{X} ) = \pi\pi \ctxpair{A, B}{X} = X`$
$`\quad \alpha\alpha( \ctxpair{A, B}{X} ) = (X\cdot A)\cdot B = X\cdot A\cdot B`$
$`\quad \gamma( \ctxpair{A, B}{X} ) = \gamma \ctxpair{A, B}{X} = \ctxpair{A\conc B}{X}`$
コンテキスタッドのモナド単位は次のように書きます。
$`\text{For }X\in |\cat{C}|\\
\quad \iota(X) = {_X 1} = (X, 1) = \ctxpair{1}{X}
`$
以上に約束した記法を用いて、コンテキスタッドに関する法則を具体的に書き下してみましょう。
- 乗法による射影の保存： $`\pi\pi \ctxpair{A, B}{X} = \pi \ctxpair{A\conc B}{X} = X`$
- 乗法による作用の保存： $`X\cdot (A\conc B) = (X\cdot A)\cdot B`$
- 単位のセクション性： $`\pi \ctxpair{1}{X} = X`$
- 単位の作用に対する中立性： $`X\cdot 1 = X`$
コンテキスタッドのモノイド構造に関する法則は：
- 結合法則： $`\ctxpair{(A\conc B)\conc C}{X} = \ctxpair{A\conc(B\conc C)}{X}`$
- 左単位法則： $`\ctxpair{1\conc A}{X} = \ctxpair{A}{X}`$
- 右単位法則：$`\ctxpair{A\conc 1}{X} = \ctxpair{A}{X}`$
法則達は、比較的単純で自然な形をしていますが、背後では暗黙の変換が色々働いていることに注意してください。
コンテキストフル射
カプチ／マイヤースは $`\mathfrak{Ctx}`$（フラクトゥール体の Ctx）という名前の構成〈construction〉を定義しています。$`\mbf{CAT}`$ 内のコンテキスタッドから二重圏を構成します。$`\mathfrak{Ctx}`$ をコンテキストフル構成〈contextful construction〉と呼ぶことにします（単に「コンテキスト構成」だと他の構成と誤認されそうなので）。
コンテキスタッドからコンテキストフル構成で得られた二重圏のプロ射〈ルーズ射〉がコンテキストフル射〈contextful {morphism | arrow}〉です。コンテキストフル射の実体はベース射なのですが、中間に余ハープーン射（後述）を考えます。「コンテキストフル射」は、次の3つの概念の総称として使います。
- 二重圏のプロ射 $`f: X \not\to Y`$ （矢印がスラッシュ付き）
- 余ハープーン射 $`f: \ctxpair{A}{X} \cohto Y`$ （矢頭〈アローヘッド〉が下半分）
- ベース射 $`f: X\cdot A \to Y`$ （通常の矢印）
これら3つの概念は別物ですが、意図的に混同して語られるかも知れません。
余ハープーン射の双対（矢印の向きを逆転）であるハープーン射は、型理論ではインスタンスを表します。インスタンスは、“コンテキスト”（型理論の意味でのコンテキスト）、“型”と共に、型理論の中核概念です。以下の過去記事で述べています。
余ハープーン射〈coharpoon morphism〉 $`f`$ は、ファイバー付き圏のトータル対象からベース対象への射と考えられます。
$`\quad f:\ctxpair{A}{X} \cohto Y \In \cat{E}`$
ここで、$`\cat{E}`$ はファイバー付き圏を表します。以下の記号の乱用です。
$`\quad \cat{E} = (\cat{E} \overset{\pi}{\to} \cat{C}) \;\in |\mbf{FibCAT}|`$
一方、ハープーン射〈harpoon morphism〉 $`h`$ は、ファイバー付き圏のベース対象からトータル対象への射と考えられます。
$`\quad h:X \hto \ctxpair{B}{Y} \In \cat{E}`$
もちろん、単なるファイバー付き圏〈ファイブレーション〉において、ベース圏とトータルにまたがる射を考えることはできません。スパンの右脚である作用を使って余ハープーン射／ハープーン射を定義します。
余ハープーン射 $`f:\ctxpair{A}{X} \cohto Y`$ の実体は、次のベース射です。
$`\quad f: X\cdot A \to Y \In \cat{C}`$
しかし、域〈ドメイン〉であるトータル対象 $`A = \ctxpair{A}{X}`$ の情報は保持するので、余ハープーン射は、トータル対象とベース射のペアとして定義されます。
$`\quad f = (\ctxpair{A}{X}, f)\\
\text{Where}\\
\quad f: X\cdot A \to Y \In \cat{C}
`$
ここでも、記号の乱用（名前のオーバーロード）が前提です。$`f = (A, f)`$ とも書かれますが、これは次のように展開されます。
$`\quad f = (A, f) = ( \ctxpair{A}{X}, f)`$
ここで、$`f = (A, f)`$ は、記号の乱用で省略されていた情報の補完ですが、$`A = \ctxpair{A}{X}`$ は冗長な情報（$`X = \pi(A)`$）の追加です。
余ハープーン射の結合
スパン $`\cat{E} = (\cat{C}, \cat{E}, \pi, \alpha)`$ はコンテキスタッド〈厳密コンテキスタッド〉の台とします。スパンの左脚であるファイバー付き圏も $`\cat{E} = (\cat{C}, \cat{E}, \pi)`$ と表します（$`\cat{E}`$ を圏、ファイバー付き圏、スパンの3種にオーバーロード）。
この状況で2つの余ハープーン射 $`f = (A, f), g = (B, g)`$ を考えます。次の条件を満たすとき、$`f, g`$ は結合可能〈composable〉です。
$`\quad \mrm{cod}(f) = \pi(B)`$
つまり、結合可能な2つの余ハープーン射は次のように書けます。
$`\quad f = (A, f) = (\ctxpair{A}{X}, f:X\cdot A \to Y)`$
$`\quad g = (B, g) = (\ctxpair{B}{Y}, g:Y\cdot B \to Z)`$
このような $`f, g`$ の結合〈composition〉（後述）を $`f;g`$ で表します。
余ハープーン射の結合可能性／結合は、通常の圏の射の結合可能性／結合とは違います。
- 余ハープーン射の結合可能性は $`\mrm{cod}(f) = \mrm{dom}(g)`$ ではない。
- 余ハープーン射の結合において $`\mrm{dom}(f;g) = \mrm{dom}(f)`$ は成立しない。
しかし、新しい $`\mrm{dom'}, \mrm{cod'}`$ を次のように定義すると、通常の圏の法則が成立するようになります。
$`\quad \mrm{dom'}(f) = \mrm{dom'}( (A, f) ) = \pi(A)`$
$`\quad \mrm{cod'}(f) = \mrm{cod'}( (A, f) ) = \mrm{cod}(f)`$
さて、いよいよ余ハープーン射の結合〈composition of coharpoon morphisms〉の具体的定義です。
余ハープーン射 $`f = (\ctxpair{A}{X}, f)`$ のベース射（のパート）は次のようです。
$`\quad f: X\cdot A \to Y \In \cat{C}`$
これを、$`Y`$ 上の局所対象（ファイバー内に居るトータル対象） $`B`$ に関してデカルト持ち上げします。
$`\quad f\lift B : \ctxpair{f^*(B)}{X\cdot A} \to \ctxpair{B}{Y} \In \cat{E}`$
トータル射 $`f\lift B`$ を作用（スパンの右脚）を使ってベース圏に落とします。
$`\quad (f\lift B)^\bullet : (X\cdot A)\cdot f^*(B) \to Y\cdot B \In \cat{C}`$
この射は、余ハープーン射 $`g = (\ctxpair{B}{Y}, g)`$ のベース射（のパート）と、ベース圏 $`\cat{C}`$ 内で結合可能です。結合すると次の射が得られます。
$`\quad (f\lift B)^\bullet ; g : (X\cdot A)\cdot f^*(B) \to Z \In \cat{C}`$
ところで、$`(X\cdot A)\cdot f^*(B) = X\cdot (A\conc f^*(B) )`$ なので、次のような余ハープーン射を構成可能です。
$`\quad (\ctxpair{A\conc f^*(B)}{X}, (f\lift B)^\bullet ; g)`$
これが、余ハープーン射 $`f`$ と $`g`$ の結合です。通常の射とは様子が違うので、余ハープーン結合〈coharpoon composition〉と呼んだほうが間違いが少ないでしょう。
双対的に、ハープーン射とハープーン結合を定義できます（定義が自明というわけではありません）。
そしてそれから
今回は、余ハープーン射と余ハープーン結合を定義しただけで、余ハープーン射／余ハープーン結合の性質を調べたり応用したりはこれからです。
余ハープーン射 $`f`$ を、コンテキストフル射（二重圏のプロ射） $`f:X \not\to Y`$ とみなすことが、コンテキストフル構成の基本となります。二重圏のタイト射はベース圏 $`\cat{C}`$ の射です。二重圏の二重射については今回は触れていません。
コンテキストフル構成を型理論に応用するときは、余ハープーン射の双対であるハープーン射から余コンテキストフル射を構成することになるでしょう。余コンテキストフル射が型理論のインスタンスをモデル化する概念です。
型理論〈依存型理論〉の難しいところは、インスタンスが通常の射とは異なる振る舞いをするところです。インスタンスをハープーン射／余コンテキストフル射として定式化することで、難しさが軽減する可能性があります。
*1:コンテキスタッドが棲息できる環境である2-圏を、カプチ／マイヤースはパラダイス〈paradise〉と呼んでいます。
