\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(A:\mathord {\textnormal {\textsf {Psh}}}(C)\)を前層とする。型\(\mathord {\textnormal {\textsf {IsRepr}}}(A):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(\mathord {\textnormal {\textsf {obj}}}:C\)
• -\(\mathord {\textnormal {\textsf {elem}}}:A(\mathord {\textnormal {\textsf {obj}}})\)
• -\(\_:\forall _{x:C}\mathord {\textnormal {\textsf {IsEquiv}}}(\lambda (f:\mathord {\textnormal {\textsf {Map}}}(x,\mathord {\textnormal {\textsf {obj}}})).\mathord {\textnormal {\textsf {elem}}}\cdot f)\)

\(\mathord {\textnormal {\textsf {IsRepr}}}(A)\)の要素がある時、\(A\)は表現可能(representable)であると言う。また、\(\mathord {\textnormal {\textsf {IsRepr}}}(A)\)の要素のことを\(A\)の普遍要素(universal element)と呼ぶ。