[003X] -- ホモトピー型理論

-型 $\mathord {\textnormal {\textsf {TruncLevel}}}:\mathcal {U}(0)$ を $\mathbb {N}+(\mathbf {1}+\mathbf {1})$ と定義する。
-要素 $-2:\mathord {\textnormal {\textsf {TruncLevel}}}$ を $\mathord {\textnormal {\textsf {in}}}_{2}(\mathord {\textnormal {\textsf {in}}}_{2}(\mathord {\star }))$ と定義する。
-要素 $-1:\mathord {\textnormal {\textsf {TruncLevel}}}$ を $\mathord {\textnormal {\textsf {in}}}_{2}(\mathord {\textnormal {\textsf {in}}}_{1}(\mathord {\star }))$ と定義する。
-要素 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ に対して、要素 $\mathord {\textnormal {\textsf {succ}}}(n):\mathord {\textnormal {\textsf {TruncLevel}}}$ を $\mathord {\textnormal {\textsf {succ}}}(-2)\equiv -1$ と $\mathord {\textnormal {\textsf {succ}}}(-1)\equiv \mathord {\textnormal {\textsf {in}}}_{1}(0)$ と $\mathord {\textnormal {\textsf {succ}}}(\mathord {\textnormal {\textsf {in}}}_{1}(n))\equiv \mathord {\textnormal {\textsf {in}}}_{1}(\mathord {\textnormal {\textsf {succ}}}(n))$ と定義する。

要素

n:\mathbb {N}

に対しては、

\mathord {\textnormal {\textsf {in}}}_{1}

を省略して

\(n\)

自身を

\mathord {\textnormal {\textsf {TruncLevel}}}

の要素とみなす。