ホモトピー型理論
[006P] 定義

関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。米田埋め込み(Yoneda embedding)\(\mathord {\textnormal {\textsf {よ}}}(C):\mathord {\textnormal {\textsf {Fun}}}(C,\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C))\)[006R][006M]\(\mathord {\textnormal {\textsf {Map}}}^{(\mathord {\textnormal {\textsf {Fun}}})}(C)\)に対応するものと定義する。