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

関数外延性を仮定する。\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(x:C\)を対象、\(A:\mathord {\textnormal {\textsf {Psh}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(C)\)を前層とする。関数

\(\lambda h.h(\mathord {\textnormal {\textsf {gen}}}(x)):\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x),A)\to A(x)\)
は同値である。

証明

射\(h:\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {よ}}}(C)(x),A)\)と対象\(y:C\)と要素\(f:\mathord {\textnormal {\textsf {よ}}}(C)(x)(y)\)に対して、同一視

\(h(f)\)\(=\) {前圏の公理}\(h(\mathord {\textnormal {\textsf {gen}}}(x)\cdot f)\)\(=\) {前層の公理}\(h(\mathord {\textnormal {\textsf {gen}}}(x))\cdot f\)
を得るので、\(h\)は\(\mathord {\textnormal {\textsf {gen}}}(x)\)における値のみで決まる。つまり、任意の要素\(a:A(x)\)に対して、\(\mathord {\textnormal {\textsf {Fiber}}}(\lambda h.h(\mathord {\textnormal {\textsf {gen}}}(x)),a)\)は命題であることが分かる。この型が要素を持つことを確認するには、\(\lambda (y,f).a\cdot f:\prod _{y:C}\mathord {\textnormal {\textsf {よ}}}(C)(x)(y)\to A(y)\)が前層の射であることを確かめればよいが、それは前層の公理から容易である。