ホモトピー型理論
[006R] 演習

関数外延性を仮定する。iiを階数、C,D,X:PreCat(i)C,D,X:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏とする。同値

Fun(X,Fun(Cat)(C,D))BiFun(C,X;D)\mathord {\textnormal {\textsf {Fun}}}(X,\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D))\simeq \mathord {\textnormal {\textsf {BiFun}}}(C,X;D)
を構成せよ。