Another attempt at fixing the counit problem for coq:dev

jwiegley · jwiegley · commit a67a044ff425 · 2024-01-30T13:37:02.000-08:00
diff --git a/Monad/Adjunction.v b/Monad/Adjunction.v
@@ -75,7 +75,9 @@ Proof.
   - simpl.
     srewrite (@fmap_counit_unit); cat.
   - rewrite <- !fmap_comp.
-    now srewrite (naturality[counit[X]]).
+    apply fmap_respects.
+    symmetry.
+    apply (naturality[counit]).
 Qed.
 
 End AdjunctionMonad.
