diff --git a/CHANGELOG.md b/CHANGELOG.md
index fc02021e8c..e2c2753c43 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -58,6 +58,17 @@ Non-backwards compatible changes
   `Codata` which used sized types have been moved inside a new folder named
   `Sized`, e.g. `Codata.Stream` has become `Codata.Sized.Stream`.
 
+#### Moved `Category` modules to `Effect`
+
+* As observed by Wen Kokke in Issue #1636, it no longer really makes sense
+  to group the modules which correspond to the variety of concepts of 
+  (effectful) type constructor arising in functional programming (esp. in haskell) 
+  such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, as this
+  obstructs the importing of the `agda-categories` development into the Standard Library,
+  and moreover needlessly restricts the applicability of categorical concepts to this
+  (highly specific) mode of use. Correspondingly, modules grouped under `*.Categorical.*`
+  which exploited these structures for effectful programming have been renamed `*.Effectful`.  
+
 ### Improvements to pretty printing and regexes
 
 * In `Text.Pretty`, `Doc` is now a record rather than a type alias. This
diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index f14ced6e38..04da69aa0f 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -117,7 +117,7 @@ sizedTypesModules = map modToFile
   , "Codata.Sized.Cofin.Literals"
   , "Codata.Sized.Colist"
   , "Codata.Sized.Colist.Bisimilarity"
-  , "Codata.Sized.Colist.Categorical"
+  , "Codata.Sized.Colist.Effectful"
   , "Codata.Sized.Colist.Properties"
   , "Codata.Sized.Conat"
   , "Codata.Sized.Conat.Bisimilarity"
@@ -125,21 +125,21 @@ sizedTypesModules = map modToFile
   , "Codata.Sized.Conat.Properties"
   , "Codata.Sized.Covec"
   , "Codata.Sized.Covec.Bisimilarity"
-  , "Codata.Sized.Covec.Categorical"
+  , "Codata.Sized.Covec.Effectful"
   , "Codata.Sized.Covec.Instances"
   , "Codata.Sized.Covec.Properties"
   , "Codata.Sized.Cowriter"
   , "Codata.Sized.Cowriter.Bisimilarity"
   , "Codata.Sized.Delay"
   , "Codata.Sized.Delay.Bisimilarity"
-  , "Codata.Sized.Delay.Categorical"
+  , "Codata.Sized.Delay.Effectful"
   , "Codata.Sized.Delay.Properties"
   , "Codata.Sized.M"
   , "Codata.Sized.M.Bisimilarity"
   , "Codata.Sized.M.Properties"
   , "Codata.Sized.Stream"
   , "Codata.Sized.Stream.Bisimilarity"
-  , "Codata.Sized.Stream.Categorical"
+  , "Codata.Sized.Stream.Effectful"
   , "Codata.Sized.Stream.Instances"
   , "Codata.Sized.Stream.Properties"
   , "Codata.Sized.Thunk"
diff --git a/README.agda b/README.agda
index 4b1825f61c..2d87cb56d2 100644
--- a/README.agda
+++ b/README.agda
@@ -64,10 +64,6 @@ module README where
 
 import README.Axiom
 
--- • Category
---     Category theory-inspired idioms used to structure functional
---     programs (functors and monads, for instance).
-
 -- • Codata
 --     Coinductive data types and properties. There are two different
 --     approaches taken. The `Codata.Sized` folder contains the new more
@@ -77,6 +73,10 @@ import README.Axiom
 -- • Data
 --     Data types and properties.
 
+-- • Effect
+--     Category theory-inspired idioms used to structure functional
+--     programs (functors and monads, for instance).
+
 import README.Data
 
 -- • Function
@@ -162,9 +162,9 @@ import Codata.Sized.Colist -- Colists.
 
 -- • Some types used to structure computations
 
-import Category.Functor      -- Functors.
-import Category.Applicative  -- Applicative functors.
-import Category.Monad        -- Monads.
+import Effect.Functor      -- Functors.
+import Effect.Applicative  -- Applicative functors.
+import Effect.Monad        -- Monads.
 
 -- • Equality
 
diff --git a/README/Data.agda b/README/Data.agda
index 0195dd430b..be35a5bfc4 100644
--- a/README/Data.agda
+++ b/README/Data.agda
@@ -157,13 +157,13 @@ import Data.Vec.Relation.Unary.All
 import Data.Maybe.Relation.Unary.All
 
 
--- 6. A `Categorical` module/folder that contains categorical
+-- 6. An `Effectful` module/folder that contains effectful
 -- interpretations of the datatype.
 
-import Data.List.Categorical
-import Data.Maybe.Categorical
-import Data.Sum.Categorical.Left
-import Data.Sum.Categorical.Right
+import Data.List.Effectful
+import Data.Maybe.Effectful
+import Data.Sum.Effectful.Left
+import Data.Sum.Effectful.Right
 
 
 -- 7. A `Function` folder that contains lifting of various types of
diff --git a/README/Data/Container/FreeMonad.agda b/README/Data/Container/FreeMonad.agda
index c5df6515c8..d131fbb373 100644
--- a/README/Data/Container/FreeMonad.agda
+++ b/README/Data/Container/FreeMonad.agda
@@ -9,7 +9,7 @@
 
 module README.Data.Container.FreeMonad where
 
-open import Category.Monad
+open import Effect.Monad
 open import Data.Empty
 open import Data.Unit
 open import Data.Bool.Base using (Bool; true)
diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
index faa2b05983..333e6f0964 100644
--- a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
+++ b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
@@ -14,15 +14,15 @@ module Algebra.Lattice.Properties.BooleanAlgebra.Expression
 
 open BooleanAlgebra B
 
-open import Category.Applicative
-import Category.Applicative.Indexed as Applicative
-open import Category.Monad
+open import Effect.Applicative
+import Effect.Applicative.Indexed as Applicative
+open import Effect.Monad
 open import Data.Fin.Base using (Fin)
 open import Data.Nat.Base
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
-import Data.Vec.Categorical as VecCat
-import Function.Identity.Categorical as IdCat
+import Data.Vec.Effectful as VecCat
+import Function.Identity.Effectful as IdCat
 open import Data.Vec.Properties using (lookup-map)
 open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
   using (Pointwise; ext)
diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
index 33fc3978ec..662c405dff 100644
--- a/src/Codata/Musical/Colist.agda
+++ b/src/Codata/Musical/Colist.agda
@@ -9,7 +9,7 @@
 module Codata.Musical.Colist where
 
 open import Level using (Level)
-open import Category.Monad
+open import Effect.Monad
 open import Codata.Musical.Notation
 open import Codata.Musical.Conat using (Coℕ; zero; suc)
 import Codata.Musical.Colist.Properties
diff --git a/src/Codata/Sized/Colist/Categorical.agda b/src/Codata/Sized/Colist/Effectful.agda
similarity index 79%
rename from src/Codata/Sized/Colist/Categorical.agda
rename to src/Codata/Sized/Colist/Effectful.agda
index 642c20d115..16191ef206 100644
--- a/src/Codata/Sized/Colist/Categorical.agda
+++ b/src/Codata/Sized/Colist/Effectful.agda
@@ -1,17 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Colist
+-- An effectful view of Colist
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Colist.Categorical where
+module Codata.Sized.Colist.Effectful where
 
 open import Codata.Sized.Conat using (infinity)
 open import Codata.Sized.Colist
