From f9ced40321b8f1e68107671e8fc2da8c58225771 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 31 Aug 2023 19:23:41 +0100
Subject: [PATCH 01/15] added `RawMonadWithJoin` plus instances

---
 CHANGELOG.md                      |  6 +++-
 src/Data/List/Effectful.agda      |  3 ++
 src/Data/Maybe/Effectful.agda     |  3 ++
 src/Data/Sum/Effectful/Left.agda  |  3 ++
 src/Data/Sum/Effectful/Right.agda |  3 ++
 src/Data/Vec/Effectful.agda       |  6 +++-
 src/Effect/Monad.agda             | 50 ++++++++++++++++++++-----------
 7 files changed, 54 insertions(+), 20 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 812fe00b6c..9427b0468d 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.
 
+* We now have `RawMonadWithJoin` packing `join : F (F A) → F A` with an underlying
+  `rawMonad : RawMonad F` when `F : Set f → Set f`.
+
 * 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.
@@ -2600,9 +2603,10 @@ Other minor changes
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
 
-* Added new instance in `Data.Vec.Categorical`:
+* Added new instances in `Data.Vec.Effectful`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
+  monadWithJoin : RawMonadWithJoin (λ (A : Set a) → Vec A n)
   ```
 
 * Added new proofs in `Data.Vec.Properties`:
diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index fa7280f68f..1c63fed589 100644
--- a/src/Data/List/Effectful.agda
+++ b/src/Data/List/Effectful.agda
@@ -66,6 +66,9 @@ monad = record
   ; _>>=_  = flip concatMap
   }
 
+monadWithJoin : ∀ {ℓ} → RawMonadWithJoin {ℓ} List
+monadWithJoin = record { rawMonad = monad }
+
 monadZero : ∀ {ℓ} → RawMonadZero {ℓ} List
 monadZero = record
   { rawMonad = monad
diff --git a/src/Data/Maybe/Effectful.agda b/src/Data/Maybe/Effectful.agda
index 405b4eab42..4c6d59c60d 100644
--- a/src/Data/Maybe/Effectful.agda
+++ b/src/Data/Maybe/Effectful.agda
@@ -67,6 +67,9 @@ monad = record
   ; _>>=_ = _>>=_
   }
 
+monadWithJoin : RawMonadWithJoin {f} Maybe
+monadWithJoin = record { rawMonad = 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..e296a3264c 100644
--- a/src/Data/Sum/Effectful/Left.agda
+++ b/src/Data/Sum/Effectful/Left.agda
@@ -62,6 +62,9 @@ monad = record
   ; _>>=_ = [ const ∘′ inj₁ , _|>′_ ]′
   }
 
+monadWithJoin : RawMonadWithJoin Sumₗ
+monadWithJoin = record { rawMonad = 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..9ecfad01f4 100644
--- a/src/Data/Sum/Effectful/Right.agda
+++ b/src/Data/Sum/Effectful/Right.agda
@@ -56,6 +56,9 @@ monad = record
   ; _>>=_ = [ _|>′_ , const ∘′ inj₂ ]′
   }
 
+monadWithJoin : RawMonadWithJoin Sumᵣ
+monadWithJoin = record { rawMonad = monad }
+
 monadZero : B → RawMonadZero Sumᵣ
 monadZero b = record
   { rawMonad = monad
diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda
index 5d8e438537..eb834217e3 100644
--- a/src/Data/Vec/Effectful.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -14,7 +14,8 @@ 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; RawMonadWithJoin; RawMonadT; mkRawMonad; mkRawMonadWithJoin)
 import Function.Identity.Effectful as Id
 open import Function.Base
 open import Level using (Level)
@@ -46,6 +47,9 @@ monad = record
   ; _>>=_ = DiagonalBind._>>=_
   }
 
+monadWithJoin : RawMonadWithJoin (λ (A : Set a) → Vec A n)
+monadWithJoin = record { rawMonad = monad }
+
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
 
diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda
index 57e410bf3d..178fde7d2a 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,23 +58,37 @@ record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
   unless : Bool → F ⊤ → F ⊤
   unless = when ∘′ not
 
--- Smart constructor
-module _ where
-
-  open RawMonad
-  open RawApplicative
-
-  mkRawMonad :
-    (F : Set f → Set f) →
-    (pure : ∀ {A} → A → F A) →
-    (bind : ∀ {A B} → F A → (A → F B) → F B) →
-    RawMonad F
-  mkRawMonad F pure _>>=_ .rawApplicative =
-    mkRawApplicative _ pure $′ λ mf mx → do
-      f ← mf
-      x ← mx
-      pure (f x)
-  mkRawMonad F pure _>>=_ ._>>=_ = _>>=_
+-- When g=f, a join/μ operator is definable
+
+record RawMonadWithJoin (F : Set f → Set f) : Set (suc f) where
+
+  field
+    rawMonad : RawMonad F
+
+  open RawMonad rawMonad public
+
+  join : F (F A) → F A
+  join = _>>= id
+
+
+-- Smart constructors
+
+module _ (F : Set f → Set f)
+         (pure : ∀ {A} → A → F A)
+         (bind : ∀ {A B} → F A → (A → F B) → F B)
+  where
+
+  open RawMonadWithJoin using (rawMonad)
+  open RawMonad using (rawApplicative; _>>=_)
+  open RawApplicative hiding (pure)
+
+  mkRawMonad : RawMonad F
+  mkRawMonad .rawApplicative = mkRawApplicative F pure
+    λ mf mx → bind mf λ f → bind mx λ x → pure (f x)
+  mkRawMonad ._>>=_ = bind
+
+  mkRawMonadWithJoin : RawMonadWithJoin F
+  mkRawMonadWithJoin .rawMonad = mkRawMonad
 
 ------------------------------------------------------------------------
 -- The type of raw monads with a zero

From 8e7588b3a56c49a2494bf22e75390f341792b3bf Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 1 Sep 2023 07:13:40 +0100
Subject: [PATCH 02/15] added more instances

---
 src/Effect/Monad/Identity.agda   | 3 +++
 src/Effect/Monad/Partiality.agda | 3 +++
 src/Effect/Monad/Reader.agda     | 3 +++
 src/Effect/Monad/State.agda      | 3 +++
 src/Effect/Monad/Writer.agda     | 3 +++
 5 files changed, 15 insertions(+)

diff --git a/src/Effect/Monad/Identity.agda b/src/Effect/Monad/Identity.agda
index 3cb7bf9f21..086537a09c 100644
--- a/src/Effect/Monad/Identity.agda
+++ b/src/Effect/Monad/Identity.agda
@@ -47,3 +47,6 @@ comonad = record
   { extract = runIdentity
   ; extend  = λ f a → mkIdentity (f a)
   }
+
+monadWithJoin : RawMonadWithJoin {a} Identity
+monadWithJoin = record { rawMonad = monad }
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index 194b079339..ef304b38c2 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -72,6 +72,9 @@ monad = record
   ; _>>=_  = bind
   }
 
+monadWithJoin : RawMonadWithJoin {f = f} _⊥
+monadWithJoin = record { rawMonad = 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..2535dacf4b 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
 
+monadWithJoin : RawMonadWithJoin (Reader R)
+monadWithJoin = record { rawMonad = monad }
+
 ------------------------------------------------------------------------
 -- Reader monad specifics
 
diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda
index 41fc3336d8..4c08b7061c 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
 
+monadWithJoin : RawMonadWithJoin (State S)
+monadWithJoin = record { rawMonad = monad }
+
 ------------------------------------------------------------------------
 -- State monad specifics
 
diff --git a/src/Effect/Monad/Writer.agda b/src/Effect/Monad/Writer.agda
index 489c7f4347..07eabd254e 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
 
+  monadWithJoin : RawMonadWithJoin (Writer 𝕎)
+  monadWithJoin = record { rawMonad = monad }
+
   ----------------------------------------------------------------------
   -- Writer monad specifics
 

From 8f080c54b64ec70628267affb25891b5b57abfbc Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 1 Sep 2023 18:11:58 +0100
Subject: [PATCH 03/15] as per Guillaume's suggestion

---
 CHANGELOG.md                      |  5 ++--
 src/Data/List/Effectful.agda      |  5 ++--
 src/Data/Maybe/Effectful.agda     |  4 ++--
 src/Data/Sum/Effectful/Left.agda  |  4 ++--
 src/Data/Sum/Effectful/Right.agda |  4 ++--
 src/Data/Vec/Effectful.agda       |  7 +++---
 src/Effect/Monad.agda             | 40 ++++++++++++++-----------------
 src/Effect/Monad/Identity.agda    |  5 ++--
 src/Effect/Monad/Partiality.agda  |  4 ++--
 src/Effect/Monad/Reader.agda      |  4 ++--
 src/Effect/Monad/State.agda       |  4 ++--
 src/Effect/Monad/Writer.agda      |  4 ++--
 12 files changed, 43 insertions(+), 47 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9427b0468d..5373af8776 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -692,8 +692,8 @@ Non-backwards compatible changes
   This reorganisation means in particular that the functor/applicative of a monad
   are not computed using `_>>=_`. This may break proofs.
 
-* We now have `RawMonadWithJoin` packing `join : F (F A) → F A` with an underlying
-  `rawMonad : RawMonad F` when `F : Set f → Set f`.
+* When `F : Set f → Set f` we moreover have a definable join/μ operator
+  `join : ⦃ M : RawMonad {f} {f} 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`,
@@ -2606,7 +2606,6 @@ Other minor changes
 * Added new instances in `Data.Vec.Effectful`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
-  monadWithJoin : RawMonadWithJoin (λ (A : Set a) → Vec A n)
   ```
 
 * Added new proofs in `Data.Vec.Properties`:
diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index 1c63fed589..9821220d2b 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,8 +67,8 @@ monad = record
   ; _>>=_  = flip concatMap
   }
 
-monadWithJoin : ∀ {ℓ} → RawMonadWithJoin {ℓ} List
-monadWithJoin = record { rawMonad = monad }
+join : List (List A) → List A
+join = Join.join where instance _ = monad
 
 monadZero : ∀ {ℓ} → RawMonadZero {ℓ} List
 monadZero = record
diff --git a/src/Data/Maybe/Effectful.agda b/src/Data/Maybe/Effectful.agda
index 4c6d59c60d..02fa005267 100644
--- a/src/Data/Maybe/Effectful.agda
+++ b/src/Data/Maybe/Effectful.agda
@@ -67,8 +67,8 @@ monad = record
   ; _>>=_ = _>>=_
   }
 
-monadWithJoin : RawMonadWithJoin {f} Maybe
-monadWithJoin = record { rawMonad = monad }
+join : Maybe (Maybe A) → Maybe A
+join = Join.join where instance _ = monad
 
 monadZero : RawMonadZero {f} Maybe
 monadZero = record
diff --git a/src/Data/Sum/Effectful/Left.agda b/src/Data/Sum/Effectful/Left.agda
index e296a3264c..0a7e9869f4 100644
--- a/src/Data/Sum/Effectful/Left.agda
+++ b/src/Data/Sum/Effectful/Left.agda
@@ -62,8 +62,8 @@ monad = record
   ; _>>=_ = [ const ∘′ inj₁ , _|>′_ ]′
   }
 
