Make a use of counit more explicit

jwiegley · Jan 30, 2024 · e2d060b · e2d060b
1 parent 26eb688
commit e2d060b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.