関数外延性を仮定する。\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。\(\prod _{x:A}\mathord {\textnormal {\textsf {IsTrunc}}}(n,B(x))\)の要素があるならば、\(\prod _{x:A}B(x)\)は\(n\)型である。
証明
\(n\)についての帰納法による。\(n\)が\(-2\)の場合は[0029]による。
\(n\)の場合に主張が成り立つと仮定し、\(\mathord {\textnormal {\textsf {succ}}}(n)\)の場合を示す。\(f:\prod _{x:A}B(x)\)と\(g:\prod _{x:A}B(x)\)に対し、\(f=g\)が\(n\)型であることを示す。関数外延性より、同値\((f=g)\simeq (\prod _{x:A}f(x)=g(x))\)を得る。各\(f(x)=g(x)\)は\(B\)についての仮定より\(n\)型であるから、帰納法の仮定と[0045]から\(f=g\)は\(n\)型である。