整合性の証明

$h$ を適用でない項として $n = h\;a_1 \cdots a_k$ と書く。

$k = 0$ ならば $n = h$ は、適用以外の形はこれしかないので、宇宙、$\Pi$、$\lambda$、変数のいずれかであり、変数は生成補題により $\dom(\Gamma)$ に属する。

$k \ge 1$ とする。適用についての生成補題を外側から内側へ $k$ 回適用すると、すべての接頭辞 $h\;a_1 \cdots a_i$ が型付け可能であり、特に最も内側の適用 $h\;a_1$ から、ある $y$、$A$、$B$ について $\Gamma \vdash h : \tPi{y}{A}{B}$ がわかる。ここで $h$ の形を考えると、まず $\lambda$ ではなく、そうなら $h\;a_1$ が正規項 $n$ の内部の $\beta$ 簡約基になってしまう。また、生成補題によりその型は宇宙に変換可能になるが、合流性により宇宙は $\tPi{y}{A}{B}$ に変換可能でないので、宇宙や $\Pi$ でもない。したがって $h$ は変数 $x$ であり、生成補題により $\dom(\Gamma)$ に属し、$\Gamma \vdash x : \tPi{y}{A}{B}$ が成り立ち、これが求める $C$ である。

$\cdot \vdash t : \tPi{P}{\Sort{0}}{P}$ と仮定する。強正規化により $t$ は正規項 $n$ に簡約され、型保存性により $\cdot \vdash n : \tPi{P}{\Sort{0}}{P}$ である。補題 D.2 を 2 回使って、そのような $n$ が存在しないことを示す。

正規形は $\lambda$ である。 補題 D.2 により、$n$ は宇宙、$\Pi$、$\lambda$、中立項のいずれかである。

• 頭部が空の文脈の変数になるはずだが、そのような変数はないので、中立項ではない。
• 生成補題により $\tPi{P}{\Sort{0}}{P}$ が宇宙に変換可能になるが、合流性がそれを排除するので、宇宙や $\Pi$ でもない。

よって $n = \tLam{x}{A}{s}$ であり、生成補題により、ある $B$ について $x : A \vdash s : B$ かつ $\tPi{P}{\Sort{0}}{P} \conv \tPi{x}{A}{B}$ である。合流性により、新鮮な $z$ について $A \conv \Sort{0}$ かつ $\subst{P}{P}{z} \conv \subst{B}{x}{z}$、すなわち $z \conv \subst{B}{x}{z}$ である。両辺で $z$ に $x$ を代入すると、補題 D.1 の (c) により変換可能性が保たれるので、$x \conv B$ を得る。本体 $s$ は正規項 $n$ の部分項なので正規である。まとめると、$A \conv \Sort{0}$ かつ $B \conv x$ のもとで $x : A \vdash s : B$ である。

本体は存在しえない。 $\Gamma = x : A$ とおく。補題 D.2 により、$s$ は宇宙、$\Pi$、$\lambda$、中立項のいずれかである。

• $s$ が宇宙または $\Pi$ なら、生成補題により $B$ は宇宙に変換可能になり、$s$ が $\lambda$ なら $B$ は $\Pi$ に変換可能になる。しかし $B \conv x$ であり、合流性により変数はどちらにも変換可能でない。
• $s$ が中立項なら、その頭部は $\dom(\Gamma) = \{x\}$ の変数なので $s = x\;a_1 \cdots a_k$ である。$k = 0$ なら $s = x$ で、生成補題により $B \conv A$ なので $x \conv B \conv A \conv \Sort{0}$ となるが、変数は宇宙に変換可能でない。$k \ge 1$ なら、補題 D.2 により $\Pi$ に変換可能な $C$ について $\Gamma \vdash x : C$ であり、変数 $x$ についての生成補題により $C \conv A \conv \Sort{0}$ なので $\Pi$ が宇宙に変換可能になり、合流性がそれを排除する。

すべての場合が矛盾に至るので、型 $\tPi{P}{\Sort{0}}{P}$ をもつ閉じた項は存在しない。