\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型とする。このとき、\(A\to B:\mathcal {U}(i)\)を\(\prod _{x:A}B\)と定義する。