\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(C:\prod _{x:A}B(x)\to \mathcal {U}(i)\)を型の族、\(a:A\)と\(b:B(a)\)を要素とする。\(\sum _{x:A}B(x)\)が可縮ならば\((\sum _{x:A}\sum _{y:B(x)}C(x,y))\mathrel {\triangleleft \triangleright }C(a,b)\)の要素を構成できる。