述語という概念により、Propositions-as-Functions なのだが、$`\mathrm{Pred}(X)`$ を型ファミリー $`\mathrm{PRED}(X)`$ に持ち上げる。すると：
- 真偽値は、型になる。
- 述語は、型ファミリーになる。
真偽値／述語を型／型ファミリーに持ち上げることにより、証明過程が通常の計算過程に対応して、定理記述が関数定義になる。証明図の構成が計算図の構成になる。
$`\mathrm{Pred}(X)`$、$`\mathrm{PRED}(X)`$、$`\mathrm{TypeFam}(X)`$ から3つの包括コンテキスタッドが定義できて、それらの間のコンテキスタッド射があるのだろう。
