Another attempt at being more specific

jwiegley · Jan 30, 2024 · 9a17d8b · 9a17d8b
1 parent 48ea563
commit 9a17d8b
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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.