NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

lemma. (co)unit and transposes [leinster2016basic, 2.2.4] [tt-001Y]

Given an adjunction with unit \(\eta \) and counit \(\epsilon \), the diagrams \[h=\eta _X \mathbin {\bullet } \mathscr {R}(h^{\sharp })\] and \[f^{\sharp }=\mathscr {L}(f) \mathbin {\bullet } \epsilon _Y\] commute.