diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76ca38cd42..93b707d2ba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -88,8 +88,7 @@ Non-backwards compatible changes
   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`.
+  (highly specific) mode of use. Correspondingly, client modules grouped under `*.Categorical.*` which exploit such structure for effectful programming have been renamed `*.Effectful`, with the originals being deprecated.
 
 ### Improvements to pretty printing and regexes
 
@@ -871,6 +870,43 @@ Deprecated modules
   Algebra.Morphism.LatticeMonomorphism         ↦ Algebra.Lattice.Morphism.LatticeMonomorphism
   ```
 
+### Moving `*.Catgeorical.*` files
+
+* As discussed above the following files have been moved:
+  ```agda
+  Codata.Sized.Colist.Categorical            ↦ Codata.Sized.Colist.Effectful
+  Codata.Sized.Covec.Categorical             ↦ Codata.Sized.Covec.Effectful
+  Codata.Sized.Delay.Categorical             ↦ Codata.Sized.Delay.Effectful
+  Codata.Sized.Stream.Categorical            ↦ Codata.Sized.Stream.Effectful
+  Data.List.Categorical                      ↦ Data.List.Effectful
+  Data.List.Categorical.Transformer          ↦ Data.List.Effectful.Transformer
+  Data.List.NonEmpty.Categorical             ↦ Data.List.NonEmpty.Effectful
+  Data.List.NonEmpty.Categorical.Transformer ↦ Data.List.NonEmpty.Effectful.Transformer
+  Data.Maybe.Categorical                     ↦ Data.Maybe.Effectful
+  Data.Maybe.Categorical.Transformer         ↦ Data.Maybe.Effectful.Transformer
+  Data.Product.Categorical.Examples          ↦ Data.Product.Effectful.Examples
+  Data.Product.Categorical.Left              ↦ Data.Product.Effectful.Left
+  Data.Product.Categorical.Left.Base         ↦ Data.Product.Effectful.Left.Base
+  Data.Product.Categorical.Right             ↦ Data.Product.Effectful.Right
+  Data.Product.Categorical.Right.Base        ↦ Data.Product.Effectful.Right.Base
+  Data.Sum.Categorical.Examples              ↦ Data.Sum.Effectful.Examples
+  Data.Sum.Categorical.Left                  ↦ Data.Sum.Effectful.Left
+  Data.Sum.Categorical.Left.Transformer      ↦ Data.Sum.Effectful.Left.Transformer
+  Data.Sum.Categorical.Right                 ↦ Data.Sum.Effectful.Right
+  Data.Sum.Categorical.Right.Transformer     ↦ Data.Sum.Effectful.Right.Transformer
+  Data.These.Categorical.Examples            ↦ Data.These.Effectful.Examples
+  Data.These.Categorical.Left                ↦ Data.These.Effectful.Left
+  Data.These.Categorical.Left.Base           ↦ Data.These.Effectful.Left.Base
+  Data.These.Categorical.Right               ↦ Data.These.Effectful.Right
+  Data.These.Categorical.Right.Base          ↦ Data.These.Effectful.Right.Base
+  Data.Vec.Categorical                       ↦ Data.Vec.Effectful
+  Data.Vec.Categorical.Transformer           ↦ Data.Vec.Effectful.Transformer
+  Data.Vec.Recursive.Categorical             ↦ Data.Vec.Recursive.Effectful
+  Function.Identity.Categorical              ↦ Function.Identity.Effectful
+  IO.Categorical                             ↦ IO.Effectful
+  Reflection.TCM.Categorical                 ↦ Reflection.TCM.Effectful
+  ```
+
 ### Moving `Relation.Binary.Properties.XLattice` files
 
 * The following files have been moved:
diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index d513da0ab8..ee49679f3a 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -53,6 +53,7 @@ unsafeModules = map modToFile
   , "Foreign.Haskell.Pair"
   , "IO"
   , "IO.Base"
+  , "IO.Categorical"
   , "IO.Infinite"
   , "IO.Instances"
   , "IO.Effectful"
@@ -121,6 +122,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"
@@ -129,6 +131,7 @@ 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"
@@ -136,6 +139,7 @@ sizedTypesModules = map modToFile
   , "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"
@@ -143,6 +147,7 @@ sizedTypesModules = map modToFile
   , "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"
