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

• -\(\_:\mathord {\textnormal {\textsf {IsEquiv}}}(F.\mathord {\textnormal {\textsf {obj}}})\)
• -\(\_:\prod _{x_{1},x_{2}:C}\mathord {\textnormal {\textsf {IsEquiv}}}(F.\mathord {\textnormal {\textsf {map}}}\lbrace x_{1},x_{2}\rbrace )\)

\(\mathord {\textnormal {\textsf {IsIso}}}(F)\)の要素がある時、\(F\)は前圏の同型(isomorphism of precategories)であると言う。