関数があるとき、引数型と戻り型の仕様が型プロファイル、単にプロファイルとも呼ぶ。プロファイル概念は集合圏の射以外でも考えられる。
引数変数を含む項を使って関数を定義するときの $`\cdots \mapsto \cdots`$ は戻り値指定〈return value disignation〉と呼ぶことにする。
戻り値指定による関数定義は、
$`\quad \big\langle x : X \mapsto \varphi : Y\big\rangle`$
この戻り値指定で定義された関数の型プロファイルは
$`\quad X \to Y`$
依存関数の場合は、
$`\quad \big\langle x : X \mapsto \varphi : F_x \big\rangle`$
この戻り値指定で定義された依存関数の型プロファイルは
$`\quad (x: X) \to F_x`$
プロファイルでも変数 $`x`$ が必要になる。この変数は束縛変数。
依存関数空間の型は、
$`\quad \prod_{x: X} F_x`$
次は同値：
- $`f: (x: X) \to F_x`$ 依存プロファイル
- $`f^\wedge : {\bf 1} \to [(x: X) \to F_x]`$ 依存関数空間へのポイント
- $`f^\wedge \in \prod_{x: X} F_x`$ 依存関数集合の要素
ややこしいのは、依存関数のプロファイルが、関数と考えることができて、関数の値指定を書けること。
$`\quad F := \big\langle x : X \mapsto \Phi : \mathrm{Type}\big\rangle`$
次のような段階的定義がある。
- $`F : X \to \mathrm{Type} \text{ in }{\bf SET}`$
- $`F_\bullet := \big\langle x : X \mapsto \Phi : \mathrm{Type}\big\rangle \text{ in }{\bf SET}`$
- $`f :(x: X) \to F_x \:\in \mathrm{Sect}(F)`$
- $`f : X \to \sum_x F_x \text{ section } \:\in \mathrm{Sect}(F)`$
- $`f := \big\langle x : X \mapsto \varphi : F_x \big\rangle \:\in \mathrm{Sect}(F)`$