-open import Category.Functor
-open import Category.Applicative
+open import Effect.Functor
+open import Effect.Applicative
 
 functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Colist A i)
 functor = record { _<$>_ = map }
diff --git a/src/Codata/Sized/Covec/Categorical.agda b/src/Codata/Sized/Covec/Effectful.agda
similarity index 79%
rename from src/Codata/Sized/Covec/Categorical.agda
rename to src/Codata/Sized/Covec/Effectful.agda
index 0ce8d85a22..d81ba9567b 100644
--- a/src/Codata/Sized/Covec/Categorical.agda
+++ b/src/Codata/Sized/Covec/Effectful.agda
@@ -1,18 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Covec
+-- An effectful view of Covec
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Covec.Categorical where
+module Codata.Sized.Covec.Effectful where
 
 open import Codata.Sized.Conat
 open import Codata.Sized.Covec
-
-open import Category.Functor
-open import Category.Applicative
+open import Effect.Functor
+open import Effect.Applicative
 
 functor : ∀ {ℓ i n} → RawFunctor {ℓ} (λ A → Covec A n i)
 functor = record { _<$>_ = map }
diff --git a/src/Codata/Sized/Covec/Instances.agda b/src/Codata/Sized/Covec/Instances.agda
index dbb5728de3..125debf78b 100644
--- a/src/Codata/Sized/Covec/Instances.agda
+++ b/src/Codata/Sized/Covec/Instances.agda
@@ -8,7 +8,7 @@
 
 module Codata.Sized.Covec.Instances where
 
-open import Codata.Sized.Covec.Categorical
+open import Codata.Sized.Covec.Effectful
 
 instance
   covecFunctor = functor
diff --git a/src/Codata/Sized/Delay/Categorical.agda b/src/Codata/Sized/Delay/Effectful.agda
similarity index 90%
rename from src/Codata/Sized/Delay/Categorical.agda
rename to src/Codata/Sized/Delay/Effectful.agda
index a71d6b7cf6..36a755b1b1 100644
--- a/src/Codata/Sized/Delay/Categorical.agda
+++ b/src/Codata/Sized/Delay/Effectful.agda
@@ -1,18 +1,18 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Delay
+-- An effectful view of Delay
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Delay.Categorical where
+module Codata.Sized.Delay.Effectful where
 
 open import Codata.Sized.Delay
 open import Function
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Data.These using (leftMost)
 
 functor : ∀ {i ℓ} → RawFunctor {ℓ} (λ A → Delay A i)
diff --git a/src/Codata/Sized/Stream/Categorical.agda b/src/Codata/Sized/Stream/Effectful.agda
similarity index 80%
rename from src/Codata/Sized/Stream/Categorical.agda
rename to src/Codata/Sized/Stream/Effectful.agda
index 71c089e7e5..388e09f31f 100644
--- a/src/Codata/Sized/Stream/Categorical.agda
+++ b/src/Codata/Sized/Stream/Effectful.agda
@@ -1,19 +1,19 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Stream
+-- An effectful view of Stream
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Sized.Stream.Categorical where
+module Codata.Sized.Stream.Effectful where
 
 open import Data.Product using (<_,_>)
 open import Codata.Sized.Stream
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Comonad
 open import Function.Base
-open import Category.Functor
-open import Category.Applicative
-open import Category.Comonad
 
 functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Stream A i)
 functor = record { _<$>_ = λ f → map f }
diff --git a/src/Codata/Sized/Stream/Instances.agda b/src/Codata/Sized/Stream/Instances.agda
index 7bdefdbf14..4581901c03 100644
--- a/src/Codata/Sized/Stream/Instances.agda
+++ b/src/Codata/Sized/Stream/Instances.agda
@@ -8,7 +8,7 @@
 
 module Codata.Sized.Stream.Instances where
 
-open import Codata.Sized.Stream.Categorical
+open import Codata.Sized.Stream.Effectful
 
 instance
   streamFunctor = functor
diff --git a/src/Data/Container/FreeMonad.agda b/src/Data/Container/FreeMonad.agda
index 630ac8cb26..4150ee082f 100644
--- a/src/Data/Container/FreeMonad.agda
+++ b/src/Data/Container/FreeMonad.agda
@@ -14,7 +14,7 @@ open import Data.Product
 open import Data.Container
 open import Data.Container.Combinator using (const; _⊎_)
 open import Data.W using (sup)
-open import Category.Monad
+open import Effect.Monad
 
 infixl 1 _⋆C_
 infix  1 _⋆_
diff --git a/src/Data/Container/Indexed/FreeMonad.agda b/src/Data/Container/Indexed/FreeMonad.agda
index dd5d993e61..e9f7bb28d6 100644
--- a/src/Data/Container/Indexed/FreeMonad.agda
+++ b/src/Data/Container/Indexed/FreeMonad.agda
@@ -10,7 +10,7 @@ module Data.Container.Indexed.FreeMonad where
 
 open import Level
 open import Function hiding (const)
-open import Category.Monad.Predicate
+open import Effect.Monad.Predicate
 open import Data.Container.Indexed
 open import Data.Container.Indexed.Combinator hiding (id; _∘_)
 open import Data.Empty
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index dd531dfe88..02f290fa65 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -11,8 +11,8 @@ module Data.Fin.Properties where
 
 open import Axiom.Extensionality.Propositional
 open import Algebra.Definitions using (Involutive)
-open import Category.Applicative using (RawApplicative)
-open import Category.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Functor using (RawFunctor)
 open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
@@ -938,7 +938,7 @@ pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
   punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
 
 ------------------------------------------------------------------------
--- Categorical
+-- Effectful
 ------------------------------------------------------------------------
 
 module _ {f} {F : Set f → Set f} (RA : RawApplicative F) where
diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda
index d99c55625c..05fd00a4cc 100644
--- a/src/Data/Fin/Substitution/Lemmas.agda
+++ b/src/Data/Fin/Substitution/Lemmas.agda
@@ -8,7 +8,7 @@
 
 module Data.Fin.Substitution.Lemmas where
 
-import Category.Applicative.Indexed as Applicative
+import Effect.Applicative.Indexed as Applicative
 open import Data.Fin.Substitution
 open import Data.Nat hiding (_⊔_; _/_)
 open import Data.Fin.Base using (Fin; zero; suc; lift)
diff --git a/src/Data/List/Categorical.agda b/src/Data/List/Effectful.agda
similarity index 98%
rename from src/Data/List/Categorical.agda
rename to src/Data/List/Effectful.agda
index 3962c9998a..c172b06a12 100644
--- a/src/Data/List/Categorical.agda
+++ b/src/Data/List/Effectful.agda
@@ -1,19 +1,19 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of List
+-- An effectful view of List
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.Categorical where
+module Data.List.Effectful where
 
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
 open import Data.Bool.Base using (false; true)
 open import Data.List.Base
 open import Data.List.Properties
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Function
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; refl)
diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index 1012f6f0ee..fddf0ffc6a 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -9,7 +9,7 @@
 module Data.List.Instances where
 
 open import Data.List.Base
