- -自然数型(type of natural numbers)N:U(0)を構成できる。Nの要素を自然数(natural number)と呼ぶ。
- -要素0:Nを構成できる。
- -要素n:Nに対して、要素succ(n):Nを構成できる。
- -n:Nを要素、iを階数、A:N→U(i)を型の族、a:A(0)を要素、f:∏{x:N}A(x)→A(succ(x))を関数とすると、要素indN(n,A,a,f):A(n)を構成できる。
- -iを階数、A:N→U(i)を型の族、a:A(0)を要素、f:∏{x:N}A(x)→A(succ(x))を関数とすると、indN(0,A,a,f)≡aと定義される。
- -n:Nを要素、iを階数、A:N→U(i)を型の族、a:A(0)を要素、f:∏{x:N}A(x)→A(succ(x))を関数とすると、indN(succ(n),A,a,f)≡f(indN(n,A,a,f))と定義される。