「外部バージョンの依存カリー同型」にて： 外部バージョンの依存カリー同型は、極限の定義をなぞっているだけなので、内部化しないと面白くはありません。面白くすることは、今考え中です。 集合圏とは限らない圏 $`\mathcal{C}`$ に対して依存カリー同型を…