主動詞： declare〈宣言する〉, define〈定義する〉, approve〈承認する〉
副動詞： request〈要求する〉, respond〈応答する〉
主語は We, One of us, I だが、省略可能。
組み合わせは：
- declare 名前 仕様 ： 名前を宣言する。存在に関しては中立。
- declare request 名前 仕様 ： 名前を宣言すると同時に、定義を要求する。
- define 名前 {仕様}? 本体 ： 名前に指示対象物を定義する。存在が保証される。
- define respond 名前 {仕様}? 本体 ： リクエストに答えて名前に指示対象物を定義する。
- approve 名前 {仕様}? ： 定義せずに仕様を承認する。
- approve request 名前 {仕様}? ： 定義せずに仕様を承認するが、定義の要求はする。
declare/define されるサブジェクトは：
- type / family = type with params / proposition = logic type / predicate = proposition with params = logic type with params
- function = instance with params / theorem = witness with params
インスタンスはセクション、関数は特にセクションの要請はない。任意の要素はセクション〈ポインティングセクション〉とみなせるので、要素はインスタンスである。パラメーター付きインスタンスは、一般のセクション。
となると、インスタンスは依存関数で、関数は非依存関数。概念的に、インスタンスの特別なものが関数となり、違和感が生じる。次のウロボロス現象が生じる。
- 関数はセクションの特別なもの（ファイバーが一定）
- セクションは関数の特別なもの（シグマ型への関数）
ミニチュア版のウロボロス現象は：
- リストはタプルの特別なもの（値の集合が一定）
- タプルはリストの特別なもの（引数ごとに値の部分集合の制限あり）
「異なる型に共通のインスタンスがあるのか？」問題もある。いずれにしても必ず分離〈make disjoint | 無交差化〉できる。
「インスタンスには型が決まる」ためには、「インスタンスとは要素である」と考えることはできない。「インスタンスは射である」なら、「射には余域が決まる」と整合する。したがって、型理論の解釈は（集合論ではなくて）圏論になる。
パラメーター付きインスタンスと関数は、非依存型理論では同じだが、以前型理論では違う概念。
ハードモデル〈モデル論的モデル〉とソフトモデル〈構成手続き〉は違う概念だが、言語のリテラル拡張〈固有名詞拡張〉により、ハードモデルはソフトモデルとして書ける。これは、言語側にセマンティック領域〈ターゲット圏〉を埋め込んでしまう方法。一方で、ターゲット圏やモデルの圏から言語（形式体系）を絞り出す方法もある。
メモ： セクション空間型は $`\langle X \leadsto \ltimes F\rangle`$ だと勘違いがないかな。$`\mathrm{Sect}(X\ltimes F \twoheadrightarrow X)`$ と同じ。$`\mathrm{Map}(X, X\ltimes F)`$ の部分集合。
