ファミリー付き圏〈category with families | CwF〉やC-システム〈C-system〉（コンテキスト圏〈contextual category〉と同じ）など、型理論の構文的側面を圏論的に定式化した圏（型理論的圏）では、「射影〈projection〉」と呼ばれる射が登場します。射影がペアで登場するときは、「第一射影〈first projection〉」、「第二射影〈second projection〉」という呼び方をします。
ところが、「第一射影」、「第二射影」が何を意味するかは、人により場合によりまったく違ってしまうのですよね。$`\newcommand{\cat}[1]{\mathcal{#1}}`$
以下の図は、型理論的圏 $`\cat{C}`$ 内の図式だとします。図式全体として可換にはなっていません（可換な部分もありますが）。
$`\quad \xymatrix{
{}
& {(Y\cdot B)\cdot p^* B} \ar[d]^{p''}
\\
X' \ar[r]^{g'} \ar[d]^{p'}
& Y\cdot B \ar[d]^{p} \ar@/^/[u]^{s'}
\\
X \ar[r]_g \ar[ur]|f \ar@/^/[u]^{s}
& Y
}\\
\quad \text{ in }\cat{C}
`$
上の図の説明：
- $`X, Y, X'`$ は、圏 $`\cat{C}`$ の対象で、型理論ではコンテキスト〈context〉と呼びます。ギリシャ文字大文字 $`\Gamma, \Delta`$ などで書く場合が多いです。
- $`B`$ は、型理論の言葉では、コンテキスト $`Y`$ における（構文的に許される）型項〈type term〉です。単に「型」と略称されます。
- '$`\cdot`$' は、コンテキスト拡張〈context extension〉と呼ばれる操作の中置演算子記号です。
- $`p, p', p''`$ は、コンテキスト拡張に伴う標準射影〈canonical projection〉です。コンテキスト拡張に対して一意的に割り当てられる射です。
- $`X', Y\cdot B, Y, X`$ の四角形はプルバック四角形です。別な言い方をすると、$`X'`$ はコスパン $`(g, p)`$ に対するファイバー積です。
- $`f;p = g`$ は成立しています。
- $`s`$ は $`p'`$ のセクション、$`s'`$ は $`p''`$ のセクションです。つまり、$`s;p' = \mathrm{id}_X`$ 、$`s';p'' = \mathrm{id}_{Y\cdot B}`$ 。型理論の言葉では、$`s, s'`$ はインスタンス項〈instance term〉です。単に「項」と略称されます。
この状況で、次のような言い方をします。
- ファミリー付き圏〈CwF〉の文脈では、コンテキスト拡張 $`Y\cdot B`$ に対して、$`p`$ を第一射影、$`s'`$ を第二射影と呼ぶ。
- $`X'`$ はファイバー積なので、$`p'`$ をファイバー積の第一射影、$`g'`$ を第二射影と呼ぶ。
- 射 $`f`$ の射影分解（「拡張包括構造のもうひとつの定式化 // 拡張包括構造と射影分解」参照）において、$`g`$ を $`f`$ の第一射影、$`s`$ を第二射影と呼ぶ。
表にまとめると：
| 第一射影 | 第二射影 | |
|---|---|---|
| 場合 1 | $`p`$ | $`s'`$ |
| 場合 2 | $`p'`$ | $`g'`$ |
| 場合 3 | $`g`$ | $`s`$ |
まー、なんてことでしょう。
