少し追記。
- 型コンテキストを型判断と呼ぶ用語法は採用しない。
- 型シーケント $`\Gamma \vdash M:\sigma`$ を型判断〈typing judgement〉と呼ぶのは許容しよう。
- 型判断の意味はセマンティック・デカルト閉圏の射になる。特に集合圏では単なる写像。型コンテキストの意味は直積の形をした集合（方体状集合〈cube-shaped set〉）。型コンテキストや型判断で使われている名前〈ラベル | インデックス | キー〉は意味論に関係ない。
- $`\Gamma \vdash M \equiv N :\sigma`$ という関数項の同値性判断（または等値性判断〈equality judgement〉）が出てくる。これは、高次圏の可逆2-射になる。集合圏の2-射は等式しかないので、同値性判断の意味は、写像の等式になる。
- ベータ変換則〈beta rule〉とエータ変換則〈eta rule〉が、同値性の生成子になる。
- 命題項＝論理式 の解釈〈意味論〉では、命題項の全体、またはその意味の集合は（ブール代数というより）ハイティング代数になると仮定する。
- 関手としての∀、∃と翻訳関手が自然変換になる条件がベック／シュバレー条件。
- モデルが置換による作用と協調することがベック／シュバレー条件。
- 真偽対象〈truth object〉を持つようなデカルト閉圏から、ハイパードクトリンを作れる。真偽対象は命題値と論理順序〈logical order | implication order〉の内部圏。命題関数＝述語。命題項＝論理式。
- ハイパードクトリンでは、真偽対象から述語空間〈述語集合〉が定義できる。
- ハイパードクトリンに対する述語空間の構造はハイティング代数だが、ハイティング代数以外に選ぶことができる。
- 述語空間関手は反変で、選ばれた射に対して左右の随伴が存在してベック／シュバレー条件を満たす。
- 選ばれた射としては射影が多いが、選ばれた射のクラスは任意でよい。
様々なレベルのプログラミングが出来る。
- 型レベル・プログラミング ： 型リテラル、型変数、型コネクティブ〈型構成子記号〉から型項を組み立てるプログラミング。
- データ・レベル・プログラミング ： データ・リテラル〈ポイント・リテラル〉、データ変数〈通常の変数〉、データ・コネクティブ〈データ構成子記号〉からデータ項を組み立てるプログラミング。データ＝ポイント
- 関数レベル・プログラミング ： 関数リテラル、関数変数、関数コネクティブから関数項を組み立てるプログラミング。
- 置換レベル・プログラミング ： 置換リテラル、置換変数、置換コネクティブから置換項を組み立てるプログラミング。
- 命題レベル・プログラミング ： 命題リテラル、命題変数〈述語変数〉、命題コネクティブ〈論理コネクティブ〉から命題項〈論理式〉を組み立てるプログラミング。
- 導出レベル・プログラミング ： 導出リテラル〈公理〉、導出変数、導出コネクティブ〈リーズニング〉から導出項〈証明〉を組み立てるプログラミング。
- リーズニング・レベル・プログラミング ： リーズニング・リテラル、リーズニング変数、リーズニング・コネクティブからリーズニング項を組み立てるプログラミング。
- 構成手続きレベル・プログラミング： 手続きリテラル、手続き変数、手続きコネクティブから構成手続き項を組み立てるプログラミング。
命題とデータは関数の特別なもの。置換は関数の集まり。
