ホモトピー型理論
[005S] 補題

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

(record{ ⁣elema,idrefl ⁣}=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))
を構成できる。

証明

[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))\triangleleft  {並び替え}x:Ap:x=aq:f(x)=f(a)f(p)=q\sum _{x:A}\sum _{p:x=a}\sum _{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
を得て、最後の型は[001N]より可縮である。