「環境付き計算と依存アクテゴリー 2/n」の続きです。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\In}{\text{ in }} %\newcommand{\u}[1]{\underline{#1}} %\newcommand{\twoto}{ \Rightarrow } \newcommand{…