\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。\(\mathcal {U}(i)\)が一価性を満たし、\(f\)が同値ならば、任意の型\(X:\mathcal {U}(i)\)に対して関数\(\lambda g.f\circ g:(X\to A)\to (X\to B)\)は同値である。
証明
一価性より、\(f\)が恒等関数の場合を示せば十分であるが、\(\lambda g.\mathord {\textnormal {\textsf {id}}}\circ g\equiv \lambda g.g\)なのでこれは同値である。