10 files changed, 61 insertions, 47 deletions
diff --git a/src/Category/Comonad.agda b/src/Category/Comonad.agda
new file mode 100644
index 0000000..0372603
--- /dev/null
+++ b/src/Category/Comonad.agda
@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Comonads
+------------------------------------------------------------------------
+
+-- Note that currently the monad laws are not included here.
+
+module Category.Comonad where
+
+open import Level
+open import Function
+
+record RawComonad {f} (W : Set f → Set f) : Set (suc f) where
+
+  infixl 1 _=>>_ _=>=_
+  infixr 1 _<<=_ _=<=_
+
+  field
+    extract : ∀ {A} → W A → A
+    extend  : ∀ {A B} → (W A → B) → (W A → W B)
+
+  duplicate : ∀ {A} → W A → W (W A)
+  duplicate = extend id
+
+  liftW : ∀ {A B} → (A → B) → W A → W B
+  liftW f = extend (f ∘′ extract)
+
+  _=>>_ : ∀ {A B} → W A → (W A → B) → W B
+  _=>>_ = flip extend
+
+  _=>=_ : ∀ {c A B} {C : Set c} → (W A → B) → (W B → C) → W A → C
+  f =>= g = g ∘′ extend f
+
+  _<<=_ : ∀ {A B} → (W A → B) → W A → W B
+  _<<=_ = extend
+
+  _=<=_ : ∀ {A B c} {C : Set c} → (W B → C) → (W A → B) → W A → C
+  _=<=_ = flip _=>=_
diff --git a/src/Category/Functor.agda b/src/Category/Functor.agda
index 99a82ee..7ca41aa 100644
--- a/src/Category/Functor.agda
+++ b/src/Category/Functor.agda
@@ -15,6 +15,7 @@ open import Relation.Binary.PropositionalEquality
 
 record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
   infixl 4 _<$>_ _<$_
+  infixl 1 _<&>_
 
   field
     _<$>_ : ∀ {A B} → (A → B) → F A → F B
@@ -22,6 +23,9 @@ record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
   _<$_ : ∀ {A B} → A → F B → F A
   x <$ y = const x <$> y
 
+  _<&>_ : ∀ {A B} → F A → (A → B) → F B
+  _<&>_ = flip _<$>_
+
 -- A functor morphism from F₁ to F₂ is an operation op such that
 -- op (F₁ f x) ≡ F₂ f (op x)
 
diff --git a/src/Category/Functor/Identity.agda b/src/Category/Functor/Identity.agda
deleted file mode 100644
index 9357eb6..0000000
--- a/src/Category/Functor/Identity.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- The identity functor
-------------------------------------------------------------------------
-
-module Category.Functor.Identity where
-
-open import Category.Functor
-
-Identity : ∀ {f} → Set f → Set f
-Identity A = A
-
-IdentityFunctor : ∀ {f} → RawFunctor (Identity {f})
-IdentityFunctor = record
-  { _<$>_ = λ x → x
-  }
diff --git a/src/Category/Monad.agda b/src/Category/Monad.agda
index 8e2ddf3..8029ad2 100644
--- a/src/Category/Monad.agda
+++ b/src/Category/Monad.agda
@@ -15,6 +15,9 @@ open import Data.Unit
 RawMonad : ∀ {f} → (Set f → Set f) → Set _
 RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M)
 
+RawMonadT : ∀ {f} (T : (Set f → Set f) → (Set f → Set f)) → Set _
+RawMonadT T = RawIMonadT {I = ⊤} (λ M _ _ → T (M _ _))
+
 RawMonadZero : ∀ {f} → (Set f → Set f) → Set _
 RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M)
 
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 →