-open import Data.List.Categorical
+open import Data.List.Effectful
 open import Data.List.Properties
   using (≡-dec)
 open import Data.List.Relation.Binary.Pointwise
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 2c8deb9f6c..133dc30b6d 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -9,7 +9,7 @@
 module Data.List.Membership.Propositional.Properties where
 
 open import Algebra using (Op₂; Selective)
-open import Category.Monad using (RawMonad)
+open import Effect.Monad using (RawMonad)
 open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List
@@ -19,7 +19,7 @@ open import Data.List.Membership.Propositional
 import Data.List.Membership.Setoid.Properties as Membershipₛ
 open import Data.List.Relation.Binary.Equality.Propositional
   using (_≋_; ≡⇒≋; ≋⇒≡)
-open import Data.List.Categorical using (monad)
+open import Data.List.Effectful using (monad)
 open import Data.Nat.Base using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤ᵇ_)
 open import Data.Nat.Properties
 open import Data.Product hiding (map)
diff --git a/src/Data/List/NonEmpty.agda b/src/Data/List/NonEmpty.agda
index 1bb7d59ab2..039f491288 100644
--- a/src/Data/List/NonEmpty.agda
+++ b/src/Data/List/NonEmpty.agda
@@ -9,7 +9,7 @@
 module Data.List.NonEmpty where
 
 open import Level using (Level)
-open import Category.Monad
+open import Effect.Monad
 open import Data.Bool.Base using (Bool; false; true; not; T)
 open import Data.Bool.Properties
 open import Data.List.Base as List using (List; []; _∷_)
diff --git a/src/Data/List/NonEmpty/Categorical.agda b/src/Data/List/NonEmpty/Effectful.agda
similarity index 91%
rename from src/Data/List/NonEmpty/Categorical.agda
rename to src/Data/List/NonEmpty/Effectful.agda
index 4a4d646da7..34edcfb0cd 100644
--- a/src/Data/List/NonEmpty/Categorical.agda
+++ b/src/Data/List/NonEmpty/Effectful.agda
@@ -1,21 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of List⁺
+-- An effectful view of List⁺
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.NonEmpty.Categorical where
+module Data.List.NonEmpty.Effectful where
 
 open import Agda.Builtin.List
-import Data.List.Categorical as List
+import Data.List.Effectful as List
 open import Data.List.NonEmpty
 open import Data.Product using (uncurry)
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-open import Category.Comonad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
+open import Effect.Comonad
 open import Function
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/NonEmpty/Instances.agda b/src/Data/List/NonEmpty/Instances.agda
index 1cadbd2553..75fcd44c4b 100644
--- a/src/Data/List/NonEmpty/Instances.agda
+++ b/src/Data/List/NonEmpty/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.List.NonEmpty.Instances where
 
-open import Data.List.NonEmpty.Categorical
+open import Data.List.NonEmpty.Effectful
 
 instance
   nonEmptyListFunctor = functor
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index 4d8ecd3e37..e961fc402b 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -8,18 +8,17 @@
 
 module Data.List.NonEmpty.Properties where
 
-open import Category.Monad
+open import Effect.Monad
 open import Data.Nat
 open import Data.Nat.Properties
 open import Data.Maybe.Properties using (just-injective)
 open import Data.Bool using (Bool; true; false)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
-open import Data.List.Categorical using () renaming (monad to listMonad)
-open import Data.List.NonEmpty.Categorical using () renaming (monad to list⁺Monad)
+open import Data.List.Effectful using () renaming (monad to listMonad)
+open import Data.List.NonEmpty.Effectful using () renaming (monad to list⁺Monad)
 open import Data.List.NonEmpty
 open import Data.List.NonEmpty.Relation.Unary.All
 open import Data.List.Relation.Unary.All using ([]; _∷_) renaming (All to ListAll)
-import Data.List.Relation.Unary.All using (All; []; _∷_)
 import Data.List.Properties as List
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Sum.Relation.Unary.All using (inj₁; inj₂)
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index fe39ec873a..82dc9e9930 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -10,11 +10,11 @@ module Data.List.Relation.Binary.BagAndSetEquality where
 
 open import Algebra using (Idempotent; CommutativeMonoid)
 open import Algebra.Structures.Biased using (isCommutativeMonoidˡ)
-open import Category.Monad using (RawMonad)
+open import Effect.Monad using (RawMonad)
 open import Data.Empty
 open import Data.Fin.Base
 open import Data.List.Base
-open import Data.List.Categorical using (monad; module MonadProperties)
+open import Data.List.Effectful using (monad; module MonadProperties)
 import Data.List.Properties as LP
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.Any.Properties hiding (++-comm)
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 1adf66c63d..0b6850f370 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -11,13 +11,12 @@ open import Relation.Binary hiding (Decidable)
 module Data.List.Relation.Binary.Subset.Propositional.Properties
   where
 
-open import Category.Monad
 open import Data.Bool.Base using (Bool; true; false; T)
 open import Data.List.Base
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All)
 import Data.List.Relation.Unary.Any.Properties as Any hiding (filter⁺)
-open import Data.List.Categorical
+open import Data.List.Effectful
 open import Data.List.Relation.Unary.Any using (Any)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
@@ -28,6 +27,7 @@ import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permuta
 open import Data.Nat using (ℕ; _≤_)
 import Data.Product as Prod
 import Data.Sum.Base as Sum
+open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; _$_)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (_↔_; module Inverse)
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index d6722ad04b..577b6a4b52 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -8,8 +8,8 @@
 
 module Data.List.Relation.Unary.All where
 
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Applicative
+open import Effect.Monad
 open import Data.Empty using (⊥)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index c9a55f72c6..8e05fc6492 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -8,14 +8,13 @@
 
 module Data.List.Relation.Unary.Any.Properties where
 
-open import Category.Monad
 open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Bool.Properties using (T-∨; T-≡)
 open import Data.Empty using (⊥)
-open import Data.Fin.Base using (Fin) renaming (zero to fzero; suc to fsuc)
+open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List
 open import Data.List.Properties using (ʳ++-defn)
-open import Data.List.Categorical using (monad)
+open import Data.List.Effectful using (monad)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties.Core
@@ -34,6 +33,7 @@ open import Data.Product.Function.NonDependent.Propositional
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
+open import Effect.Monad
 open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
@@ -512,12 +512,12 @@ module _ {P : A → Set p} where
 -- tabulate
 
 tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f)
-tabulate⁺ fzero    p = here p
-tabulate⁺ (fsuc i) p = there (tabulate⁺ i p)
+tabulate⁺ zero    p = here p
+tabulate⁺ (suc i) p = there (tabulate⁺ i p)
 
 tabulate⁻ : ∀ {n} {f : Fin n → A} → Any P (tabulate f) → ∃ λ i → P (f i)
-tabulate⁻ {n = suc n} (here p)   = fzero , p
-tabulate⁻ {n = suc n} (there p) = Prod.map fsuc id (tabulate⁻ p)
+tabulate⁻ {n = suc _} (here p)  = zero , p
+tabulate⁻ {n = suc _} (there p) = Prod.map suc id (tabulate⁻ p)
 
 ------------------------------------------------------------------------
 -- filter
