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

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

\((\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]を適用する。レトラクト

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