[003W] $$n$$ 型

[002N]で型は高次グルーポイドの構造を持つと説明したが、その豊富な構造をすべて把握するのは容易ではない。 $$n$$ 次元より上の構造が自明になっているような型は $$n$$ 型と呼ばれ、比較的解析が容易である。

次数 $$n$$ は $$-2$$ から数えるのが都合がよい。

-型 $\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}}}

の要素とみなす。

$\mathord {\textnormal {\textsf {TruncLevel}}}$ は実質 $\mathbb {N}$ と同じであるが、 $$0$$ の代わりに $$-2$$ から数えたものである。特に、次の帰納法原理を満たす:型の族 $A:\mathord {\textnormal {\textsf {TruncLevel}}}\to \mathcal {U}(i)$ に対して、関数 $h:\prod _{x:\mathord {\textnormal {\textsf {TruncLevel}}}}A(x)$ を構成するためには、

- $$a:A(-2)$$
- $f:\prod _{x:\mathord {\textnormal {\textsf {TruncLevel}}}}A(x)\to A(\mathord {\textnormal {\textsf {succ}}}(x))$

を構成すれば十分である。

[003Y] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ に対して、型 $\mathord {\textnormal {\textsf {IsTrunc}}}(n,A):\mathcal {U}(i)$ を次のように定義する。

- $\mathord {\textnormal {\textsf {IsTrunc}}}(-2,A)\equiv \mathord {\textnormal {\textsf {IsContr}}}(A)$
- $\mathord {\textnormal {\textsf {IsTrunc}}}(\mathord {\textnormal {\textsf {succ}}}(n),A)\equiv \prod _{x_{1},x_{2}:A}\mathord {\textnormal {\textsf {IsTrunc}}}(n,x_{1}=x_{2})$

\mathord {\textnormal {\textsf {IsTrunc}}}(n,A)

の要素がある時、

\(A\)

は

\(n\)

型(

\(n\)

-type)である、または

\(n\)

-truncatedであると言う。

[0053] 定義

$$i$$ を階数、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。型 $\mathord {\langle n\rangle \mathord {\textnormal {\textsf {-Type}}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {Type}}}:\mathcal {U}(i),\mathord {\textnormal {\textsf {is-trunc}}}:\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {Type}}})\mathclose {|\negmedspace \} }$ と定義する。

$$-1$$ 型は特別に命題と呼ばれ、[003Z]でより詳しく調べる。 $$0$$ 型は特別に集合と呼ばれ、[004B]でより詳しく調べる。

$$n$$ 型の一般的な性質をいくつか見る。まず、 $$n$$ 型はレトラクトで閉じる([0045])。

[0046] 補題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $r:\mathord {\textnormal {\textsf {Retract}}}(A,B)$ を要素、 $a_{1},a_{2}:A$ を要素とすると、 $\mathord {\textnormal {\textsf {Retract}}}(a_{1}=a_{2},r.\mathord {\textnormal {\textsf {section}}}(a_{1})=r.\mathord {\textnormal {\textsf {section}}}(a_{2}))$ の要素を構成できる。

証明

$f\equiv r.\mathord {\textnormal {\textsf {section}}}$ と $g\equiv r.\mathord {\textnormal {\textsf {retraction}}}$ と $p\equiv r.\mathord {\textnormal {\textsf {r-s}}}$ と定義する。 $F:a_{1}=a_{2}\to f(a_{1})=f(a_{2})$ を $\mathord {\textnormal {\textsf {ap}}}(f)$ と定義する。 $G:f(a_{1})=f(a_{2})\to a_{1}=a_{2}$ を $\lambda q.(p(a_{2})\circ \mathord {\textnormal {\textsf {ap}}}(g,q))\circ {(p(a_{1}))}^{-1}$ と定義する。 $\prod _{z:a_{1}=a_{2}}G(F(z))=z$ を示すには、同一視型の帰納法により $G(F(\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace ))=\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace$ を示せばよいが、 $G(F(\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace ))\equiv p(a_{1})\circ {(p(a_{1}))}^{-1}$ なので[0047]を適用すればよい。

