[0030] 規則

• -空型(empty type)\(\mathbf {0}:\mathcal {U}(0)\)を構成できる。
• -\(c:\mathbf {0}\)を要素、\(i\)を階数、\(A:\mathbf {0}\to \mathcal {U}(i)\)を型の族とすると、要素\(\mathord {\textnormal {\textsf {ind}}}_{\mathbf {0}}(c,A):A(c)\)を構成できる。