diff --git a/Monad/Adjunction.v b/Monad/Adjunction.v index f4613cfd..d8b4703a 100644 --- a/Monad/Adjunction.v +++ b/Monad/Adjunction.v @@ -75,7 +75,7 @@ Proof. - simpl. srewrite (@fmap_counit_unit); cat. - rewrite <- !fmap_comp. - srewrite (naturality[counit]); cat. + now srewrite (naturality[counit[X]]). Qed. End AdjunctionMonad.