diff --git a/src/Data/Maybe/Categorical.agda b/src/Data/Maybe/Effectful.agda
similarity index 91%
rename from src/Data/Maybe/Categorical.agda
rename to src/Data/Maybe/Effectful.agda
index 37e72132d2..a96ba580e0 100644
--- a/src/Data/Maybe/Categorical.agda
+++ b/src/Data/Maybe/Effectful.agda
@@ -1,19 +1,19 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Maybe
+-- An effectful view of Maybe
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.Maybe.Categorical where
+module Data.Maybe.Effectful where
 
 open import Level
 open import Data.Maybe.Base
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-import Function.Identity.Categorical as Id
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
+import Function.Identity.Effectful as Id
 open import Function
 
 private
diff --git a/src/Data/Maybe/Instances.agda b/src/Data/Maybe/Instances.agda
index 76b9712a6d..d3efe8fb90 100644
--- a/src/Data/Maybe/Instances.agda
+++ b/src/Data/Maybe/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.Maybe.Instances where
 
-open import Data.Maybe.Categorical
+open import Data.Maybe.Effectful
 
 instance
   maybeFunctor = functor
diff --git a/src/Data/Maybe/Relation/Unary/All.agda b/src/Data/Maybe/Relation/Unary/All.agda
index a65337e05b..9b882d8f5a 100644
--- a/src/Data/Maybe/Relation/Unary/All.agda
+++ b/src/Data/Maybe/Relation/Unary/All.agda
@@ -8,8 +8,8 @@
 
 module Data.Maybe.Relation.Unary.All where
 
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Applicative
+open import Effect.Monad
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any using (Any; just)
 open import Data.Product as Prod using (_,_)
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index a05910dc7e..8e81c2b4b9 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -8,7 +8,7 @@
 
 module Data.Nat.InfinitelyOften where
 
-open import Category.Monad using (RawMonad)
+open import Effect.Monad using (RawMonad)
 open import Level using (Level; 0ℓ)
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base
diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda
index e55737835d..72920edf82 100644
--- a/src/Data/Nat/Show.agda
+++ b/src/Data/Nat/Show.agda
@@ -12,9 +12,9 @@ open import Data.Bool.Base using (_∧_)
 open import Data.Char.Base as Char using (Char)
 open import Data.Digit using (showDigit; toDigits; toNatDigits)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.List.Categorical using (module TraversableA)
+open import Data.List.Effectful using (module TraversableA)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
-import Data.Maybe.Categorical as Maybe
+import Data.Maybe.Effectful as Maybe
 open import Data.Nat
 open import Data.Product using (proj₁)
 open import Data.String as String using (String)
diff --git a/src/Data/Product/Categorical/Examples.agda b/src/Data/Product/Effectful/Examples.agda
similarity index 89%
rename from src/Data/Product/Categorical/Examples.agda
rename to src/Data/Product/Effectful/Examples.agda
index dc73acad71..49b3e7968c 100644
--- a/src/Data/Product/Categorical/Examples.agda
+++ b/src/Data/Product/Effectful/Examples.agda
@@ -8,16 +8,16 @@
 
 open import Algebra
 
-module Data.Product.Categorical.Examples
+module Data.Product.Effectful.Examples
   {a e b} {A : Monoid a e} {B : Set b} where
 
 open import Level using (Lift; lift; _⊔_)
-open import Category.Functor using (RawFunctor)
-open import Category.Monad using (RawMonad)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Monad using (RawMonad)
 open import Data.Product
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function
-import Function.Identity.Categorical as Id
+import Function.Identity.Effectful as Id
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
@@ -31,7 +31,7 @@ private
 
   module A = Monoid A
 
-  open import Data.Product.Categorical.Left A.rawMonoid b
+  open import Data.Product.Effectful.Left A.rawMonoid b
 
   _≈_ : Rel (A.Carrier × Lift a B) (e ⊔ a ⊔ b)
   _≈_ = Pointwise A._≈_ _≡_
diff --git a/src/Data/Product/Categorical/Left.agda b/src/Data/Product/Effectful/Left.agda
similarity index 86%
rename from src/Data/Product/Categorical/Left.agda
rename to src/Data/Product/Effectful/Left.agda
index 8e82eb7486..c37577fa71 100644
--- a/src/Data/Product/Categorical/Left.agda
+++ b/src/Data/Product/Effectful/Left.agda
@@ -6,7 +6,7 @@
 --
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
--- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
+-- (a ⊔ b). See the Data.Product.Effectful.Examples for how this is
 -- done.
 ------------------------------------------------------------------------
 
@@ -15,15 +15,15 @@
 open import Algebra
 open import Level
 
-module Data.Product.Categorical.Left
+module Data.Product.Effectful.Left
   {a e} (A : RawMonoid a e) (b : Level) where
 
 open import Data.Product
-import Data.Product.Categorical.Left.Base as Base
-open import Category.Applicative using (RawApplicative)
-open import Category.Monad using (RawMonad; RawMonadT)
+import Data.Product.Effectful.Left.Base as Base
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; RawMonadT)
 open import Function.Base using (id; flip; _∘_; _∘′_)
-import Function.Identity.Categorical as Id
+import Function.Identity.Effectful as Id
 
 open RawMonoid A
 
diff --git a/src/Data/Product/Categorical/Left/Base.agda b/src/Data/Product/Effectful/Left/Base.agda
similarity index 81%
rename from src/Data/Product/Categorical/Left/Base.agda
rename to src/Data/Product/Effectful/Left/Base.agda
index c7465d4d44..5cace74835 100644
--- a/src/Data/Product/Categorical/Left/Base.agda
+++ b/src/Data/Product/Effectful/Left/Base.agda
@@ -6,7 +6,7 @@
 --
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
--- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
+-- (a ⊔ b). See the Data.Product.Effectful.Examples for how this is
 -- done.
 ------------------------------------------------------------------------
 
@@ -14,12 +14,12 @@
 
 open import Level
 
-module Data.Product.Categorical.Left.Base
+module Data.Product.Effectful.Left.Base
   {a} (A : Set a) (b : Level) where
 
 open import Data.Product using (_×_; map₂; proj₁; proj₂; <_,_>)
-open import Category.Functor using (RawFunctor)
-open import Category.Comonad using (RawComonad)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Comonad using (RawComonad)
 
 ------------------------------------------------------------------------
 -- Definitions
diff --git a/src/Data/Product/Categorical/Right.agda b/src/Data/Product/Effectful/Right.agda
similarity index 86%
rename from src/Data/Product/Categorical/Right.agda
rename to src/Data/Product/Effectful/Right.agda
index d20533ef91..cbdff773d0 100644
--- a/src/Data/Product/Categorical/Right.agda
+++ b/src/Data/Product/Effectful/Right.agda
@@ -6,7 +6,7 @@
 --
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
--- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
+-- (a ⊔ b). See the Data.Product.Effectful.Examples for how this is
 -- done.
 ------------------------------------------------------------------------
 
@@ -15,15 +15,15 @@
 open import Algebra
 open import Level
 
-module Data.Product.Categorical.Right
+module Data.Product.Effectful.Right
   (a : Level) {b e} (B : RawMonoid b e) where
 
 open import Data.Product
-import Data.Product.Categorical.Right.Base as Base
-open import Category.Applicative using (RawApplicative)
-open import Category.Monad using (RawMonad; RawMonadT)
+import Data.Product.Effectful.Right.Base as Base
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; RawMonadT)
 open import Function.Base using (id; flip; _∘_; _∘′_)
