「判断形式を普通に書く」より：
型理論の判断形式を使うと、非常に簡潔に書けます。しかし、簡潔さの代償として、多くの情報を暗黙化します。コラリア／ディ-リベールティも簡潔な記述を目指しているので、えげつない「記号の乱用、短縮記法、完全な省略」を使っています。その記法は簡潔さ（≒難読さ）の極北とも言えるものです。
なんでそこまで簡潔にしないといけないの？ そうしないと死んでしまうの？
簡潔にしないと死んでしまうなら、しょうがないです。短く簡潔に書くことにしましょう。しかし、行き当たりばったりに短くするんではなくて、短くするための系統的手法を使って欲しい。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\In}{\text{ in }}
`$
この記事では以下の手法を使って短く簡潔に書く方法を紹介します。
- 演算子記号の優先順位
- 演算子記号の省略
- コアージョン〈coercion | 型強制〉
内容：
何をしたいのか
圏 $`\cat{C}`$ のなかで次のような図式を考えます。$`\text{p.b.}`$ はプルバック四角形であることを示します。
$`\quad \xymatrix{
\cdot \ar[rr]\ar[d]
\ar@{}[drr]|{\text{p.b.}}
&{}
&\cdot \ar[d]
\\
\cdot \ar[rr] \ar[d]
\ar@{}[drr]|{\text{p.b.}}
&{}
&\cdot \ar[d]
\\
\cdot \ar[r]
&{\cdot} \ar[r]
&\cdot
}\\
\quad \In \cat{C}`$
この図式の頂点と辺（矢印）に、できるだけ短いラベルを付けたいのです。
基本的な対象と射には一文字の名前〈ラベル〉を付けます。対象はラテン文字大文字（$`A, X`$ など）、射はラテン文字小文字（$`f, u`$ など）とします。基本的な対象と射から構成可能な対象と射のラベルは、一文字の名前に次の記号操作で組み立てた記号例だとします。
- 単に並べる（併置）
- ピリオドを挟んで並べる。
- 上付きアスタリスクを付ける。
併置
対象と射以外に関手も考えます。ラテン文字大文字 $`F, G`$ あたりを関手として使います。対象、射、関手を表わす文字（または記号列）の併置の意味を次のように定めます。
- 射と射の併置は、反図式順結合： $`gf := g\circ f`$
- 関手と対象の併置は、対象への関手適用： $`FA := F(A)`$
- 関手と射の併置は、射への関手適用： $`Ff := F(f)`$
- 関手と関手の併置は、反図式順結合： $`GF := G\cdot F`$
反図式順結合記号 $`\circ, \cdot`$ と適用の丸括弧は省略しますが、演算子記号（を補完した場合）の優先順位は、関手適用より射の結合が優先されるとします。例えば、$`Fgf`$ は $`F(g\circ f)`$ であり $`F(g)\circ f`$ ではありません。
$`GFf`$ は $`(G\cdot F)(f)`$ と解釈しても $`G(F(f))`$ と解釈しても、どっちでも同じです。
以上の規則では、射と対象の併置、例えば $`Af`$ は許されません。後で、射と対象の併置にも意味を与えます。
ピリオド
ピリオドは、ファイバー積〈fibered product〉を表わす中置演算子記号だとします。ピリオドの左右は、コスパンを構成する射であり、演算の結果はファイバー積（コスパンの極限対象）だとします。以下の図のようです。
$`\quad \xymatrix{
{f.g} \ar[r] \ar[d]
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]^g
\\
\cdot \ar[r]_f
&{\cdot}
}\\
\quad \In \cat{C}`$
ファイバー積は一意には決まりませんが、なにかひとつを選んだ結果が $`f.g`$ です。
ピリオドは、演算子記号としての優先順位は低くなります。以下の図をみてください。
$`\quad \xymatrix{
{gf.h} \ar[rr] \ar[d]
\ar@{}[drr]|{\text{p.b.}}
&{}
&\cdot \ar[d]^h
\\
\cdot \ar[r]_f
&{\cdot} \ar[r]_g
&\cdot
}\\
\quad \In \cat{C}`$
上付きアスタリスク
圏 $`\cat{C}`$ に対して、$`\cat{C}/A`$ はオーバー圏〈over category〉だとします。$`\cat{C}`$ がプルバックを持つ圏（ファイバー積を自由に作れる圏）なら、$`f:A \to B\In \cat{C}`$ に対して、以下のような関手を定義できます。
$`\quad f^* : \cat{C}/B \to \cat{C}/A \In \mbf{CAT}`$
$`(u: Y\to B)\in |\cat{C}/B|`$ に対して、関手 $`f^*`$ による値は $`f^*(u)`$ です。それは、以下のようなプルバック四角形として描けます。
$`\quad \xymatrix{
\cdot \ar[r] \ar[d]_{f^*(u)}
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]^u
\\
A \ar[r]_f
&B
}\\
\quad \In \cat{C}`$
$`f^*(u)`$ は、$`f`$ による $`u`$ のファイバー引き戻しです。$`u`$ による $`f`$ のファイバー引き戻しも同様です。ファイバー積もピリオド演算子で書き込むと次のようになります。
$`\quad \xymatrix{
{f.u} \ar[r]^{u^*(f)} \ar[d]_{f^*(u)}
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]^u
\\
A \ar[r]_f
&B
}\\
\quad \In \cat{C}`$
コアージョン
圏 $`\cat{C}`$ には、特定されたひとつの対象 $`Z`$ があり、任意の対象 $`X`$ から $`Z`$ に向かう射 $`\pi_X : X \to Z`$ も特定されているとします。
$`Af`$ のように、対象と射の結合が出現したとき、対象 $`A`$ は $`\pi_A`$ のことだと解釈します。型が不整合なときに、型が整合するように再解釈することをコアージョンといいます。これは、対象を射だと再解釈するコアージョンです。
例として、次の図式を考えます。
$`\quad \xymatrix{
{}
&{}
&\cdot \ar[d]_g
\\
\cdot \ar[rr]^h
&{}
&B \ar[d]_{\pi_B}
\\
X \ar[r]^f
&A \ar[r]^{\pi_A}
&Z
}\\
\quad \In \cat{C}`$
$`Af, Bg, Bh`$ を書き込むと次のようです。
$`\quad \xymatrix{
{}
&{}
&\cdot \ar[d]_g \ar@/^1pc/[dd]^{Bg}
\\
\cdot \ar[rr]^h \ar[drr]|{Bh}
&{}
&B \ar[d]_{\pi_B}
\\
X \ar[r]^f \ar@/_1pc/[rr]_{Af}
&A \ar[r]^{\pi_A}
&Z
}\\
\quad \text{commutative }\In \cat{C}`$
簡潔で短いラベル
最初の節に挙げたプルバック四角形が積み重なった図式に対して、今まで述べた手法を使って、簡潔で短いラベルを付けてみます。
$`\quad \xymatrix{
{B^*Af.g} \ar[rr]^{g^*B^*Af} \ar[d]_{(B^*Af)^*g}
\ar@{}[drr]|{\text{p.b.}}
&{}
&Y \ar[d]^g
\\
{Af.B} \ar[rr]|{B^*Af} \ar[d]_{(Af)^*B}
\ar@{}[drr]|{\text{p.b.}}
&{}
&B \ar[d]^{\pi_B}
\\
X \ar[r]_f
&A \ar[r]_{\pi_A}
&Z
}\\
\quad \In \cat{C}`$
図式を見ながらならなんとか解釈できると思います。では、テキストだけ出されたらどうでしょう？
- $`{B^*Af.g}`$
- $`{g^*B^*Af}`$
- $`{(B^*Af)^*g}`$
- $`{Af.B}`$
- $`{B^*Af}`$
- $`{(Af)^*B}`$
なかなかキビシイですよね。コラリア／ディ-リベールティ論文（「判断形式を普通に書く」参照）では、これとは違った流儀ですが、同程度に短い記法を使っています。これ以上に短くするのは困難そうなので「簡潔さ（≒難読さ）の極北」と言ったのです。
