[000K] 規則-単位型(unit type)\(\mathbf {1}:\mathcal {U}(0)\)を構成できる。-要素\(\mathord {\star }:\mathbf {1}\)を構成できる。-要素\(a:\mathbf {1}\)に対し、\(a\equiv \mathord {\star }\)と定義される。