From 9a17d8b639ccf5968148d8d798a2986d8e21e3bb Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Tue, 30 Jan 2024 14:08:11 -0800 Subject: [PATCH] Another attempt at being more specific --- Adjunction/Natural/Transformation/Universal.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v index 998c41ee..dedf46c2 100644 --- a/Adjunction/Natural/Transformation/Universal.v +++ b/Adjunction/Natural/Transformation/Universal.v @@ -28,21 +28,21 @@ Next Obligation. proper; now rewrites. Qed. Next Obligation. rewrite fmap_comp. rewrite <- comp_assoc. - srewrite (naturality[unit[A]]). + srewrite (naturality[@Transformation.unit _ _ _ _ A]). rewrite comp_assoc. srewrite (@Transformation.fmap_counit_unit); cat. Qed. Next Obligation. rewrite fmap_comp. rewrite comp_assoc. - srewrite_r (naturality[counit[A]]). + srewrite_r (naturality[@Transformation.counit _ _ _ _ A]). rewrite <- comp_assoc. srewrite (@Transformation.counit_fmap_unit); cat. Qed. Next Obligation. rewrite fmap_comp. rewrite <- comp_assoc. - srewrite (naturality[unit[A]]). + srewrite (naturality[@Transformation.unit _ _ _ _ A]). now rewrite comp_assoc. Qed. Next Obligation. @@ -56,7 +56,7 @@ Qed. Next Obligation. rewrite fmap_comp. rewrite comp_assoc. - srewrite_r (naturality[counit[A]]). + srewrite_r (naturality[@Transformation.counit _ _ _ _ A]). now rewrite <- comp_assoc. Qed.