ホモトピー型理論
[002V] 規則

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