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

iiを階数、A,B,C:U(i)A,B,C:\mathcal {U}(i)を型、f:ABf:A\to Bg:BCg:B\to Cを型、c:Cc:Cを要素とすると、(y:Fiber(g,c)Fiber(f,y.elem))Fiber(gf,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)の要素を構成できる。

証明

次のようにわかる。

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