\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:\mathcal {U}(i)\)を仮定\(x:A\)の下での型とする。

• -関数型(function type)\(\prod _{x:A}B:\mathcal {U}(i)\)を構成できる。\(\prod _{x:A}B\)の要素を関数(function)と呼ぶ。
• -仮定\(x:A\)の下での要素\(b:B\)に対し、ラムダ抽象(lambda abstraction)\(\lambda x.b:\prod _{x:A}B\)を構成できる。
• -要素\(f:\prod _{x:A}B\)と\(a:A\)に対し、関数適用(function application)\(f(a):B[x\mapsto a]\)を構成できる。
• -\(b:B\)を仮定\(x:A\)の下での要素、\(a:A\)を要素とする。このとき、\((\lambda x.b)(a)\equiv b[x\mapsto a]\)と定義される。
• -要素\(f:\prod _{x:A}B\)に対し、\(f\equiv \lambda x.f(x)\)と定義される。