\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。型\(\mathord {\textnormal {\textsf {Psh}}}(C):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。
- -\(\mathord {\textnormal {\textsf {Carrier}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to \mathcal {U}(i)\)
- -\(\mathord {\textnormal {\textsf {act}}}:\prod _{\lbrace x_{1},x_{2}:C\rbrace }\mathord {\textnormal {\textsf {Carrier}}}(x_{2})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Carrier}}}(x_{1})\)
- -\(\_:\forall _{x:C}\mathord {\textnormal {\textsf {IsSet}}}(\mathord {\textnormal {\textsf {Carrier}}}(x))\)
- -\(\_:\forall _{x:C}\forall _{a:\mathord {\textnormal {\textsf {Carrier}}}(x)}\mathord {\textnormal {\textsf {act}}}(a,\mathord {\textnormal {\textsf {id}}})=a\)
- -\(\_:\forall _{x_{1},x_{2},x_{3}:C}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\forall _{a:\mathord {\textnormal {\textsf {Carrier}}}(x_{3})}\mathord {\textnormal {\textsf {act}}}(a,f_{2}\circ f_{1})=\mathord {\textnormal {\textsf {act}}}(\mathord {\textnormal {\textsf {act}}}(a,f_{2}),f_{1})\)