\(i\)を階数とする。
- -型\(\top :\mathcal {U}(0)\)を\(\mathbf {1}\)と定義する。
- -型\(P,Q:\mathcal {U}(i)\)に対して、型\(P\land Q:\mathcal {U}(i)\)を\(P\times Q\)と定義する。
- -型\(\bot :\mathcal {U}(0)\)を\(\mathbf {0}\)と定義する。
- -型\(P,Q:\mathcal {U}(i)\)に対して、型\(P\lor Q:\mathcal {U}(i)\)を\({\| P+Q\| }_{-1}\)と定義する。
- -型\(P,Q:\mathcal {U}(i)\)に対して、型\(P\Rightarrow Q:\mathcal {U}(i)\)を\(P\to Q\)と定義する。
- -型\(P:\mathcal {U}(i)\)に対して、型\(\neg P:\mathcal {U}(i)\)を\(P\Rightarrow \bot \)と定義する。
- -型\(P,Q:\mathcal {U}(i)\)に対して、型\(P\Leftrightarrow Q:\mathcal {U}(i)\)を\((P\Rightarrow Q)\land (Q\Rightarrow P)\)と定義する。
- -型\(A:\mathcal {U}(i)\)と型の族\(P:A\to \mathcal {U}(i)\)に対して、型\(\forall _{x:A}P(x):\mathcal {U}(i)\)を\(\prod _{x:A}P(x)\)と定義する。
- -型\(A:\mathcal {U}(i)\)と型の族\(B:A\to \mathcal {U}(i)\)に対して、型\(\exists _{x:A}B(x):\mathcal {U}(i)\)を\({\| \sum _{x:A}B(x)\| }_{-1}\)と定義する。