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

\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(A,B:\mathord {\textnormal {\textsf {Psh}}}(C)\)を前層とする。型\(\mathord {\textnormal {\textsf {Hom}}}(A,B):\mathcal {U}(i)\)

\(\lbrace h:\prod _{\lbrace x:C\rbrace }A(x)\to B(x)\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\forall _{a:A(x_{2})}h(a\cdot f)=h(a)\cdot f\rbrace \)
と定義する。\(\mathord {\textnormal {\textsf {Hom}}}(A,B)\)の要素を前層の射(morphism of presheaves)と呼ぶ。