おそらくメイト、メイトの元になる単位

まず、メイト対応のもとになる単位の構造

• ベクトル空間の双対空間 K→V^*V
• 関数計算（インフォーマルなラムダ計算とか）の恒等射のネーム 1→[A, A]（指数）
• 関手の随伴対 η::Id⇒G*F
• 米田埋め込み id::1⇒A*A^{^}（A^{^}は対象Aの米田埋め込み）

ベクトル空間の双対と関手の随伴では余単位があり、完全なニョロニョロ構造がある。関数計算ではapply（evalだが、ベクトル空間のevとは少し違う）がほぼ余単位だが、applyは双対の余単位としては形が崩れているが、随伴として見るとちゃんと余単位になっている。

ベクトル空間、関数計算、関手の三者では、モノイド積と指数の随伴性に持ち込むと同じことになる。ベクトル空間では、指数が双対とテンソル積でかけるのが特殊事情。これは、A⊃B ≡ ¬A∨B に対応する。

米田埋め込みの場合は、余単位が見つからないが、どこかに余単位がいるような気がする。その余単位を使ってニョロニョロ関係式を書けるんじゃないかと思っているが、今のところ妄想。