[002V] 規則

• -自然数型(type of natural numbers)\(\mathbb {N}:\mathcal {U}(0)\)を構成できる。\(\mathbb {N}\)の要素を自然数(natural number)と呼ぶ。
• -要素\(0:\mathbb {N}\)を構成できる。
• -要素\(n:\mathbb {N}\)に対して、要素\(\mathord {\textnormal {\textsf {succ}}}(n):\mathbb {N}\)を構成できる。
• -\(n:\mathbb {N}\)を要素、\(i\)を階数、\(A:\mathbb {N}\to \mathcal {U}(i)\)を型の族、\(a:A(0)\)を要素、\(f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))\)を関数とすると、要素\(\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(n,A,a,f):A(n)\)を構成できる。
• -\(i\)を階数、\(A:\mathbb {N}\to \mathcal {U}(i)\)を型の族、\(a:A(0)\)を要素、\(f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))\)を関数とすると、\(\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(0,A,a,f)\equiv a\)と定義される。
• -\(n:\mathbb {N}\)を要素、\(i\)を階数、\(A:\mathbb {N}\to \mathcal {U}(i)\)を型の族、\(a:A(0)\)を要素、\(f:\prod _{\lbrace x:\mathbb {N}\rbrace }A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))\)を関数とすると、\(\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(\mathord {\textnormal {\textsf {succ}}}(n),A,a,f)\equiv f(\mathord {\textnormal {\textsf {ind}}}_{\mathbb {N}}(n,A,a,f))\)と定義される。