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

\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(F,G:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)を関手とする。型\(\mathord {\textnormal {\textsf {NatTrans}}}(F,G):\mathcal {U}(i)\)

\(\lbrace t:\prod _{x:C}\mathord {\textnormal {\textsf {Map}}}(F(x),G(x))\mid \forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G(f)\circ t(x_{1})=t(x_{2})\circ F(f)\rbrace \)
と定義する。\(\mathord {\textnormal {\textsf {NatTrans}}}(F,G)\)の要素を\(F\)から\(G\)への自然変換(natural transformation)と呼ぶ。自然変換\(t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)\)が満たすべき性質(\(\forall _{x_{1},x_{2}:C}\forall _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}G(f)\circ t(x_{1})=t(x_{2})\circ F(f)\))を\(t\)自然性(naturality)と言う。