\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数とする。型\(\mathord {\textnormal {\textsf {IsHAE}}}(f):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(\mathord {\textnormal {\textsf {inv}}}:B\to A\)
• -\(\mathord {\textnormal {\textsf {unit}}}:\mathord {\textnormal {\textsf {inv}}}\circ f\sim \mathord {\textnormal {\textsf {id}}}\)
• -\(\mathord {\textnormal {\textsf {counit}}}:f\circ \mathord {\textnormal {\textsf {inv}}}\sim \mathord {\textnormal {\textsf {id}}}\)
• -\(\mathord {\textnormal {\textsf {coh}}}:\prod _{x:A}f(\mathord {\textnormal {\textsf {unit}}}(x))=\mathord {\textnormal {\textsf {counit}}}(f(x))\)

\(\mathord {\textnormal {\textsf {IsHAE}}}(f)\)の要素がある時、\(f\)は半随伴同値(half adjoint equivalence)であると言う。