関数外延性を仮定する。\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。\(f\)は同値であると仮定して、次を示せ。

1. 1任意の型\(X:\mathcal {U}(i)\)に対して、関数\(\lambda g.f\circ g:(X\to A)\to (X\to B)\)は同値である。
2. 2任意の型\(Y:\mathcal {U}(i)\)に対して、関数\(\lambda h.h\circ f:(B\to Y)\to (A\to Y)\)は同値である。