https://x.com/m_hiyama/status/1965268093120512343 にて：
異なる分野を対応付けると概念が節約できて覚えることが劇的に減る。
だけど、用語はまったく減らないし、用語法がシッチャカメッチャカになって混乱するのは永遠の悩み。
シッチャカメッチャカにならないように、少数のコンフリクトしない用語だけを使って概要（とても大雑把）を整理しておきます。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\hyp}{\text{－} }
`$
- 型理論では、型システムの構文圏〈{syntax | syntactic} category〉$`\cat{C}`$ が出てくる。
- $`\cat{C}`$ の対象をコンテキスト〈context〉、射をコンテキスト射〈context morphism〉と呼ぶ。
- インスティチューション理論では、$`\cat{C}`$ の反対圏 $`\cat{S} := \cat{C}^\op`$ が出てくる。
- $`\cat{S}`$ の対象を指標〈signature〉、射を指標射〈signature morphism〉と呼ぶ。
型理論とインスティチューション理論では、興味の中心や手法は違いますが、扱っているモノ自体は同じです。以下、インスティチューション理論の指標達の圏 $`\cat{S}`$ について述べます。
- 圏 $`\cat{S}`$ の広い部分圏 $`\cat{S}^\mrm{sharp}`$ がある*1。部分圏 $`\cat{S}^\mrm{sharp}`$ の射はシャープ指標射〈sharp signature morphism〉、あるいは単にシャープ射〈sharp morphism〉と呼ぶ。
- 包含関手 $`\cat{S}^\mrm{sharp}\hookrightarrow \cat{S}`$ は、クライスリ包含〈Kleisli inclusion〉である。つまり、背後に相対モナドがあり、$`\cat{S}`$ はその相対モナドのクライスリ圏である。
- 背後にある相対モナドを構文モナド〈{syntax | syntactic} monad〉と呼ぶ。呼び名は「モナド」でも、実際は相対モナド。構文モナドを $`T = (T, \eta, (\hyp)^\#)/J`$ とする。
構文モナドの話。
- 構文モナド（と呼ぶ相対モナド） $`T`$ のルート関手 $`J:\cat{S}^\mrm{sharp} \to \cat{T}`$ の余域 $`\cat{T}`$ はターゲット圏〈target category〉と呼ぶ。ターゲット圏は暗黙に指定されることが多い。暗黙だと明示的言及もない。
- 構文モナドの $`T:|\cat{S}^\mrm{sharp}| \to |\cat{T}|`$ は項コンストラクタ〈term constructor〉
- 指標達の圏は構文モナド（と呼ぶ相対モナド）のクライスリ圏なので、$`\cat{S} = \mrm{Kl}(T)`$
- $`\cat{S}^\mrm{sharp}, \cat{S}, \cat{T}`$ などを含む外側の圏をアンビエント圏〈ambient category〉と呼び。アンビエント圏は圏達の圏なので通常2-圏である。2-圏なので、アンビエント・ドクトリン〈ambient doctrine〉とも呼ぶ。アンビエント圏は暗黙に指定されることが多い。暗黙だと明示的言及もない。
- アンビエント圏を $`\cat{A}`$ とする。
以上から次の図式ができます。
$`\quad \xymatrix {
{}
&{\mrm{EM}(T) } \ar@/^/[ddr]^U
&{}
\\
{}
&{\mrm{Kl}(T) } \ar[u] \ar[dr]^E
&{}
\\
{\cat{S}^\mrm{sharp} } \ar[rr]_J \ar[ur]^K \ar@/^/[uur]^F
&{}
&{\cat{T} }
}\\
\quad \text{ in }\cat{A}\\
\text{where}\\
\quad K \dashv_J E\\
\quad F \dashv_J U
`$
ここで：
- $`\mrm{Kl}(T)`$ は、構文モナド（と呼ぶ相対モナド） $`T`$ のクライスリ圏
- $`K`$ は、クライスリ包含
- $`E`$ は、クライスリ拡張
- $`K \dashv_J E`$ は、相対随伴系で、相対モナド $`T`$ のクライスリ分解〈Kleisli resolution〉
- $`\mrm{EM}(T)`$ は、構文モナド（と呼ぶ相対モナド） $`T`$ のアイレンベルク／ムーア圏
- $`F`$ は、自由関手
- $`U`$ は、忘却関手
- $`F \dashv_J U`$ は、相対随伴系で、相対モナド $`T`$ のアイレンベルク／ムーア分解〈Eilenberg-Moore resolution〉
- 上向きの無名の矢印は、クライスリ圏をアイレンベルク／ムーア圏に埋め込む規準的関手
*1:$`\cat{S}^\sharp`$ あるいは $`\cat{S}_\sharp`$ と書いてもいいかも知れません。
