From e2d060b252270a0c4a4679236ca98d0d852df18c Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 30 Jan 2024 12:02:31 -0800 Subject: [PATCH] Make a use of counit more explicit --- Monad/Adjunction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.