相対モナド $`T`$ を、記号の乱用をしないで書くと：
$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%
\quad T = (C^T, \eta^T, \mrm{Ext}^T)/J
`$
ここで、$`J:\cat{C}\to \cat{D}`$ はルート関手〈root functor〉とします。各構成素を次のように呼ぶことにします。
- $`C^T`$ は、相対モナド $`T`$ のコンストラクタ〈constructor〉
- $`\eta^T`$ は、相対モナド $`T`$ の単位〈unit〉
- $`\mrm{Ext}^T`$ は、相対モナド $`T`$ の{クライスリ}?拡張〈{Kleisli}? extension〉
$`C^T`$ は台関手〈underlying functor〉と呼んでましたが、定義の上では関手ではない（関手である必要はない）ので「コンストラクタ」にします。ただし、結果的には関手にすることができます。
通常、記号の乱用と略記を使って次のように書きます。
$`\newcommand{\hyp}{\text{－} }
%
\quad T = (T, \eta, (\hyp)^\#)/J
`$
相対モナド $`T`$ のアイレンベルク／ムーア代数 $`A`$ を、記号の乱用をせずに書けば：
$`\quad A = (U(A), \mrm{EMExt}^A)`$
各構成素は:
- $`U(A)`$ は、アイレンベルク／ムーア代数 $`A`$ の台対象〈underlying object〉
- $`\mrm{EMExt}^A`$ は、アイレンベルク／ムーア代数 $`A`$ のアイレンベルク／ムーア拡張〈Eilenberg-Moore extension〉
「相対モナドのアイレンベルク／ムーア圏」では、アイレンベルク／ムーア代数を $`(A, \alpha)`$ のように書いたのですが、さらに記号の乱用をして次のように書くことにします。
$`\quad A = (A, (\hyp)^A)`$
つまり、右肩に付けた $`A`$ により、アイレンベルク／ムーア拡張を表すことにします。次のようになります。
$`\text{For }X \in |\cat{C}|\\
\text{For }v:J(X)\to A \text{ in } \cat{D}\\
\quad v^A : T(X) \to A \text{ in } \cat{D}
`$
型理論の構文論の文脈で相対モナドが登場するときは、次のように想定します。
- 相対モナドは、構文モナド〈{syntax | syntactic} monad〉である。
- $`\cat{C}`$ の要素は、型コンテキスト〈{type | typing} context〉である。
- 相対モナドのコンストラクタは、項コンストラクタ〈term constructor〉である。
- 相対モナドのクライスリ圏の反対圏は、コンテキスト達の圏〈category of contexts〉となる*1。
- 相対モナドのアイレンベルク／ムーア代数は、型システムのモデル〈model〉となる。
- アイレンベルク／ムーア代数への
クライスリ射 $`v:J(X)\to A \text{ in } \cat{D}`$ *2は、コンテキストへの$`A`$-付値〈$`A`$-valuation〉となる。
相対モナドのルート関手 $`J`$ の余域 $`\cat{D}`$ は、型システムのモデルであるアイレンベルク／ムーア代数が棲んでいるので、意味領域〈semantic domain〉です。$`J(X)`$ は、構文的対象物であるコンテキスト $`X`$ を意味的対象物とみなしたものです。
型理論は構文論中心なので、モデルはあまり出てこないのですが、もし意味論を扱うなら、相対モナドとそのアイレンベルク／ムーア代数を使うのが便利そうです。
