依存関数

1. 型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, F) \to I) = \Pi(I, F)`$
2. 関数型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, [F, G]) \to I) = \Pi(I, [F, G])`$

一番は依存リストで、ニ番はインデックス付き関数〈indexed function = indexed family of functions〉だな。

1. 値-indexed 値 ＝ 関数 $`X \to Y \text{ in }{\bf Set}`$
2. 値-indexed 型 ＝ 型ファミリー $`X \to |{\bf Set}| \text{ in }{\bf SET}`$
3. 型-indexed 型 ＝ 総称型、型構成子、型レベル関数 $`|{\bf Set}|\to |{\bf Set}|\text{ in }{\bf SET}`$
4. 値-indexed 関数 ＝ 高階関数（の一種）、反カリー化して多変数関数 $`X \to Z^Y\text{ in }{\bf Set}`$
5. 型-indexed 関数 ＝ 多相関数 $`|{\bf Set}| \to \mathrm{Mor}({\bf Set})\text{ in }{\bf SET}`$
6. 関数-indexed 関数 ＝ 高階関数（の一種）、作用素 $`Y^X \to T^S \text{ in }{\bf Set}`$

	値-indexed	関数-indexed	型-indexed
値	関数	汎関数	？（例：デフォルト）
関数	高階関数	高階関数〈作用素〉	多相関数
型	ファミリー	？（例：域、余域）	型構成子