[005R] 命題iiiを階数、A,B:U(i)A,B:\mathcal {U}(i)A,B:U(i)を型、f:A→Bf:A\to Bf:A→Bを関数とする。 1型IsTruncMap(−2,f)\mathord {\textnormal {\textsf {IsTruncMap}}}(-2,f)IsTruncMap(−2,f)とIsEquiv(f)\mathord {\textnormal {\textsf {IsEquiv}}}(f)IsEquiv(f)は論理的に同値である。2要素n:TruncLeveln:\mathord {\textnormal {\textsf {TruncLevel}}}n:TruncLevelに対して、次の型は論理的に同値である。 -IsTruncMap(succ(n),f)\mathord {\textnormal {\textsf {IsTruncMap}}}(\mathord {\textnormal {\textsf {succ}}}(n),f)IsTruncMap(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 )∏x1,x2:AIsTruncMap(n,ap(f){x1,x2})証明1は定義から自明である。2は次のように分かる。 IsTruncMap(succ(n),f)\mathord {\textnormal {\textsf {IsTruncMap}}}(\mathord {\textnormal {\textsf {succ}}}(n),f)IsTruncMap(succ(n),f)↔\leftrightarrow ↔ {定義}∏y:B∏z1,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})∏y:B∏z1,z2:Fiber(f,y)IsTrunc(n,z1=z2)↔\leftrightarrow ↔ {並び替え}∏x1:A∏y:B∏p1:f(x1)=y∏z2:Fiber(f,y)IsTrunc(n,record{ ∣elem≡x1,id≡p1∣ }=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})∏x1:A∏y:B∏p1:f(x1)=y∏z2:Fiber(f,y)IsTrunc(n,record{∣elem≡x1,id≡p1∣}=z2)↔\leftrightarrow ↔ {p1p_{1}p1についての帰納法}∏x1:A∏z2:Fiber(f,f(x1))IsTrunc(n,record{ ∣elem≡x1,id≡refl∣ }=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})∏x1:A∏z2:Fiber(f,f(x1))IsTrunc(n,record{∣elem≡x1,id≡refl∣}=z2)↔\leftrightarrow ↔ {[005S]}∏x1:A∏z2: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})))∏x1:A∏z2:Fiber(f,f(x1))IsTrunc(n,Fiber(ap(f),proj2(z2)))↔\leftrightarrow ↔ {並び替え}∏x2,x1:A∏p: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))∏x2,x1:A∏p:f(x2)=f(x1)IsTrunc(n,Fiber(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 )∏x2,x1:AIsTruncMap(n,ap(f){x2,x1})