-monadWithJoin : RawMonadWithJoin Sumₗ
-monadWithJoin = record { rawMonad = monad }
+join : {B : Set (a ⊔ b)} → Sumₗ (Sumₗ B) → Sumₗ B
+join = Join.join where instance _ = monad
 
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
diff --git a/src/Data/Sum/Effectful/Right.agda b/src/Data/Sum/Effectful/Right.agda
index 9ecfad01f4..f07a589d4d 100644
--- a/src/Data/Sum/Effectful/Right.agda
+++ b/src/Data/Sum/Effectful/Right.agda
@@ -56,8 +56,8 @@ monad = record
   ; _>>=_ = [ _|>′_ , const ∘′ inj₂ ]′
   }
 
-monadWithJoin : RawMonadWithJoin Sumᵣ
-monadWithJoin = record { rawMonad = monad }
+join : {A : Set (a ⊔ b)} → Sumᵣ (Sumᵣ A) → Sumᵣ A
+join = Join.join where instance _ = monad
 
 monadZero : B → RawMonadZero Sumᵣ
 monadZero b = record
diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda
index eb834217e3..cf3f25144b 100644
--- a/src/Data/Vec/Effectful.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -14,8 +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; RawMonadWithJoin; RawMonadT; mkRawMonad; mkRawMonadWithJoin)
+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)
@@ -47,8 +46,8 @@ monad = record
   ; _>>=_ = DiagonalBind._>>=_
   }
 
-monadWithJoin : RawMonadWithJoin (λ (A : Set a) → Vec A n)
-monadWithJoin = record { rawMonad = monad }
+join : Vec (Vec A n) n → Vec A n
+join = Join.join where instance _ = monad
 
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda
index 178fde7d2a..179fc90e82 100644
--- a/src/Effect/Monad.agda
+++ b/src/Effect/Monad.agda
@@ -58,37 +58,33 @@ record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
   unless : Bool → F ⊤ → F ⊤
   unless = when ∘′ not
 
