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

\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。

  1. 1関手\(F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)に対して、恒等自然変換\(\mathord {\textnormal {\textsf {id}}}\lbrace F\rbrace :\mathord {\textnormal {\textsf {NatTrans}}}(F,F)\)\(\lambda x.\mathord {\textnormal {\textsf {id}}}\lbrace F(x)\rbrace \)と定義する。\(\mathord {\textnormal {\textsf {id}}}\lbrace F\rbrace \)の自然性を確認せよ。
  2. 2関手\(F_{1},F_{2},F_{3}:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)と自然変換\(t_{1}:\mathord {\textnormal {\textsf {NatTrans}}}(F_{1},F_{2})\)\(t_{2}:\mathord {\textnormal {\textsf {NatTrans}}}(F_{2},F_{3})\)に対して、合成\(t_{2}\circ t_{1}:\mathord {\textnormal {\textsf {NatTrans}}}(F_{1},F_{3})\)\(\lambda x.t_{2}(x)\circ t_{1}(x)\)と定義する。\(t_{2}\circ t_{1}\)の自然性を確認せよ。