fix Categories.Monad.Strong

agda · Mar 13, 2024 · 5050aa0 · 5050aa0
1 parent e0f3c4f
commit 5050aa0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Categories/Monad/Strong.agda b/src/Categories/Monad/Strong.agda
@@ -16,7 +16,7 @@ open import Categories.Functor renaming (id to idF)
 open import Categories.Category.Monoidal
 open import Categories.Category.Product
 open import Categories.NaturalTransformation hiding (id)
-open import Categories.Monad
+open import Categories.Monad hiding (id)
 
 private
   variable
@@ -96,4 +96,4 @@ record RightStrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ
     rightStrength : RightStrength V M
 
   module M = Monad M
-  open RightStrength rightStrength public
+  open RightStrength rightStrength public