関数外延性を仮定する。\(i\)を階数とする。前圏\(\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i):\mathord {\textnormal {\textsf {PreCat}}}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のように定義する。

• -\(\mathord {\textnormal {\textsf {Obj}}}\equiv \lbrace A:\mathcal {U}(i)\mid \mathord {\textnormal {\textsf {IsSet}}}(A)\rbrace \)
• -\(\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (A,B).(A\to B)\)
• -恒等射は[0010]、合成は[0011]による。
• -[0048]より、各\(\mathord {\textnormal {\textsf {Map}}}(A,B)\)は集合である。
• -他の公理は自明である。