diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
index 88a5cc5518..64ac6d7864 100644
--- a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
+++ b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
@@ -20,8 +20,8 @@ open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
-import Data.Vec.Effectful as VecCat
-import Function.Identity.Effectful as IdCat
+import Data.Vec.Effectful as Vec
+import Function.Identity.Effectful as Identity
 open import Data.Vec.Properties using (lookup-map)
 open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
   using (Pointwise; ext)
@@ -165,18 +165,18 @@ lift n = record
     }
   }
   where
-  open RawApplicative VecCat.applicative
+  open RawApplicative Vec.applicative
     using (pure; zipWith) renaming (_<$>_ to map)
 
   ⟦_⟧Id : ∀ {n} → Expr n → Vec Carrier n → Carrier
-  ⟦_⟧Id = Semantics.⟦_⟧ IdCat.applicative
+  ⟦_⟧Id = Semantics.⟦_⟧ Identity.applicative
 
   ⟦_⟧Vec : ∀ {m n} → Expr n → Vec (Vec Carrier m) n → Vec Carrier m
-  ⟦_⟧Vec = Semantics.⟦_⟧ VecCat.applicative
+  ⟦_⟧Vec = Semantics.⟦_⟧ Vec.applicative
 
   open module R {n} (i : Fin n) =
     Reflection setoid var
       (λ e ρ → Vec.lookup (⟦ e ⟧Vec ρ) i)
       (λ e ρ → ⟦ e ⟧Id (Vec.map (flip Vec.lookup i) ρ))
       (λ e ρ → sym $ reflexive $
-                 Naturality.natural (VecCat.lookup-morphism i) e ρ)
+                 Naturality.natural (Vec.lookup-morphism i) e ρ)
diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda
index 71ab8535d8..43778816c3 100644
--- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda
+++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda
@@ -130,11 +130,11 @@ _>>=_ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} {j k} →
 m >>= f = (f ⋆) m
 
 -- Note that the monad-like structure above is not an indexed monad
--- (as defined in Category.Monad.Indexed). If it were, then _>>=_
+-- (as defined in Effect.Monad.Indexed). If it were, then _>>=_
 -- would have a type similar to
 --
 --   ∀ {I} {T U : Rel I t} {i j k} →
 --   Star T i j → (T i j → Star U j k) → Star U i k.
 --                  ^^^^^
 -- Note, however, that there is no scope for applying T to any indices
--- in the definition used in Category.Monad.Indexed.
+-- in the definition used in Effect.Monad.Indexed.
diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index 0bdfe0cf2f..a4b3c1860d 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -23,8 +23,8 @@ open import Data.String.Base using (String; fromList; replicate)
 open import Function.Base using (_∘_; _∘′_; _$_)
 
 open import Effect.Monad using (RawMonad)
-import Data.List.Effectful as Cat
-open RawMonad (Cat.monad {Level.zero})
+import Data.List.Effectful as List
+open RawMonad (List.monad {Level.zero})
 
 import Data.Nat.Properties as ℕₚ
 open import Data.List.Extrema.Core ℕₚ.≤-totalOrder using (⊓ᴸ)