6 files changed, 15 insertions, 30 deletions
diff --git a/src/Category/Monad/Continuation.agda b/src/Category/Monad/Continuation.agda
index 396f75c..f112541 100644
--- a/src/Category/Monad/Continuation.agda
+++ b/src/Category/Monad/Continuation.agda
@@ -9,7 +9,7 @@ module Category.Monad.Continuation where
 open import Category.Applicative
 open import Category.Applicative.Indexed
 open import Category.Monad
-open import Category.Monad.Identity
+open import Function.Identity.Categorical as Id using (Identity)
 open import Category.Monad.Indexed
 open import Function
 open import Level
@@ -32,7 +32,7 @@ DContTIMonad K Mon = record
   where open RawMonad Mon
 
 DContIMonad : ∀ {i f} {I : Set i} (K : I → Set f) → RawIMonad (DCont K)
-DContIMonad K = DContTIMonad K IdentityMonad
+DContIMonad K = DContTIMonad K Id.monad
 
 ------------------------------------------------------------------------
 -- Delimited continuation operations
@@ -59,4 +59,4 @@ DContTIMonadDCont K Mon = record
 
 DContIMonadDCont : ∀ {i f} {I : Set i}
                    (K : I → Set f) → RawIMonadDCont K (DCont K)
-DContIMonadDCont K = DContTIMonadDCont K IdentityMonad
+DContIMonadDCont K = DContTIMonadDCont K Id.monad
diff --git a/src/Category/Monad/Identity.agda b/src/Category/Monad/Identity.agda
deleted file mode 100644
index f01c249..0000000
--- a/src/Category/Monad/Identity.agda
+++ /dev/null
@@ -1,18 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- The identity monad
-------------------------------------------------------------------------
-
-module Category.Monad.Identity where
-
-open import Category.Monad
-
-Identity : ∀ {f} → Set f → Set f
-Identity A = A
-
-IdentityMonad : ∀ {f} → RawMonad (Identity {f})
-IdentityMonad = record
-  { return = λ x → x
-  ; _>>=_  = λ x f → f x
-  }
diff --git a/src/Category/Monad/Indexed.agda b/src/Category/Monad/Indexed.agda
index 1619d9c..b498b74 100644
--- a/src/Category/Monad/Indexed.agda
+++ b/src/Category/Monad/Indexed.agda
@@ -46,6 +46,9 @@ record RawIMonad {i f} {I : Set i} (M : IFun I f) :
 
   open RawIApplicative rawIApplicative public
 
+RawIMonadT : ∀ {i f} {I : Set i} (T : IFun I f → IFun I f) → Set (i ⊔ suc f)
+RawIMonadT T = ∀ {M} → RawIMonad M → RawIMonad (T M)
+
 record RawIMonadZero {i f} {I : Set i} (M : IFun I f) :
                      Set (i ⊔ suc f) where
   field
diff --git a/src/Category/Monad/Partiality.agda b/src/Category/Monad/Partiality.agda
index f781391..8137e2d 100644
--- a/src/Category/Monad/Partiality.agda
+++ b/src/Category/Monad/Partiality.agda
@@ -6,12 +6,12 @@
 
 module Category.Monad.Partiality where
 
-open import Coinduction
+open import Codata.Musical.Notation
 open import Category.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)
-open import Data.Sum hiding (map)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Function
 open import Function.Equivalence using (_⇔_; equivalence)
 open import Level using (_⊔_)
@@ -373,7 +373,7 @@ module _ {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where
     open RawMonad ¬¬-Monad
 
     not-now-is-never : (x : A ⊥) → (∄ λ y → x ≳ now y) → x ≳ never
-    not-now-is-never (now x)   hyp with hyp (, now refl)
+    not-now-is-never (now x)   hyp with hyp (-, now refl)
     ... | ()
     not-now-is-never (later x) hyp =
       later (♯ not-now-is-never (♭ x) (hyp ∘ Prod.map id laterˡ))
diff --git a/src/Category/Monad/Partiality/All.agda b/src/Category/Monad/Partiality/All.agda
index d33fbec..4d6c4b9 100644
--- a/src/Category/Monad/Partiality/All.agda
+++ b/src/Category/Monad/Partiality/All.agda
@@ -8,7 +8,7 @@ module Category.Monad.Partiality.All where
 
 open import Category.Monad
 open import Category.Monad.Partiality as Partiality using (_⊥; ⇒≈)
-open import Coinduction
+open import Codata.Musical.Notation
 open import Function
 open import Level
 open import Relation.Binary using (_Respects_; IsEquivalence)
diff --git a/src/Category/Monad/State.agda b/src/Category/Monad/State.agda
index 4a45571..aeecf29 100644
--- a/src/Category/Monad/State.agda
+++ b/src/Category/Monad/State.agda
@@ -8,7 +8,7 @@ module Category.Monad.State where
 
 open import Category.Applicative.Indexed
 open import Category.Monad
-open import Category.Monad.Identity
+open import Function.Identity.Categorical as Id using (Identity)
 open import Category.Monad.Indexed
 open import Data.Product
 open import Data.Unit
@@ -53,11 +53,11 @@ record RawIMonadState {i f} {I : Set i} (S : I → Set f)
   field
     monad : RawIMonad M
     get   : ∀ {i} → M i i (S i)
-    put   : ∀ {i j} → S j → M i j (Lift ⊤)
+    put   : ∀ {i j} → S j → M i j (Lift f ⊤)
 
   open RawIMonad monad public
 
-  modify : ∀ {i j} → (S i → S j) → M i j (Lift ⊤)
+  modify : ∀ {i j} → (S i → S j) → M i j (Lift f ⊤)
   modify f = get >>= put ∘ f
 
 StateTIMonadState : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
@@ -101,10 +101,10 @@ State : ∀ {f} → Set f → Set f → Set f
 State S = StateT S Identity
 
 StateMonad : ∀ {f} (S : Set f) → RawMonad (State S)
-StateMonad S = StateTMonad S IdentityMonad
+StateMonad S = StateTMonad S Id.monad
 
 StateMonadState : ∀ {f} (S : Set f) → RawMonadState S (State S)
-StateMonadState S = StateTMonadState S IdentityMonad
+StateMonadState S = StateTMonadState S Id.monad
 
 LiftMonadState : ∀ {f S₁} (S₂ : Set f) {M} →
                  RawMonadState S₁ M →