-import Function.Identity.Categorical as Id
+import Function.Identity.Effectful as Id
 
 open RawMonoid B
 
diff --git a/src/Data/Product/Categorical/Right/Base.agda b/src/Data/Product/Effectful/Right/Base.agda
similarity index 81%
rename from src/Data/Product/Categorical/Right/Base.agda
rename to src/Data/Product/Effectful/Right/Base.agda
index 55264e6460..3095902589 100644
--- a/src/Data/Product/Categorical/Right/Base.agda
+++ b/src/Data/Product/Effectful/Right/Base.agda
@@ -6,7 +6,7 @@
 --
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
--- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
+-- (a ⊔ b). See the Data.Product.Effectful.Examples for how this is
 -- done.
 ------------------------------------------------------------------------
 
@@ -14,12 +14,12 @@
 
 open import Level
 
-module Data.Product.Categorical.Right.Base
+module Data.Product.Effectful.Right.Base
   {b} (B : Set b) (a : Level) where
 
 open import Data.Product using (_×_; map₁; proj₁; proj₂; <_,_>)
-open import Category.Functor using (RawFunctor)
-open import Category.Comonad using (RawComonad)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Comonad using (RawComonad)
 
 ------------------------------------------------------------------------
 -- Definitions
diff --git a/src/Data/Sum/Categorical/Examples.agda b/src/Data/Sum/Effectful/Examples.agda
similarity index 88%
rename from src/Data/Sum/Categorical/Examples.agda
rename to src/Data/Sum/Effectful/Examples.agda
index 014e9daee7..06f8685a0d 100644
--- a/src/Data/Sum/Categorical/Examples.agda
+++ b/src/Data/Sum/Effectful/Examples.agda
@@ -1,18 +1,18 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Usage examples of the categorical view of the Sum type
+-- Usage examples of the effectful view of the Sum type
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.Sum.Categorical.Examples where
+module Data.Sum.Effectful.Examples where
 
 open import Level
 open import Data.Sum.Base
-import Data.Sum.Categorical.Left as Sumₗ
-open import Category.Functor
-open import Category.Monad
+import Data.Sum.Effectful.Left as Sumₗ
+open import Effect.Functor
+open import Effect.Monad
 
 -- Note that these examples are simple unit tests, because the type
 -- checker verifies them.
diff --git a/src/Data/Sum/Categorical/Left.agda b/src/Data/Sum/Effectful/Left.agda
similarity index 88%
rename from src/Data/Sum/Categorical/Left.agda
rename to src/Data/Sum/Effectful/Left.agda
index 5583018724..41e9589e5f 100644
--- a/src/Data/Sum/Categorical/Left.agda
+++ b/src/Data/Sum/Effectful/Left.agda
@@ -1,20 +1,20 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A Categorical view of the Sum type (Left-biased)
+-- An effectful view of the Sum type (Left-biased)
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 open import Level
 
-module Data.Sum.Categorical.Left {a} (A : Set a) (b : Level) where
+module Data.Sum.Effectful.Left {a} (A : Set a) (b : Level) where
 
 open import Data.Sum.Base
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-import Function.Identity.Categorical as Id
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
+import Function.Identity.Effectful as Id
 open import Function
 
 -- To minimize the universe level of the RawFunctor, we require that elements of
diff --git a/src/Data/Sum/Categorical/Right.agda b/src/Data/Sum/Effectful/Right.agda
similarity index 85%
rename from src/Data/Sum/Categorical/Right.agda
rename to src/Data/Sum/Effectful/Right.agda
index a991c490dd..d238e8210a 100644
--- a/src/Data/Sum/Categorical/Right.agda
+++ b/src/Data/Sum/Effectful/Right.agda
@@ -1,21 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A Categorical view of the Sum type (Right-biased)
+-- An effectful view of the Sum type (Right-biased)
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 open import Level
 
-module Data.Sum.Categorical.Right (a : Level) {b} (B : Set b) where
+module Data.Sum.Effectful.Right (a : Level) {b} (B : Set b) where
 
 open import Data.Sum.Base
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Function
-import Function.Identity.Categorical as Id
+import Function.Identity.Effectful as Id
 
 Sumᵣ : Set (a ⊔ b) → Set (a ⊔ b)
 Sumᵣ A = A ⊎ B
diff --git a/src/Data/These/Categorical/Left.agda b/src/Data/These/Effectful/Left.agda
similarity index 80%
rename from src/Data/These/Categorical/Left.agda
rename to src/Data/These/Effectful/Left.agda
index e41e2303b7..a3631c75e2 100644
--- a/src/Data/These/Categorical/Left.agda
+++ b/src/Data/These/Effectful/Left.agda
@@ -8,14 +8,14 @@
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
 -- (a ⊔ b).
--- See the Data.Product.Categorical.Examples for how this is done in a
+-- See the Data.Product.Effectful.Examples for how this is done in a
 -- Product-based similar setting.
 
 -- This functor can be understood as a notion of computation which can
 -- either fail (this), succeed (that) or accumulate warnings whilst
 -- delivering a successful computation (these).
 