--- When g=f, a join/μ operator is definable
+-- When level g=f, a join/μ operator is definable
 
-record RawMonadWithJoin (F : Set f → Set f) : Set (suc f) where
-
-  field
-    rawMonad : RawMonad F
-
-  open RawMonad rawMonad public
+module Join {F : Set f → Set f} ⦃ M : RawMonad {f} {f} F ⦄ where
+  open RawMonad M
 
   join : F (F A) → F A
   join = _>>= id
 
 
--- Smart constructors
-
-module _ (F : Set f → Set f)
-         (pure : ∀ {A} → A → F A)
-         (bind : ∀ {A B} → F A → (A → F B) → F B)
-  where
+-- Smart constructor
 
-  open RawMonadWithJoin using (rawMonad)
-  open RawMonad using (rawApplicative; _>>=_)
-  open RawApplicative hiding (pure)
+module _ where
 
-  mkRawMonad : RawMonad F
-  mkRawMonad .rawApplicative = mkRawApplicative F pure
-    λ mf mx → bind mf λ f → bind mx λ x → pure (f x)
-  mkRawMonad ._>>=_ = bind
+  open RawMonad
+  open RawApplicative
 
-  mkRawMonadWithJoin : RawMonadWithJoin F
-  mkRawMonadWithJoin .rawMonad = mkRawMonad
+  mkRawMonad :
+    (F : Set f → Set f) →
+    (pure : ∀ {A} → A → F A) →
+    (bind : ∀ {A B} → F A → (A → F B) → F B) →
+    RawMonad F
+  mkRawMonad F pure _>>=_ .rawApplicative =
+    mkRawApplicative _ pure $′ λ mf mx → do
+      f ← mf
+      x ← mx
+      pure (f x)
+  mkRawMonad F pure _>>=_ ._>>=_ = _>>=_
 
 ------------------------------------------------------------------------
 -- The type of raw monads with a zero
diff --git a/src/Effect/Monad/Identity.agda b/src/Effect/Monad/Identity.agda
index 086537a09c..d855805ddd 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
@@ -48,5 +49,5 @@ comonad = record
   ; extend  = λ f a → mkIdentity (f a)
   }
 
-monadWithJoin : RawMonadWithJoin {a} Identity
-monadWithJoin = record { rawMonad = monad }
+join : Identity (Identity A) → Identity A
+join = Join.join where instance _ = monad
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index ef304b38c2..b158617b94 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -72,8 +72,8 @@ monad = record
   ; _>>=_  = bind
   }
 
-monadWithJoin : RawMonadWithJoin {f = f} _⊥
-monadWithJoin = record { rawMonad = monad }
+join : (A ⊥) ⊥ → A ⊥
+join = Join.join where instance _ = monad
 
 private module M {f} = RawMonad (monad {f})
 
diff --git a/src/Effect/Monad/Reader.agda b/src/Effect/Monad/Reader.agda
index 2535dacf4b..ced383bfac 100644
--- a/src/Effect/Monad/Reader.agda
+++ b/src/Effect/Monad/Reader.agda
@@ -52,8 +52,8 @@ applicative = Trans.applicative Id.applicative
 monad : RawMonad (Reader R)
 monad = Trans.monad Id.monad
 
-monadWithJoin : RawMonadWithJoin (Reader R)
-monadWithJoin = record { rawMonad = monad }
+join : Reader R (Reader R A) → Reader R A
+join = Join.join where instance _ = monad
 
 ------------------------------------------------------------------------
 -- Reader monad specifics
diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda
index 4c08b7061c..d58b3eeedf 100644
--- a/src/Effect/Monad/State.agda
+++ b/src/Effect/Monad/State.agda
@@ -59,8 +59,8 @@ applicative = Trans.applicative Id.monad
 monad : RawMonad (State S)
 monad = Trans.monad Id.monad
 
-monadWithJoin : RawMonadWithJoin (State S)
-monadWithJoin = record { rawMonad = monad }
+join : State S (State S A) → State S A
+join = Join.join where instance _ = monad
 
 ------------------------------------------------------------------------
 -- State monad specifics
