From 6ceeb6fa22d810d21fba1ecf2afa902c2f3caa66 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 30 Jan 2024 16:38:09 -0800 Subject: [PATCH] Make some uses explicit --- Adjunction/Natural/Transformation/Universal.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v index f8364bab..47bdadf7 100644 --- a/Adjunction/Natural/Transformation/Universal.v +++ b/Adjunction/Natural/Transformation/Universal.v @@ -26,21 +26,21 @@ Next Obligation. proper; now rewrites. Qed. Next Obligation. rewrite fmap_comp. rewrite <- comp_assoc. - srewrite (naturality[unit[A]]). - rewrite comp_assoc. + rewrite (@naturality _ _ _ _ unit[A] _ _ x). + rewrite comp_assoc; simpl. srewrite (@Transformation.fmap_counit_unit); cat. Qed. Next Obligation. rewrite fmap_comp. rewrite comp_assoc. - srewrite_r (naturality[counit[A]]). - rewrite <- comp_assoc. + rewrite <- (@naturality _ _ _ _ counit[A] _ _ x). + rewrite <- comp_assoc; simpl. srewrite (@Transformation.counit_fmap_unit); cat. Qed. Next Obligation. rewrite fmap_comp. rewrite <- comp_assoc. - srewrite (naturality[unit[A]]). + rewrite (@naturality _ _ _ _ unit[A] _ _ g). now rewrite comp_assoc. Qed. Next Obligation. @@ -54,7 +54,7 @@ Qed. Next Obligation. rewrite fmap_comp. rewrite comp_assoc. - srewrite_r (naturality[counit[A]]). + rewrite <- (@naturality _ _ _ _ counit[A] _ _ f). now rewrite <- comp_assoc. Qed.