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

\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。\(\mathord {\textnormal {\textsf {Map}}}^{(\mathord {\textnormal {\textsf {Fun}}})}(C):\mathord {\textnormal {\textsf {BiFun}}}(\mathord {\textnormal {\textsf {Op}}}(C),C;\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i))\)を次のように定義する。

  • -\(\mathord {\textnormal {\textsf {obj}}}\equiv \lambda (x_{1},x_{2}).\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\)
  • -\(\mathord {\textnormal {\textsf {map}}}_{1}\equiv \lambda (x_{11},x_{12},f,x_{2}).\lambda h.h\circ f\)
  • -\(\mathord {\textnormal {\textsf {map}}}_{2}\equiv \lambda (x_{1},x_{21},x_{22},f).\lambda h.f\circ h\)