ホモトピー型理論
[002L] 補題

\(i\)を階数、\(A,B,C:\mathcal {U}(i)\)を型、\(f:A\to B\)\(g:B\to C\)を型、\(c:C\)を要素とすると、\((\sum _{y:\mathord {\textnormal {\textsf {Fiber}}}(g,c)}\mathord {\textnormal {\textsf {Fiber}}}(f,y.\mathord {\textnormal {\textsf {elem}}}))\mathrel {\triangleleft \triangleright }\mathord {\textnormal {\textsf {Fiber}}}(g\circ f,c)\)の要素を構成できる。

証明

次のようにわかる。

\(\sum _{y:\mathord {\textnormal {\textsf {Fiber}}}(g,c)}\mathord {\textnormal {\textsf {Fiber}}}(f,y.\mathord {\textnormal {\textsf {elem}}})\)\(\mathrel {\triangleleft \triangleright }\) {並び換え}\(\sum _{x:A}\sum _{y:B}\sum _{p:f(x)=y}g(y)=c\)\(\mathrel {\triangleleft \triangleright }\) {[001W][0025][001N]}\(\sum _{x:A}g(f(x))=c\)