$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\hyp}{ \text{-} }
`$
$`\mrm{K}^X_I`$ を $`I`$ 上の定数ファミリーとして、$`A`$ を任意のファミリーとする。ファミリーの射
$`\quad \mrm{K}^X_I \to A \text{ on }I`$
は、グロタンディーク同型により次のようなバンドル射〈ファイブレーション射〉と解釈できる。
$`\require{AMScd}
\begin{CD}
X \times I @>f>> \sum_I A\\
@V{\pi_1}VV @VV{\pi}V \\
I @= I
\end{CD}`$
このことを次のように書く。$`X \rtimes I`$ は $`I`$ 上の自明バンドル。
$`\quad f \in \{X \rtimes I \to \sum_I A\}_I`$
圏 $`{\bf Fib}[I]`$ のホムセットを中括弧記法＋下付き添字で表している。
$`\quad \{X \rtimes I \to \sum_I A\}_I \equiv {\bf Fib}[I](X \rtimes I, \sum_I A)`$
依存カリー化は次の写像。$`\mrm{DCurry}(f) = f^\wedge`$
$`\quad \mrm{DCurry} : \{X \rtimes I \to \sum_I A\}_I \to \{X \to \prod_I A \}`$
依存評価射は、
$`\quad \mrm{dev} : \prod_I A \times I \to \sum_I A`$
ベータ等式は：
$`\quad \mrm{dev}(f^\wedge, \hyp) = f`$
あるいは、
$`\quad \mrm{dev}\circ \langle f^\wedge, \hyp \rangle = f(\hyp)`$
幾つかの同型がある。
- $`{\bf Ind}[I](\mrm{K}^X_I, A)\cong {\bf Fib}[I](X \rtimes I, \sum_I A)`$ グロタンディーク
- $`\{X \rtimes I \to \sum_I A\}_I \cong \{X \to \prod_I A \}_{\bf 1}`$ カリー
- $`\{X \to \prod_I A \}_{\bf 1} \cong (\prod_I A)^X \cong \prod_I (A^X)`$ 指数法則
- $`\{X \rtimes I \to \sum_I C\}_I \cong \{X \rtimes I \to C \rtimes I \}_I \cong\{X \times I \to C \}_{\bf 1}`$
- $`\prod_I C \cong C^I`$ 依存関数と関数