--- It is a good alternative to Data.Product.Categorical when the notion
+-- It is a good alternative to Data.Product.Effectful when the notion
 -- of warnings does not have a neutral element (e.g. List⁺).
 
 {-# OPTIONS --without-K --safe #-}
@@ -23,14 +23,14 @@
 open import Level
 open import Algebra
 
-module Data.These.Categorical.Left {c ℓ} (W : Semigroup c ℓ) (b : Level) where
+module Data.These.Effectful.Left {c ℓ} (W : Semigroup c ℓ) (b : Level) where
 
 open Semigroup W
-open import Data.These.Categorical.Left.Base Carrier b public
+open import Data.These.Effectful.Left.Base Carrier b public
 
 open import Data.These.Base
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Applicative
+open import Effect.Monad
 
 module _ {a b} {A : Set a} {B : Set b} where
 
diff --git a/src/Data/These/Categorical/Left/Base.agda b/src/Data/These/Effectful/Left/Base.agda
similarity index 87%
rename from src/Data/These/Categorical/Left/Base.agda
rename to src/Data/These/Effectful/Left/Base.agda
index 22af90c78e..4c789e12d3 100644
--- a/src/Data/These/Categorical/Left/Base.agda
+++ b/src/Data/These/Effectful/Left/Base.agda
@@ -7,7 +7,7 @@
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
 -- (a ⊔ b).
--- See the Data.Product.Categorical.Examples for how this is done in a
+-- See the Data.Product.Effectful.Examples for how this is done in a
 -- Product-based similar setting.
 ------------------------------------------------------------------------
 
@@ -15,12 +15,12 @@
 
 open import Level
 
-module Data.These.Categorical.Left.Base {a} (A : Set a) (b : Level) where
+module Data.These.Effectful.Left.Base {a} (A : Set a) (b : Level) where
 
 open import Data.These.Base
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Function
 
 Theseₗ : Set (a ⊔ b) → Set (a ⊔ b)
diff --git a/src/Data/These/Categorical/Right.agda b/src/Data/These/Effectful/Right.agda
similarity index 79%
rename from src/Data/These/Categorical/Right.agda
rename to src/Data/These/Effectful/Right.agda
index 849985b559..a1a33dbfc3 100644
--- a/src/Data/These/Categorical/Right.agda
+++ b/src/Data/These/Effectful/Right.agda
@@ -7,14 +7,14 @@
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
 -- (a ⊔ b).
--- See the Data.Product.Categorical.Examples for how this is done in a
+-- See the Data.Product.Effectful.Examples for how this is done in a
 -- Product-based similar setting.
 
 -- This functor can be understood as a notion of computation which can
 -- either fail (that), succeed (this) or accumulate warnings whilst
 -- delivering a successful computation (these).
 
--- It is a good alternative to Data.Product.Categorical when the notion
+-- It is a good alternative to Data.Product.Effectful when the notion
 -- of warnings does not have a neutral element (e.g. List⁺).
 
 {-# OPTIONS --without-K --safe #-}
@@ -22,14 +22,14 @@
 open import Level
 open import Algebra
 
-module Data.These.Categorical.Right (a : Level) {c ℓ} (W : Semigroup c ℓ) where
+module Data.These.Effectful.Right (a : Level) {c ℓ} (W : Semigroup c ℓ) where
 
 open Semigroup W
-open import Data.These.Categorical.Right.Base a Carrier public
+open import Data.These.Effectful.Right.Base a Carrier public
 
 open import Data.These.Base
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Applicative
+open import Effect.Monad
 
 module _ {a b} {A : Set a} {B : Set b} where
 
diff --git a/src/Data/These/Categorical/Right/Base.agda b/src/Data/These/Effectful/Right/Base.agda
similarity index 87%
rename from src/Data/These/Categorical/Right/Base.agda
rename to src/Data/These/Effectful/Right/Base.agda
index 0ef76df24f..99a441492a 100644
--- a/src/Data/These/Categorical/Right/Base.agda
+++ b/src/Data/These/Effectful/Right/Base.agda
@@ -7,7 +7,7 @@
 -- To minimize the universe level of the RawFunctor, we require that
 -- elements of B are "lifted" to a copy of B at a higher universe level
 -- (a ⊔ b).
--- See the Data.Product.Categorical.Examples for how this is done in a
+-- See the Data.Product.Effectful.Examples for how this is done in a
 -- Product-based similar setting.
 ------------------------------------------------------------------------
 
@@ -15,12 +15,12 @@
 
 open import Level
 
-module Data.These.Categorical.Right.Base (a : Level) {b} (B : Set b) where
+module Data.These.Effectful.Right.Base (a : Level) {b} (B : Set b) where
 
 open import Data.These.Base
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Function
 
 Theseᵣ : Set (a ⊔ b) → Set (a ⊔ b)
diff --git a/src/Data/Trie/NonEmpty.agda b/src/Data/Trie/NonEmpty.agda
index 142bc1f96c..d0ffed95b8 100644
--- a/src/Data/Trie/NonEmpty.agda
+++ b/src/Data/Trie/NonEmpty.agda
@@ -12,14 +12,14 @@ module Data.Trie.NonEmpty {k e r} (S : StrictTotalOrder k e r) where
 
 open import Level
 open import Size
-open import Category.Monad
+open import Effect.Monad
 open import Data.Product as Prod using (∃; uncurry; -,_)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; concatMap)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) hiding (module Maybe)
 open import Data.These as These using (These; this; that; these)
 open import Function as F
-import Function.Identity.Categorical as Identity
+import Function.Identity.Effectful as Identity
 open import Relation.Unary using (_⇒_; IUniversal)
 
 open StrictTotalOrder S
diff --git a/src/Data/Vec/Categorical.agda b/src/Data/Vec/Effectful.agda
similarity index 86%
rename from src/Data/Vec/Categorical.agda
rename to src/Data/Vec/Effectful.agda
index e099fcc044..27079012fd 100644
--- a/src/Data/Vec/Categorical.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -1,21 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of Vec
+-- An effectful view of Vec
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.Vec.Categorical {a n} where
+module Data.Vec.Effectful {a n} where
 
-open import Category.Applicative using (RawApplicative)
-open import Category.Applicative.Indexed using (Morphism)
-open import Category.Functor as Fun using (RawFunctor)
-import Function.Identity.Categorical as Id
-open import Category.Monad using (RawMonad)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base as Vec hiding (_⊛_)
 open import Data.Vec.Properties
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Applicative.Indexed using (Morphism)
+open import Effect.Functor as Fun using (RawFunctor)
+open import Effect.Monad using (RawMonad)
+import Function.Identity.Effectful as Id
 open import Function hiding (Morphism)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Instances.agda b/src/Data/Vec/Instances.agda
index 038b78d616..3f6d1b8bf6 100644
--- a/src/Data/Vec/Instances.agda
+++ b/src/Data/Vec/Instances.agda
@@ -9,7 +9,7 @@
 module Data.Vec.Instances where
 
 open import Data.Vec.Base
-open import Data.Vec.Categorical
+open import Data.Vec.Effectful
 open import Data.Vec.Properties
   using (≡-dec)
 open import Level
diff --git a/src/Data/Vec/Recursive/Categorical.agda b/src/Data/Vec/Recursive/Effectful.agda
similarity index 89%
rename from src/Data/Vec/Recursive/Categorical.agda
rename to src/Data/Vec/Recursive/Effectful.agda
index 3548fab9eb..b49abb3197 100644
--- a/src/Data/Vec/Recursive/Categorical.agda
+++ b/src/Data/Vec/Recursive/Effectful.agda
@@ -1,22 +1,21 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of vectors defined by recursion
+-- An effectful view of vectors defined by recursion
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.Vec.Recursive.Categorical where
+module Data.Vec.Recursive.Effectful where
 
 open import Agda.Builtin.Nat
 open import Data.Product hiding (map)
 open import Data.Vec.Recursive
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Function
 
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-
 ------------------------------------------------------------------------
 -- Functor and applicative
 
diff --git a/src/Category/Applicative.agda b/src/Effect/Applicative.agda
similarity index 93%
rename from src/Category/Applicative.agda
rename to src/Effect/Applicative.agda
index ce38b5ba36..99eb762c28 100644
--- a/src/Category/Applicative.agda
+++ b/src/Effect/Applicative.agda
@@ -9,11 +9,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Applicative where
+module Effect.Applicative where
 
 open import Level using (Level; suc; _⊔_)
 open import Data.Unit
-open import Category.Applicative.Indexed
+open import Effect.Applicative.Indexed
 
 private
   variable
diff --git a/src/Category/Applicative/Indexed.agda b/src/Effect/Applicative/Indexed.agda
similarity index 97%
rename from src/Category/Applicative/Indexed.agda
rename to src/Effect/Applicative/Indexed.agda
index 96334c4f93..5174a6710a 100644
--- a/src/Category/Applicative/Indexed.agda
+++ b/src/Effect/Applicative/Indexed.agda
@@ -9,9 +9,9 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Applicative.Indexed where
+module Effect.Applicative.Indexed where
 
-open import Category.Functor using (RawFunctor)
+open import Effect.Functor using (RawFunctor)
 open import Data.Product using (_×_; _,_)
 open import Function hiding (Morphism)
 open import Level
