ホモトピー型理論
[005R] 命題

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

  1. 1型\(\mathord {\textnormal {\textsf {IsTruncMap}}}(-2,f)\)と\(\mathord {\textnormal {\textsf {IsEquiv}}}(f)\)は論理的に同値である。
  2. 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 )\)