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

• -\(\mathord {\textnormal {\textsf {obj}}}:C.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}\)
• -\(\mathord {\textnormal {\textsf {map}}}:\prod _{\lbrace x_{1},x_{2}:C.\mathord {\textnormal {\textsf {Obj}}}\rbrace }C.\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to D.\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {obj}}}(x_{1}),\mathord {\textnormal {\textsf {obj}}}(x_{2}))\)
• -\(\_:\prod _{x:C.\mathord {\textnormal {\textsf {Obj}}}}\mathord {\textnormal {\textsf {map}}}(C.\mathord {\textnormal {\textsf {id}}}(x))=D.\mathord {\textnormal {\textsf {id}}}(\mathord {\textnormal {\textsf {obj}}}(x))\)
• -\(\_:\prod _{x_{1},x_{2},x_{3}:C.\mathord {\textnormal {\textsf {Obj}}}}\prod _{f_{1}:C.\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\prod _{f_{2}:C.\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\mathord {\textnormal {\textsf {map}}}(C.\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1}))=D.\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {map}}}(f_{2}),\mathord {\textnormal {\textsf {map}}}(f_{1}))\)

\(\mathord {\textnormal {\textsf {Fun}}}(C,D)\)の要素を\(C\)から\(D\)への関手(functor)と呼ぶ。