\(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))\)の要素があることである。