型理論では、「代入〈substitution〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。
ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰もが曖昧多義語を自力で難なく解釈できるわけでもなくて、混同・混乱・誤解してしまうこともあります。「代入」の曖昧性を一度は分析しておく意義はあるでしょう。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\ot}{\leftarrow}
\newcommand{\op}{\mathrm{op}}
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Ent}{ \sqsubseteq }
\newcommand{\rev}{\mathop{\triangleleft} }
\newcommand{\snoc}{\mathop{\blacktriangleleft} }
`$
内容：
- 型理論を語ることの難しさ： 標準はない
- 「代入」の意味
- 型理論と圏論の記法
- 構文か意味か
- 型理論の構文圏
- 様々な代入
- 代入レコードのオペレーション項への作用と代入結合
- 構成手続きとしての代入レコード
- コンテキスト射の表現としての構成手続き
- 指標射の表現としての還元手続き
- おわりに
型理論を語ることの難しさ： 標準はない
集合論は、そんなにたくさんはありません。有名どころは：
ツェルメロ／フレンケル集合論が圧倒的多数派で、事実上の独占状態になっています。通常の用途では、「集合論 ＝ ツェルメロ／フレンケル集合論」だとしてかまいません。
論理も、古典論理が圧倒的多数派なので、「論理 ＝ 古典論理」で問題ありません。
しかし、型理論は何百もあり、圧倒的多数派は存在せず、現状は群雄割拠の時代です。「型とはなんぞや？」に対しても、それぞれの型理論がそれぞれの答を準備しています。「集合論・圏論 vs. 型理論」から再掲すると：
- Sets-as-Types
- Algebras-as-Types
- Coalgebras-as-Types
- Propositions-as-Types
- Categories-as-Types
- Logical Relations-as-Types*1
- ‥‥
この記事で想定してる型理論は、カートメル／ヴォエヴォドスキー／パルムグレンの型理論（「 カートメル／ヴォエヴォドスキー／パルムグレンの型理論」参照）です。カートメル／ヴォエヴォドスキー／パルムグレンの型理論のキャッチフレーズは次です。
- Families-as-Types
- Functors-as-Types
一般的には「関手が型だ」と考えますが、特に関手の域が離散圏のときは「ファミリーが型だ」となります。
型理論の構文としては、スターリングのGAT構文（「GAT〈ガット〉の構文： スターリングの論文から」「実用になる型理論の記法」参照）を念頭に置いています。
「代入」の意味
とりあえず見渡すと、「代入」が6種類くらいの意味で使われているようです。それぞれの意味ごとに別な呼び名を用意しましょう。
- 代入文〈substitution statement〉 ： $`\xi := M`$ という形式の構文的対象物
- 代入レコード〈substitution record〉 ： 代入文の順序付き名前付きのコレクション（名前は代入文の左辺）
- 代入作用〈substitution action〉 ： 代入レコードの項に対する作用
- 代入結合〈substitution composition〉 ： 2つの代入レコード対する二項演算
- 構成手続き〈construction procedure〉としての代入レコード ： コンテキスト射の構文的表現（それが構成手続き）としての代入レコード
- 還元手続き〈reduction procedure〉としての代入レコード ： 指標射の構文的表現（それが還元手続き）としての代入レコード
これらを理解するには、さらに次の用語の理解が必要です。
- 構文的対象物〈syntactic object〉*2
- 順序付き名前付きのコレクション
- 項
- 作用
- コンテキスト射
- 指標射
- 構文的表現
これらの用語も解説していきます。
型理論と圏論の記法
型理論と圏論では、記法のコンフリクト（競合／かち合い）が起きているので、そのことをハッキリさせておきます。
まず、「圏」という言葉は、1-圏に限らず2-圏、3-圏などの高次圏をも意味するとします。また、「圏」が0-圏（つまり、単なる集合）かも知れません。任意の n に対して、n-圏は、高次の恒等射を追加して考えれば(n + 1)-圏とみなせます。とはいえ、「圏 ＝ 1-圏」の場合が多いですが。
$`\cat{C}`$ を圏（つまり、n-圏）だとして、次の左右は同じ意味です。
$`\quad A\In \cat{C} \iff A \in |\cat{C}|`$
$`\quad f : A \to B \In \cat{C} \iff f\in \cat{C}(A, B)`$
$`\quad \alpha :: f \twoto g: A\to B \In \cat{C} \iff \alpha\in \cat{C}(A,B)(f, g)`$
このとき使われているコロンは、プロファイルコロン〈profile colon〉と呼ぶことにします。
一方、型理論の居住関係〈inhabitation relation〉を表すコロンは居住記号〈inhabitation symbol〉と呼ぶことにします。
圏論における内部ホムを構成する演算子記号は $`[\hyp,\hyp]`$ が多数派ですが、型理論では矢印 $`\hyp\to\hyp`$ が演算子記号に使われます。ここでは、折衷案で $`[\hyp \to \hyp]`$ を内部ホムの記号とします。
圏論のプロファイル記述と型理論の居住記号を区別して書きたいときは、居住記号に $`\in:`$ を使います。多くのケースで、次の左右は同じ意味です。右が型理論、左が圏論です。
$`\quad a \in: A \iff a : \mbf{1} \to A \In \cat{C}`$
$`\quad f \in: A \to B \iff f:\mbf{1} \to [A\to B]\In \cat{C}`$
型理論では圏 $`\cat{C}`$ が暗黙化されます。集合圏を想定しているなら、次のようです。
$`\quad a \in: A \iff a : \mbf{1} \to A \In \mbf{Set}`$
$`\quad f \in: A \to B \iff f:\mbf{1} \to [A\to B]\In \mbf{Set}`$
さらに、ポインティング写像と要素を同一視して、集合論の記法で書くなら：
$`\quad a \in: A \iff a \in A`$
$`\quad f \in: A \to B \iff f \in \mrm{Map}(A, B)`$
以下では、プロファイルコロンと居住記号が紛らわしいときは、居住記号に上記のように $`\in:`$ を使います。型理論的文脈だとハッキリとわかっているときは、居住記号にコロンを使ってかまいません。内部ホムは常に $`[\hyp \to\hyp]`$ を使います。
構文か意味か
以下は同義語で、どっちを使うかは好みの問題です。
- ソート ＝ 型
- オペレーション ＝ 関数
圏論的解釈をするなら、ソートは圏の対象であり、オペレーションは特別な射*3のことです。このように、ソート／オペレーション（型／関数 と言っても同じ）を意味的対象物〈semantic object〉と解釈する場合、その意味的対象物を表現する構文的対象物〈syntactic object〉を「項〈term〉」と呼びます。
- ソートを表現する構文的対象物はソート項〈型項〉
- オペレーションを表現する構文的対象物はオペレーション項〈関数項〉
論理では、項〈個体項〉と式〈論理式〉を区別することがありますが、ほとんどの分野・場合で、項〈term〉と式〈expression〉は同義語です。例えば、ラムダ計算のラムダ項とラムダ式は同義語です。ラムダ抽象だけをラムダ項／式と思っているなら、それは単なる勘違いです。
型理論ではしばしば、ソート項〈型項〉を単にソート〈型〉とも呼び、オペレーション項〈関数項〉を単にオペレーションとも呼びます。構文論中心に考えるなら、そういう呼び方になります。しかしそうなると、意味的対象物をなんて呼ぶか？ 呼び分ける必要があるなら、ソート実体〈sort entity〉、オペレーション実体〈operation entity〉と呼ぶことにします。
| 構文論中心 | 意味論中心 |
|---|---|
| ソート ＝ ソート項 | ソート ＝ ソート実体 |
| オペレーション ＝ オペレーション項 | オペレーション ＝ オペレーション実体 |
型理論は構文論の議論が多いので、ソートがソート項を意味し、オペレーションがオペレーション項を意味する場面が多いです。さらに、次のようなアンバランスな規約が多数派です。
- 「ソート〈型〉」はソート項〈型項〉を意味する。
- 単に「項」と言ったら、それはオペレーション項〈関数項〉を意味する。
- 「ソート」が（文脈により）ソート実体を意味することもある。
- 「項」が（文脈により）オペレーション実体を意味することもある。
オペレーション項をインスタンス項と呼ぶこともあります（僕はけっこう使います）が、「インスタンス」がこれまた曖昧多義語なので（「型理論のインスタンスとは」参照）、「インスタンス」は使わないほうが吉かも知れません。
型理論の構文圏
なにか（意味）を表す予定の記号的なデータ構造が構文的対象物〈syntactic object〉です。構文的対象物は、文字・記号・名前などを基本データとして形式文法〈formal grammar〉を使って定義されます。
型理論に出てくる構文的対象物達を編成して圏に仕立てることが出来ます。そのような圏を（型理論の）構文圏〈{syntax | syntactic} category〉と呼ぶことにします。習慣として、構文圏の対象をコンテキスト〈context〉、射をコンテキスト射〈context morphism〉と呼びます。コンテキスト射の別名が“代入”ですが、この意味での代入は、用語「代入」の4番目の用法である「構成手続きとしての代入レコード」のことです。
コンテキストと指標〈signature〉は同義語です。この2つの言葉が指すモノはまったく同じです。指標については「構造記述のための指標と名前 1/n 基本」「インターフェイスとしての指標、設計者と利用者と実装」を参照してください。
コンテキストと指標は同じモノですが、コンテキストの圏〈category of contexts〉 $`\cat{C}`$ と指標の圏〈category of signatures〉 $`\cat{S}`$ は違います（同じ圏ではない）。互いに反対圏なのです。次の関係が成立しています。
- $`|\cat{S}| = |\cat{C}|`$
- $`\cat{C}^\op = \cat{S}`$
- $`\cat{S}^\op = \cat{C}`$
詳しくは次の過去記事に書いています。
$`\cat{C}`$ を型理論の構文圏だとして、次のような事情です。
- $`\Gamma\in |\cat{C}|`$ をコンテキストと呼ぶ。（ギリシャ文字大文字を使うのは習慣）
- 同じ $`\Gamma`$ を $`\Gamma \in |\cat{C}^\op|`$ とみなしたモノを指標と呼ぶ。
- $`\varphi : \Gamma \to \Delta \In \cat{C}`$ をコンテキスト射と呼ぶ。
- 同じ $`\varphi`$ を $`\varphi : \Delta \to \Gamma \In \cat{C}^\op`$ とみなした射を指標射と呼ぶ。
コンテキスト／指標は、宣言文を並べた構文的対象物ですが、コンテキスト射／指標射もまた構文的対象物で表現可能です（「表現」の正確な意味は後述）。コンテキスト射／指標射に関わる諸々の構文的対象物を（多義的に）「代入」と呼ぶのです。
様々な代入
やっと本題の「代入」の話です。
構文的メタ変数に関しては「実用になる型理論の記法」とだいたい同じ約束を採用します。
- 変数名を表すメタ変数は $`\xi, \eta`$ など
- オペレーション名を表すメタ変数は $`\theta`$ など
- ソート項を表すメタ変数は $`A, B`$ など
- オペレーション項を表すメタ変数は $`M, N`$ など
なんらかのモノを順序付きで並べたコレクション型データをリスト〈list〉と呼びます（普通どおり）。順番は一切なくて、モノを名前〈キー〉で識別するコレクション型データをディクショナリ〈dictionary〉と呼びます。
成分〈component | item〉に順番（あるいは順序位置）があり、名前〈キー〉でも参照できるコレクション型データは、ここではレコード〈record〉と呼ぶことにします。レコードは、リストとディクショナリの両方の性格を持つので、囲み記号は丸括弧でも波括弧でもどっちでもいいとします。成分の区切り記号はカンマか改行とします。レコードは、名前とナニカのペアのコレクションですが、以下の表現はどれもレコードとして許容します。
丸括弧囲みカンマ区切り：
$`( (\xi, X), (\eta, Y) )`$
波括弧区切りカンマ区切り：
$`\{ (\xi, X), (\eta, Y) \}`$
丸括弧囲み改行区切り：
$`( \\
\quad (\xi, X)\\
\quad (\eta, Y)\\
)`$
波括弧囲み改行区切り：
$`\{\\
\quad (\xi, X) \\
\quad (\eta, Y) \\
\}`$
指標内に出現する宣言文では、ペア $`(\xi, X)`$ を $`x : X`$ と書きます。コロンは型理論の居住記号なので、そのことを明示したいなら $`\xi \in: X`$ です。
代入文では、ペアの区切りに '$`:=`$' を使います。以下が代入文の構文です。
$`\quad \xi := M`$
ここで、$`\xi`$ は名前、$`M`$ はオペレーション項です。名前 $`\xi`$ は、前もって次の形の宣言文で宣言されているとします。
$`\quad \xi \in: A`$
宣言文の右辺 $`A`$ はソート項です。
代入文を幾つか並べたレコード（リストでもディクショナリでもなくてレコード！）が代入レコードです。代入レコードは、単なる構文的対象物のことであり、用途や意味については何も言ってません。
代入レコードのオペレーション項への作用と代入結合
構文記述のために、「型理論のコロン、ターンスタイル、カンマ」で導入した構文的なスノック（レコードの末尾に成分〈項目〉を追加する）演算の演算記号として '$`\snoc`$' を使います。
オペレーション項 $`M`$ と代入レコード $`\varphi`$ は、BNF記法で次のように定義されます。
$`\quad M ::= \xi \mid \theta \rev \varphi`$
$`\quad \varphi ::= () \mid \varphi \snoc (\xi := M)`$
ここで、'$`\rev`$' は、オブジェクト構文レベルの引数渡し記号で、$`\xi`$ は変数名（を表すメタ変数）、$`\theta`$ はオペレーション名（を表すメタ変数）です。日本語散文で記述するなら：
- オペレーション項は、変数〈名前〉、または、オペレーション記号に引数を渡した形である。（引数は代入レコードになっている。）
- 代入レコードは、空レコード、または、既にある代入レコードに代入文を追加（演算記号 '$`\snoc`$'）したレコードである。
すべてのオペレーション項の集合（構文的集合）を $`\mbf{OpTerm}`$ 、すべての代入レコードの集合を $`\mbf{SubstRec}`$ とします。次のような写像を定義します。
$`\quad \mrm{ract} : \mbf{OpTerm}\times \mbf{SubstRec} \to \mbf{OpTerm} \In \mbf{Set}`$
$`\quad \mrm{opcmp} : \mbf{SubstRec}\times \mbf{SubstRec} \to \mbf{SubstRec} \In \mbf{Set}`$
$`\mrm{ract}`$ は「右からの作用〈right action〉」にちなんでいます。$`\mrm{opcmp}`$ は「反対〈opposite〉の向きの結合〈合成 | composition〉」からです*4。これらを相互再帰的に定義します。$`\mrm{ract}`$ の中置演算子記号を $`\hyp[\hyp]`$ 、$`\mrm{opcmp}`$ の中置演算子記号を $`\hyp \circ \hyp`$ として記述します。構文的写像の記述はわかりにくいかも知れないので、この節の補足として色付き記述について書いています。
右からの代入作用：
- $`\xi [()] := \xi`$ （左 変数、右 空レコード）
- $`\xi [(\xi := M)] := M`$ （左 変数、右 単項レコード）
- $`\xi \ne \eta`$ のとき $`\xi [(\eta := M)] := \xi`$ （左 変数、右 単項レコード）
- $`\xi [\varphi \snoc (\eta := N)] := (\xi[\varphi])[(\eta := N)]`$ （左 変数、右 スノック演算による構成）
- $`(\theta\rev \psi) [\varphi] := \theta\rev [\psi \circ \varphi]`$ （左 引数渡し、右 任意レコード）
反対向きの代入結合：
- $`() \circ \varphi := ()`$ （左 空レコード、右 任意レコード）
- $`\psi \circ () := \psi`$ （左 任意レコード、右 空レコード）
- $`(\psi \snoc (\eta := N) ) \circ \varphi := (\psi \circ \varphi) \snoc (\eta := N[\varphi])`$ （左 レコード・スノック演算、右 任意レコード）
以上の定義が、相互再帰的な定義として well-defined なことは確認が必要です。漏れがないことは、以下の表で確認できます。
代入作用のとき：
| 空レコード | 単項レコード | スノック | |
|---|---|---|---|
| 変数 | ルール1 | ルール2, 3 | ルール4 |
| 引数渡し | ルール5 | ルール5 | ルール5 |
代入結合のとき（丸括弧は、そのルールからただちに分かることを示す）：
| 空レコード | スノック | 任意レコード | |
|---|---|---|---|
| 空レコード | (ルール1, 2) | (ルール1) | ルール1 |
| スノック | (ルール2) | (ルール3) | ルール3 |
| 任意レコード | ルール2 |
なお、いま定義した“右からの代入作用”と“反対向きの代入結合”は、構文圏を作るときの素材にはなりますが、ただちに圏を定義しているわけではないので注意してください。
上の定義では、次のコンフリクトが起きています。
- 定義のメタレベルの記号 '$`:=`$' と、オブジェクトレベルの代入記号 '$`:=`$' がコンフリクトしている。
- 定義のメタレベルの丸括弧と、オブジェクトレベルの丸括弧がコンフリクトしている。
以下のように色分けして記述することにします。$`\require{color}
\newcommand{O}[1]{\textcolor{orange}{#1} }
\newcommand{R}[1]{\textcolor{red}{#1} }
\newcommand{G}[1]{\textcolor{green}{#1} }
`$
- 定義のメタレベルの記号は赤色
- 構文的写像〈構文的作用素〉の記号はオレンジ色
- 構文的変数は緑色
- その他は黒色
右からの代入作用：
- $`\G{\xi} \O{[}()\O{]} \R{:=} \G{\xi}`$ （左 変数、右 空レコード）
- $`\G{\xi} \O{[}(\G{\xi} := \G{M})\O{]} \R{:=} \G{M}`$ （左 変数、右 単項レコード）
- $`\G{\xi} \ne \G{\eta}`$ のとき $`\G{\xi} \O{[}(\G{\eta} := \G{M})\O{]} \R{:=} \G{\xi}`$ （左 変数、右 単項レコード）
- $`\G{\xi} \O{[} \G{\varphi} \O{\snoc} \R{(}\eta := \G{N}\R{)} \O{]} \R{:=} \R{(}\xi \O{[} \varphi \O{]} \R{)} \O{[}(\eta := N)\O{]}`$ （左 変数、右 スノック演算による構成）
- $`\R{(} \G{\theta} \rev \G{\psi} \R{)} \O{[} \G{\varphi} \O{]} \R{:=} \G{\theta}\rev \O{[} \G{\psi} \O{\circ} \G{\varphi}\O{]}`$ （左 引数渡し、右 任意レコード）
赤色の '$`\R{:=}`$' は定義のメタレベルで、黒色の '$`:=`$' はオブジェクトレベルの記号です。赤色の丸括弧は定義のメタレベルで、黒色の丸括弧はオブジェクトレベルの記号です。
[/補足]
構成手続きとしての代入レコード
代入レコードは、代入文を並べたものなので次のように書けます。
$`\quad (\xi_1 := M_1, \cdots, \xi_n := M_n)`$
あるいは、次のように書かれるかも知れません。
$`\{ \\
\quad \xi_1 := M_1\\
\quad \cdots\\
\quad \xi_n := M_n\\
\}`$
他にも構文のバリエーションはいくらでもあるでしょうが、構文のバリエーションはどうでもいいのです。
さて一方、指標は宣言文を並べたものです。宣言文の名前とソート項の区切り記号は $`\in:`$ として書けば次のようです。
$`\quad (\xi_1 \in: A_1, \cdots, \xi \in: A_n)`$
指標の構文のバリエーションも、もちろん山のようにあります。もちろんどうでもいいです。
型理論における（正確に言えば、カートメル／ヴォエヴォドスキー／パルムグレンの型理論における）構文圏は、指標（コンテキストと言っても同じ）を対象として、代入レコードを射とする圏です（次節に補足コメントあり）。ただし、若干の追加構造が必要です。
$`\Sigma`$ を指標とするとき、$`\Sigma`$ に出現する名前（宣言文の左辺）の集合を $`\mrm{Name}(\Sigma)`$ とします。同じ名前が重複して出現することはないので、レコードとしての $`\Sigma`$ の長さと、集合 $`\mrm{Name}(\Sigma)`$ の基数は同じです。
$`\varphi`$ を代入レコードとするとき、指標と同様に $`\mrm{Name}(\varphi)`$ を定義します。
$`M`$ をオペレーション項として、$`M`$ に出現する変数名の集合を $`\mrm{Var}(M)`$ とします*5。$`\mrm{Var}(M)`$ は名前の有限集合です。$`\mrm{Var}(M) = \emptyset`$ である項 $`M`$ は閉じた項〈closed term〉と呼ばれたりします。
型理論の構文圏の射は、2つの指標 $`\Sigma, \Gamma`$ と1つの代入レコード $`\varphi`$ をまとめた $`(\Sigma, \Gamma, \varphi)`$ ですが、色々と条件が付きます。この条件はめんどくさいです。
まず、$`\mrm{Name}(\varphi) = \mrm{Name}(\Gamma)`$ である必要があります。名前の集合が一致するだけでなくて、名前の出現の順番も一致することが要求されます。$`\mrm{Name}(\varphi)`$ の名前達と $`\mrm{Name}(\Gamma)`$ の名前達は、共に次の順番で出現するとします。
$`\quad \eta_1, \cdots, \eta_m`$
すると、代入レコード $`\varphi`$ は次の形に書けます。
$`\{\\
\quad \eta_1 := M_1\\
\quad \eta_2 := M_2\\
\quad \cdots \\
\quad \eta_m := M_m \\
\}`$
$`M_j`$ に出現する名前に次の制限が付きます。
- $`\mrm{Var}(M_1) \subseteq \mrm{Name}(\Sigma)`$
- $`\mrm{Var}(M_2) \subseteq \mrm{Name}(\Sigma) \cup \{\eta_1\}`$
- $`\cdots`$
- $`\mrm{Var}(M_m) \subseteq \mrm{Name}(\Sigma) \cup \{\eta_1, \cdots, \eta_{m - 1}\}`$
ここで問題があって、$`\mrm{Name}(\Sigma)\cap\mrm{Name}(\Gamma)\ne \emptyset`$ だとマズイことになります。これを回避するために、事前のリネームが必要です。鬱陶しい。
名前に関する条件だけではなくて、代入レコードのオペレーション項と指標のソート項のあいだに居住関係が成立していることも要求されます。この条件を確認するためには、いわゆる“型推論”が必要になります。めんどうな話なので、型推論に関しては割愛します。
単なる代入レコードではなくて、色々な条件をクリアした三組 $`(\Sigma, \Gamma, \varphi)`$ を構成手続き〈construction procedure〉と呼ぶことにします。構成手続きは構文的に定義されるので構文的対象物です。
コンテキスト射の表現としての構成手続き
ラムダ計算では、項に出現する変数を系統的かつ安全にリネームすることをアルファ変換〈alpha conversion〉と呼びます。ラムダ項だけではなくて、今扱っているソート項／オペレーション項、指標、代入レコードなどに対してもアルファ変換は定義できます。
アルファ変換で互いに移りあえる2つの構文的対象物はアルファ同値〈alpha equivalent〉だといいます。アルファ同値は実際に同値関係になります。
前節で「構文圏は、指標（コンテキストと言っても同じ）を対象として、代入レコードを射とする圏」と書きましたが、これは端折った言い方です。ほんとは次のようになります。
- 構文圏の対象は、指標のアルファ同値類
- 構文圏の射は、構成手続きの同値類で、指標のアルファ同値類とコンパチブルなもの
上記の射の定義は曖昧〈雰囲気的〉ですが、リネームの影響を無視した概念です。構成手続きは、固定された特定の名前に基づいて定義されるので、“射そのもの”というより“射の代表元”です。有理数が分数で表現／表示されるのと同様に、射は構成手続きで表現／表示されます。
型理論や論理がめんどくさくなる一因は、「名前は必要だが、名前が邪魔になる」というジレンマです。どこで名前を使い、どこで名前を捨象するかに気を使う必要があります。ほんとにめんどくさーーい。
指標射の表現としての還元手続き
前節の「構文圏」とは、コンテキスト（の同値類）を対象とする圏です。コンテキストと指標は同じものです。が、コンテキストの圏と指標の圏では、射の向きが逆転します。射が変わるのではなくて、形式的・名目的に逆にするだけです。
もとの圏と反対圏では言葉づかいを変えます。
| コンテキストの圏 | 指標の圏 |
| コンテキスト | 指標 |
| コンテキスト射 | 指標射 |
| 構成手続き | 還元手続き |
指標の圏では、指標のあいだの指標射は還元手続きにより表現・表示されます。しかし、還元手続きと構成手続きは（向き以外は）同じものです。
もとの圏と反対圏を一緒に考えなくてはならないことも、型理論がめんどくさくなる一因です。めんどくさーーい。
おわりに
「代入〈substitution〉」と呼ばれる様々なモノを再度まとめると：
- 代入文 $`\xi := M`$
- 代入レコード $`\varphi = (\xi_1 := M_1, \cdots, \xi_n := M_n)`$
- 代入作用 $`\hyp [\hyp]`$
- 代入結合 $`\hyp \circ \hyp`$
- 構成手続き $`\varphi: \Sigma \to \Gamma \In \cat{C}`$ （$`\varphi`$ は色々な条件を満たす）
- 還元手続き $`\varphi: \Gamma \to \Sigma \In \cat{C}^\op`$ （$`\varphi`$ は色々な条件を満たす）
他にも「代入」と呼ばれるモノはあるかも知れません。「代入」のような曖昧多義語に出会ったときは、立ち止まって分析して、曖昧性を解決しましょう。