diff --git a/src/Category/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda
similarity index 94%
rename from src/Category/Applicative/Predicate.agda
rename to src/Effect/Applicative/Predicate.agda
index 2c3396b931..7d3d1ba532 100644
--- a/src/Category/Applicative/Predicate.agda
+++ b/src/Effect/Applicative/Predicate.agda
@@ -9,9 +9,9 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Applicative.Predicate where
+module Effect.Applicative.Predicate where
 
-open import Category.Functor.Predicate
+open import Effect.Functor.Predicate
 open import Data.Product
 open import Function
 open import Level
diff --git a/src/Category/Comonad.agda b/src/Effect/Comonad.agda
similarity index 97%
rename from src/Category/Comonad.agda
rename to src/Effect/Comonad.agda
index 077ff043d0..88f3e6c664 100644
--- a/src/Category/Comonad.agda
+++ b/src/Effect/Comonad.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Comonad where
+module Effect.Comonad where
 
 open import Level
 open import Function
diff --git a/src/Category/Functor.agda b/src/Effect/Functor.agda
similarity index 97%
rename from src/Category/Functor.agda
rename to src/Effect/Functor.agda
index ea50c846fb..d269c7a64c 100644
--- a/src/Category/Functor.agda
+++ b/src/Effect/Functor.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Functor where
+module Effect.Functor where
 
 open import Function hiding (Morphism)
 open import Level
diff --git a/src/Category/Functor/Predicate.agda b/src/Effect/Functor/Predicate.agda
similarity index 95%
rename from src/Category/Functor/Predicate.agda
rename to src/Effect/Functor/Predicate.agda
index 0d5e62ac1c..cde7c77c53 100644
--- a/src/Category/Functor/Predicate.agda
+++ b/src/Effect/Functor/Predicate.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Functor.Predicate where
+module Effect.Functor.Predicate where
 
 open import Function
 open import Level
diff --git a/src/Category/Monad.agda b/src/Effect/Monad.agda
similarity index 94%
rename from src/Category/Monad.agda
rename to src/Effect/Monad.agda
index f56e0bde2a..fcf30e08f5 100644
--- a/src/Category/Monad.agda
+++ b/src/Effect/Monad.agda
@@ -8,10 +8,10 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Monad where
+module Effect.Monad where
 
 open import Function
-open import Category.Monad.Indexed
+open import Effect.Monad.Indexed
 open import Data.Unit
 open import Level
 
diff --git a/src/Category/Monad/Continuation.agda b/src/Effect/Monad/Continuation.agda
similarity index 88%
rename from src/Category/Monad/Continuation.agda
rename to src/Effect/Monad/Continuation.agda
index 31770a289f..7d241f4bd7 100644
--- a/src/Category/Monad/Continuation.agda
+++ b/src/Effect/Monad/Continuation.agda
@@ -6,13 +6,13 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Monad.Continuation where
+module Effect.Monad.Continuation where
 
-open import Category.Applicative
-open import Category.Applicative.Indexed
-open import Category.Monad
-open import Function.Identity.Categorical as Id using (Identity)
-open import Category.Monad.Indexed
+open import Effect.Applicative
+open import Effect.Applicative.Indexed
+open import Effect.Monad
+open import Function.Identity.Effectful as Id using (Identity)
+open import Effect.Monad.Indexed
 open import Function
 open import Level
 
diff --git a/src/Category/Monad/Indexed.agda b/src/Effect/Monad/Indexed.agda
similarity index 96%
rename from src/Category/Monad/Indexed.agda
rename to src/Effect/Monad/Indexed.agda
index 8fbba04e80..2c73243aa2 100644
--- a/src/Category/Monad/Indexed.agda
+++ b/src/Effect/Monad/Indexed.agda
@@ -8,9 +8,9 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Monad.Indexed where
+module Effect.Monad.Indexed where
 
-open import Category.Applicative.Indexed
+open import Effect.Applicative.Indexed
 open import Function
 open import Level
 