diff --git a/src/Effect/Monad/Writer.agda b/src/Effect/Monad/Writer.agda
index 07eabd254e..1d11f01556 100644
--- a/src/Effect/Monad/Writer.agda
+++ b/src/Effect/Monad/Writer.agda
@@ -55,8 +55,8 @@ module _ {𝕎 : RawMonoid w ℓ} where
   monad : RawMonad (Writer 𝕎)
   monad = Trans.monad Id.monad
 
-  monadWithJoin : RawMonadWithJoin (Writer 𝕎)
-  monadWithJoin = record { rawMonad = monad }
+  join : Writer 𝕎 (Writer 𝕎 A) → Writer 𝕎 A
+  join = Join.join where instance _ = monad
 
   ----------------------------------------------------------------------
   -- Writer monad specifics

From 5ddc0500bede15158641475b7f0163bdd70e2d2a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 1 Sep 2023 18:23:15 +0100
Subject: [PATCH 04/15] tidying up

---
 CHANGELOG.md          | 4 ++--
 src/Effect/Monad.agda | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5373af8776..6f6472b267 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -693,7 +693,7 @@ Non-backwards compatible changes
   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 ⦄ → F (F A) → F A`.
+  `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`,
@@ -2603,7 +2603,7 @@ Other minor changes
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
 
-* Added new instances in `Data.Vec.Effectful`:
+* Added new instance in `Data.Vec.Effectful`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
   ```
diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda
index 179fc90e82..96fb95095f 100644
--- a/src/Effect/Monad.agda
+++ b/src/Effect/Monad.agda
@@ -60,13 +60,12 @@ record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
 
 -- When level g=f, a join/μ operator is definable
 
-module Join {F : Set f → Set f} ⦃ M : RawMonad {f} {f} F ⦄ where
+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

From 5e34552dbbf88ce68206709d3500d453bfec4772 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 2 Sep 2023 16:33:11 +0100
Subject: [PATCH 05/15] deprecated `Data.Vec.Base.join`

---
 CHANGELOG.md           |  5 +++++
 src/Data/Vec/Base.agda | 20 +++++++++++++++++---
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6f6472b267..f07096476a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1393,6 +1393,11 @@ Deprecated names
   map-compose     ↦  map-∘
   ```
 
+* In `Data.Vec.Base`:
+  ```
+  join ↦  Data.Vec.Effectful.join
+  ```
+
 * In `Data.Vec.Properties`:
   ```
   updateAt-id-relative      ↦  updateAt-id-local
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 9f6d86b792..e8cbabefbb 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -189,9 +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 +355,20 @@ 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
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+join : Vec (Vec A n) n → Vec A n
+join = _>>= id where open DiagonalBind
+
+{-# WARNING_ON_USAGE join
+"Warning: join was deprecated in v2.0
+Please use Data.Vec.Effectful.join instead."
+#-}

From fc87627a3ae17334a3c2415679084c52aef77bea Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 2 Sep 2023 16:47:15 +0100
Subject: [PATCH 06/15] hide `join` on import

---
 src/Data/Vec/Effectful.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda
index cf3f25144b..9cec18aadc 100644
--- a/src/Data/Vec/Effectful.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -10,7 +10,7 @@ module Data.Vec.Effectful where
 
 open import Data.Nat.Base using (ℕ)
 open import Data.Fin.Base using (Fin)
-open import Data.Vec.Base as Vec hiding (_⊛_)
+open import Data.Vec.Base as Vec hiding (_⊛_; join)
 open import Data.Vec.Properties
 open import Effect.Applicative as App using (RawApplicative)
 open import Effect.Functor as Fun using (RawFunctor)

From e315619b741f3bd217618aeda7d969cc19dab46b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 2 Sep 2023 18:30:54 +0100
Subject: [PATCH 07/15] fixed `import` problem

---
 src/Data/Vec/Effectful/Transformer.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec/Effectful/Transformer.agda b/src/Data/Vec/Effectful/Transformer.agda
index 9c3847f40e..9b22fd96e7 100644
--- a/src/Data/Vec/Effectful/Transformer.agda
+++ b/src/Data/Vec/Effectful/Transformer.agda
@@ -16,7 +16,7 @@ open import Effect.Monad
 open import Function.Base
 open import Level
 
-import Data.Vec.Effectful as Vec
+open import Data.Vec.Effectful as Vec using (join)
 
 private
   variable
@@ -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 (join bs)
   } where open RawMonad M; open Vec.TraversableM {m = f} {n = g} M
 
 monadT : RawMonadT {f} {g} (VecT n)

