\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数、\(b:B\)を要素とする。型\(\mathord {\textnormal {\textsf {Fiber}}}(f,b):\mathcal {U}(i)\)を\(\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}:A,\mathord {\textnormal {\textsf {id}}}:f(\mathord {\textnormal {\textsf {elem}}})=b\mathclose {|\negmedspace \} }\)と定義する。