依存カリー同型と依存フビニ定理

カリー同型とフビニ定理は切っても切れない。フビニ定理は、カリー同型で互いに移る高階関数と多変数関数の積分が一致することを主張している。

同様に、依存カリー同型と依存フビニ定理は切っても切れない。依存フビニ定理は、カリー同型で互いに移る高階依存ファミリー〈繰り返し依存ファミリー〉とテレスコープ〈複項依存ファミリー〉のシグマ構成〈グロタンディーク構成〉が本質的に一致することを主張している。

依存版のカリー同型/フビニ定理は、精密に議論する必要がある。

これかな?$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{cat}[1]{\mathcal{#1} }
`$

$`\mrm{Fam}(\int_{x\in A} B(x), \cat{C}) \cong \Pi(\lambda\, x\in A. \mrm{Fam}(B(x), \cat{C}) )
%`$

あるいは、

$`[ \sum_{x\in A} B(x), \cat{C}] \cong \prod(\lambda\, x\in A. [B(x), \cat{C}])
%`$

あるいは、

$`\cat{C}^{\sum_{x\in A} B(x)} \cong \prod_{x\in A} \cat{C}^{B(x)}
%`$

フビニは:

$`\int_{(a, b)\in \int_{x\in A} B(x)} F(a, b) \cong
\int_{x\in A}(\lambda\, x\in A. \int_{y\in B(x)} F(x, y))
`$

あるいは

$`\sum(\sum(A \mid B)\mid F) \cong
\sum(A \mid \lambda\, x.\sum(B(x) \mid F(x, -)))
`$