\(i\)を階数、\(C_{1},C_{2},D:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏とする。型\(\mathord {\textnormal {\textsf {BiFun}}}(C_{1},C_{2};D):\mathcal {U}(i)\)を次のレコード型と定義する。
- -\(\mathord {\textnormal {\textsf {obj}}}:C_{1}.\mathord {\textnormal {\textsf {Obj}}}\to C_{2}.\mathord {\textnormal {\textsf {Obj}}}\to D.\mathord {\textnormal {\textsf {Obj}}}\)
- -\(\mathord {\textnormal {\textsf {map}}}_{1}:\prod _{\lbrace x_{11},x_{12}:C_{1}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{11},x_{12})\to (\prod _{x_{2}:C_{2}}\mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {obj}}}(x_{11},x_{2}),\mathord {\textnormal {\textsf {obj}}}(x_{12},x_{2})))\)
- -\(\mathord {\textnormal {\textsf {map}}}_{2}:\prod _{x_{1}:C_{1}}\prod _{\lbrace x_{21},x_{22}:C_{2}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{21},x_{22})\to \mathord {\textnormal {\textsf {Map}}}(\mathord {\textnormal {\textsf {obj}}}(x_{1},x_{21}),\mathord {\textnormal {\textsf {obj}}}(x_{1},x_{22}))\)
- -\(\_:\forall _{x_{1}:C_{1}}\forall _{x_{2}:C_{2}}\mathord {\textnormal {\textsf {map}}}_{1}(\mathord {\textnormal {\textsf {id}}}\lbrace x_{1}\rbrace ,x_{2})=\mathord {\textnormal {\textsf {id}}}\lbrace \mathord {\textnormal {\textsf {obj}}}(x_{1},x_{2})\rbrace \)
- -\(\_:\forall _{x_{11},x_{12},x_{13}:C_{1}}\forall _{x_{2}:C_{2}}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{11},x_{12})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{12},x_{13})}\mathord {\textnormal {\textsf {map}}}_{1}(f_{2}\circ f_{1},x_{2})=\mathord {\textnormal {\textsf {map}}}_{1}(f_{2},x_{2})\circ \mathord {\textnormal {\textsf {map}}}_{1}(f_{1},x_{2})\)
- -\(\_:\forall _{x_{1}:C_{1}}\forall _{x_{2}:C_{2}}\mathord {\textnormal {\textsf {map}}}_{2}(x_{1},\mathord {\textnormal {\textsf {id}}}\lbrace x_{2}\rbrace )=\mathord {\textnormal {\textsf {id}}}\lbrace \mathord {\textnormal {\textsf {obj}}}(x_{1},x_{2})\rbrace \)
- -\(\_:\forall _{x_{1}:C_{1}}\forall _{x_{21},x_{22},x_{23}:C_{2}}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{21},x_{22})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{22},x_{23})}\mathord {\textnormal {\textsf {map}}}_{2}(x_{1},f_{2}\circ f_{1})=\mathord {\textnormal {\textsf {map}}}_{2}(x_{1},f_{2})\circ \mathord {\textnormal {\textsf {map}}}_{2}(x_{1},f_{1})\)
- -\(\_:\forall _{x_{11},x_{12}:C_{1}}\forall _{x_{21},x_{22}:C_{2}}\forall _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{11},x_{12})}\forall _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{21},x_{22})}\mathord {\textnormal {\textsf {map}}}_{1}(f_{1},x_{22})\circ \mathord {\textnormal {\textsf {map}}}_{2}(x_{11},f_{2})=\mathord {\textnormal {\textsf {map}}}_{2}(x_{12},f_{2})\circ \mathord {\textnormal {\textsf {map}}}_{1}(f_{1},x_{21})\)