\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族とする。関数型\(\prod _{x:A}B(x)\)が関数外延性(function extensionality)を満たすとは、\(\prod _{f:\prod _{x:A}B(x)}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{g:\prod _{x:A}B(x)}\prod _{x:A}f(x)=g(x))\)の要素があることである。
[001Y] 関数外延性
関数\(f,g:\prod _{x:A}B(x)\)の「正しい」同一視のしかたは任意の\(x:A\)に対して\(f(x)\)と\(g(x)\)を同一視することである。つまり、同値\((f=g)\simeq (\prod _{x:A}f(x)=g(x))\)が期待される。しかし、関数\((\prod _{x:A}f(x)=g(x))\to f=g\)は関数型の規則と同一視型の規則からは構成できないことが知られている[Streicher--1993-0000]。そのため、この同値を得るためには何らかの公理が必要である。
要素\(\lambda x.\mathord {\textnormal {\textsf {refl}}}\lbrace f(x)\rbrace :\prod _{x:A}f(x)=f(x)\)があるので[001S]を適用できて、\(\prod _{x:A}B(x)\)が関数外延性を持つ時、任意の関数\(f:\prod _{x:A}B(x)\)と\(g:\prod _{x:A}B(x)\)に対して同値\((f=g)\simeq (\prod _{x:A}f(x)=g(x))\)を得る。
関数外延性公理(function extensionality axiom)はすべての関数型が関数外延性を満たすことを要請する。
証明
1から2を示す。\(c:\prod _{x:A}\mathord {\textnormal {\textsf {IsContr}}}(B(x))\)を仮定する。仮定\(c\)より、関数\(f:\prod _{x:A}B(x)\)と同一視\(p:\prod _{x:A}\prod _{y:B(x)}f(x)=y\)を得る。同一視\(q:\prod _{g:\prod _{x:A}B(x)}f=g\)を構成すればよい。任意の\(g:\prod _{x:A}B(x)\)に対して、\(\lambda x.p(x,g(x)):\prod _{x:A}f(x)=g(x)\)を得るが、関数外延性と[001S]により\(f=g\)の要素を得る。
2から1を示す。\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(f:\prod _{x:A}B(x)\)を関数とする。[001A]より、\(\sum _{g:\prod _{x:A}B(x)}\prod _{x:A}f(x)=g(x)\)は\(\prod _{x:A}\sum _{y:B(x)}f(x)=y\)のレトラクトであるが、後者は仮定と[001N]により可縮である。よって、[001K]から前者も可縮である。