型は∞グルーポイドという高次元の構造を持つのであったが、その豊富な構造ゆえ型を解析するのは必ずしも容易ではない。高次元の構造を解析する常套手段はより低次元の構造で近似することである。型の\(n\)型による最良の近似を導入する。
\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。
- -\(n\)切り詰め(\(n\)-truncation)\({\| A\| }_{n}:\mathcal {U}(i)\)を構成できる。
- -\({\| A\| }_{n}\)は\(n\)型である(ことを示す要素を構成できる)。
- -要素\(a:A\)に対して、要素\({|a|}_{n}:{\| A\| }_{n}\)を構成できる。
- -\(c:{\| A\| }_{n}\)を要素、\(j\)を階数、\(B:{\| A\| }_{n}\to \mathcal {U}(j)\)を型の族、\(f:\prod _{x:A}B({|x|}_{n})\)を関数とする。\(\prod _{z:{\| A\| }_{n}}\mathord {\textnormal {\textsf {IsTrunc}}}(n,B(z))\)の要素があるなら、要素\(\mathord {\textnormal {\textsf {ind}}}_{{\| A\| }_{n}}(c,B,f):B(c)\)を構成できる。
- -\(a:A\)を要素、\(j\)を階数、\(B:{\| A\| }_{n}\to \mathcal {U}(j)\)を型の族、\(f:\prod _{x:A}B({|x|}_{n})\)を関数とする。\(\prod _{z:{\| A\| }_{n}}\mathord {\textnormal {\textsf {IsTrunc}}}(n,B(z))\)の要素があるなら、\(\mathord {\textnormal {\textsf {ind}}}_{{\| A\| }_{n}}(a,B,f)\equiv f(a)\)を定義される。
[0050]は帰納的型の規則と類似している。実際、\({\| A\| }_{n}\)を高次帰納的型([0003])の一種と捉えることもできる。\(\lambda a.{|a|}_{n}\)は構成子である。それより下の規則は帰納法原理を表すが、帰納法が使える状況は\(B\)が\(n\)型の族である場合に制限されている。
\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。次は論理的に同値である。
- 1\(A\)は\(n\)型である。
- 2関数\(\lambda x.{|x|}_{n}:A\to {\| A\| }_{n}\)は同値である。
- 3\(A\)は\({\| A\| }_{n}\)のレトラクトである。
2から3は自明である。3から1は[0045]による。
1から2を示す。\(A\)が\(n\)型なので、帰納法より関数\(g:{\| A\| }_{n}\to A\)であって任意の\(a:A\)に対して\(g({|a|}_{n})\equiv a\)となるものを構成できる。特に、\(g\circ (\lambda x.{|x|}_{n})\sim \mathord {\textnormal {\textsf {id}}}\)である。\((\lambda x.{|x|}_{n})\circ g\sim \mathord {\textnormal {\textsf {id}}}\)を示す。各\(z:{\| A\| }_{n}\)に対して\({|g(z)|}_{n}=z\)は[0052]より\(n\)型なので、帰納法により\(\prod _{x:A}{|g({|x|}_{n})|}_{n}={|x|}_{n}\)を示せばよいがこれは定義から明らかである。
\({\| A\| }_{n}\)の性質を調べる際には一価性が不可欠である。一価性をどう使うかは次の[0056]にまとめられる。
一価性と関数外延性を仮定する。\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(B:A\to \mathcal {U}(i)\)を型の族、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。任意の\(x:A\)に対して\(B(x)\)は\(n\)型であると仮定する。[0054]より、帰納法で型の族\(T:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\to \mathcal {U}(i)\)であって、任意の\(u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)に対して\(T(u)\)は\(n\)型であり、任意の\(x:A\)に対して\(T({|x|}_{\mathord {\textnormal {\textsf {succ}}}(n)})\equiv B(x)\)であるものを構成できる。[004X]と[004F]より\(\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u)\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型なので、関数\(\lambda z.\mathord {\textnormal {\textsf {pair}}}({|\mathord {\textnormal {\textsf {proj}}}_{1}(z)|}_{\mathord {\textnormal {\textsf {succ}}}(n)},\mathord {\textnormal {\textsf {proj}}}_{2}(z)):(\sum _{x:A}B(x))\to (\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u))\)は関数
\(H:{\| \sum _{x:A}B(x)\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\to (\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u))\)
を誘導する。この時、関数
\(H\)は同値である。
\(\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u)\)が\({\| \sum _{x:A}B(x)\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)と同じ帰納法原理を満たすことを見る。\(C:(\sum _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u))\to \mathcal {U}(i)\)を型の族とし、各\(C(u)\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型であると仮定する。\(f:\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {pair}}}({|z|}_{\mathord {\textnormal {\textsf {succ}}}(n)},\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\)を関数とする。\(D:\prod _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}T(u)\to \mathcal {U}(i)\)を\(C\)のカリー化、\(g:\prod _{x:A}\prod _{y:B(x)}D({|x|}_{\mathord {\textnormal {\textsf {succ}}}(n)},y)\)を\(f\)のカリー化とする。[0048]より各\(\prod _{v:T(u)}D(u,v)\)は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型なので、帰納法で関数\(h:\prod _{u:{\| A\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}}\prod _{v:T(u)}D(u,v)\)を得る。\(h\)を逆カリー化すればよい。
[0056]を使う例として、\({\| A\| }_{n}\)の同一視型の特徴付けを与える。\(n\)が\(-2\)の場合は自明なので、興味があるのはそれ以外の場合である。
一価性と関数外延性を仮定する。\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2}:A\)を要素、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とすると、同値\(({|a_{1}|}_{\mathord {\textnormal {\textsf {succ}}}(n)}={|a_{2}|}_{\mathord {\textnormal {\textsf {succ}}}(n)})\simeq {\| a_{1}=a_{2}\| }_{n}\)を構成できる。
[0056]を型の族\(\lambda x.{\| a_{1}=x\| }_{n}:A\to \mathcal {U}(i)\)に適用すると、[001S]より、\({\| \sum _{x:A}{\| a_{1}=x\| }_{n}\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)が可縮であることを示せば十分である。要素\(c_{1}:{\| \sum _{x:A}{\| a_{1}=x\| }_{n}\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)を\({|\mathord {\textnormal {\textsf {pair}}}(a_{1},{|\mathord {\textnormal {\textsf {refl}}}|}_{n})|}_{\mathord {\textnormal {\textsf {succ}}}(n)}\)と定義する。任意の\(w:{\| \sum _{x:A}{\| a_{1}=x\| }_{n}\| }_{\mathord {\textnormal {\textsf {succ}}}(n)}\)に対して同一視\(c_{1}=w\)を構成する。[0052]よりこの同一視型は\(\mathord {\textnormal {\textsf {succ}}}(n)\)型なので、帰納法より任意の\(x:A\)と\(v:{\| a_{1}=x\| }_{n}\)に対して同一視\(c_{1}={|\mathord {\textnormal {\textsf {pair}}}(x,v)|}_{\mathord {\textnormal {\textsf {succ}}}(n)}\)を構成すればよい。この同一視型は定義から\(n\)型なので、帰納法より任意の\(x:A\)と\(y:a_{1}=x\)に対して同一視\(c_{1}={|\mathord {\textnormal {\textsf {pair}}}(x,{|y|}_{n})|}_{\mathord {\textnormal {\textsf {succ}}}(n)}\)を構成すればよいが、同一視型の帰納法で\(\mathord {\textnormal {\textsf {refl}}}\)を与えればよい。