[000F] 記法

• -\(\mathord {\textnormal {\textsf {El}}}\)はよく省略する。つまり、要素\(A:\mathcal {U}(i)\)そのものを型とみなす。
• -\(\mathord {\textnormal {\textsf {Lift}}}\)はよく省略する。つまり、要素\(A:\mathcal {U}(i)\)は\(\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)の要素でもあるとみなす。
• -\(\mathcal {U}(i)\)と\(\lceil \mathcal {U}\rceil (i)\)を表記上区別しない。つまり、\(\mathcal {U}(i)\)そのものを\(\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)の要素とみなす。