[002L] 補題iiiを階数、A,B,C:U(i)A,B,C:\mathcal {U}(i)A,B,C:U(i)を型、f:A→Bf:A\to Bf:A→Bとg:B→Cg:B\to Cg:B→Cを型、c:Cc:Cc:Cを要素とすると、(∑y:Fiber(g,c)Fiber(f,y.elem))◃▹Fiber(g∘f,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))◃▹Fiber(g∘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}}})∑y:Fiber(g,c)Fiber(f,y.elem)◃▹\mathrel {\triangleleft \triangleright }◃▹ {並び換え}∑x:A∑y:B∑p:f(x)=yg(y)=c\sum _{x:A}\sum _{y:B}\sum _{p:f(x)=y}g(y)=c∑x:A∑y:B∑p:f(x)=yg(y)=c◃▹\mathrel {\triangleleft \triangleright }◃▹ {[001W]と[0025]と[001N]}∑x:Ag(f(x))=c\sum _{x:A}g(f(x))=c∑x:Ag(f(x))=c