依存型に一般化したカリー同型：$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{ \text{ in } }
`$
$`\quad \cat{C} \in |{\bf Cat}|\\
\quad A:I \to |\cat{C}|_0 \In {\bf Set}\\
\quad \prod_{i\in I} \cat{C}(X, A_i)
\cong \cat{C}(X, \Pi_I A_\bullet) \In {\bf Set}
`$
圏に一般化：
$`\quad \cat{K} \in |{\bf s2CAT}|\\
\quad \cat{A}:\cat{I} \to |\cat{K}|_{\le 1} \In {\bf CAT}\\
\quad \prod_{\cat{I} } \cat{K}(\cat{X}, \cat{A}[\bullet])
\cong \cat{K}(\cat{X}, \Pi_{\cat{I}} \cat{A}[\bullet] ) \In {\bf s2CAT}
`$
特に：
$`\quad {\bf Cat} \in |{\bf s2CAT}|\\
\quad \cat{A}:\cat{I} \to |{\bf Cat}|_{\le 1} \In {\bf CAT}\\
\quad \prod_{\cat{I} } {\bf Cat}(\cat{X}, \cat{A}[\bullet])
\cong {\bf Cat}(\cat{X}, \Pi_{\cat{I}} \cat{A}[\bullet] ) \In {\bf s2CAT}
`$
双対化してみる。
$`\quad \cat{C} \in |{\bf Cat}|\\
\quad B:I \to |\cat{C}|_0 \In {\bf Set}\\
\quad \prod_{i\in I} \cat{C}(B_i, Y)
\cong \cat{C}(\Sigma_I B_\bullet, Y) \In {\bf Set}
`$
圏に一般化：
$`\quad \cat{K} \in |{\bf s2CAT}|\\
\quad \cat{B}:\cat{I} \to |\cat{K}|_{\le 1} \In {\bf CAT}\\
\quad \prod_{\cat{I} } \cat{K}(\cat{B}[\bullet], \cat{Y} )
\cong \cat{K}(\Sigma_{\cat{I}} \cat{B}[\bullet], \cat{Y} ) \In {\bf s2CAT}
`$
特に：
$`\quad {\bf Cat} \in |{\bf s2CAT}|\\
\quad \cat{B}:\cat{I} \to |{\bf Cat}|_{\le 1} \In {\bf CAT}\\
\quad \prod_{\cat{I} } {\bf Cat}(\cat{B}[\bullet], \cat{Y} )
\cong {\bf Cat}(\Sigma_{\cat{I}}\cat{B}[\bullet] ,\cat{X} ) \In {\bf s2CAT}
`$
これは、依存2-型理論といえる。インスティチューション理論と組み合わせたい。