From 3cff6e971e0c795a4bcd97cf655c5c9f2e73e31b Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 2 Sep 2023 18:31:30 +0100
Subject: [PATCH 08/15] fixed typo

---
 src/Data/Vec.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 #-}

From e00b84c025da2778b8eb15459c3bb4b4ae45e99c Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 9 Sep 2023 10:20:06 +0100
Subject: [PATCH 09/15] correctly reinstated `DiagonalBind.join` for its
 deprecation

---
 CHANGELOG.md           |  2 +-
 src/Data/Vec/Base.agda | 11 ++++++-----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f07096476a..b6d21f0789 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1395,7 +1395,7 @@ Deprecated names
 
 * In `Data.Vec.Base`:
   ```
-  join ↦  Data.Vec.Effectful.join
+  DiagonalBind.join ↦  Data.Vec.Effectful.join
   ```
 
 * In `Data.Vec.Properties`:
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index e8cbabefbb..4fec6dba20 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -189,6 +189,10 @@ 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 = diagonal
+
+
 ------------------------------------------------------------------------
 -- Operations for reducing vectors
 
@@ -365,10 +369,7 @@ transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
 
 -- Version 2.0
 
-join : Vec (Vec A n) n → Vec A n
-join = _>>= id where open DiagonalBind
-
-{-# WARNING_ON_USAGE join
-"Warning: join was deprecated in v2.0
+{-# WARNING_ON_USAGE DiagonalBind.join
+"Warning: DiagonalBind.join was deprecated in v2.0
 Please use Data.Vec.Effectful.join instead."
 #-}

From c08caac6aa8175dc0a650cfab3ee34f1b094c84c Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 9 Sep 2023 10:30:07 +0100
Subject: [PATCH 10/15] and have now removed it

---
 CHANGELOG.md           | 6 ------
 src/Data/Vec/Base.agda | 8 --------
 2 files changed, 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b6d21f0789..89aa9b5e26 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1393,11 +1393,6 @@ Deprecated names
   map-compose     ↦  map-∘
   ```
 
-* In `Data.Vec.Base`:
-  ```
-  DiagonalBind.join ↦  Data.Vec.Effectful.join
-  ```
-
 * In `Data.Vec.Properties`:
   ```
   updateAt-id-relative      ↦  updateAt-id-local
@@ -2601,7 +2596,6 @@ 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)
 
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 4fec6dba20..36190cfe98 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -189,9 +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 = diagonal
-
 
 ------------------------------------------------------------------------
 -- Operations for reducing vectors
@@ -368,8 +365,3 @@ transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
 -- not guaranteed.
 
 -- Version 2.0
-
-{-# WARNING_ON_USAGE DiagonalBind.join
-"Warning: DiagonalBind.join was deprecated in v2.0
-Please use Data.Vec.Effectful.join instead."
-#-}

From 723eead405ec7c93bd40bf32d2ac3f1088fbbfc9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 9 Sep 2023 10:38:11 +0100
Subject: [PATCH 11/15] ... and now removed reference to it

---
 src/Data/Vec/Effectful.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda
index 9cec18aadc..cf3f25144b 100644
--- a/src/Data/Vec/Effectful.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -10,7 +10,7 @@ module Data.Vec.Effectful where
 
 open import Data.Nat.Base using (ℕ)
 open import Data.Fin.Base using (Fin)
-open import Data.Vec.Base as Vec hiding (_⊛_; join)
+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)

From e95bf760a3b1c9b0aa32784a31e8452578c62187 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 9 Sep 2023 10:44:11 +0100
Subject: [PATCH 12/15] simplified imports, in favour of
 `Data.Vec.Base.diagonal`

---
 src/Data/Vec/Effectful/Transformer.agda | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Data/Vec/Effectful/Transformer.agda b/src/Data/Vec/Effectful/Transformer.agda
index 9b22fd96e7..77ee70e3c7 100644
--- a/src/Data/Vec/Effectful/Transformer.agda
+++ b/src/Data/Vec/Effectful/Transformer.agda
@@ -9,15 +9,13 @@
 module Data.Vec.Effectful.Transformer where
 
 open import Data.Nat.Base using (ℕ)
-open import Data.Vec.Base as Vec using (Vec; []; _∷_)
+open import Data.Vec.Base as Vec using (Vec; []; _∷_; diagonal)
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
 open import Function.Base
 open import Level
 
-open import Data.Vec.Effectful as Vec using (join)
-
 private
   variable
     f g : Level
@@ -50,7 +48,7 @@ monad {f} {g} M = record
   ; _>>=_ = λ ma k → mkVecT $ do
                       a ← runVecT ma
                       bs ← mapM {a = f} (runVecT ∘′ k) a
-                      pure (join bs)
+                      pure (diagonal bs)
   } where open RawMonad M; open Vec.TraversableM {m = f} {n = g} M
 
 monadT : RawMonadT {f} {g} (VecT n)