[0045] 命題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $r:\mathord {\textnormal {\textsf {Retract}}}(A,B)$ と $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $$B$$ が $$n$$ 型ならば、 $$A$$ も $$n$$ 型である。

証明

$$n$$ についての帰納法による。 $$n$$ が $$-2$$ の時は[001K]による。

$$n$$ について主張が成り立つと仮定し、 $\mathord {\textnormal {\textsf {succ}}}(n)$ の場合を示す。 $x_{1},x_{2}:A$ に対して、 $\mathord {\textnormal {\textsf {IsTrunc}}}(n,x_{1}=x_{2})$ を示せばよいが、[0046]と帰納法の仮定から直ちに従う。

$$n$$ 型はいくつかの型の構成で閉じる。

[0048] 命題

関数外延性を仮定する。 $$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $\prod _{x:A}\mathord {\textnormal {\textsf {IsTrunc}}}(n,B(x))$ の要素があるならば、 $\prod _{x:A}B(x)$ は $$n$$ 型である。

証明

$$n$$ についての帰納法による。 $$n$$ が $$-2$$ の場合は[0029]による。

$$n$$ の場合に主張が成り立つと仮定し、 $\mathord {\textnormal {\textsf {succ}}}(n)$ の場合を示す。 $f:\prod _{x:A}B(x)$ と $g:\prod _{x:A}B(x)$ に対し、 $$f=g$$ が $$n$$ 型であることを示す。関数外延性より、同値 $(f=g)\simeq (\prod _{x:A}f(x)=g(x))$ を得る。各 $$f(x)=g(x)$$ は $$B$$ についての仮定より $$n$$ 型であるから、帰納法の仮定と[0045]から $$f=g$$ は $$n$$ 型である。

[004X] 命題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $$A$$ が $$n$$ 型で、任意の $$x:A$$ に対して $$B(x)$$ が $$n$$ 型ならば、 $\sum _{x:A}B(x)$ も $$n$$ 型である。

証明

$$n$$ についての帰納法による。 $$n$$ が $$-2$$ の場合は容易である。

$$n$$ の場合に主張が成り立つと仮定し、 $\mathord {\textnormal {\textsf {succ}}}(n)$ の場合を示す。 $c_{1},c_{2}:\sum _{x:A}B(x)$ に対し、 $c_{1}=c_{2}$ が $$n$$ 型であることを示す。[002B]より、同値

(c_{1}=c_{2})\simeq (\sum _{z:\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})}\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2}))

を得る。仮定より、

\mathord {\textnormal {\textsf {proj}}}_{1}(c_{1})=\mathord {\textnormal {\textsf {proj}}}_{1}(c_{2})

と各

\mathord {\textnormal {\textsf {transport}}}(B,z,\mathord {\textnormal {\textsf {proj}}}_{2}(c_{1}))=\mathord {\textnormal {\textsf {proj}}}_{2}(c_{2})

は

\(n\)

型である。よって、帰納法の仮定を適用すればよい。

[004F] 命題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $$A$$ が $$n$$ 型ならば、 $$A$$ は $\mathord {\textnormal {\textsf {succ}}}(n)$ 型である。

証明

$$n$$ についての帰納法による。 $$n$$ が $$-2$$ の場合は[001L]による。

$$n$$ の場合に主張が成り立つと仮定して、 $\mathord {\textnormal {\textsf {succ}}}(n)$ の場合を示す。 $$A$$ が $\mathord {\textnormal {\textsf {succ}}}(n)$ 型と仮定して、任意の $x_{1},x_{2}:A$ に対して $x_{1}=x_{2}$ が $\mathord {\textnormal {\textsf {succ}}}(n)$ 型であることを示せばよいが、仮定と帰納法の過程から直ちに従う。

[0052] 系

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2}:A$ を要素、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $$A$$ が $$n$$ 型ならば、 $a_{1}=a_{2}$ も $$n$$ 型である。

相対的な $$n$$ 型の概念も導入する。

[005Q] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。型 $\mathord {\textnormal {\textsf {IsTruncMap}}}(n,f):\mathcal {U}(i)$ を $\prod _{y:B}\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {Fiber}}}(f,y))$ と定義する。