diff --git a/src/Codata/Sized/Colist/Categorical.agda b/src/Codata/Sized/Colist/Categorical.agda
new file mode 100644
index 0000000000..6cee36ca22
--- /dev/null
+++ b/src/Codata/Sized/Colist/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Colist.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Colist.Categorical where
+
+open import Codata.Sized.Colist.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Colist.Categorical was deprecated in v2.0.
+Use Codata.Sized.Colist.Effectful instead."
+#-}
diff --git a/src/Codata/Sized/Covec/Categorical.agda b/src/Codata/Sized/Covec/Categorical.agda
new file mode 100644
index 0000000000..0da702ff2c
--- /dev/null
+++ b/src/Codata/Sized/Covec/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Covec.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Covec.Categorical where
+
+open import Codata.Sized.Covec.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Covec.Categorical was deprecated in v2.0.
+Use Codata.Sized.Covec.Effectful instead."
+#-}
diff --git a/src/Codata/Sized/Delay/Categorical.agda b/src/Codata/Sized/Delay/Categorical.agda
new file mode 100644
index 0000000000..2aa88bb896
--- /dev/null
+++ b/src/Codata/Sized/Delay/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Delay.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Delay.Categorical where
+
+open import Codata.Sized.Delay.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Delay.Categorical was deprecated in v2.0.
+Use Codata.Sized.Delay.Effectful instead."
+#-}
diff --git a/src/Codata/Sized/Stream/Categorical.agda b/src/Codata/Sized/Stream/Categorical.agda
new file mode 100644
index 0000000000..597d7b7bfc
--- /dev/null
+++ b/src/Codata/Sized/Stream/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Codata.Sized.Stream.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --sized-types #-}
+
+module Codata.Sized.Stream.Categorical where
+
+open import Codata.Sized.Stream.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Codata.Sized.Stream.Categorical was deprecated in v2.0.
+Use Codata.Sized.Stream.Effectful instead."
+#-}
diff --git a/src/Data/List/Categorical.agda b/src/Data/List/Categorical.agda
new file mode 100644
index 0000000000..dc3391f1c4
--- /dev/null
+++ b/src/Data/List/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Categorical where
+
+open import Data.List.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.List.Categorical was deprecated in v2.0.
+Use Data.List.Effectful instead."
+#-}
diff --git a/src/Data/List/Categorical/Transformer.agda b/src/Data/List/Categorical/Transformer.agda
new file mode 100644
index 0000000000..75b83f14f3
--- /dev/null
+++ b/src/Data/List/Categorical/Transformer.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Categorical.Transformer where
+
+open import Data.List.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.List.Categorical.Transformer was deprecated in v2.0.
+Use Data.List.Effectful.Transformer instead."
+#-}
diff --git a/src/Data/List/NonEmpty/Categorical.agda b/src/Data/List/NonEmpty/Categorical.agda
new file mode 100644
index 0000000000..442c1a0df1
--- /dev/null
+++ b/src/Data/List/NonEmpty/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.NonEmpty.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Categorical where
+
+open import Data.List.NonEmpty.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.List.NonEmpty.Categorical was deprecated in v2.0.
+Use Data.List.NonEmpty.Effectful instead."
+#-}
diff --git a/src/Data/List/NonEmpty/Categorical/Transformer.agda b/src/Data/List/NonEmpty/Categorical/Transformer.agda
new file mode 100644
index 0000000000..7842b65054
--- /dev/null
+++ b/src/Data/List/NonEmpty/Categorical/Transformer.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.List.NonEmpty.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.NonEmpty.Categorical.Transformer where
+
+open import Data.List.NonEmpty.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.List.NonEmpty.Categorical.Transformer was deprecated in v2.0.
+Use Data.List.NonEmpty.Effectful.Transformer instead."
+#-}
diff --git a/src/Data/Maybe/Categorical.agda b/src/Data/Maybe/Categorical.agda
new file mode 100644
index 0000000000..e6ec7a7a2c
--- /dev/null
+++ b/src/Data/Maybe/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Maybe.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Maybe.Categorical where
+
+open import Data.Maybe.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.Maybe.Categorical was deprecated in v2.0.
+Use Data.Maybe.Effectful instead."
+#-}
diff --git a/src/Data/Maybe/Categorical/Transformer.agda b/src/Data/Maybe/Categorical/Transformer.agda
new file mode 100644
index 0000000000..aca111a00a
--- /dev/null
+++ b/src/Data/Maybe/Categorical/Transformer.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Maybe.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Maybe.Categorical.Transformer where
+
+open import Data.Maybe.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.Maybe.Categorical.Transformer was deprecated in v2.0.
+Use Data.Maybe.Effectful.Transformer instead."
+#-}
diff --git a/src/Data/Product/Categorical/Examples.agda b/src/Data/Product/Categorical/Examples.agda
new file mode 100644
index 0000000000..e832d67b19
--- /dev/null
+++ b/src/Data/Product/Categorical/Examples.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Examples` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Examples where
+
+open import Data.Product.Effectful.Examples public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Examples was deprecated in v2.0.
+Use Data.Product.Effectful.Examples instead."
+#-}
diff --git a/src/Data/Product/Categorical/Left.agda b/src/Data/Product/Categorical/Left.agda
new file mode 100644
index 0000000000..de68a8575e
--- /dev/null
+++ b/src/Data/Product/Categorical/Left.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Left` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Left where
+
+open import Data.Product.Effectful.Left public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Left was deprecated in v2.0.
+Use Data.Product.Effectful.Left instead."
+#-}
diff --git a/src/Data/Product/Categorical/Left/Base.agda b/src/Data/Product/Categorical/Left/Base.agda
new file mode 100644
index 0000000000..ffa7fed34c
--- /dev/null
+++ b/src/Data/Product/Categorical/Left/Base.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Left.Base` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Left.Base where
+
+open import Data.Product.Effectful.Left.Base public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Left.Base was deprecated in v2.0.
+Use Data.Product.Effectful.Left.Base instead."
+#-}
diff --git a/src/Data/Product/Categorical/Right.agda b/src/Data/Product/Categorical/Right.agda
new file mode 100644
index 0000000000..bdd34822e3
--- /dev/null
+++ b/src/Data/Product/Categorical/Right.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Right` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Right where
+
+open import Data.Product.Effectful.Right public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Right was deprecated in v2.0.
+Use Data.Product.Effectful.Right instead."
+#-}
diff --git a/src/Data/Product/Categorical/Right/Base.agda b/src/Data/Product/Categorical/Right/Base.agda
new file mode 100644
index 0000000000..556009642a
--- /dev/null
+++ b/src/Data/Product/Categorical/Right/Base.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Product.Categorical.Right.Base` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Product.Categorical.Right.Base where
+
+open import Data.Product.Effectful.Right.Base public
+
+{-# WARNING_ON_IMPORT
+"Data.Product.Categorical.Right.Base was deprecated in v2.0.
+Use Data.Product.Effectful.Right.Base instead."
+#-}
diff --git a/src/Data/Sum/Categorical/Examples.agda b/src/Data/Sum/Categorical/Examples.agda
new file mode 100644
index 0000000000..5a74842598
--- /dev/null
+++ b/src/Data/Sum/Categorical/Examples.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Examples` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Examples where
+
+open import Data.Sum.Effectful.Examples public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Examples was deprecated in v2.0.
+Use Data.Sum.Effectful.Examples instead."
+#-}
diff --git a/src/Data/Sum/Categorical/Left.agda b/src/Data/Sum/Categorical/Left.agda
new file mode 100644
index 0000000000..b1a26c995d
--- /dev/null
+++ b/src/Data/Sum/Categorical/Left.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Left` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Left where
+
+open import Data.Sum.Effectful.Left public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Left was deprecated in v2.0.
+Use Data.Sum.Effectful.Left instead."
+#-}
diff --git a/src/Data/Sum/Categorical/Left/Transformer.agda b/src/Data/Sum/Categorical/Left/Transformer.agda
new file mode 100644
index 0000000000..de39522246
--- /dev/null
+++ b/src/Data/Sum/Categorical/Left/Transformer.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Left.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Left.Transformer where
+
+open import Data.Sum.Effectful.Left.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Left.Transformer was deprecated in v2.0.
+Use Data.Sum.Effectful.Left.Transformer instead."
+#-}
diff --git a/src/Data/Sum/Categorical/Right.agda b/src/Data/Sum/Categorical/Right.agda
new file mode 100644
index 0000000000..724d6a5b3a
--- /dev/null
+++ b/src/Data/Sum/Categorical/Right.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Right` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Right where
+
+open import Data.Sum.Effectful.Right public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Right was deprecated in v2.0.
+Use Data.Sum.Effectful.Right instead."
+#-}
diff --git a/src/Data/Sum/Categorical/Right/Transformer.agda b/src/Data/Sum/Categorical/Right/Transformer.agda
new file mode 100644
index 0000000000..52fbb16f11
--- /dev/null
+++ b/src/Data/Sum/Categorical/Right/Transformer.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Sum.Categorical.Right.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Sum.Categorical.Right.Transformer where
+
+open import Data.Sum.Effectful.Right.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.Sum.Categorical.Right.Transformer was deprecated in v2.0.
+Use Data.Sum.Effectful.Right.Transformer instead."
+#-}
diff --git a/src/Data/These/Categorical/Left.agda b/src/Data/These/Categorical/Left.agda
new file mode 100644
index 0000000000..73576b3bd0
--- /dev/null
+++ b/src/Data/These/Categorical/Left.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.These.Categorical.Left` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.These.Categorical.Left where
+
+open import Data.These.Effectful.Left public
+
+{-# WARNING_ON_IMPORT
+"Data.These.Categorical.Left was deprecated in v2.0.
+Use Data.These.Effectful.Left instead."
+#-}
diff --git a/src/Data/These/Categorical/Left/Base.agda b/src/Data/These/Categorical/Left/Base.agda
new file mode 100644
index 0000000000..7c7e3add7d
--- /dev/null
+++ b/src/Data/These/Categorical/Left/Base.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.These.Categorical.Left.Base` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.These.Categorical.Left.Base where
+
+open import Data.These.Effectful.Left.Base public
+
+{-# WARNING_ON_IMPORT
+"Data.These.Categorical.Left.Base was deprecated in v2.0.
+Use Data.These.Effectful.Left.Base instead."
+#-}
diff --git a/src/Data/These/Categorical/Right.agda b/src/Data/These/Categorical/Right.agda
new file mode 100644
index 0000000000..2e42e8d4a8
--- /dev/null
+++ b/src/Data/These/Categorical/Right.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.These.Categorical.Right` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.These.Categorical.Right where
+
+open import Data.These.Effectful.Right public
+
+{-# WARNING_ON_IMPORT
+"Data.These.Categorical.Right was deprecated in v2.0.
+Use Data.These.Effectful.Right instead."
+#-}
diff --git a/src/Data/These/Categorical/Right/Base.agda b/src/Data/These/Categorical/Right/Base.agda
new file mode 100644
index 0000000000..05acbcf139
--- /dev/null
+++ b/src/Data/These/Categorical/Right/Base.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.These.Categorical.Right.Base` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.These.Categorical.Right.Base where
+
+open import Data.These.Effectful.Right.Base public
+
+{-# WARNING_ON_IMPORT
+"Data.These.Categorical.Right.Base was deprecated in v2.0.
+Use Data.These.Effectful.Right.Base instead."
+#-}
diff --git a/src/Data/Vec/Categorical.agda b/src/Data/Vec/Categorical.agda
new file mode 100644
index 0000000000..aaad325cac
--- /dev/null
+++ b/src/Data/Vec/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Vec.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Categorical where
+
+open import Data.Vec.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.Vec.Categorical was deprecated in v2.0.
+Use Data.Vec.Effectful instead."
+#-}
diff --git a/src/Data/Vec/Categorical/Transformer.agda b/src/Data/Vec/Categorical/Transformer.agda
new file mode 100644
index 0000000000..9d90b030f7
--- /dev/null
+++ b/src/Data/Vec/Categorical/Transformer.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Vec.Effectful.Transformer` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Categorical.Transformer where
+
+open import Data.Vec.Effectful.Transformer public
+
+{-# WARNING_ON_IMPORT
+"Data.Vec.Categorical.Transformer was deprecated in v2.0.
+Use Data.Vec.Effectful.Transformer instead."
+#-}
diff --git a/src/Data/Vec/Recursive/Categorical.agda b/src/Data/Vec/Recursive/Categorical.agda
new file mode 100644
index 0000000000..1dba5fd7b0
--- /dev/null
+++ b/src/Data/Vec/Recursive/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Data.Vec.Recursive.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Recursive.Categorical where
+
+open import Data.Vec.Recursive.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Data.Vec.Recursive.Categorical was deprecated in v2.0.
+Use Data.Vec.Recursive.Effectful instead."
+#-}
diff --git a/src/Function/Identity/Categorical.agda b/src/Function/Identity/Categorical.agda
new file mode 100644
index 0000000000..7fbdec019e
--- /dev/null
+++ b/src/Function/Identity/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Function.Identity.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Function.Identity.Categorical where
+
+open import Function.Identity.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Function.Identity.Categorical was deprecated in v2.0.
+Use Function.Identity.Effectful instead."
+#-}
diff --git a/src/IO/Categorical.agda b/src/IO/Categorical.agda
new file mode 100644
index 0000000000..9e264a5283
--- /dev/null
+++ b/src/IO/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `IO.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --guardedness #-}
+
+module IO.Categorical where
+
+open import IO.Effectful public
+
+{-# WARNING_ON_IMPORT
+"IO.Categorical was deprecated in v2.0.
+Use IO.Effectful instead."
+#-}
diff --git a/src/Reflection/TCM/Categorical.agda b/src/Reflection/TCM/Categorical.agda
new file mode 100644
index 0000000000..f1c5d76319
--- /dev/null
+++ b/src/Reflection/TCM/Categorical.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Reflection.TCM.Effectful` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Reflection.TCM.Categorical where
+
+open import Reflection.TCM.Effectful public
+
+{-# WARNING_ON_IMPORT
+"Reflection.TCM.Categorical was deprecated in v2.0.
+Use Reflection.TCM.Effectful instead."
+#-}