From d4f71bfed53633629a54cdb2e901eaa656c0ce98 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Sat, 9 Sep 2023 10:52:02 +0100
Subject: [PATCH 13/15] fixed `import` bug

---
 src/Data/Vec/Effectful/Transformer.agda | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec/Effectful/Transformer.agda b/src/Data/Vec/Effectful/Transformer.agda
index 77ee70e3c7..cf491fdb84 100644
--- a/src/Data/Vec/Effectful/Transformer.agda
+++ b/src/Data/Vec/Effectful/Transformer.agda
@@ -9,13 +9,15 @@
 module Data.Vec.Effectful.Transformer where
 
 open import Data.Nat.Base using (ℕ)
-open import Data.Vec.Base as Vec using (Vec; []; _∷_; diagonal)
+open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
 open import Function.Base
 open import Level
 
+import Data.Vec.Effectful as Vec
+
 private
   variable
     f g : Level
@@ -48,7 +50,7 @@ monad {f} {g} M = record
   ; _>>=_ = λ ma k → mkVecT $ do
                       a ← runVecT ma
                       bs ← mapM {a = f} (runVecT ∘′ k) a
-                      pure (diagonal bs)
+                      pure (Vec.diagonal bs)
   } where open RawMonad M; open Vec.TraversableM {m = f} {n = g} M
 
 monadT : RawMonadT {f} {g} (VecT n)

From dffbad3688709e76153c7dfcd2bda2e777c103f0 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 13 Sep 2023 00:56:19 +0100
Subject: [PATCH 14/15] made `monad` an explicit argument to `Join.join`

