ラムダ計算の意味論においては、カリー同型が中心的な概念です。となると、依存ラムダ計算の意味論には依存カリー同型が必要になります。とりあえずは一番具体的なデカルト閉圏である集合圏において依存カリー同型を考えてみます。$`\newcommand{\id}{\mathr…