[006A] -- ホモトピー型理論

[006A] 命題

関数外延性を仮定する。 $$i$$ を階数、 $C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)$ を前圏、 $F,G:\mathord {\textnormal {\textsf {Fun}}}(C,D)$ を関手、 $t:\mathord {\textnormal {\textsf {NatTrans}}}(F,G)$ を自然変換とする。次は論理的に同値である。

1任意の $$x:C$$ に対して、 $t(x):\mathord {\textnormal {\textsf {Map}}}(F(x),G(x))$ は同型である。
2 $$t$$ は前圏 $\mathord {\textnormal {\textsf {Fun}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C,D)$ の射として同型である。

証明

2から1は自明である。

1から2を示す。各 $$x:C$$ に対して、射 $s(x),u(x):\mathord {\textnormal {\textsf {Map}}}(G(x),F(x))$ と同一視 $p(x):s(x)\circ t(x)=\mathord {\textnormal {\textsf {id}}}$ と $q(x):t(x)\circ u(x)=\mathord {\textnormal {\textsf {id}}}$ を得る。[0068]より、 $$s$$ と $$u$$ の自然性を確認すれば十分である。 $x_{1},x_{2}:C$ を対象、 $f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})$ を射とする。 $F(f)\circ s(x_{1})=s(x_{2})\circ G(f)$ を言うには、[005G]より $F(f)\circ s(x_{1})\circ t(x_{1})=s(x_{2})\circ G(f)\circ t(x_{1})$ を示せば十分で、これは次のように分かる。

F(f)\circ s(x_{1})\circ t(x_{1})

\(=\)

{

p(x_{1})

}

\(F(f)\)

\(=\)

{

{(p(x_{2}))}^{-1}

}

s(x_{2})\circ t(x_{2})\circ F(f)

\(=\)

{

\(t\)

の自然性}

s(x_{2})\circ G(f)\circ t(x_{1})

\(u\)

の自然性も同様である。