コンテキストと拡張、いろいろ

我々は、様々なレベルのコンテキスト（ライブラリ、モジュール／セクション）を行為〈activity〉により拡張していくのだが、拡張のための行為は二種類しかない。

1. 関数定義 （λΠ計算ベース）
2. 帰納的型定義 （CICベース）

関数定義は def で、帰納的型定義は inductive 、これだけ。他のキーワード（例： theorem, structure）はシンタックスシュガー。

関数定義〈定理記述〉は、宇宙単相と宇宙多相がある。宇宙とカリー／ハワード対応は意識する。混合コンテキストには次が入る。

1. 関数定義
   1. 計算項の型判断
   2. 関数名への計算項割り当て
   3. 定義的等式〈definitional equality〉
   4. 定義展開〈unfold〉書き換え規則
2. 帰納的型定義
   1. 型名
   2. 型名名前空間
   3. コンストラクタ疑似関数（1つ以上、複数可能、0個なら空型）
   4. リカーサー

定理は証明ボディに名前を付けたもの。推論規則は定理なので、引数型＝前提命題と戻り型＝結論命題を持つ。推論規則の引数は、多くの場合命題ではなくて、証明／証拠である。証明項／証拠ラベル／定理名〈計算項／要素ラベル／関数名〉は交換可能である。

命題コネクティブ〈型演算子〉と証明コンビネータ〈計算コンビネータ〉は区别すべし。だが、命題型宇宙だと、Trueからの命題への証明が証明無関係〈proof irrelevance〉原理により本質的に1つしかないので、証明と命題の区别は困難である。