diff --git a/src/Category/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
similarity index 99%
rename from src/Category/Monad/Partiality.agda
rename to src/Effect/Monad/Partiality.agda
index ec43f899c7..579f4a4653 100644
--- a/src/Category/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -6,10 +6,10 @@
 
 {-# OPTIONS --without-K --safe --guardedness #-}
 
-module Category.Monad.Partiality where
+module Effect.Monad.Partiality where
 
 open import Codata.Musical.Notation
-open import Category.Monad
+open import Effect.Monad
 open import Data.Bool.Base using (Bool; false; true)
 open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.Product as Prod hiding (map)
diff --git a/src/Category/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda
similarity index 97%
rename from src/Category/Monad/Partiality/All.agda
rename to src/Effect/Monad/Partiality/All.agda
index 37dc555397..64e961eccd 100644
--- a/src/Category/Monad/Partiality/All.agda
+++ b/src/Effect/Monad/Partiality/All.agda
@@ -6,10 +6,10 @@
 
 {-# OPTIONS --without-K --safe --guardedness #-}
 
-module Category.Monad.Partiality.All where
+module Effect.Monad.Partiality.All where
 
-open import Category.Monad
-open import Category.Monad.Partiality as Partiality using (_⊥; ⇒≈)
+open import Effect.Monad
+open import Effect.Monad.Partiality as Partiality using (_⊥; ⇒≈)
 open import Codata.Musical.Notation
 open import Function
 open import Level
diff --git a/src/Category/Monad/Partiality/Instances.agda b/src/Effect/Monad/Partiality/Instances.agda
similarity index 77%
rename from src/Category/Monad/Partiality/Instances.agda
rename to src/Effect/Monad/Partiality/Instances.agda
index 3f51261c95..8e41343258 100644
--- a/src/Category/Monad/Partiality/Instances.agda
+++ b/src/Effect/Monad/Partiality/Instances.agda
@@ -6,9 +6,9 @@
 
 {-# OPTIONS --without-K --safe --guardedness #-}
 
-module Category.Monad.Partiality.Instances where
+module Effect.Monad.Partiality.Instances where
 
-open import Category.Monad.Partiality
+open import Effect.Monad.Partiality
 
 instance
   partialityMonad = monad
diff --git a/src/Category/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda
similarity index 92%
rename from src/Category/Monad/Predicate.agda
rename to src/Effect/Monad/Predicate.agda
index 33954def0a..de634a1195 100644
--- a/src/Category/Monad/Predicate.agda
+++ b/src/Effect/Monad/Predicate.agda
@@ -8,11 +8,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Monad.Predicate where
+module Effect.Monad.Predicate where
 
-open import Category.Applicative.Indexed
-open import Category.Monad
-open import Category.Monad.Indexed
+open import Effect.Applicative.Indexed
+open import Effect.Monad
+open import Effect.Monad.Indexed
 open import Data.Unit
 open import Data.Product
 open import Function
diff --git a/src/Category/Monad/Reader.agda b/src/Effect/Monad/Reader.agda
similarity index 94%
rename from src/Category/Monad/Reader.agda
rename to src/Effect/Monad/Reader.agda
index 8bfedfb965..65d967889e 100644
--- a/src/Category/Monad/Reader.agda
+++ b/src/Effect/Monad/Reader.agda
@@ -8,13 +8,13 @@
 
 open import Level
 
-module Category.Monad.Reader {r} (R : Set r) (a : Level) where
+module Effect.Monad.Reader {r} (R : Set r) (a : Level) where
 
 open import Function
-open import Function.Identity.Categorical as Id using (Identity)
-open import Category.Applicative.Indexed
-open import Category.Monad.Indexed
-open import Category.Monad
+open import Function.Identity.Effectful as Id using (Identity)
+open import Effect.Applicative.Indexed
+open import Effect.Monad.Indexed
+open import Effect.Monad
 open import Data.Unit
 
 private
diff --git a/src/Category/Monad/State.agda b/src/Effect/Monad/State.agda
similarity index 96%
rename from src/Category/Monad/State.agda
rename to src/Effect/Monad/State.agda
index 5ea4a5ac90..1df53ebfc2 100644
--- a/src/Category/Monad/State.agda
+++ b/src/Effect/Monad/State.agda
@@ -6,12 +6,12 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Category.Monad.State where
+module Effect.Monad.State where
 
-open import Category.Applicative.Indexed
-open import Category.Monad
-open import Function.Identity.Categorical as Id using (Identity)
-open import Category.Monad.Indexed
+open import Effect.Applicative.Indexed
+open import Effect.Monad
+open import Function.Identity.Effectful as Id using (Identity)
+open import Effect.Monad.Indexed
 open import Data.Product
 open import Data.Unit
 open import Function
diff --git a/src/Function/Identity/Categorical.agda b/src/Function/Identity/Effectful.agda
similarity index 74%
rename from src/Function/Identity/Categorical.agda
rename to src/Function/Identity/Effectful.agda
index 13794c5d06..6d4c32a64e 100644
--- a/src/Function/Identity/Categorical.agda
+++ b/src/Function/Identity/Effectful.agda
@@ -1,17 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- A categorical view of the identity function
+-- An effectful view of the identity function
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Function.Identity.Categorical {ℓ} where
+module Function.Identity.Effectful {ℓ} where
 
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
-open import Category.Comonad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
+open import Effect.Comonad
 open import Function
 
 Identity : Set ℓ → Set ℓ
diff --git a/src/Function/Identity/Instances.agda b/src/Function/Identity/Instances.agda
index f7b94a01fa..09037f38fd 100644
--- a/src/Function/Identity/Instances.agda
+++ b/src/Function/Identity/Instances.agda
@@ -8,7 +8,7 @@
 
 module Function.Identity.Instances where
 
-open import Function.Identity.Categorical
+open import Function.Identity.Effectful
 
 instance
   identityFunctor = functor
diff --git a/src/Reflection/AST/DeBruijn.agda b/src/Reflection/AST/DeBruijn.agda
index eac7d9c17d..174abe2874 100644
--- a/src/Reflection/AST/DeBruijn.agda
+++ b/src/Reflection/AST/DeBruijn.agda
@@ -12,9 +12,9 @@ open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
 open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.Maybe.Base using (Maybe; nothing; just)
-import Data.Maybe.Categorical as Maybe
-import Function.Identity.Categorical as Identity
-open import Category.Applicative using (RawApplicative)
+import Data.Maybe.Effectful as Maybe
+import Function.Identity.Effectful as Identity
+open import Effect.Applicative using (RawApplicative)
 
 open import Reflection
 open import Reflection.AST.Argument.Visibility using (Visibility)
diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
index 7ba2187eca..8c02aa7ade 100644
--- a/src/Reflection/AST/Traversal.agda
+++ b/src/Reflection/AST/Traversal.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Category.Applicative using (RawApplicative)
+open import Effect.Applicative using (RawApplicative)
 
 module Reflection.AST.Traversal
   {F : Set → Set} (AppF : RawApplicative F) where
diff --git a/src/Reflection/AnnotatedAST.agda b/src/Reflection/AnnotatedAST.agda
index deee5ac6a9..a48deda10f 100644
--- a/src/Reflection/AnnotatedAST.agda
+++ b/src/Reflection/AnnotatedAST.agda
@@ -13,7 +13,7 @@
 module Reflection.AnnotatedAST where
 
 open import Level                        using (Level; 0ℓ; suc; _⊔_)
-open import Category.Applicative         using (RawApplicative)
+open import Effect.Applicative         using (RawApplicative)
 open import Data.Bool.Base               using (Bool; false; true; if_then_else_)
 open import Data.List.Base               using (List; []; _∷_)
 open import Data.List.Relation.Unary.All using (All; _∷_; [])
diff --git a/src/Reflection/TCM/Categorical.agda b/src/Reflection/TCM/Effectful.agda
similarity index 90%
rename from src/Reflection/TCM/Categorical.agda
rename to src/Reflection/TCM/Effectful.agda
index b877468469..ab37b3f40d 100644
--- a/src/Reflection/TCM/Categorical.agda
+++ b/src/Reflection/TCM/Effectful.agda
@@ -6,11 +6,11 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Reflection.TCM.Categorical where
+module Reflection.TCM.Effectful where
 
-open import Category.Functor
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Functor
+open import Effect.Applicative
+open import Effect.Monad
 open import Data.List.Base using ([])
 open import Function.Base using (_∘_)
 open import Level
diff --git a/src/Reflection/TCM/Instances.agda b/src/Reflection/TCM/Instances.agda
index 340681be94..4580f75192 100644
--- a/src/Reflection/TCM/Instances.agda
+++ b/src/Reflection/TCM/Instances.agda
@@ -8,7 +8,7 @@
 
 module Reflection.TCM.Instances where
 
-open import Reflection.TCM.Categorical
+open import Reflection.TCM.Effectful
 
 instance
   tcFunctor = functor
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 9437a46346..a76cf75db0 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -8,7 +8,7 @@
 
 module Relation.Nullary.Negation where
 
-open import Category.Monad
+open import Effect.Monad
 open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
 open import Data.Empty
 open import Data.Product as Prod
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index aae9d84cee..97db3329bc 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -23,8 +23,8 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function
 import Function.Equality as FunS
 open import Data.Empty
-open import Category.Applicative
-open import Category.Monad
+open import Effect.Applicative
+open import Effect.Monad
 open import Level
 
 infix  5 ¬¬_
diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda
index acb1e17c6d..552aa9a1b2 100644
--- a/src/Text/Format/Generic.agda
+++ b/src/Text/Format/Generic.agda
@@ -12,7 +12,7 @@ open import Data.Maybe.Base using (Maybe)
 module Text.Format.Generic where
 
 open import Level using (0ℓ)
-open import Category.Applicative
+open import Effect.Applicative
 open import Data.List.Base as List
 open import Data.Maybe as Maybe
 open import Data.Nat.Base
@@ -20,7 +20,7 @@ open import Data.Product
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base
 open import Data.String.Base
-import Data.Sum.Categorical.Left as Sumₗ
+import Data.Sum.Effectful.Left as Sumₗ
 open import Function
 open import Function.Nary.NonDependent using (0ℓs; Sets)
 open import Function.Strict
diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index d9247d71d0..08c60701bf 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -22,8 +22,8 @@ open import Data.Product       using (uncurry)
 open import Data.String.Base   using (String; fromList; replicate)
 open import Function.Base
 
-open import Category.Monad using (RawMonad)
-import Data.List.Categorical as Cat
+open import Effect.Monad using (RawMonad)
+import Data.List.Effectful as Cat
 open RawMonad (Cat.monad {Level.zero})
 
 import Data.Nat.Properties as ℕₚ