2023-02-26から1日間の記事一覧

依存カリー同型と依存ベータ変換

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\hyp}{ \text{-} } `$$`\mrm{K}^X_I`$ を $`I`$ 上の定数ファミリーとして、$`A`$ を任意のファミリーとする。ファミリーの射$`\quad \mrm{K}^X_I \to A \text{ on }I`$は、グロタンディーク同型により次…