[005S] 補題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数、 $$a:A$$ と $c:\mathord {\textnormal {\textsf {Fiber}}}(f,f(a))$ を要素とすると、同値

(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv a,\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }=c)\simeq \mathord {\textnormal {\textsf {Fiber}}}(\mathord {\textnormal {\textsf {ap}}}(f)\lbrace \mathord {\textnormal {\textsf {proj}}}_{1}(c),a\rbrace ,\mathord {\textnormal {\textsf {proj}}}_{2}(c))

を構成できる。

証明

[001S]を適用する。レトラクト

\sum _{z:\mathord {\textnormal {\textsf {Fiber}}}(f,f(a))}\mathord {\textnormal {\textsf {Fiber}}}(\mathord {\textnormal {\textsf {ap}}}(f)\lbrace \mathord {\textnormal {\textsf {proj}}}_{1}(c),a\rbrace ,\mathord {\textnormal {\textsf {proj}}}_{2}(c))

\triangleleft

{並び替え}

\sum _{x:A}\sum _{p:x=a}\sum _{q:f(x)=f(a)}f(p)=q

\triangleleft

{[0026]}

\sum _{q:f(a)=f(a)}f(\mathord {\textnormal {\textsf {refl}}})=q

を得て、最後の型は[001N]より可縮である。

[005R] 命題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。

1型 $\mathord {\textnormal {\textsf {IsTruncMap}}}(-2,f)$ と $\mathord {\textnormal {\textsf {IsEquiv}}}(f)$ は論理的に同値である。
2要素$n:\mathord {\textnormal {\textsf {TruncLevel}}}$に対して、次の型は論理的に同値である。
- - $\mathord {\textnormal {\textsf {IsTruncMap}}}(\mathord {\textnormal {\textsf {succ}}}(n),f)$
- - $\prod _{x_{1},x_{2}:A}\mathord {\textnormal {\textsf {IsTruncMap}}}(n,\mathord {\textnormal {\textsf {ap}}}(f)\lbrace x_{1},x_{2}\rbrace )$

証明

1は定義から自明である。

2は次のように分かる。

\mathord {\textnormal {\textsf {IsTruncMap}}}(\mathord {\textnormal {\textsf {succ}}}(n),f)

\leftrightarrow

{定義}

\prod _{y:B}\prod _{z_{1},z_{2}:\mathord {\textnormal {\textsf {Fiber}}}(f,y)}\mathord {\textnormal {\textsf {IsTrunc}}}(n,z_{1}=z_{2})

\leftrightarrow

{並び替え}

\prod _{x_{1}:A}\prod _{y:B}\prod _{p_{1}:f(x_{1})=y}\prod _{z_{2}:\mathord {\textnormal {\textsf {Fiber}}}(f,y)}\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv x_{1},\mathord {\textnormal {\textsf {id}}}\equiv p_{1}\mathclose {|\negmedspace \} }=z_{2})

\leftrightarrow

{

p_{1}

についての帰納法}

\prod _{x_{1}:A}\prod _{z_{2}:\mathord {\textnormal {\textsf {Fiber}}}(f,f(x_{1}))}\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}\equiv x_{1},\mathord {\textnormal {\textsf {id}}}\equiv \mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }=z_{2})

\leftrightarrow

{[005S]}

\prod _{x_{1}:A}\prod _{z_{2}:\mathord {\textnormal {\textsf {Fiber}}}(f,f(x_{1}))}\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {Fiber}}}(\mathord {\textnormal {\textsf {ap}}}(f),\mathord {\textnormal {\textsf {proj}}}_{2}(z_{2})))

\leftrightarrow

{並び替え}

\prod _{x_{2},x_{1}:A}\prod _{p:f(x_{2})=f(x_{1})}\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {Fiber}}}(\mathord {\textnormal {\textsf {ap}}}(f),p))

\leftrightarrow

{定義}

\prod _{x_{2},x_{1}:A}\mathord {\textnormal {\textsf {IsTruncMap}}}(n,\mathord {\textnormal {\textsf {ap}}}(f)\lbrace x_{2},x_{1}\rbrace )

[003W] \(n\)型

[003W] $\(n\)$ 型