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

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

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

証明

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

2は次のように分かる。

IsTruncMap(succ(n),f)\mathord {\textnormal {\textsf {IsTruncMap}}}(\mathord {\textnormal {\textsf {succ}}}(n),f)\leftrightarrow  {定義}y:Bz1,z2:Fiber(f,y)IsTrunc(n,z1=z2)\prod _{y:B}\prod _{z_{1},z_{2}:\mathord {\textnormal {\textsf {Fiber}}}(f,y)}\mathord {\textnormal {\textsf {IsTrunc}}}(n,z_{1}=z_{2})\leftrightarrow  {並び替え}x1:Ay:Bp1:f(x1)=yz2:Fiber(f,y)IsTrunc(n,record{ ⁣elemx1,idp1 ⁣}=z2)\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  {p1p_{1}についての帰納法}x1:Az2:Fiber(f,f(x1))IsTrunc(n,record{ ⁣elemx1,idrefl ⁣}=z2)\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]}x1:Az2:Fiber(f,f(x1))IsTrunc(n,Fiber(ap(f),proj2(z2)))\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  {並び替え}x2,x1:Ap:f(x2)=f(x1)IsTrunc(n,Fiber(ap(f),p))\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  {定義}x2,x1:AIsTruncMap(n,ap(f){x2,x1})\prod _{x_{2},x_{1}:A}\mathord {\textnormal {\textsf {IsTruncMap}}}(n,\mathord {\textnormal {\textsf {ap}}}(f)\lbrace x_{2},x_{1}\rbrace )