\(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)\)の要素を構成できる。
証明
次のようにわかる。