diff --git a/CHANGELOG.md b/CHANGELOG.md
index 812fe00b6c..80bd2f2bc4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -692,6 +692,9 @@ Non-backwards compatible changes
   This reorganisation means in particular that the functor/applicative of a monad
   are not computed using `_>>=_`. This may break proofs.
 
+* When `F : Set f → Set f` we moreover have a definable join/μ operator
+  `join : (M : RawMonad F) → F (F A) → F A`.
+
 * We now have `RawEmpty` and `RawChoice` respectively packing `empty : M A` and
   `(<|>) : M A → M A → M A`. `RawApplicativeZero`, `RawAlternative`, `RawMonadZero`,
   `RawMonadPlus` are all defined in terms of these.
@@ -2593,14 +2596,13 @@ Other minor changes
 
   diagonal           : Vec (Vec A n) n → Vec A n
   DiagonalBind._>>=_ : Vec A n → (A → Vec B n) → Vec B n
-  join               : Vec (Vec A n) n → Vec A n
 
   _ʳ++_              : Vec A m → Vec A n → Vec A (m + n)
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
 
-* Added new instance in `Data.Vec.Categorical`:
+* Added new instance in `Data.Vec.Effectful`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
   ```
diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index fa7280f68f..3d4e557468 100644
--- a/src/Data/List/Effectful.agda
+++ b/src/Data/List/Effectful.agda
@@ -25,6 +25,7 @@ open P.≡-Reasoning
 private
   variable
     ℓ : Level
+    A : Set ℓ
 
 ------------------------------------------------------------------------
 -- List applicative functor
@@ -66,6 +67,9 @@ monad = record
   ; _>>=_  = flip concatMap
   }
 
+join : List (List A) → List A
+join = Join.join monad
+
 monadZero : ∀ {ℓ} → RawMonadZero {ℓ} List
 monadZero = record
   { rawMonad = monad
diff --git a/src/Data/Maybe/Effectful.agda b/src/Data/Maybe/Effectful.agda
index 405b4eab42..7e0bf0216b 100644
--- a/src/Data/Maybe/Effectful.agda
+++ b/src/Data/Maybe/Effectful.agda
@@ -67,6 +67,9 @@ monad = record
   ; _>>=_ = _>>=_
   }
 
+join : Maybe (Maybe A) → Maybe A
+join = Join.join monad
+
 monadZero : RawMonadZero {f} Maybe
 monadZero = record
   { rawMonad = monad
diff --git a/src/Data/Sum/Effectful/Left.agda b/src/Data/Sum/Effectful/Left.agda
index 6d0f453b7b..68c632afe4 100644
--- a/src/Data/Sum/Effectful/Left.agda
+++ b/src/Data/Sum/Effectful/Left.agda
@@ -62,6 +62,9 @@ monad = record
   ; _>>=_ = [ const ∘′ inj₁ , _|>′_ ]′
   }
 
+join : {B : Set (a ⊔ b)} → Sumₗ (Sumₗ B) → Sumₗ B
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
 
diff --git a/src/Data/Sum/Effectful/Right.agda b/src/Data/Sum/Effectful/Right.agda
index 19b4995b1e..7658967128 100644
--- a/src/Data/Sum/Effectful/Right.agda
+++ b/src/Data/Sum/Effectful/Right.agda
@@ -56,6 +56,9 @@ monad = record
   ; _>>=_ = [ _|>′_ , const ∘′ inj₂ ]′
   }
 
+join : {A : Set (a ⊔ b)} → Sumᵣ (Sumᵣ A) → Sumᵣ A
+join = Join.join monad
+
 monadZero : B → RawMonadZero Sumᵣ
 monadZero b = record
   { rawMonad = monad
diff --git a/src/Data/Vec.agda b/src/Data/Vec.agda
index d9f1b89664..62b16e0cc6 100644
--- a/src/Data/Vec.agda
+++ b/src/Data/Vec.agda
@@ -9,7 +9,7 @@
 
 -- See `Data.Vec.Functional` for an alternative implementation as
 -- functions from finite sets, which is more suitable for reasoning
--- about fixed sized vectors and for when ease of retrevial is
+-- about fixed sized vectors and for when ease of retrieval is
 -- important.
 
 {-# OPTIONS --cubical-compatible --safe #-}
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 9f6d86b792..4371f5680c 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -189,8 +189,6 @@ module DiagonalBind where
   _>>=_ : Vec A n → (A → Vec B n) → Vec B n
   xs >>= f = diagonal (map f xs)
 
-  join : Vec (Vec A n) n → Vec A n
-  join = _>>= id
 
 ------------------------------------------------------------------------
 -- Operations for reducing vectors
@@ -358,3 +356,4 @@ last xs with initLast xs
 transpose : Vec (Vec A n) m → Vec (Vec A m) n
 transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
+
diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda
index 5d8e438537..3d4c1a75e7 100644
--- a/src/Data/Vec/Effectful.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -14,7 +14,7 @@ open import Data.Vec.Base as Vec hiding (_⊛_)
 open import Data.Vec.Properties
 open import Effect.Applicative as App using (RawApplicative)
 open import Effect.Functor as Fun using (RawFunctor)
-open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)
+open import Effect.Monad using (RawMonad; module Join; RawMonadT; mkRawMonad)
 import Function.Identity.Effectful as Id
 open import Function.Base
 open import Level using (Level)
@@ -46,6 +46,9 @@ monad = record
   ; _>>=_ = DiagonalBind._>>=_
   }
 
+join : Vec (Vec A n) n → Vec A n
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
 
diff --git a/src/Data/Vec/Effectful/Transformer.agda b/src/Data/Vec/Effectful/Transformer.agda
index 9c3847f40e..cf491fdb84 100644
--- a/src/Data/Vec/Effectful/Transformer.agda
+++ b/src/Data/Vec/Effectful/Transformer.agda
@@ -50,7 +50,7 @@ monad {f} {g} M = record
   ; _>>=_ = λ ma k → mkVecT $ do
                       a ← runVecT ma
                       bs ← mapM {a = f} (runVecT ∘′ k) a
-                      pure (Vec.DiagonalBind.join bs)
+                      pure (Vec.diagonal bs)
   } where open RawMonad M; open Vec.TraversableM {m = f} {n = g} M
 
 monadT : RawMonadT {f} {g} (VecT n)
diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda
index 57e410bf3d..0448f0d6cd 100644
--- a/src/Effect/Monad.agda
+++ b/src/Effect/Monad.agda
@@ -16,7 +16,7 @@ open import Data.Unit.Polymorphic.Base using (⊤)
 open import Effect.Choice
 open import Effect.Empty
 open import Effect.Applicative
-open import Function.Base using (flip; _$′_; _∘′_)
+open import Function.Base using (id; flip; _$′_; _∘′_)
 open import Level using (Level; suc; _⊔_)
 
 private
@@ -58,7 +58,16 @@ record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
   unless : Bool → F ⊤ → F ⊤
   unless = when ∘′ not
 
+-- When level g=f, a join/μ operator is definable
+
+module Join {F : Set f → Set f} (M : RawMonad F) where
+  open RawMonad M
+
+  join : F (F A) → F A
+  join = _>>= id
+
 -- Smart constructor
+
 module _ where
 
   open RawMonad
diff --git a/src/Effect/Monad/Identity.agda b/src/Effect/Monad/Identity.agda
index 3cb7bf9f21..b828d00fcc 100644
--- a/src/Effect/Monad/Identity.agda
+++ b/src/Effect/Monad/Identity.agda
@@ -18,6 +18,7 @@ open import Level
 private
   variable
     a : Level
+    A : Set a
 
 record Identity (A : Set a) : Set a where
   constructor mkIdentity
@@ -47,3 +48,6 @@ comonad = record
   { extract = runIdentity
   ; extend  = λ f a → mkIdentity (f a)
   }
+
+join : Identity (Identity A) → Identity A
+join = Join.join monad
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index 194b079339..5fb6ec3455 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -72,6 +72,9 @@ monad = record
   ; _>>=_  = bind
   }
 
+join : (A ⊥) ⊥ → A ⊥
+join = Join.join monad
+
 private module M {f} = RawMonad (monad {f})
 
 -- Non-termination.
diff --git a/src/Effect/Monad/Reader.agda b/src/Effect/Monad/Reader.agda
index 79267a5ab2..42e6091d00 100644
--- a/src/Effect/Monad/Reader.agda
+++ b/src/Effect/Monad/Reader.agda
@@ -52,6 +52,9 @@ applicative = Trans.applicative Id.applicative
 monad : RawMonad (Reader R)
 monad = Trans.monad Id.monad
 
+join : Reader R (Reader R A) → Reader R A
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- Reader monad specifics
 
diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda
index 41fc3336d8..2b06c8b087 100644
--- a/src/Effect/Monad/State.agda
+++ b/src/Effect/Monad/State.agda
@@ -59,6 +59,9 @@ applicative = Trans.applicative Id.monad
 monad : RawMonad (State S)
 monad = Trans.monad Id.monad
 
+join : State S (State S A) → State S A
+join = Join.join monad
+
 ------------------------------------------------------------------------
 -- State monad specifics
 
diff --git a/src/Effect/Monad/Writer.agda b/src/Effect/Monad/Writer.agda
index 489c7f4347..60f4dc2b72 100644
--- a/src/Effect/Monad/Writer.agda
+++ b/src/Effect/Monad/Writer.agda
@@ -55,6 +55,9 @@ module _ {𝕎 : RawMonoid w ℓ} where
   monad : RawMonad (Writer 𝕎)
   monad = Trans.monad Id.monad
 
+  join : Writer 𝕎 (Writer 𝕎 A) → Writer 𝕎 A
+  join = Join.join monad
+
   ----------------------------------------------------------------------
   -- Writer monad specifics