\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型とする。型\(A\times B:\mathcal {U}(i)\)を\(\sum _{x:A}B\)と定義する。