1から2を示す。定義から、関数\(\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(y,x_{1})\to \mathord {\textnormal {\textsf {Map}}}(y,x_{2})\)は両側可逆であることが分かる。よって、[004K]よりこれは同値である。

2から1を示す。\(\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})\to \mathord {\textnormal {\textsf {Map}}}(x_{2},x_{2})\)が同値なので、射\(h:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})\)と同一視\(p:f\circ h=\mathord {\textnormal {\textsf {id}}}\)を得る。関数\(\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{1})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\)が同値なので、同一視

\(f\circ h\circ f\)\(=\) {\(p\)}\(f\)\(=\) {前圏の公理}\(f\circ \mathord {\textnormal {\textsf {id}}}\) から同一視\(q:h\circ f=\mathord {\textnormal {\textsf {id}}}\)を得る。よって、\(f\)は同型である。

1と3の同値性も同様である。