---
 CHANGELOG.md                      | 2 +-
 src/Data/List/Effectful.agda      | 2 +-
 src/Data/Maybe/Effectful.agda     | 2 +-
 src/Data/Sum/Effectful/Left.agda  | 2 +-
 src/Data/Sum/Effectful/Right.agda | 2 +-
 src/Data/Vec/Base.agda            | 7 -------
 src/Data/Vec/Effectful.agda       | 2 +-
 src/Effect/Monad.agda             | 2 +-
 src/Effect/Monad/Identity.agda    | 2 +-
 src/Effect/Monad/Partiality.agda  | 2 +-
 src/Effect/Monad/Reader.agda      | 2 +-
 src/Effect/Monad/State.agda       | 2 +-
 src/Effect/Monad/Writer.agda      | 2 +-
 13 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89aa9b5e26..80bd2f2bc4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -693,7 +693,7 @@ Non-backwards compatible changes
   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`.
+  `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`,
diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index 9821220d2b..3d4e557468 100644
--- a/src/Data/List/Effectful.agda
+++ b/src/Data/List/Effectful.agda
@@ -68,7 +68,7 @@ monad = record
   }
 
 join : List (List A) → List A
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 monadZero : ∀ {ℓ} → RawMonadZero {ℓ} List
 monadZero = record
diff --git a/src/Data/Maybe/Effectful.agda b/src/Data/Maybe/Effectful.agda
index 02fa005267..7e0bf0216b 100644
--- a/src/Data/Maybe/Effectful.agda
+++ b/src/Data/Maybe/Effectful.agda
@@ -68,7 +68,7 @@ monad = record
   }
 
 join : Maybe (Maybe A) → Maybe A
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 monadZero : RawMonadZero {f} Maybe
 monadZero = record
diff --git a/src/Data/Sum/Effectful/Left.agda b/src/Data/Sum/Effectful/Left.agda
index 0a7e9869f4..68c632afe4 100644
--- a/src/Data/Sum/Effectful/Left.agda
+++ b/src/Data/Sum/Effectful/Left.agda
@@ -63,7 +63,7 @@ monad = record
   }
 
 join : {B : Set (a ⊔ b)} → Sumₗ (Sumₗ B) → Sumₗ B
-join = Join.join where instance _ = monad
+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 f07a589d4d..7658967128 100644
--- a/src/Data/Sum/Effectful/Right.agda
+++ b/src/Data/Sum/Effectful/Right.agda
@@ -57,7 +57,7 @@ monad = record
   }
 
 join : {A : Set (a ⊔ b)} → Sumᵣ (Sumᵣ A) → Sumᵣ A
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 monadZero : B → RawMonadZero Sumᵣ
 monadZero b = record
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 36190cfe98..967f856568 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -358,10 +358,3 @@ transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
 
 
-------------------------------------------------------------------------
--- DEPRECATED
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 2.0
diff --git a/src/Data/Vec/Effectful.agda b/src/Data/Vec/Effectful.agda
index cf3f25144b..3d4c1a75e7 100644
--- a/src/Data/Vec/Effectful.agda
+++ b/src/Data/Vec/Effectful.agda
@@ -47,7 +47,7 @@ monad = record
   }
 
 join : Vec (Vec A n) n → Vec A n
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 ------------------------------------------------------------------------
 -- Get access to other monadic functions
diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda
index 96fb95095f..0448f0d6cd 100644
--- a/src/Effect/Monad.agda
+++ b/src/Effect/Monad.agda
@@ -60,7 +60,7 @@ record RawMonad (F : Set f → Set g) : Set (suc f ⊔ g) where
 
 -- When level g=f, a join/μ operator is definable
 
-module Join {F : Set f → Set f} ⦃ M : RawMonad F ⦄ where
+module Join {F : Set f → Set f} (M : RawMonad F) where
   open RawMonad M
 
   join : F (F A) → F A
diff --git a/src/Effect/Monad/Identity.agda b/src/Effect/Monad/Identity.agda
index d855805ddd..b828d00fcc 100644
--- a/src/Effect/Monad/Identity.agda
+++ b/src/Effect/Monad/Identity.agda
@@ -50,4 +50,4 @@ comonad = record
   }
 
 join : Identity (Identity A) → Identity A
-join = Join.join where instance _ = monad
+join = Join.join monad
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index b158617b94..5fb6ec3455 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -73,7 +73,7 @@ monad = record
   }
 
 join : (A ⊥) ⊥ → A ⊥
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 private module M {f} = RawMonad (monad {f})
 
diff --git a/src/Effect/Monad/Reader.agda b/src/Effect/Monad/Reader.agda
index ced383bfac..42e6091d00 100644
--- a/src/Effect/Monad/Reader.agda
+++ b/src/Effect/Monad/Reader.agda
@@ -53,7 +53,7 @@ monad : RawMonad (Reader R)
 monad = Trans.monad Id.monad
 
 join : Reader R (Reader R A) → Reader R A
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 ------------------------------------------------------------------------
 -- Reader monad specifics
diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda
index d58b3eeedf..2b06c8b087 100644
--- a/src/Effect/Monad/State.agda
+++ b/src/Effect/Monad/State.agda
@@ -60,7 +60,7 @@ monad : RawMonad (State S)
 monad = Trans.monad Id.monad
 
 join : State S (State S A) → State S A
-join = Join.join where instance _ = monad
+join = Join.join monad
 
 ------------------------------------------------------------------------
 -- State monad specifics
diff --git a/src/Effect/Monad/Writer.agda b/src/Effect/Monad/Writer.agda
index 1d11f01556..60f4dc2b72 100644
--- a/src/Effect/Monad/Writer.agda
+++ b/src/Effect/Monad/Writer.agda
@@ -56,7 +56,7 @@ module _ {𝕎 : RawMonoid w ℓ} where
   monad = Trans.monad Id.monad
 
   join : Writer 𝕎 (Writer 𝕎 A) → Writer 𝕎 A
-  join = Join.join where instance _ = monad
+  join = Join.join monad
 
   ----------------------------------------------------------------------
   -- Writer monad specifics

From d2c54e378a688e2119e8d27d3ae561d3e342a15e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 13 Sep 2023 01:09:00 +0100
Subject: [PATCH 15/15] `fix-whitespace`

---
 src/Data/Vec/Base.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 967f856568..4371f5680c 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -357,4 +357,3 @@ transpose : Vec (Vec A n) m → Vec (Vec A m) n
 transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
 
-