カリー同型は、複関数〈multifunction | 多重関数 | 多変数関数〉と高階関数〈higher-order function〉との1：1対応を与える。同様に、依存カリー同型は、依存複関数と依存高階関数のあいだの対応を与える。さらに、関数を関手に一般化するると、依存複関手と依存高階関手のあいだの対応を与える。$`\newcommand{\cat}[1]{\mathcal{#1} }
%`$
依存複関手はテレスコープ〈telescope〉と呼び、依存高階関手は繰り返しファミリー〈iterated family〉と呼ぶ。長さ2のテレスコープ〈2項依存関手〉の場合を述べる。
$`(\cat{C}, F, G)`$ を長さ2のテレスコープとすると、
$`G:\int_{\cat{C}} F \to {\bf CAT}`$
依存カリー化を次のように定義する。
$`G^{\cap F} := \lambda\, x: \cat{C}.\int_{F(x)}G_x(-)`$
ここで：
- 積分記号はグロタンディーク構成。
- $`x:\cat{C}`$ は $`x`$ が圏 $`\cat{C}`$ の対象または射を走る変数だと宣言している。
- $`G_x(-) = G(x, -)`$
$`[\cat{C}, {\bf CAT}]`$ をインデックス付き圏の全体とする。インデックス付き圏は圏のファミリーと言っても同じ。さらに、
$`[*, {\bf CAT}] := \int_{x : {\bf Cat}} [x, {\bf CAT}]`$
と定義する。すると、標準的なファイブレーションがある。
$`\pi: [*, {\bf CAT}] \to {\bf Cat}`$
一方で、忘却関手もある。
$`U: [*, {\bf CAT}] \to {\bf CAT}`$
次に、$`H:\cat{C} \to [*, {\bf CAT}]`$ に対して依存反カリー化を定義する。
$`H`$ と標準射影の結合を $`\underline{H}`$ とする。依存反カリー化 $`H_\cup`$ は次のプロファイルを持つ二項依存関手になる。
$`H_\cup : \int_\cat{C} \underline{H} \to {\bf CAT}`$
$`H_\cup`$ は、$`(\cat{C}, \underline{H}, H_\cup)`$ というテレスコープで書ける。つまり、高階ファミリーの依存反カリー化はテレスコープ〈複項依存関手〉になる。
示すべきは次：
- $`(G^{\cap F})_{\cup} \cong G`$
- $`(H_\cup)^{\cap \underline{H}} \cong H`$
