diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 2f42f32..7f8637a 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -31,10 +31,13 @@ open import Cubical.GradLemma        using (gradLemma)
 open import Cat.Category
 open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation
-open import Cat.Category.Monad.Monoidal as Monoidal public
-open import Cat.Category.Monad.Kleisli  as Kleisli
+import Cat.Category.Monad.Monoidal
+import Cat.Category.Monad.Kleisli
 open import Cat.Categories.Fun
 
+module Monoidal = Cat.Category.Monad.Monoidal
+module Kleisli = Cat.Category.Monad.Kleisli
+
 -- | The monoidal- and kleisli presentation of monads are equivalent.
 module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
   private
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index d64d3f7..4409039 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -16,9 +16,7 @@ open import Cubical.GradLemma        using (gradLemma)
 open import Cat.Category
 open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation
-open import Cat.Category.Monad using (Monoidal≃Kleisli)
-import Cat.Category.Monad.Monoidal as Monoidal
-import Cat.Category.Monad.Kleisli  as Kleisli
+open import Cat.Category.Monad
 open import Cat.Categories.Fun
 
 -- Utilities