[005S] 補題iiiを階数、A,B:U(i)A,B:\mathcal {U}(i)A,B:U(i)を型、f:A→Bf:A\to Bf:A→Bを関数、a:Aa:Aa:Aとc:Fiber(f,f(a))c:\mathord {\textnormal {\textsf {Fiber}}}(f,f(a))c:Fiber(f,f(a))を要素とすると、同値 (record{ ∣elem≡a,id≡refl∣ }=c)≃Fiber(ap(f){proj1(c),a},proj2(c))(\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))(record{∣elem≡a,id≡refl∣}=c)≃Fiber(ap(f){proj1(c),a},proj2(c)) を構成できる。証明[001S]を適用する。レトラクト ∑z:Fiber(f,f(a))Fiber(ap(f){proj1(c),a},proj2(c))\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))∑z:Fiber(f,f(a))Fiber(ap(f){proj1(c),a},proj2(c))◃\triangleleft ◃ {並び替え}∑x:A∑p:x=a∑q:f(x)=f(a)f(p)=q\sum _{x:A}\sum _{p:x=a}\sum _{q:f(x)=f(a)}f(p)=q∑x:A∑p:x=a∑q:f(x)=f(a)f(p)=q◃\triangleleft ◃ {[0026]}∑q:f(a)=f(a)f(refl)=q\sum _{q:f(a)=f(a)}f(\mathord {\textnormal {\textsf {refl}}})=q∑q:f(a)=f(a)f(refl)=q を得て、最後の型は[001N]より可縮である。