\(i\)を階数、\(C,D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(F:\mathord {\textnormal {\textsf {Fun}}}(C,D)\)を関手、\(y:D\)を対象とする。型\(\mathord {\textnormal {\textsf {Fiber}}}^{\cong }(F,y):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(\mathord {\textnormal {\textsf {obj}}}:C\)
• -\(\mathord {\textnormal {\textsf {iso}}}:F(\mathord {\textnormal {\textsf {obj}}})\cong y\)