導出と置換の書き方

$`\newcommand{\Sep}{\mathrel{\|} }
\newcommand{\Subst}[2]{ {\scriptsize \begin{bmatrix} #1\\ #2 \end{bmatrix} } }
%`$

$`\quad \alpha \Sep \varphi: \Gamma \to B`$

ここで：

1. 型コンテキストはギリシャ文字小文字
2. 命題コンテキストはギリシャ大文字
3. 命題はラテン文字大文字
4. 導出はギリシャ小文字後半

これは以下と同じ。

$`\quad \varphi: \Gamma \to B \text{ in }\mathrm{Prop}[\alpha]`$

$`f:\beta \to\alpha`$ を型コンテキストのあいだの多写像として、置換結果は次の導出になる。

$`\quad \beta \Sep \varphi': \Gamma\Subst{f(\vec{y})}{ \vec{x}} \to B\Subst{f(\vec{y})}{ \vec{x}} `$