diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,9 @@
+# Revision history for monad-ideals
+
+## 0.1.0.0 -- 2024-04-23
+
+* Created based on [category-extras-0.53.5](https://hackage.haskell.org/package/category-extras-0.53.5)
+  with updates
+
+  - Changes needed to work with current ecosystem
+  - Implement coproduct of ideal monads (product of coideal comonads)
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,33 @@
+Copyright 2008 Edward Kmett
+Copyright 2007 Iavor Diatchki
+Copyright 2004-2008 Dave Menendez
+Copyright 2024 Koji Miyazato
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Koji Miyazato nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,137 @@
+# monad-ideals: Ideal Monads and coproduct of Monads
+
+Revives `Control.Monad.Ideal` from old versions of [category-extras](https://hackage.haskell.org/package/category-extras-0.53.25).
+
+## Ideal Monads
+
+Ideal monads[^1] are certain kind of monads. Informally, an ideal monad `M`
+is a `Monad` which can be written as a disjoint union of "pure" values and "impure" values,
+and its `join` operation on "impure" values never produces "pure" values.
+
+[^1]: N. Ghani and T. Uustalu, [“Coproducts of ideal monads,”](http://www.numdam.org/article/ITA_2004__38_4_321_0.pdf) Theoret. Inform. and Appl., vol. 38, pp. 321–342, 2004.
+
+```haskell
+data M a = Pure a | Impure (...)
+
+pure :: a -> M a
+pure = Pure
+
+join :: M (M a) -> M a
+join (Pure ma) = ma
+join (Impure ...) = Impure (...)
+  -- Impure values of @M a@ never becomes pure again 
+```
+
+Formally, an ideal monad `m` is a `Monad` equipped with 
+
+- `Functor m₀`, called the ideal part of `m`
+- Natural isomorphism `iso :: ∀a. Either a (m₀ a) -> m a` (and its inverse `iso⁻¹ :: ∀a. m a -> Either a (m₀ a)`)
+- Natural transformation `idealize :: ∀a. m₀ (m a) -> m₀ a`
+
+satisfying these two properties.
+
+- `iso . Left === pure :: ∀a. a -> m a`
+- `either id (iso . Right . idealize) . iso⁻¹ === join :: m (m a) -> m a`
+
+This package provides `MonadIdeal`, a type class to represent ideal monads in terms of
+its ideal part `m₀` (instead of a subclass of `Monad` to represent ideal monad itself.)
+
+```haskell
+class (Isolated m0, Bind m0) => MonadIdeal m0 where
+  idealBind :: m0 a -> (a -> Ideal m0 b) -> m0 b
+
+type Ideal m0 a
+
+-- | Constructor of @Ideal@
+ideal :: Either a (m0 a) -> Ideal m0 a
+
+-- | Deconstructor of @Ideal@
+runIdeal :: Ideal m0 a -> Either a (m0 a)
+```
+
+Here, `Ideal m0` corresponds to the ideal monad which would have `m0` as its ideal part.
+
+## `Isolated` class
+
+There is a generalization to ideal monads, which are almost ideal monads,
+but lack a condition that says "an impure value does not become a pure value by the `join` operation".
+
+A monad `m` in this class has natural isomorphism `Either a (m₀ a) -> m a` with some functor `m₀`, and
+`pure` is the part of `m` which is not `m₀`. Formally, the defining data of this class are:
+
+- `Functor m₀`, called the impure part of `m`
+- Natural isomorphism `iso :: ∀a. Either a (m₀ a) -> m a` (and its inverse `iso⁻¹ :: ∀a. m a -> Either a (m₀ a)`)
+- `iso . Left === pure :: ∀a. a -> m a`
+
+Combined with the monad laws of `m`, `join :: ∀a. m (m a) -> m a` must be equal to the following natural transformation
+with some `impureJoin`.
+
+```haskell
+join :: ∀a. m (m a) -> m a
+join mma = case iso⁻¹ mma of
+  Left ma -> ma
+  Right m₀ma -> impureJoin m₀ma
+  where
+    impureJoin :: ∀a. m₀ (m a) -> m a
+```
+
+The `Isolated` class is a type class for a functor which can be thought of as an
+impure part of some monad.
+
+```haskell
+newtype Unite f a = Unite { runUnite :: Either a (f a) }
+
+class Functor m0 => Isolated m0 where
+  impureBind :: m0 a -> (a -> Unite m0 b) -> Unite m0 b
+```
+
+## Coproduct of monads
+
+Coproduct `m ⊕ n` of two monads[^2] `m, n` is the coproduct (category-theoretic sum) in the category of monad
+and [monad morphisms](https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html). [^3]
+
+In basic terms, `m ⊕ n` is a monad with the following functions and properties.
+
+- Monad morphism `inject1 :: ∀a. m a -> (m ⊕ n) a`
+- Monad morphism `inject2 :: ∀a. n a -> (m ⊕ n) a`
+- Function `eitherMonad` which takes two monad morphisms and return a monad morphism.
+
+  ```
+  eitherMonad :: (∀a. m a -> t a) -> (∀a. n a -> t a) -> (∀a. (m ⊕ n) a -> t a)
+  ```
+
+- Given arbitrary monads `m, n, t`,
+
+  - For all monad morphisms `f1` and `f2`,
+
+    - `eitherMonad f1 f2 . inject1 = f1`
+    - `eitherMonad f1 f2 . inject2 = f2`
+
+  - For any monad morphism `f :: ∀a. (m ⊕ n) a -> t a`, `f` equals to `eitherMonad f1 f2` for some unique `f1, f2`.
+    Or, equvalently, `f = eitherMonad (f . inject1) (f . inject2)`.
+
+Coproduct of two monads does not always exist, but for ideal monads or monads with `Isolated` impure parts,
+their coproducts exist. This package provides a type constructor `(:+)` below.
+
+```haskell
+-- Control.Monad.Coproduct
+data (:+) (m :: Type -> Type) (n :: Type -> Type) (a :: Type)
+```
+
+Using this type constructor, coproduct of monad can be constructed in two ways.
+
+- If `m0, n0` are `Isolated` i.e. the impure part of monads `Unite m0, Unite n0` respectively,
+  `m0 :+ n0` is also `Isolated` and `Unite (m0 :+ n0)` is the coproduct of monads `Unite m0 ⊕ Unite n0`.
+
+- If `m0, n0` are `MonadIdeal` i.e. the ideal part of ideal monads `Ideal m0, Ideal n0` respectively,
+  `m0 :+ n0` is also `MonadIdeal` and `Ideal (m0 :+ n0)` is the coproduct of monads `Ideal m0 ⊕ Ideal n0`.
+
+[^2]: Jiří Adámek, Nathan Bowler, Paul B. Levy and Stefan Milius, ["Coproducts of Monads on Set."](https://arxiv.org/abs/1409.3804) (https://doi.org/10.48550/arXiv.1409.3804)
+
+[^3]: To name the same concept to monad morphism, the term "monad transformation" is used in `transformers` package ([Control.Monad.Trans.Class](https://hackage.haskell.org/package/transformers-0.6.0.3/docs/Control-Monad-Trans-Class.html#t:MonadTrans).)
+
+## Duals
+
+This package also provides the duals of ideal monads and coproducts of them: _Coideal comonads_ and _products_ of them.
+
+--------
diff --git a/monad-ideals.cabal b/monad-ideals.cabal
new file mode 100644
--- /dev/null
+++ b/monad-ideals.cabal
@@ -0,0 +1,69 @@
+cabal-version:      3.0
+name:               monad-ideals
+version:            0.1.0.0
+
+synopsis:           Ideal Monads and coproduct of them
+description:
+  Type class to represent ideal monads in terms of the
+  "ideal part" of ideal monads. See README for more.
+
+license:            BSD-3-Clause
+license-file:       LICENSE
+author:             Koji Miyazato
+maintainer:         viercc@gmail.com
+homepage:           https://github.com/viercc/monad-ideals
+copyright: Copyright (C) 2008 Edward A. Kmett, 
+           Copyright (C) 2004--2008 Dave Menendez, 
+           Copyright (C) 2007 Iavor Diatchki,
+           Copyright (C) 2024 Koji Miyazato
+
+category:           Control
+build-type:         Simple
+
+extra-doc-files:    CHANGELOG.md, README.md
+tested-with: GHC ==8.10.7, GHC ==9.0.2, GHC ==9.2.8, GHC ==9.4.8, GHC ==9.6.5, GHC ==9.8.2
+
+source-repository head
+  type:     git
+  location: https://github.com/viercc/monad-ideals.git
+  branch:   main
+
+common warnings
+    ghc-options: -Wall -Wcompat
+
+library
+    import:           warnings
+
+    exposed-modules:
+        Control.Functor.Internal.Mutual,
+        Control.Monad.Ideal,
+        Control.Monad.Isolated,
+        Control.Monad.Coproduct,
+        Control.Comonad.Coideal,
+
+        Data.List.TwoOrMore,
+        Data.List.NotOne,
+        Data.Functor.KeepLeft,
+
+    build-depends:
+      base >=4.14 && < 4.21,
+      bifunctor-classes-compat >= 0.1 && < 1,
+      comonad >= 5.0.8 && < 5.1,
+      semigroupoids >= 6.0.0 && < 6.1,
+
+    hs-source-dirs:   src
+    default-language: Haskell2010
+
+test-suite monad-ideals-test
+    import:           warnings
+    default-language: Haskell2010
+    type:             exitcode-stdio-1.0
+
+    hs-source-dirs:   test
+    main-is:        Main.hs
+    other-modules:
+        CoidealExample
+    build-depends:
+        base,
+        comonad,
+        monad-ideals
diff --git a/src/Control/Comonad/Coideal.hs b/src/Control/Comonad/Coideal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Comonad/Coideal.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Coideal
+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+module Control.Comonad.Coideal
+  ( -- * Coideal Comonads
+    ComonadCoideal (..),
+    Coideal(..),
+    buildCoideal,
+
+    -- * Mutual recursion for (co)ideal (co)monad (co)products
+    Mutual (..),
+
+    -- * Coideal Comonad Product
+    (:*)(..),
+    project1, project2,
+    (&&&&)
+  )
+where
+
+import Control.Arrow ((&&&))
+import Control.Comonad
+
+import Control.Functor.Internal.Mutual
+
+newtype Coideal f a = Coideal { runCoideal :: (a, f a) }
+  deriving (Functor, Foldable, Traversable)
+
+class (Functor w) => ComonadCoideal w where
+  coidealExtend :: (Coideal w a -> b) -> w a -> w b
+
+coidealize :: (ComonadCoideal w) => w a -> w (Coideal w a)
+coidealize = coidealExtend id
+
+instance (ComonadCoideal w) => Comonad (Coideal w) where
+  extract = fst . runCoideal
+  extend f = fmap f . Coideal . (id &&& coidealize . snd . runCoideal)
+
+buildCoideal :: (a -> w a) -> a -> Coideal w a
+buildCoideal phi = Coideal . (id &&& phi)
+
+-- * (Co)ideal (Co)products
+
+newtype (:*) w v a = CoidealProduct { runCoidealProduct :: (Mutual (,) w v a, Mutual (,) v w a) }
+  deriving Functor
+
+deriving instance
+  (
+    Eq (m0 ((,) a (Mutual (,) n0 m0 a))),
+    Eq (n0 ((,) a (Mutual (,) m0 n0 a)))
+  ) => Eq ((:*) m0 n0 a)
+deriving instance
+  (
+    Show (m0 ((,) a (Mutual (,) n0 m0 a))),
+    Show (n0 ((,) a (Mutual (,) m0 n0 a)))
+  ) => Show ((:*) m0 n0 a)
+
+project1 :: (Functor w) => (w :* v) a -> w a
+project1 = fmap fst . runMutual . fst . runCoidealProduct
+
+project2 :: (Functor v) => (w :* v) a -> v a
+project2 = fmap fst . runMutual . snd . runCoidealProduct
+
+instance (ComonadCoideal w, ComonadCoideal v) => ComonadCoideal (w :* v) where
+  coidealExtend k (CoidealProduct (wv, vw)) = CoidealProduct (extendMutual1 k wv, extendMutual2 k vw)
+
+extendMutual1 ::
+  (ComonadCoideal w, ComonadCoideal v) =>
+  (Coideal (w :* v) a -> b) ->
+  Mutual (,) w v a ->
+  Mutual (,) w v b
+extendMutual1 k (Mutual wv) =
+  Mutual $ coidealExtend (\(Coideal ((a, vw), w')) -> (k (Coideal (a, CoidealProduct (Mutual w', vw))), extendMutual2 k vw)) wv
+
+extendMutual2 ::
+  (ComonadCoideal w, ComonadCoideal v) =>
+  (Coideal (v :* w) a -> b) ->
+  Mutual (,) w v a ->
+  Mutual (,) w v b
+extendMutual2 k (Mutual wv) =
+  Mutual $ coidealExtend (\(Coideal ((a, vw), w')) -> (k (Coideal (a, CoidealProduct (vw, Mutual w'))), extendMutual1 k vw)) wv
+
+(&&&&) :: (ComonadCoideal s) => (forall a. s a -> w a) -> (forall a. s a -> v a) -> s b -> (w :* v) b
+tw &&&& tv = CoidealProduct . (unfoldMutual' tw tv &&& unfoldMutual' tv tw)
+
+unfoldMutual' :: (ComonadCoideal s) => (forall a. s a -> w a) -> (forall a. s a -> v a) -> s b -> Mutual (,) w v b
+unfoldMutual' = unfoldMutual (\k sa -> coidealExtend (k . runCoideal) sa)
diff --git a/src/Control/Functor/Internal/Mutual.hs b/src/Control/Functor/Internal/Mutual.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/Internal/Mutual.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Functor.Internal.Mutual
+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+module Control.Functor.Internal.Mutual where
+
+import Data.Bifunctor
+
+newtype Mutual p m n a = Mutual {runMutual :: m (p a (Mutual p n m a))}
+
+deriving instance (Eq (m (p a (Mutual p n m a))), Eq (n (p a (Mutual p m n a)))) => Eq (Mutual p n m a)
+deriving instance (Show (m (p a (Mutual p n m a))), Show (n (p a (Mutual p m n a)))) => Show (Mutual p n m a)
+
+instance (Bifunctor p, Functor m, Functor n) => Functor (Mutual p m n) where
+  fmap f = Mutual . fmap (bimap f (fmap f)) . runMutual
+
+foldMutual
+  :: Bifunctor p
+  => (forall a b. t a -> (a -> p b (t b)) -> t b)
+  -> (forall a. m a -> t a)
+  -> (forall a. n a -> t a)
+  -> Mutual p m n c -> t c
+foldMutual bind mt nt = (`bind` second (foldMutual bind nt mt)) . mt . runMutual
+
+unfoldMutual
+  :: Bifunctor p
+  => (forall a b. (p a (s a) -> b) -> s a -> s b)
+  -> (forall a. s a -> w a)
+  -> (forall a. s a -> v a)
+  -> s c -> Mutual p w v c
+unfoldMutual ext sw sv = Mutual . sw . ext (second (unfoldMutual ext sv sw))
diff --git a/src/Control/Monad/Coproduct.hs b/src/Control/Monad/Coproduct.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Coproduct.hs
@@ -0,0 +1,205 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.Coproduct
+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+module Control.Monad.Coproduct(
+  -- * Ideal Monad Coproduct
+  (:+)(..),
+  inject1,
+  inject2,
+  (||||),
+  eitherMonad,
+
+  -- * Mutual recursion for ideal monad coproducts
+  Mutual (..),
+) where
+
+import Data.Functor.Bind
+import Control.Monad.Isolated
+import Control.Monad.Ideal
+import Control.Functor.Internal.Mutual (Mutual(..), foldMutual)
+
+import Data.Bifunctor (Bifunctor(..))
+
+-- * Coproduct of Monads
+
+-- | Coproduct of impure parts of two `Monad`s.
+-- 
+-- === As the coproduct of 'Isolated'
+-- 
+-- Given @'Isolated' m0@ and @Isolated n0@, the functor @m0 :+ n0@ is @Isolated@ too. In other words,
+-- given two @Monad@s @Unite m0@ and @Unite n0@, this type constructs a new @Monad (Unite (m0 :+ n0))@.
+--
+-- Furthermore, as the name suggests,
+-- @Unite (m0 :+ n0)@ is the coproduct of @Unite m0@ and @Unite n0@ as a @Monad@.
+--
+-- - @'hoistUnite' 'inject1' :: Unite m0 ~> Unite (m0 :+ n0)@ is a monad morphism
+-- - @'hoistUnite' 'inject2' :: Unite n0 ~> Unite (m0 :+ n0)@ is a monad morphism
+-- - @'eitherMonad' mt nt :: (m0 :+ n0) ~> t@ is an impure monad morphism,
+--   given @(mt :: m0 ~> t)@ and @(nt :: n0 ~> t)@ are impure monad morphisms.
+-- - Any impure monad morphisms @(m0 :+ n0) ~> t@ can be uniquely rewritten as @(eitherMonad mt nt)@.
+--
+-- Here, a natural transformation @nat :: f ~> g@ is an /impure monad morphism/ means
+-- @f@ is an @Isolated@, @g@ is a @Monad@, and @nat@ becomes a monad morphism when combined with @pure@ as below.
+--
+-- @
+-- either pure nat . runUnite :: Unite f ~> g
+-- @
+--
+-- === As the coproduct of 'MonadIdeal'
+-- 
+-- Given @'MonadIdeal' m0@ and @MonadIdeal n0@, the functor @m0 :+ n0@ is @MonadIdeal@ too.
+-- It is the coproduct of @m0@ and @n0@ as a @MonadIdeal@.
+--
+-- - @inject1 :: m0 ~> (m0 :+ n0)@ is a @MonadIdeal@ morphism
+-- - @inject2 :: n0 ~> (m0 :+ n0)@ is a @MonadIdeal@ morphism
+-- - @(mt |||| nt) :: (m0 :+ n0) ~> t0@ is a @MonadIdeal@ morphism, given
+--   @mt, nt@ are @MonadIdeal@ morphisms.
+-- - Any @MonadIdeal@ morphism @(m0 :+ n0) ~> t0@ can be uniquely rewritten as @(mt |||| nt)@.
+--
+-- Here, a @MonadIdeal@ morphism is a natural transformation @nat@ between @MonadIdeal@ such that
+-- preserves @idealBind@.
+-- 
+-- @
+-- nat (idealBind ma k) = idealBind (nat ma) ('hoistIdeal' nat . k)
+-- @
+-- 
+newtype (:+) m0 n0 a = Coproduct { runCoproduct :: Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a) }
+
+deriving instance
+  (
+    Eq (m0 (Either a (Mutual Either n0 m0 a))),
+    Eq (n0 (Either a (Mutual Either m0 n0 a)))
+  ) => Eq ((:+) m0 n0 a)
+deriving instance
+  (
+    Show (m0 (Either a (Mutual Either n0 m0 a))),
+    Show (n0 (Either a (Mutual Either m0 n0 a)))
+  ) => Show ((:+) m0 n0 a)
+
+inject1 :: (Functor m0) => m0 a -> (m0 :+ n0) a
+inject1 = Coproduct . Left . Mutual . fmap Left
+
+inject2 :: (Functor n0) => n0 a -> (m0 :+ n0) a
+inject2 = Coproduct . Right . Mutual . fmap Left
+
+instance (Functor m0, Functor n0) => Functor (m0 :+ n0) where
+  fmap f = Coproduct . bimap (fmap f) (fmap f) . runCoproduct
+
+instance (MonadIdeal m0, MonadIdeal n0) => Apply (m0 :+ n0) where
+  (<.>) = apDefault
+
+instance (MonadIdeal m0, MonadIdeal n0) => Bind (m0 :+ n0) where
+  (>>-) = bindDefault
+
+instance (Isolated m0, Isolated n0) => Isolated (m0 :+ n0) where
+  impureBind copro k = case runCoproduct copro of
+    Left mn -> imbindMutual1 mn k
+    Right nm -> imbindMutual2 nm k
+
+instance (MonadIdeal m0, MonadIdeal n0) => MonadIdeal (m0 :+ n0) where
+  idealBind copro k = Coproduct $ case runCoproduct copro of
+    Left mn -> Left $ bindMutual1 mn k
+    Right nm -> Right $ bindMutual2 nm k
+
+bindMutual1 :: (MonadIdeal m0, MonadIdeal n0) => Mutual Either m0 n0 a -> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b
+bindMutual1 (Mutual mn) k =
+  Mutual $
+    mn `idealBind` \next ->
+      case next of
+        Left a -> case runIdeal (k a) of
+          Left b -> pure (Left b)
+          Right (Coproduct (Left mn')) -> ideal . Right $ runMutual mn'
+          Right (Coproduct (Right nm')) -> pure (Right nm')
+        Right nm -> pure . Right $ bindMutual2 nm k
+
+bindMutual2 :: (MonadIdeal m0, MonadIdeal n0) => Mutual Either m0 n0 a -> (a -> Ideal (n0 :+ m0) b) -> Mutual Either m0 n0 b
+bindMutual2 (Mutual mn) k =
+  Mutual $
+    mn `idealBind` \next ->
+      case next of
+        Left a -> case runIdeal (k a) of
+          Left b -> pure (Left b)
+          Right (Coproduct (Left nm')) -> pure (Right nm')
+          Right (Coproduct (Right mn')) -> ideal . Right $ runMutual mn'
+        Right nm -> pure . Right $ bindMutual1 nm k
+
+(||||) :: (MonadIdeal t) => (forall a. m0 a -> t a) -> (forall a. n0 a -> t a) -> (m0 :+ n0) b -> t b
+mt |||| nt = either (foldMutual' mt nt) (foldMutual' nt mt) . runCoproduct
+
+foldMutual' :: (MonadIdeal t) => (forall a. m0 a -> t a) -> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
+foldMutual' = foldMutual (\ta k -> ta `idealBind` ideal . k)
+
+
+
+{- |
+
+> MonadCoproduct m0 n0 a
+>   ~ a + Mutual f g a + Mutual g f a
+>   ~ a + f (a + Mutual g f a) + Mutual g f a
+>   ~ (a + Mutual g f a) + f (a + Mutual g f a)
+>   ~ m0 (a + Mutual g f a)
+
+-}
+
+imbindMutual1 :: (Isolated m0, Isolated n0)
+  => Mutual Either m0 n0 a
+  -> (a -> Unite (m0 :+ n0) b)
+  -> Unite (m0 :+ n0) b
+imbindMutual1 (Mutual mna) k =
+  review1 $ impureBind mna $ \na -> case na of
+    Left a -> view1 (k a)
+    Right na' -> view1 (imbindMutual2 na' k)
+
+imbindMutual2 :: (Isolated m0, Isolated n0)
+  => Mutual Either n0 m0 a
+  -> (a -> Unite (m0 :+ n0) b)
+  -> Unite (m0 :+ n0) b
+imbindMutual2 (Mutual nma) k =
+  review2 $ impureBind nma $ \ma -> case ma of
+    Left a -> view2 (k a)
+    Right ma' -> view2 (imbindMutual1 ma' k)
+
+view1 :: Unite (m0 :+ n0) a -> Unite m0 (Either a (Mutual Either n0 m0 a))
+view1 (Unite (Left a)) = Unite (Left (Left a))
+view1 (Unite (Right copro)) = case runCoproduct copro of
+  Left mn -> Unite (Right (runMutual mn))
+  Right nm -> Unite (Left (Right nm))
+
+review1 :: Unite m0 (Either a (Mutual Either n0 m0 a)) -> Unite (m0 :+ n0) a 
+review1 (Unite (Left (Left a))) = Unite (Left a)
+review1 (Unite (Left (Right nm))) = Unite (Right (Coproduct (Right nm)))
+review1 (Unite (Right mn)) = Unite (Right (Coproduct (Left (Mutual mn))))
+
+view2 :: Unite (m0 :+ n0) a -> Unite n0 (Either a (Mutual Either m0 n0 a))
+view2 (Unite (Left a)) = Unite (Left (Left a))
+view2 (Unite (Right copro)) = case runCoproduct copro of
+  Left mn -> Unite (Left (Right mn))
+  Right nm -> Unite (Right (runMutual nm))
+
+review2 :: Unite n0 (Either a (Mutual Either m0 n0 a)) -> Unite (m0 :+ n0) a 
+review2 (Unite (Left (Left a))) = Unite (Left a)
+review2 (Unite (Left (Right mn))) = Unite (Right (Coproduct (Left mn)))
+review2 (Unite (Right nm)) = Unite (Right (Coproduct (Right (Mutual nm))))
+
+eitherMonad :: (Isolated m0, Isolated n0, Monad t)
+  => (forall a. m0 a -> t a)
+  -> (forall a. n0 a -> t a)
+  -> (m0 :+ n0) b -> t b
+eitherMonad mt nt copro = case runCoproduct copro of
+  Left fg -> foldMutual'' mt nt fg
+  Right gf -> foldMutual'' nt mt gf
+
+foldMutual'' :: (Monad t)
+  => (forall a. m0 a -> t a)
+  -> (forall a. n0 a -> t a)
+  -> Mutual Either m0 n0 b -> t b
+foldMutual'' = foldMutual (\ta k -> ta >>= either pure id . k)
diff --git a/src/Control/Monad/Ideal.hs b/src/Control/Monad/Ideal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Ideal.hs
@@ -0,0 +1,122 @@
+
+{-# LANGUAGE RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.Ideal
+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+module Control.Monad.Ideal
+  ( -- * Ideal Monads
+    MonadIdeal (..), idealize,
+
+    Ideal, ideal, runIdeal, hoistIdeal,
+
+    destroyIdeal,
+
+    bindDefault,
+    impureBindDefault,
+    
+    -- * Relation between @MonadIdeal@, @Bind@, and @Isolated@
+    -- 
+    -- $relation_to_bind_and_isolate
+  )
+where
+
+import Prelude
+import Control.Arrow ((|||))
+
+import Data.Functor.Bind (Bind (..))
+import Control.Applicative (WrappedMonad (..))
+
+import Control.Monad.Isolated
+
+-- | Ideal monad is a special case of @Unite m0@
+type Ideal = Unite
+
+-- | Constructor of @Ideal@, for backward compatibility
+ideal :: Either a (m0 a) -> Ideal m0 a
+ideal = Unite
+
+-- | Deconstructor of @Ideal@, for backward compatibility
+runIdeal :: Ideal m0 a -> Either a (m0 a)
+runIdeal = runUnite
+
+-- | Alias of 'hoistUnite' for naming consistently
+hoistIdeal :: (forall a. m0 a -> n a) -> Ideal m0 b -> Ideal n b
+hoistIdeal = hoistUnite
+
+-- | @m0@ is the "ideal part" of an ideal monad.
+--
+-- ==== Laws
+--
+-- Methods inherited from superclasses must be equivalent to the
+-- canocical ones.
+--
+-- - @'(>>-)' === 'bindDefault'@
+-- - @'impureBind' === 'impureBindDefault'@
+class (Bind m0, Isolated m0) => MonadIdeal m0 where
+  idealBind :: m0 a -> (a -> Ideal m0 b) -> m0 b
+
+infixl 1 `idealBind`
+
+idealize :: (MonadIdeal m0) => m0 (Ideal m0 a) -> m0 a
+idealize = (`idealBind` id)
+
+-- | 'MonadIdeal' implies 'Bind'
+bindDefault :: MonadIdeal m0 => m0 a -> (a -> m0 b) -> m0 b
+bindDefault ma k = ma `idealBind` ideal . Right . k
+
+-- | 'MonadIdeal' implies 'Isolated'
+impureBindDefault :: MonadIdeal m0 => m0 a -> (a -> Unite m0 b) -> Unite m0 b
+impureBindDefault ma k = ideal . Right $ ma `idealBind` k
+
+-- | @Ideal ((,) s) ~ (,) (Maybe s)@
+instance (Semigroup s) => MonadIdeal ((,) s) where
+  idealBind (s1, a) k = case runIdeal (k a) of
+    Left b -> (s1, b)
+    Right (s2, b) -> (s1 <> s2, b)
+
+-- | Any @Monad m@ can be an ideal of @Ideal m@
+instance (Monad m) => MonadIdeal (WrappedMonad m) where
+  idealBind (WrapMonad ma) k = WrapMonad $ ma >>= either pure unwrapMonad . runIdeal . k
+
+destroyIdeal :: (m0 a -> a) -> Ideal m0 a -> a
+destroyIdeal phi = (id ||| phi) . runIdeal
+
+{- $relation_to_bind_and_isolate
+
+@MonadIdeal@ is a requirement stronger than both of 'Bind' and 'Isolated'.
+In fact, these subset relations hold.
+
+- Every @MonadIdeal@ is @Bind@
+- Every @MonadIdeal@ is @Isolated@
+
+These are /strict/ subset relation and neither of three classes can be dropped.
+
+- 'Data.List.NotOne.NotOne' is both @Bind@ and @Isolated@, but not @MonadIdeal@.
+
+- @NullBind c@ is @Bind@ but can't be @Isolated@, because @Unite (NullBind c)@ can't be a @Monad@ in a compatible way.
+
+    @
+    newtype NullBind c a = NullBind (Maybe c)
+    instance Bind (NullBind c a) where
+      _ >>- _ = NullBind Nothing
+    @
+
+- @Toggle@ shown below is @Isolated@, but can't be a @Bind@ in a compatible way.
+
+    @
+    newtype Toggle a = Toggle a
+      deriving Functor
+
+    instance Isolated Toggle where
+      impureBind (Toggle a) k = case k a of
+        Unite (Left b)           -> Unite (Right (Toggle b))
+        Unite (Right (Toggle b)) -> Unite (Left b)
+    @
+
+-}
diff --git a/src/Control/Monad/Isolated.hs b/src/Control/Monad/Isolated.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Isolated.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.Isolated
+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+module Control.Monad.Isolated(
+  -- * Impure part isolated from a Monad
+  Isolated(..),
+
+  -- * (Re)Unite a Monad from pure and impure parts
+  Unite(..),
+  hoistUnite,
+) where
+
+import Data.Functor.Bind
+import Data.Semigroup.Traversable
+import Data.Semigroup.Foldable
+import Data.Bifunctor (Bifunctor(..))
+import Data.Proxy
+import Control.Applicative (WrappedMonad(..))
+
+newtype Unite f a = Unite { runUnite :: Either a (f a) }
+  deriving (Show, Read, Eq, Ord)
+
+hoistUnite :: (forall a. f a -> g a) -> Unite f b -> Unite g b
+hoistUnite fg = Unite . fmap fg . runUnite
+
+instance (Functor g) => Functor (Unite g) where
+  fmap f = Unite . bimap f (fmap f) . runUnite
+
+instance (Foldable g) => Foldable (Unite g) where
+  foldMap f = either f (foldMap f) . runUnite
+
+instance (Foldable1 g) => Foldable1 (Unite g) where
+  foldMap1 f = either f (foldMap1 f) . runUnite
+
+instance (Traversable g) => Traversable (Unite g) where
+  traverse f = fmap Unite . either (fmap Left . f) (fmap Right . traverse f) . runUnite
+
+instance (Traversable1 g) => Traversable1 (Unite g) where
+  traverse1 f = fmap Unite . either (fmap Left . f) (fmap Right . traverse1 f) . runUnite
+
+-- | @Isolated m0@ is a @Functor@ which can be thought of as an impure part of a @Monad@.
+-- 
+-- ==== Examples
+-- 
+-- - 'Proxy' is @Isolated@ by being same to the 'Nothing' part of the 'Maybe' monad.
+--
+-- - 'Data.List.NotOne.NotOne' is @Isolated@ by being the list monad ('[]') minus singleton lists,
+--   the 'pure' part of the list monad.
+--
+-- ==== Non-example
+--
+-- Not every @Monad@ can be isolated its pure and impure parts as the sum of functors.
+-- For example, the reader monad cannot be written as a sum of two functors.
+--
+-- ==== Laws
+-- 
+-- 'impureBind' must be implemented so that the @Monad (Unite m0)@ instance derived from
+-- it is lawful.
+-- 
+-- @
+-- return a = Unite (Left a)
+-- 
+-- Unite (Left a) >>= k = k a
+-- Unite (Right ma) >>= k = ma \`impureBind\` k
+-- @
+-- 
+-- Translating the @Monad@ laws on @Unite m0@ in terms of @impureBind@,
+-- the following equations are the @Isolated@ laws on its own.
+--
+-- - (Right identity)
+--
+--     @
+--     ma \`impureBind\` Unite . Left === Unite (Right ma)
+--     @
+--
+-- - (Associativity)
+--
+--     @
+--     (ma \`impureBind\` f) \`impureBind\` g === ma `impureBind` \a -> either g (\`impureBind\` g) (runUnite fa)
+--     @
+class Functor m0 => Isolated m0 where
+  impureBind :: m0 a -> (a -> Unite m0 b) -> Unite m0 b
+
+infixl 1 `impureBind`
+
+instance Isolated m0 => Apply (Unite m0) where
+  (<.>) = apDefault
+
+instance Isolated m0 => Applicative (Unite m0) where
+  pure = Unite . Left
+  (<*>) = (<.>)
+
+instance Isolated m0 => Bind (Unite m0) where
+  Unite (Left a) >>- k = k a
+  Unite (Right ma) >>- k = ma `impureBind` k
+
+instance Isolated m0 => Monad (Unite m0) where
+  (>>=) = (>>-)
+
+instance Isolated Proxy where
+  _ `impureBind` _ = Unite (Right Proxy)
+
+instance Semigroup s => Isolated ((,) s) where
+  (s, a) `impureBind` k = case runUnite (k a) of
+    Left b -> Unite (Right (s, b))
+    Right (s', b) -> Unite (Right (s <> s', b))
+
+instance Monad m => Isolated (WrappedMonad m) where
+  WrapMonad ma `impureBind` k = Unite . Right . WrapMonad $ ma >>= \a ->
+    case runUnite (k a) of
+      Left b -> pure b
+      Right (WrapMonad mb) -> mb
diff --git a/src/Data/Functor/KeepLeft.hs b/src/Data/Functor/KeepLeft.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/KeepLeft.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE DeriveTraversable #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Functor.KeepLeft
+-- Copyright   :  (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+module Data.Functor.KeepLeft where
+
+import Data.Functor.Const (Const(..))
+import Data.Semigroup (First(..))
+import Data.Bitraversable (Bitraversable (..))
+import Data.Bifoldable (Bifoldable)
+import Data.Bifunctor (Bifunctor)
+
+import Data.Functor.Classes ( Eq1, Ord1, Eq2, Ord2 )
+import Data.Functor.Bind.Class ( Apply(..), Bind(..) )
+import Control.Monad.Isolated ( Isolated(..) )
+import Control.Monad.Ideal ( MonadIdeal(..), impureBindDefault )
+
+import Data.Semigroup.Bifoldable (Bifoldable1)
+import Data.Semigroup.Bitraversable (Bitraversable1)
+import Data.Semigroup.Traversable.Class (Bitraversable1(..))
+
+-- | Another choices of instances for 'Const'. @'KeepLeft' c@ have 'Apply' instance isomorphic to
+--   @Const ('First' c)@, which can also (exceptionally) have 'Bind' instance.
+--
+-- The most used constant functor 'Const' lacks the instance of 'Bind', due to incompatibility
+-- between 'Bind' and 'Apply'.
+-- 
+-- @
+-- instance (Semigroup c) => 'Apply' ('Const' c)
+-- @
+-- 
+-- While any @Semigroup c@ instance yields a lawful @Apply (Const c)@ instance, large number of
+-- them do not have @Bind (Const c)@ instance compatible to @Apply@. One of few exceptional @Semigroup@
+-- instance is the one defined as below, which is isomorphic to @'First' c@ semigroup.
+--
+-- @
+-- (<>) :: c -> c -> c
+-- x <> _ = x
+-- @
+newtype KeepLeft c a = KeepLeft { getKeepLeft :: c }
+  deriving stock (Show, Read, Eq, Ord, Functor, Foldable, Traversable)
+  deriving (Semigroup) via (First c)
+  deriving (Eq1, Ord1, Apply) via (Const (First c))
+  deriving (Eq2, Ord2, Bifunctor, Bifoldable, Bifoldable1) via Const
+
+instance Bitraversable KeepLeft where
+  bitraverse f _ (KeepLeft c) = KeepLeft <$> f c
+
+instance Bitraversable1 KeepLeft where
+  bitraverse1 f _ (KeepLeft c) = KeepLeft <$> f c
+
+instance Bind (KeepLeft c) where
+  KeepLeft c >>- _ = KeepLeft c
+
+instance Isolated (KeepLeft c) where
+  impureBind = impureBindDefault
+
+-- | @Ideal (KeepLeft c) a ~ Either c a@
+instance MonadIdeal (KeepLeft c) where
+  idealBind (KeepLeft c) _ = KeepLeft c
diff --git a/src/Data/List/NotOne.hs b/src/Data/List/NotOne.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/NotOne.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE DeriveTraversable #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.List.NotOne
+-- Copyright   :  (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+module Data.List.NotOne where
+
+import Data.Maybe (mapMaybe)
+import Data.Foldable (toList)
+
+import Data.Functor.Bind
+import Data.Functor.Plus (Alt(..), Plus(..))
+import Control.Monad.Isolated
+
+import Data.List.TwoOrMore
+
+-- | List sans singleton
+data NotOne a = Zero | Multiple (TwoOrMore a)
+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable)
+
+notOne :: [a] -> Either a (NotOne a)
+notOne [] = Right Zero
+notOne [a] = Left a
+notOne (a1 : a2 : as) = Right . Multiple $ TwoOrMore a1 a2 as
+
+getMultiple :: NotOne a -> Maybe (TwoOrMore a)
+getMultiple Zero = Nothing
+getMultiple (Multiple as) = Just as
+
+instance Semigroup (NotOne a) where
+  Zero <> bs = bs
+  Multiple (TwoOrMore a1 a2 as) <> bs = Multiple $ TwoOrMore a1 a2 (as ++ toList bs)
+
+instance Monoid (NotOne a) where
+  mempty = Zero
+
+instance Apply NotOne where
+  Zero <.> _ = Zero
+  Multiple _ <.> Zero = Zero
+  Multiple as <.> Multiple bs = Multiple (as <.> bs)
+
+instance Alt NotOne where
+  (<!>) = (<>)
+
+instance Plus NotOne where
+  zero = mempty
+
+-- | @(>>-) = flip foldMap@
+instance Bind NotOne where
+  Zero >>- _ = Zero
+  Multiple as >>- k = case mapMaybe (getMultiple . k) (toList as) of
+    [] -> Zero
+    [bs] -> Multiple bs
+    bs1 : bs2 : bss -> Multiple $ join (TwoOrMore bs1 bs2 bss)
+
+instance Isolated NotOne where
+  impureBind as k = Unite . notOne $ toList as >>= toList . k
diff --git a/src/Data/List/TwoOrMore.hs b/src/Data/List/TwoOrMore.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/List/TwoOrMore.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE DeriveTraversable #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.List.TwoOrMore
+-- Copyright   :  (C) 2024 Koji Miyazato
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
+-- Stability   :  experimental
+module Data.List.TwoOrMore(TwoOrMore(..), twoOrMore, toNonEmpty) where
+
+import Data.Foldable (toList)
+import Data.List.NonEmpty (NonEmpty((:|)))
+import Data.Semigroup.Foldable (Foldable1(..))
+
+import Data.Functor.Bind
+import Data.Functor.Alt (Alt(..))
+import Control.Monad.Isolated
+import Control.Monad.Ideal (MonadIdeal(..), impureBindDefault, Ideal, runIdeal)
+
+
+-- | List of two or more elements
+data TwoOrMore a = TwoOrMore a a [a]
+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable)
+
+instance Foldable1 TwoOrMore where
+  foldMap1 f (TwoOrMore a1 a2 as) = f a1 <> foldMap1 f (a2 :| as)
+  toNonEmpty (TwoOrMore a1 a2 as) = a1 :| (a2 : as)
+
+twoOrMore :: NonEmpty a -> Either a (TwoOrMore a)
+twoOrMore (a1 :| as) = case as of
+  [] -> Left a1
+  a2 : as' -> Right (TwoOrMore a1 a2 as')
+
+instance Semigroup (TwoOrMore a) where
+  TwoOrMore a1 a2 as <> bs = TwoOrMore a1 a2 (as ++ toList bs)
+
+instance Apply TwoOrMore where
+  TwoOrMore x1 x2 xs <.> TwoOrMore y1 y2 ys = TwoOrMore (x1 y1) (x1 y2) (fmap x1 ys ++ (x2 : xs <*> y1 : y2 : ys))
+
+instance Alt TwoOrMore where
+  (<!>) = (<>)
+
+-- | @(>>-) = flip foldMap1@
+instance Bind TwoOrMore where
+  TwoOrMore a1 a2 as >>- k = case k a1 of
+    TwoOrMore b1 b2 bs -> TwoOrMore b1 b2 $ bs ++ ((a2 : as) >>= toList . k)
+
+instance Isolated TwoOrMore where
+  impureBind = impureBindDefault
+
+-- | @Ideal TwoOrMore ~ NonEmpty@
+instance MonadIdeal TwoOrMore where
+  idealBind as k = bindNonEmpty as (idealToNonEmpty . k)
+
+idealToNonEmpty :: Ideal TwoOrMore a -> NonEmpty a
+idealToNonEmpty = either pure toNonEmpty . runIdeal
+
+bindNonEmpty :: TwoOrMore a -> (a -> NonEmpty b) -> TwoOrMore b
+bindNonEmpty (TwoOrMore a1 a2 as) k = case (k a1, k a2) of
+  (b1 :| [], b2 :| []) -> TwoOrMore b1 b2 $ as >>= toList . k
+  (b1 :| [], b2 :| bs) -> TwoOrMore b1 b2 $ bs ++ (as >>= toList . k)
+  (b1 :| b2 : bs, bs') -> TwoOrMore b1 b2 $ bs ++ toList bs' ++ (as >>= toList . k)
diff --git a/test/CoidealExample.hs b/test/CoidealExample.hs
new file mode 100644
--- /dev/null
+++ b/test/CoidealExample.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE RankNTypes #-}
+module CoidealExample where
+
+import Control.Comonad
+import Control.Comonad.Coideal
+import Numeric.Natural (Natural)
+
+-- * The example coideal
+
+-- | Example coideal comonad
+data A x = Src x x | Tgt x
+  deriving (Show, Eq, Functor)
+
+instance Comonad A where
+  extract (Src x _) = x
+  extract (Tgt x) = x
+
+  duplicate ax@(Src _ x1) = Src ax (Tgt x1)
+  duplicate ax@(Tgt _) = Tgt ax
+
+-- | the only one nontrivial cokleisli arrow
+advance :: A x -> x
+advance ax = case ax of
+  Src _ x' -> x'
+  Tgt x -> x
+
+-- Accumulating store
+data Accum x = Accum Natural (Natural -> x)
+  deriving Functor
+
+instance Comonad Accum where
+  extract (Accum _ f) = f 0
+  duplicate (Accum n f) = Accum n $ \m1 -> Accum (n + m1) (\m2 -> f (m1 + m2))
+
+data Accum' x = Accum' Natural (Natural -> x)
+  deriving Functor
+
+fromAccum' :: Coideal Accum' x -> Accum x
+fromAccum' wx' = case runCoideal wx' of
+  (x, Accum' n f) -> Accum n (\m -> if m == 0 then x else f (m - 1))
+
+toAccum' :: Accum x -> Coideal Accum' x
+toAccum' (Accum n f) = Coideal (f 0, Accum' n (\m -> f (m + 1)))
+
+instance ComonadCoideal Accum' where
+  coidealExtend k (Accum' n f) = Accum' n $ \m1 -> k (toAccum' $ Accum (n + 1 + m1) (\m2 -> f (m1 + m2)))
+
+-- | Comonad morphism to A.
+nextMultipleOf :: Natural -> Accum x -> A x
+nextMultipleOf d (Accum n f) = case n `mod` d of
+  0 -> Tgt (f 0)
+  r -> Src (f 0) (f (d - r))
+
+-- | ComonadIdeal morphism to A'
+nextMultipleOf' :: Natural -> Accum' x -> A' x
+nextMultipleOf' d (Accum' n f) = case n `mod` d of
+  0 -> Tgt'
+  r -> Src' (f (d - r - 1))
+
+-- | The coideal part of A
+data A' x = Src' x | Tgt'
+  deriving (Show, Eq, Functor)
+
+instance ComonadCoideal A' where
+  coidealExtend f (Src' x) = Src' (f $ Coideal (x, Tgt'))
+  coidealExtend _ Tgt' = Tgt'
+
+fromA' :: Coideal A' x -> A x
+fromA' ax' = case runCoideal ax' of
+  (x, Src' x') -> Src x x'
+  (x, Tgt') -> Tgt x
+
+toA' :: A x -> Coideal A' x
+toA' (Src x x') = Coideal (x, Src' x')
+toA' (Tgt x) = Coideal (x, Tgt')
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,218 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ExtendedDefaultRules #-}
+{-# OPTIONS_GHC -Wno-type-defaults #-}
+{-# LANGUAGE TypeOperators #-}
+module Main (main) where
+
+import System.IO (stderr, hPutStrLn)
+import System.Exit (exitFailure)
+
+import Data.Char (toUpper)
+import Data.Foldable (toList)
+import Data.Proxy
+import Data.Semigroup (Min(..))
+import Numeric.Natural (Natural)
+
+import Data.List.NonEmpty (NonEmpty(..))
+import Control.Monad.Isolated
+import Control.Monad.Ideal
+import Data.Functor.KeepLeft
+import Data.List.TwoOrMore
+import Data.List.NotOne
+import Control.Monad.Coproduct
+
+import Control.Comonad.Coideal
+import CoidealExample
+
+putErr :: String -> IO ()
+putErr = hPutStrLn stderr
+
+(===) :: (Show a, Eq a) => a -> a -> String -> IO ()
+(===) x y name = if x == y then pure () else putErr errMsg >> exitFailure
+  where
+    sx = show x
+    sy = show y
+    errMsg = "failure: " ++ name ++ "\n\t" ++ sx ++ " =/= " ++ sy
+
+infix 1 ===
+
+item :: String -> (String -> IO ()) -> IO ()
+item = flip ($)
+
+main :: IO ()
+main = do
+  testsIsolated
+  testsIdeal
+  testsKeepLeft
+  testsTwoOrMore
+  testsNotOne
+  testsCoproduct
+  testsCoideal
+
+testsIsolated :: IO ()
+testsIsolated = do
+  -- Unite
+  item "fmapUnite" $ fmap @(Unite []) succ (Unite (Left 1)) === Unite (Left 2)
+  item "fmapUnite" $ fmap @(Unite []) succ (Unite (Right [1,1])) === Unite (Right [2,2])
+  item "toListUnite" $ toList (Unite (Left 'a')) === ['a']
+  item "hoistUnite" $ hoistUnite toList (Unite (Left 'a')) === Unite (Left 'a')
+  item "hoistUnite" $ hoistUnite toList (Unite (Right Nothing)) === Unite (Right [])
+
+  item "Isolated Proxy" $
+    (Proxy `impureBind` pure) === Unite (Right Proxy)
+  item "Isolated ((,) s)" $
+    ((Min 1, 2) `impureBind` \x -> Unite (Right (Min x, x + 1)))
+      ===
+    Unite (Right (Min 1, 3))
+
+testsIdeal :: IO ()
+testsIdeal = do
+  item "MonadIdeal ((,) s)" $
+    ((Min 1, 2) `idealBind` pure) === (Min 1, 2)
+  item "MonadIdeal ((,) s)" $
+    ((Min 1, 2) `idealBind` \x -> (ideal . Right) (Min 0, x + 1))
+      ===
+    (Min 0, 3)
+
+testsKeepLeft :: IO ()
+testsKeepLeft = do
+  item "Semigroup (KeepLeft c)" $ KeepLeft 1 <> KeepLeft 5 === KeepLeft 1
+  item "Semigroup (KeepLeft c)" $ KeepLeft 1 <> KeepLeft 6 === KeepLeft 1
+  item "Semigroup (KeepLeft c)" $ KeepLeft 2 <> KeepLeft 5 === KeepLeft 2
+  item "Semigroup (KeepLeft c)" $ KeepLeft 2 <> KeepLeft 6 === KeepLeft 2
+  
+  item "MonadIdeal (KeepLeft c)" $
+    (KeepLeft 1 `idealBind` pure) === KeepLeft 1
+  item "MonadIdeal (KeepLeft c)" $
+    (KeepLeft 1 `idealBind` \a -> ideal . Right $ KeepLeft (10 + a)) === KeepLeft 1
+
+testsTwoOrMore :: IO ()
+testsTwoOrMore = do
+  item "twoOrMore" $ twoOrMore ("a" :| []) === Left "a"
+  item "twoOrMore" $ twoOrMore ("a" :| ["b", "c"]) === Right (TwoOrMore "a" "b" ["c"])
+
+  let abc = TwoOrMore 'a' 'b' ['c']
+
+  item "MonadIdeal TwoOrMore" $
+    (abc `idealBind` \x -> pure (toUpper x)) === TwoOrMore 'A' 'B' ['C']
+  item "MonadIdeal TwoOrMore" $
+    (abc `idealBind` \x -> ideal . Right $ TwoOrMore x x [x, x]) === TwoOrMore 'a' 'a' "aabbbbcccc"
+  
+testsNotOne :: IO ()
+testsNotOne = do
+  item "notOne" $ notOne "" === Right Zero
+  item "notOne" $ notOne "a" === Left 'a'
+  item "notOne" $ notOne "abcd" === Right (Multiple $ TwoOrMore 'a' 'b' "cd")
+
+  let abc = Multiple $ TwoOrMore 'a' 'b' ['c']
+      empty' = Zero
+      quadruple x = Multiple $ TwoOrMore x x [x, x]
+
+  item "Isolated NotOne" $
+    (abc `impureBind` \x -> pure (toUpper x)) === Unite (Right (fmap toUpper abc))
+  item "Isolated NotOne" $
+    (abc `impureBind` \x -> if x == 'a' then pure 'M' else Unite (Right empty')) === pure 'M'
+  item "Isolated NotOne" $
+    (abc `impureBind` \x -> Unite . Right $ quadruple x)
+      ===
+    (Unite . Right . Multiple $ TwoOrMore 'a' 'a' "aabbbbcccc")
+
+impure :: f a -> Unite f a
+impure = Unite . Right
+
+injectMonad1 :: Functor m0 => Unite m0 a -> Unite (m0 :+ n0) a
+injectMonad1 = hoistUnite inject1
+
+injectMonad2 :: Functor n0 => Unite n0 a -> Unite (m0 :+ n0) a
+injectMonad2 = hoistUnite inject2
+
+testsCoproduct :: IO ()
+testsCoproduct = do
+  let abc = Multiple $ TwoOrMore 'a' 'b' ['c']
+      double x = Multiple $ TwoOrMore x x [] 
+      quadruple x = Multiple $ TwoOrMore x x [x, x]
+      abc' = TwoOrMore 'a' 'b' ['c']
+  item "Coproduct-inject1-inject1" $
+    let m1 :: Unite (NotOne :+ NotOne) Char
+        m1 = do
+          x <- injectMonad1 $ impure abc
+          injectMonad1 $ impure (quadruple x)
+        m2 = injectMonad1 $ impure abc >>= impure . quadruple
+    in m1 === m2
+  item "Coproduct-inject2-inject2" $
+    let m1 :: Unite (NotOne :+ NotOne) Char
+        m1 = do
+          x <- injectMonad2 $ impure abc
+          injectMonad2 $ impure (quadruple x)
+        m2 = injectMonad2 $ impure abc >>= impure . quadruple
+    in m1 === m2
+  
+  item "Coproduct-collapse" $
+    let m1 :: Unite (NotOne :+ NotOne) Char
+        m1 = do
+          x <- injectMonad1 $ impure abc
+          y <- injectMonad2 $ impure abc
+          injectMonad2 $ if x == y then pure () else impure Zero
+          pure y
+        m2 = injectMonad1 $ impure abc
+    in m1 === m2
+  
+  item "Coproduct-eitherMonad" $
+    let m1 :: [Char]
+        m1 = either pure (eitherMonad toList toList) . runUnite $ do
+          x <- injectMonad1 $ impure abc
+          y <- if x == 'a' then injectMonad2 (impure abc) else injectMonad1 (impure abc)
+          if y == 'b' then injectMonad2 (impure (double y)) else pure y
+        m2 = "abbcabbcabbc"
+    in m1 === m2
+  
+  let f :: Char -> Ideal (TwoOrMore :+ TwoOrMore) Char
+      f 'a' = ideal . Right $ inject1 (TwoOrMore 'A' 'A' [])
+      f 'b' = ideal . Right $ inject2 (TwoOrMore 'B' 'B' [])
+      f c   = ideal . Left $ c
+  
+  item "Coproduct-idealBind" $
+    let m1 :: (TwoOrMore :+ TwoOrMore) Char
+        m1 = inject1 abc' `idealBind` f
+        
+        m2 :: (TwoOrMore :+ TwoOrMore) Char
+        m2 = Coproduct $ Left $ Mutual $
+          TwoOrMore
+            (Left 'A')
+            (Left 'A')
+            [
+              Right (Mutual $ TwoOrMore (Left 'B') (Left 'B') [])
+            , Left 'c'
+            ]
+    in m1 === m2
+  
+  item "Coproduct-||||" $
+    let m1 = id |||| id $ inject1 abc' `idealBind` f
+        m2 = TwoOrMore 'A' 'A' ['B', 'B', 'c']
+    in m1 === m2
+
+accumToProd :: Accum' x -> (A' :* A') x
+accumToProd = nextMultipleOf' 3 &&&& nextMultipleOf' 5
+
+s1 :: Accum' Natural
+(_, s1) = runCoideal $ toAccum' (Accum 1 id)
+
+testsCoideal :: IO ()
+testsCoideal = do
+  let 
+      w1, w2 :: (A' :* A') Natural
+      w1 = accumToProd s1
+      w2 = CoidealProduct (cons 2 path, path)
+        where
+          cons :: a -> Mutual (,) A' A' a -> Mutual (,) A' A' a
+          cons a as = Mutual $ Src' (a, as)
+          
+          nil :: Mutual (,) A' A' a
+          nil = Mutual Tgt'
+
+          infixr 4 `cons`
+
+          path :: Mutual (,) A' A' Natural
+          path = 4 `cons` 5 `cons` 9 `cons` 11 `cons` 14 `cons` nil
+  item "Coideal-&&&&" $ w1 === w2