diff --git a/README.md b/README.md
index ef54baf..b6e2035 100644
--- a/README.md
+++ b/README.md
@@ -64,22 +64,22 @@ are some examples:
     ```
 
     Using the `elaborateWriterT` elaborator, you'll get "Goodbye world!", whereas with the `elaborateWriterTransactionalT` elaborator, you'll get "Hello world!".
-    For more details, please refer to the [complete code](heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
+    For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/develop/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
 
 * Extracting Multi-shot Delimited Continuations
 
     In handling higher-order effects, it's easy to work with multi-shot delimited continuations.
     This enables an almost complete emulation of "Algebraic Effects and Handlers".
     For more details, please refer to
-    [Example 3 - Delimited Continuation](<docs/examples/03 Delimited Continuation.md>) .
+    [Example 3 - Delimited Continuation](<https://github.com/sayo-hs/heftia/blob/develop/docs/examples/03%20Delimited%20Continuation.md>) .
 
 Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being
 eliminated.
 
-Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs).
+Heftia is the current main focus of the [Sayo Project](https://github.com/sayo-hs).
 
 ## Documentation
-Examples with explanations can be found in the [docs/examples/](docs/examples/) directory.
+Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.
 
 ## Future Plans
 * Benchmarking
@@ -90,17 +90,16 @@ Examples with explanations can be found in the [docs/examples/](docs/examples/)
     and others.
 
 ## License
-The license is MPL 2.0. Please refer to the [NOTICE](NOTICE).
+The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/develop/NOTICE).
 Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed
 under CC BY-SA 4.0.
 
 ## Your contributions are welcome!
-Please see [CONTRIBUTING.md](CONTRIBUTING.md).
+Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/develop/CONTRIBUTING.md).
 
 ## Credits
-Parts of this project have been adapted or inspired by the following resources:
+Parts of this project have been inspired by the following resources:
 
 * **[Hefty Algebras -- The Artifact](https://github.com/heft-lang/POPL2023)**
     * **Copyright** (c) 2023 Casper Bach Poulsen and Cas van der Rest
     * **License**: MIT
-    * **Modifications**: The inspiration for the idea of Heftia. Code was used in the Data.{[Free](https://github.com/sayo-hs/heftia/blob/165a5246ffbf473210bfb26a17da3e37d79a5346/heftia/src/Data/Free/Sum.hs),[Hefty](https://github.com/sayo-hs/heftia/blob/165a5246ffbf473210bfb26a17da3e37d79a5346/heftia/src/Data/Hefty/Sum.hs)}.Sum.
diff --git a/heftia-effects/README.md b/heftia-effects/README.md
index ff32901..32d46ee 120000
--- a/heftia-effects/README.md
+++ b/heftia-effects/README.md
@@ -1 +1 @@
-../heftia/README.md
\ No newline at end of file
+../README.md
\ No newline at end of file
diff --git a/heftia/README.md b/heftia/README.md
deleted file mode 100644
index cfa99dc..0000000
--- a/heftia/README.md
+++ /dev/null
@@ -1,95 +0,0 @@
-# Heftia
-Heftia, a composition of hefty trees and co-Yoneda, is a higher-order effects
-version of Freer.
-
-The paper
-* Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular
-    Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7,
-    POPL, Article 62 (January 2023), 31 pages. <https://doi.org/10.1145/3571255>
-
-inspires this library.
-Hefty trees, proposed by the above paper, are extensions of free monads,
-allowing for a straightforward treatment of higher-order effects.
-
-This library offers Heftia monads and Freer monads, encoded into data
-types in several ways to enable tuning in pursuit of high performance.
-
-Additionally, it's designed to operate as a handler system based
-on [`classy-effects`](https://github.com/sayo-hs/classy-effects), which aims to
-standardize and unify the definitions of effects in Haskell.
-
-Compared to existing Effect System libraries in Haskell that handle higher-order effects, this
-library's approach allows for a more effortless and flexible handling of higher-order effects. Here
-are some examples:
-
-* Two interpretations of the `censor` effect for Writer
-
-    Let's consider the following Writer effectful program:
-
-    ```hs
-    hello :: (Writer String m, Monad m) => m ()
-    hello = do
-        tell "Hello"
-        tell " world!"
-
-    censorHello :: (Writer String m, Monad m) => m ()
-    censorHello =
-        censor
-            (\s -> if s == "Hello" then "Goodbye" else s)
-            hello
-    ```
-
-    For `censorHello`, should the final written string be `"Goodbye world!"`? Or should it be `"Hello world!"`?
-    With Heftia, you can freely choose either behavior depending on which higher-order effect interpreter (which we call an elaborator) you use.
-
-    ```hs
-    main :: IO ()
-    main = runFreerEffects do
-        (s :: String, _) <-
-            interpretTell
-                . runElaborate' (elaborateWriterT @String)
-                $ censorHello
-
-        (sTransactional :: String, _) <-
-            interpretTell
-                . runElaborate' (elaborateWriterTransactionalT @String)
-                $ censorHello
-
-        sendIns $ putStrLn $ "Normal: " <> s
-        sendIns $ putStrLn $ "Transactional: " <> sTransactional
-    ```
-
-    Using the `elaborateWriterT` elaborator, you'll get "Goodbye world!", whereas with the `elaborateWriterTransactionalT` elaborator, you'll get "Hello world!".
-    For more details, please refer to the [complete code](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/Example/Writer/Main.hs) and the [implementation of the elaborator](https://github.com/sayo-hs/heftia/blob/master/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs).
-
-* Extracting Multi-shot Delimited Continuations
-
-    In handling higher-order effects, it's easy to work with multi-shot delimited continuations.
-    This enables an almost complete emulation of "Algebraic Effects and Handlers".
-    For more details, please refer to
-    [Example 3 - Delimited Continuation](<https://github.com/sayo-hs/heftia/blob/master/docs/examples/03%20Delimited%20Continuation.md>) .
-
-Furthermore, the structure of Heftia is theoretically straightforward, with ad-hoc elements being
-eliminated.
-
-Heftia is the second objective of the [Sayo Project](https://github.com/sayo-hs).
-
-## Documentation
-Examples with explanations can be found in the [docs/examples/](https://github.com/sayo-hs/heftia/tree/master/docs/examples) directory.
-
-## Future Plans
-* Benchmarking
-* Enriching the documentation
-* Completing missing definitions such as
-    * the Heftia monad transformer encoded in tree structure
-    * handlers for the `Accum`, `Coroutine`, `Fresh`, `Input`, `Output` effect classes
-
-    and others.
-
-## License
-The license is MPL 2.0. Please refer to the [NOTICE](https://github.com/sayo-hs/heftia/blob/master/NOTICE).
-Additionally, this README.md and the documents under the `docs`/`docs-ja` directory are licensed
-under CC BY-SA 4.0.
-
-## Your contributions are welcome!
-Please see [CONTRIBUTING.md](https://github.com/sayo-hs/heftia/blob/master/CONTRIBUTING.md).
diff --git a/heftia/README.md b/heftia/README.md
new file mode 120000
index 0000000..32d46ee
--- /dev/null
+++ b/heftia/README.md
@@ -0,0 +1 @@
+../README.md
\ No newline at end of file
diff --git a/heftia/heftia.cabal b/heftia/heftia.cabal
index beb06b4..88ebbe9 100644
--- a/heftia/heftia.cabal
+++ b/heftia/heftia.cabal
@@ -35,8 +35,7 @@ maintainer:         Yamada Ryo <ymdfield@outlook.jp>
 
 -- A copyright notice.
 copyright:
-    2023 Yamada Ryo,
-    2023 Casper Bach Poulsen and Cas van der Rest
+    2023 Yamada Ryo
 category: Control, Monads
 
 extra-source-files:
@@ -59,8 +58,9 @@ library
         Control.Effect.Free
         Control.Effect.ExtensibleChurch
         Control.Effect.ExtensibleTree
+        Control.Effect.ExtensibleTreeA
+        Control.Effect.ExtensibleFastA
         Control.Hefty
-        Control.Hefty.SFunctor
         Control.Freer
         Control.Monad.Freer
         Control.Monad.Freer.Church
diff --git a/heftia/src/Control/Effect/ExtensibleChurch.hs b/heftia/src/Control/Effect/ExtensibleChurch.hs
index cd55d09..acf0b70 100644
--- a/heftia/src/Control/Effect/ExtensibleChurch.hs
+++ b/heftia/src/Control/Effect/ExtensibleChurch.hs
@@ -2,6 +2,15 @@
 -- License, v. 2.0. If a copy of the MPL was not distributed with this
 -- file, You can obtain one at https://mozilla.org/MPL/2.0/.
 
+{- |
+Copyright   :  (c) 2023-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the Church-encoded Freer monad.
+-}
 module Control.Effect.ExtensibleChurch where
 
 import Control.Effect.Free (EffectfulF)
diff --git a/heftia/src/Control/Effect/ExtensibleFastA.hs b/heftia/src/Control/Effect/ExtensibleFastA.hs
new file mode 100644
index 0000000..356e492
--- /dev/null
+++ b/heftia/src/Control/Effect/ExtensibleFastA.hs
@@ -0,0 +1,27 @@
+-- This Source Code Form is subject to the terms of the Mozilla Public
+-- License, v. 2.0. If a copy of the MPL was not distributed with this
+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+{- |
+Copyright   :  (c) 2023-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the fast-encoded free applicative.
+
+See "Control.Applicative.Free.Fast".
+-}
+module Control.Effect.ExtensibleFastA where
+
+import Control.Applicative.Free.Fast (Ap)
+import Control.Effect.Free (EffectfulF)
+import Control.Effect.Hefty (Effectful)
+import Data.Hefty.Extensible (ExtensibleUnion)
+
+infixr 4 !!
+infixr 3 !
+
+type (!!) = Effectful ExtensibleUnion Ap
+type (!) = EffectfulF ExtensibleUnion Ap
diff --git a/heftia/src/Control/Effect/ExtensibleTree.hs b/heftia/src/Control/Effect/ExtensibleTree.hs
index d756cfc..856e433 100644
--- a/heftia/src/Control/Effect/ExtensibleTree.hs
+++ b/heftia/src/Control/Effect/ExtensibleTree.hs
@@ -2,6 +2,15 @@
 -- License, v. 2.0. If a copy of the MPL was not distributed with this
 -- file, You can obtain one at https://mozilla.org/MPL/2.0/.
 
+{- |
+Copyright   :  (c) 2023-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the tree-structured encoded Freer monad.
+-}
 module Control.Effect.ExtensibleTree where
 
 import Control.Effect.Free (EffectfulF)
diff --git a/heftia/src/Control/Effect/ExtensibleTreeA.hs b/heftia/src/Control/Effect/ExtensibleTreeA.hs
new file mode 100644
index 0000000..f6abff5
--- /dev/null
+++ b/heftia/src/Control/Effect/ExtensibleTreeA.hs
@@ -0,0 +1,28 @@
+-- This Source Code Form is subject to the terms of the Mozilla Public
+-- License, v. 2.0. If a copy of the MPL was not distributed with this
+-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+
+{- |
+Copyright   :  (c) 2023-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the tree-structured encoded free
+applicative.
+
+See "Control.Applicative.Free".
+-}
+module Control.Effect.ExtensibleTreeA where
+
+import Control.Applicative.Free (Ap)
+import Control.Effect.Free (EffectfulF)
+import Control.Effect.Hefty (Effectful)
+import Data.Hefty.Extensible (ExtensibleUnion)
+
+infixr 4 !!
+infixr 3 !
+
+type (!!) = Effectful ExtensibleUnion Ap
+type (!) = EffectfulF ExtensibleUnion Ap
diff --git a/heftia/src/Control/Effect/Free.hs b/heftia/src/Control/Effect/Free.hs
index 392b8d4..22e2b5f 100644
--- a/heftia/src/Control/Effect/Free.hs
+++ b/heftia/src/Control/Effect/Free.hs
@@ -6,7 +6,7 @@
 -- file, You can obtain one at https://mozilla.org/MPL/2.0/.
 
 {- |
-Copyright   :  (c) 2023 Yamada Ryo
+Copyright   :  (c) 2023-2024 Yamada Ryo
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
 Stability   :  experimental
@@ -18,17 +18,16 @@ on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).
 module Control.Effect.Free where
 
 import Control.Applicative (Alternative)
-import Control.Effect.Class (LiftIns (LiftIns), NopS, SendIns, sendIns, type (~>))
+import Control.Effect.Class (LiftIns (LiftIns), NopS, SendIns, sendIns, unliftIns, type (~>))
+import Control.Effect.Class.Machinery.HFunctor (caseH, type (:+:) (Inr))
 import Control.Effect.Hefty (
     DecompF,
     EffHeadF,
-    EffUnion (EffUnion),
+    EffTailF,
     Effectful (Effectful),
     MemberF,
     MultiToUnionF,
     SumToUnionF,
-    unEffUnion,
-    unEffUnionH,
     unEffectful,
  )
 import Control.Freer (Freer, InsClass, interpretFreer, liftIns, retractFreer, transformFreer)
@@ -58,7 +57,7 @@ import Data.Hefty.Union (
  )
 import Data.Kind (Type)
 
--- | A common wrapper data type for representing first-order effectful programs.
+-- | A common wrapper data type for representing first-order extensible effectful programs.
 newtype
     EffectfulF
         (u :: [SigClass] -> SigClass)
@@ -98,10 +97,10 @@ instance (MemberF u e es, Freer c fr) => SendIns e (EffectfulF u fr es) where
 
 -- | Interpret the leading first-order effect class.
 interpretF ::
-    forall er r f u c.
-    (Freer c f, Union u, DecompF u er r) =>
-    (EffHeadF u er ~> EffectfulF u f r) ->
-    EffectfulF u f er ~> EffectfulF u f r
+    forall er f u c.
+    (Freer c f, Union u, DecompF u er) =>
+    (MultiToUnionF u (EffHeadF er) ~> EffectfulF u f (EffTailF er)) ->
+    EffectfulF u f er ~> EffectfulF u f (EffTailF er)
 interpretF i =
     overEffectfulF $ interpretFreer \u ->
         case decomp u of
@@ -110,30 +109,34 @@ interpretF i =
 
 -- | Interpret the leading first-order effect class using a monad transformer.
 interpretTF ::
-    forall t er r f u.
-    (MonadFreer f, Union u, DecompF u er r, MonadTrans t, Monad (t (EffectfulF u f r))) =>
-    (EffHeadF u er ~> t (EffectfulF u f r)) ->
-    EffectfulF u f er ~> t (EffectfulF u f r)
+    forall t er f u.
+    (MonadFreer f, Union u, DecompF u er, MonadTrans t, Monad (t (EffectfulF u f (EffTailF er)))) =>
+    (MultiToUnionF u (EffHeadF er) ~> t (EffectfulF u f (EffTailF er))) ->
+    EffectfulF u f er ~> t (EffectfulF u f (EffTailF er))
 interpretTF i = retractFreer . transformFreer (caseF i lift) . splitEffF @f
 {-# INLINE interpretTF #-}
 
 -- | Interpret the leading first-order effect class using a delimited continuation.
 interpretKF ::
-    forall er r' a r f u.
-    (MonadFreer f, Union u, DecompF u er r) =>
-    (a -> EffectfulF u f r r') ->
-    (forall x. (x -> EffectfulF u f r r') -> EffHeadF u er x -> EffectfulF u f r r') ->
+    forall er r a f u.
+    (MonadFreer f, Union u, DecompF u er) =>
+    (a -> EffectfulF u f (EffTailF er) r) ->
+    ( forall x.
+      (x -> EffectfulF u f (EffTailF er) r) ->
+      MultiToUnionF u (EffHeadF er) x ->
+      EffectfulF u f (EffTailF er) r
+    ) ->
     EffectfulF u f er a ->
-    EffectfulF u f r r'
+    EffectfulF u f (EffTailF er) r
 interpretKF k i = (`runContT` k) . interpretContTF \e -> ContT (`i` e)
 {-# INLINE interpretKF #-}
 
 -- | Interpret the leading first-order effect class using a continuation monad transformer.
 interpretContTF ::
-    forall er r' r f u.
-    (MonadFreer f, Union u, DecompF u er r) =>
-    (EffHeadF u er ~> ContT r' (EffectfulF u f r)) ->
-    EffectfulF u f er ~> ContT r' (EffectfulF u f r)
+    forall er r f u.
+    (MonadFreer f, Union u, DecompF u er) =>
+    (MultiToUnionF u (EffHeadF er) ~> ContT r (EffectfulF u f (EffTailF er))) ->
+    EffectfulF u f er ~> ContT r (EffectfulF u f (EffTailF er))
 interpretContTF i =
     transCont
         . interpretFreerK (detransContT . caseF i lift)
@@ -157,37 +160,37 @@ transformAllF f = overEffectfulF $ transformFreer f
 {-# INLINE transformAllF #-}
 
 raiseF ::
-    forall e1 e f u c.
-    (Freer c f, Union u) =>
-    EffectfulF u f e ~> EffectfulF u f (e1 + e)
+    forall er f u c.
+    (Freer c f, Union u, DecompF u er) =>
+    EffectfulF u f (EffTailF er) ~> EffectfulF u f er
 raiseF = transformAllF weaken
 {-# INLINE raiseF #-}
 
 raise2F ::
-    forall e1 e2 e f u c.
-    (Freer c f, Union u) =>
-    EffectfulF u f e ~> EffectfulF u f (e1 + e2 + e)
+    forall e2 e1r f u c.
+    (Freer c f, Union u, DecompF u e1r) =>
+    EffectfulF u f (EffTailF e1r) ~> EffectfulF u f (e2 + e1r)
 raise2F = transformAllF weaken2
 {-# INLINE raise2F #-}
 
 raise3F ::
-    forall e1 e2 e3 e f u c.
-    (Freer c f, Union u) =>
-    EffectfulF u f e ~> EffectfulF u f (e1 + e2 + e3 + e)
+    forall e3 e2 e1r f u c.
+    (Freer c f, Union u, DecompF u e1r) =>
+    EffectfulF u f (EffTailF e1r) ~> EffectfulF u f (e3 + e2 + e1r)
 raise3F = transformAllF weaken3
 {-# INLINE raise3F #-}
 
 raise4F ::
-    forall e1 e2 e3 e4 e f u c.
-    (Freer c f, Union u) =>
-    EffectfulF u f e ~> EffectfulF u f (e1 + e2 + e3 + e4 + e)
+    forall e4 e3 e2 e1r f u c.
+    (Freer c f, Union u, DecompF u e1r) =>
+    EffectfulF u f (EffTailF e1r) ~> EffectfulF u f (e4 + e3 + e2 + e1r)
 raise4F = transformAllF weaken4
 {-# INLINE raise4F #-}
 
 raiseUnderF ::
-    forall e1 e2 e f u c.
-    (Freer c f, Union u) =>
-    EffectfulF u f (e1 + e) ~> EffectfulF u f (e1 + e2 + e)
+    forall e1r e2 f u c.
+    (Freer c f, Union u, DecompF u e1r) =>
+    EffectfulF u f (e2 + EffTailF e1r) ~> EffectfulF u f (e2 + e1r)
 raiseUnderF = transformAllF weakenUnder
 {-# INLINE raiseUnderF #-}
 
@@ -199,18 +202,18 @@ flipEffF = transformAllF flipUnion
 {-# INLINE flipEffF #-}
 
 splitEffF ::
-    forall f' er r f u c.
-    (Freer c f', Freer c f, Union u, DecompF u er r) =>
-    EffectfulF u f er ~> f' (EffHeadF u er + EffectfulF u f r)
+    forall f' er f u c.
+    (Freer c f', Freer c f, Union u, DecompF u er) =>
+    EffectfulF u f er ~> f' (MultiToUnionF u (EffHeadF er) + EffectfulF u f (EffTailF er))
 splitEffF (EffectfulF f) =
     f & interpretFreer \u -> case decomp u of
         Left e -> liftIns $ L1 e
         Right e -> liftIns $ R1 $ EffectfulF $ liftIns e
 
 mergeEffF ::
-    forall f' e r f u c.
-    (Freer c f', Freer c f, Union u) =>
-    f' (MultiToUnionF u e + EffectfulF u f r) ~> EffectfulF u f (e + r)
+    forall f' er f u c.
+    (Freer c f', Freer c f, Union u, DecompF u er) =>
+    f' (MultiToUnionF u (EffHeadF er) + EffectfulF u f (EffTailF er)) ~> EffectfulF u f er
 mergeEffF =
     EffectfulF
         . interpretFreer
@@ -219,18 +222,18 @@ mergeEffF =
                 (transformFreer weaken . unEffectfulF)
             )
 
-fromEffectful :: forall e f u c. (Freer c f, Union u) => Effectful u f NopS e ~> EffectfulF u f e
-fromEffectful =
+toEffectfulF :: forall e f u c. (Freer c f, Union u) => Effectful u f NopS e ~> EffectfulF u f e
+toEffectfulF =
     EffectfulF
-        . transformFreer (caseF (absurdUnion . unEffUnionH) id . unEffUnion)
+        . transformFreer (caseH absurdUnion unliftIns)
         . unHefty
         . unEffectful
-{-# INLINE fromEffectful #-}
+{-# INLINE toEffectfulF #-}
 
-toEffectful :: forall e f u c. Freer c f => EffectfulF u f e ~> Effectful u f NopS e
-toEffectful =
+fromEffectfulF :: forall e f u c. Freer c f => EffectfulF u f e ~> Effectful u f NopS e
+fromEffectfulF =
     Effectful
         . Hefty
-        . transformFreer (EffUnion . R1)
+        . transformFreer (Inr . LiftIns)
         . unEffectfulF
-{-# INLINE toEffectful #-}
+{-# INLINE fromEffectfulF #-}
diff --git a/heftia/src/Control/Effect/Hefty.hs b/heftia/src/Control/Effect/Hefty.hs
index d23d3d6..dd2ab7c 100644
--- a/heftia/src/Control/Effect/Hefty.hs
+++ b/heftia/src/Control/Effect/Hefty.hs
@@ -5,7 +5,7 @@
 -- file, You can obtain one at https://mozilla.org/MPL/2.0/.
 
 {- |
-Copyright   :  (c) 2023 Yamada Ryo
+Copyright   :  (c) 2023-2024 Yamada Ryo
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
 Stability   :  experimental
@@ -17,14 +17,25 @@ on [@classy-effects@](https://hackage.haskell.org/package/classy-effects).
 module Control.Effect.Hefty where
 
 import Control.Applicative (Alternative)
-import Control.Effect.Class (LiftIns (LiftIns), NopI, NopS, SendIns, SendSig, sendIns, sendSig)
-import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:))
+import Control.Arrow ((>>>))
+import Control.Effect.Class (
+    LiftIns (LiftIns),
+    NopI,
+    NopS,
+    SendIns,
+    SendSig,
+    sendIns,
+    sendSig,
+    unliftIns,
+ )
+import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
 import Control.Freer (Freer, InsClass, interpretFreer, liftIns, transformFreer)
 import Control.Hefty (Hefty (Hefty), SigClass, overHefty, unHefty)
 import Control.Monad (MonadPlus)
 import Control.Monad.Base (MonadBase)
 import Control.Monad.IO.Class (MonadIO)
-import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
+import Data.Coerce (coerce)
+import Data.Free.Sum (type (+))
 import Data.Hefty.Union (
     ForallHFunctor,
     HFunctorUnion,
@@ -39,7 +50,8 @@ import Data.Hefty.Union (
 import Data.Kind (Type)
 
 {- |
-A common wrapper data type for representing first-order & higher-order effectful programs.
+A common wrapper data type for representing first-order & higher-order extensible effectful
+programs.
 -}
 newtype
     Effectful
@@ -49,13 +61,8 @@ newtype
         (ef :: InsClass)
         (a :: Type) = Effectful {unEffectful :: Hefty f (EffUnion u eh ef) a}
 
--- | Open union for higher-order effect classes and first-order effect classes.
-newtype EffUnion u eh ef f a = EffUnion
-    {unEffUnion :: (EffUnionH u (NormalizeSig eh) f + SumToUnionF u ef) a}
-
--- | A wrapper to provide an instance of t'HFunctor' for the open union.
-newtype EffUnionH (u :: [SigClass] -> SigClass) (e :: SigClass) f a = EffUnionH
-    {unEffUnionH :: SumToUnion u e f a}
+-- | Open union for first-order & higher-order effect classes.
+type EffUnion u eh ef = SumToUnion u (NormalizeSig eh) :+: LiftIns (SumToUnionF u ef)
 
 -- | Manipulate the inside of the t'Effectful' wrapper.
 overEffectful ::
@@ -83,12 +90,6 @@ type TailHFunctor u e = ForallHFunctor u (SumToUnionList u (NormalizeSig e))
 -- | t'HFunctor' constraint for effect classes that are either single or in an open union.
 type HeadHFunctor u e = HFunctor (MultiToUnionH u e)
 
-instance HFunctors u eh => HFunctor (EffUnion u eh ef) where
-    hfmap f = EffUnion . caseF (L1 . hfmap f) R1 . unEffUnion
-    {-# INLINE hfmap #-}
-
-deriving newtype instance HFunctor (SumToUnion u e) => HFunctor (EffUnionH u e)
-
 {- |
 Convert a given list of higher-order effect classes into a suitable representation type for each
 case of being empty, single, or multiple.
@@ -156,36 +157,81 @@ newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a}
     deriving newtype (HFunctor)
 
 {- |
-The higher-order effect class @er@ can be decomposed into the sum of t'EffHeadH' @u@ @er@ and @r@
-(@er ≅ EffHeadH u er :+: r@).
+The higher-order effect class @er@ can be decomposed into the sum of t'EffHead' @er@ and t'EffTail'
+@er@ (@er ≅ EffHead er :+: EffTail er@).
 -}
-type DecompH u er r =
-    SumToUnionList u (NormalizeSig er) ~ EffHeadH u er ': SumToUnionList u (NormalizeSig r)
+type DecompH u er =
+    SumToUnionList u (NormalizeSig er)
+        ~ MultiToUnionH u (EffHead er)
+        ': SumToUnionList u (NormalizeSig (EffTail er))
 
 {- |
-The first-order effect class @er@ can be decomposed into the sum of t'EffHeadF' @u@ @er@ and @r@
-(@er ≅ EffHeadF u er + r@).
+The first-order effect class @er@ can be decomposed into the sum of t'EffHeadF' @er@ and t'EffTailF'
+@er@ (@er ≅ EffHeadF er + EffTailF er@).
 -}
-type DecompF u er r = DecompH u (LiftIns er) (LiftIns r)
+type DecompF u er = DecompH u (LiftIns er)
 
-type family EffHead u e where
-    EffHead u (e :+: r) = MultiToUnion u e
-    EffHead u (SingleSig e) = e
+type family EffHead e where
+    EffHead (LiftIns e) = LiftIns (EffHeadF e)
+    EffHead (e :+: r) = e
+    EffHead e = e
 
-type EffHeadH u er = EffHead u (NormalizeSig er)
-type EffHeadF u er = EffHeadH u (LiftIns er) NopI
+type family EffHeadF e where
+    EffHeadF (e + r) = e
+    EffHeadF e = e
+
+type family EffTail e where
+    EffTail (LiftIns e) = LiftIns (EffTailF e)
+    EffTail (e :+: r) = r
+    EffTail e = NopS
+
+type family EffTailF e where
+    EffTailF (e + r) = r
+    EffTailF e = NopI
+
+compEff ::
+    (Freer c f, Union u, HFunctors u eh, DecompF u er) =>
+    Effectful u f eh (EffHeadF er + EffTailF er) ~> Effectful u f eh er
+compEff = coerce
+{-# INLINE compEff #-}
+
+compEffH ::
+    (Freer c f, Union u, HFunctors u er, DecompH u er) =>
+    Effectful u f (EffHead er :+: EffTail er) ef ~> Effectful u f er ef
+compEffH = coerce
+{-# INLINE compEffH #-}
+
+decompEff ::
+    (Freer c f, Union u, HFunctors u eh, DecompF u er) =>
+    Effectful u f eh er ~> Effectful u f eh (EffHeadF er + EffTailF er)
+decompEff = coerce
+{-# INLINE decompEff #-}
+
+decompEffH ::
+    (Freer c f, Union u, HFunctors u er, DecompH u er) =>
+    Effectful u f er ef ~> Effectful u f (EffHead er :+: EffTail er) ef
+decompEffH = coerce
+{-# INLINE decompEffH #-}
 
 deriving newtype instance Functor (Hefty f (EffUnion u eh ef)) => Functor (Effectful u f eh ef)
-deriving newtype instance Applicative (Hefty f (EffUnion u eh ef)) => Applicative (Effectful u f eh ef)
-deriving newtype instance Alternative (Hefty f (EffUnion u eh ef)) => Alternative (Effectful u f eh ef)
+deriving newtype instance
+    Applicative (Hefty f (EffUnion u eh ef)) =>
+    Applicative (Effectful u f eh ef)
+deriving newtype instance
+    Alternative (Hefty f (EffUnion u eh ef)) =>
+    Alternative (Effectful u f eh ef)
 deriving newtype instance Monad (Hefty f (EffUnion u eh ef)) => Monad (Effectful u f eh ef)
 deriving newtype instance MonadPlus (Hefty f (EffUnion u eh ef)) => MonadPlus (Effectful u f eh ef)
-deriving newtype instance (MonadBase b (Hefty f (EffUnion u eh ef)), Monad b) => MonadBase b (Effectful u f eh ef)
+deriving newtype instance
+    (MonadBase b (Hefty f (EffUnion u eh ef)), Monad b) =>
+    MonadBase b (Effectful u f eh ef)
 deriving newtype instance MonadIO (Hefty f (EffUnion u eh ef)) => MonadIO (Effectful u f eh ef)
 deriving newtype instance MonadFail (Hefty f (EffUnion u eh ef)) => MonadFail (Effectful u f eh ef)
 
 deriving stock instance Foldable (Hefty f (EffUnion u eh ef)) => Foldable (Effectful u f eh ef)
-deriving stock instance Traversable (Hefty f (EffUnion u eh ef)) => Traversable (Effectful u f eh ef)
+deriving stock instance
+    Traversable (Hefty f (EffUnion u eh ef)) =>
+    Traversable (Effectful u f eh ef)
 
 deriving newtype instance Eq (Hefty f (EffUnion u eh ef) a) => Eq (Effectful u f eh ef a)
 deriving newtype instance Ord (Hefty f (EffUnion u eh ef) a) => Ord (Effectful u f eh ef a)
@@ -195,7 +241,7 @@ deriving newtype instance Show (Hefty f (EffUnion u eh ef) a) => Show (Effectful
 type MemberF u e ef = MemberH u (LiftIns e) (LiftIns ef)
 
 instance (MemberF u e ef, Freer c fr) => SendIns e (Effectful u fr eh ef) where
-    sendIns = Effectful . Hefty . liftIns . EffUnion . R1 . injectRec . LiftIns
+    sendIns = Effectful . Hefty . liftIns . Inr . LiftIns . injectRec . LiftIns
     {-# INLINE sendIns #-}
 
 type MemberH u e eh = MemberRec u e (SumToUnionList u (NormalizeSig eh))
@@ -203,26 +249,25 @@ type MemberH u e eh = MemberRec u e (SumToUnionList u (NormalizeSig eh))
 -- enhance: introduce 'HFunctorCoercible' for performance
 instance (MemberH u e eh, Freer c fr, HFunctor e) => SendSig e (Effectful u fr eh ef) where
     sendSig =
-        Effectful . Hefty . liftIns . EffUnion . L1 . EffUnionH . injectRec . hfmap unEffectful
+        Effectful . Hefty . liftIns . Inl . injectRec . hfmap unEffectful
     {-# INLINE sendSig #-}
 
 -- | Using the provided interpretation function, interpret first-order effects.
 interpret ::
-    forall e r f u c.
-    (Freer c f, Union u) =>
-    (MultiToUnionF u e ~> Effectful u f NopS r) ->
-    Effectful u f NopS (e + r) ~> Effectful u f NopS r
+    forall er f u c.
+    (Freer c f, Union u, DecompF u er) =>
+    (MultiToUnionF u (EffHeadF er) ~> Effectful u f NopS (EffTailF er)) ->
+    Effectful u f NopS er ~> Effectful u f NopS (EffTailF er)
 interpret i =
     overEffectful
         . overHefty
         $ interpretFreer
-        $ caseF
-            (absurdUnion . unEffUnionH)
-            ( \u -> case decomp u of
+        $ caseH
+            absurdUnion
+            ( unliftIns >>> decomp >>> \case
                 Left e -> unHefty $ unEffectful $ i e
-                Right e -> liftIns $ EffUnion $ R1 e
+                Right e -> liftIns $ Inr $ LiftIns e
             )
-            . unEffUnion
 
 {- |
 Using the provided interpretation function, interpret first-order effects. For actions (scopes)
@@ -232,25 +277,23 @@ Note that if the interpretation function is stateful (i.e., not a monad morphism
 maintained across the scopes.
 -}
 interpretRec ::
-    forall e eh r f u c.
-    (Freer c f, Union u, HFunctors u eh) =>
-    (MultiToUnionF u e ~> Effectful u f eh r) ->
-    Effectful u f eh (e + r) ~> Effectful u f eh r
+    forall er eh f u c.
+    (Freer c f, Union u, HFunctors u eh, DecompF u er) =>
+    (MultiToUnionF u (EffHeadF er) ~> Effectful u f eh (EffTailF er)) ->
+    Effectful u f eh er ~> Effectful u f eh (EffTailF er)
 interpretRec i =
     overEffectful
         . overHefty
         $ interpretFreer
-        $ caseF
+        $ caseH
             ( liftIns
-                . EffUnion
-                . L1
-                . hfmap (unEffectful . interpretRec i . Effectful)
+                . Inl
+                . hfmap (unEffectful . interpretRec @er i . Effectful)
             )
-            ( \u -> case decomp u of
+            ( unliftIns >>> decomp >>> \case
                 Left e -> unHefty $ unEffectful $ i e
-                Right e -> liftIns $ EffUnion $ R1 e
+                Right e -> liftIns $ Inr $ LiftIns e
             )
-            . unEffUnion
 
 {- |
 Using the provided interpretation function, interpret higher-order effects. For actions (scopes)
@@ -260,50 +303,54 @@ Note that if the interpretation function is stateful (i.e., not a monad morphism
 maintained across the scopes.
 -}
 interpretRecH ::
-    forall e r ef f u c.
-    (Freer c f, Union u, HeadHFunctor u e, HFunctors u r) =>
-    (MultiToUnionH u e (Effectful u f r ef) ~> Effectful u f r ef) ->
-    Effectful u f (e :+: r) ef ~> Effectful u f r ef
+    forall er ef f u c.
+    (Freer c f, Union u, HeadHFunctor u (EffHead er), HFunctors u (EffTail er), DecompH u er) =>
+    ( MultiToUnionH u (EffHead er) (Effectful u f (EffTail er) ef)
+        ~> Effectful u f (EffTail er) ef
+    ) ->
+    Effectful u f er ef ~> Effectful u f (EffTail er) ef
 interpretRecH i =
     overEffectful
         . overHefty
         $ interpretFreer
-        $ caseF
-            ( \(EffUnionH u) -> case decomp u of
-                Left e ->
-                    unHefty $ unEffectful $ i $ hfmap int e
-                Right e ->
-                    liftIns $ EffUnion $ L1 $ EffUnionH $ hfmap (unEffectful . int) e
+        $ caseH
+            ( decomp >>> \case
+                Left e -> unHefty $ unEffectful $ i $ hfmap int e
+                Right e -> liftIns $ Inl $ hfmap (unEffectful . int) e
             )
-            (liftIns . EffUnion . R1)
-            . unEffUnion
+            (liftIns . Inr . coerce)
   where
-    int :: Hefty f (EffUnion u (e :+: r) ef) ~> Effectful u f r ef
-    int = interpretRecH i . Effectful
+    int :: Hefty f (EffUnion u er ef) ~> Effectful u f (EffTail er) ef
+    int = interpretRecH @er i . Effectful
     {-# INLINE int #-}
 
 reinterpret ::
-    forall e r f u c.
-    (Freer c f, HFunctorUnion u) =>
-    (MultiToUnionF u e ~> Effectful u f NopS (e + r)) ->
-    Effectful u f NopS (e + r) ~> Effectful u f NopS (e + r)
-reinterpret f = interpret f . raiseUnder
+    forall er f u c.
+    (Freer c f, HFunctorUnion u, DecompF u er) =>
+    (MultiToUnionF u (EffHeadF er) ~> Effectful u f NopS er) ->
+    Effectful u f NopS er ~> Effectful u f NopS er
+reinterpret f = interpret f . raiseUnder . decompEff
 {-# INLINE reinterpret #-}
 
 reinterpretRec ::
-    forall e eh r f u c.
-    (Freer c f, Union u, HFunctors u eh) =>
-    (MultiToUnionF u e ~> Effectful u f eh (e + r)) ->
-    Effectful u f eh (e + r) ~> Effectful u f eh (e + r)
-reinterpretRec f = interpretRec f . raiseUnder
+    forall er eh f u c.
+    (Freer c f, Union u, HFunctors u eh, DecompF u er) =>
+    (MultiToUnionF u (EffHeadF er) ~> Effectful u f eh er) ->
+    Effectful u f eh er ~> Effectful u f eh er
+reinterpretRec f = interpretRec f . raiseUnder . decompEff
 {-# INLINE reinterpretRec #-}
 
 reinterpretRecH ::
-    forall e r ef f u c.
-    (Freer c f, HFunctorUnion u, HeadHFunctor u e, TailHFunctor u r) =>
-    (MultiToUnionH u e (Effectful u f (e :+: r) ef) ~> Effectful u f (e :+: r) ef) ->
-    Effectful u f (e :+: r) ef ~> Effectful u f (e :+: r) ef
-reinterpretRecH f = interpretRecH f . raiseUnderH
+    forall er ef f u c.
+    ( Freer c f
+    , HFunctorUnion u
+    , DecompH u er
+    , HeadHFunctor u (EffHead er)
+    , TailHFunctor u (EffTail er)
+    ) =>
+    (MultiToUnionH u (EffHead er) (Effectful u f er ef) ~> Effectful u f er ef) ->
+    Effectful u f er ef ~> Effectful u f er ef
+reinterpretRecH f = interpretRecH f . raiseUnderH . decompEffH
 {-# INLINE reinterpretRecH #-}
 
 transformAllFH ::
@@ -318,16 +365,9 @@ transformAllFH fh ff =
     overEffectful
         . overHefty
         $ transformFreer
-        $ EffUnion
-            . caseF
-                ( L1
-                    . EffUnionH
-                    . fh
-                    . hfmap (unEffectful . transformAllFH fh ff . Effectful)
-                    . unEffUnionH
-                )
-                (R1 . ff)
-            . unEffUnion
+        $ caseH
+            (Inl . fh . hfmap (unEffectful . transformAllFH @eh' @ef' @eh @ef fh ff . Effectful))
+            (Inr . LiftIns . ff . unliftIns)
 
 transformAll ::
     forall ef' ef eh f u c.
@@ -348,34 +388,34 @@ transformAllH f = transformAllFH f id
 {-# INLINE transformAllH #-}
 
 raise ::
-    forall e1 e eh f u c.
-    (Freer c f, Union u, HFunctors u eh) =>
-    Effectful u f eh e ~> Effectful u f eh (e1 + e)
+    forall er eh f u c.
+    (Freer c f, Union u, HFunctors u eh, DecompF u er) =>
+    Effectful u f eh (EffTailF er) ~> Effectful u f eh er
 raise = transformAll weaken
 {-# INLINE raise #-}
 
 raiseH ::
-    forall e1 e ef f u c.
-    (Freer c f, Union u, HFunctors u e) =>
-    Effectful u f e ef ~> Effectful u f (e1 :+: e) ef
+    forall er ef f u c.
+    (Freer c f, Union u, HFunctors u (EffTail er), DecompH u er) =>
+    Effectful u f (EffTail er) ef ~> Effectful u f er ef
 raiseH = transformAllH weaken
 {-# INLINE raiseH #-}
 
 raiseUnder ::
-    forall e1 e2 e eh f u c.
-    (Freer c f, Union u, HFunctors u eh) =>
-    Effectful u f eh (e1 + e) ~> Effectful u f eh (e1 + e2 + e)
+    forall e1r e2 eh f u c.
+    (Freer c f, Union u, HFunctors u eh, DecompF u e1r) =>
+    Effectful u f eh (e2 + EffTailF e1r) ~> Effectful u f eh (e2 + e1r)
 raiseUnder = transformAll weakenUnder
 {-# INLINE raiseUnder #-}
 
 raiseUnderH ::
-    forall e1 e2 e ef f u c.
+    forall e1r e2 ef f u c.
     ( Freer c f
-    , Union u
-    , HeadHFunctor u e1
-    , HFunctors u (e1 :+: e)
-    , HFunctors u (e1 :+: e2 :+: e)
+    , HFunctorUnion u
+    , DecompH u e1r
+    , HeadHFunctor u e2
+    , TailHFunctor u (EffTail e1r)
     ) =>
-    Effectful u f (e1 :+: e) ef ~> Effectful u f (e1 :+: e2 :+: e) ef
+    Effectful u f (e2 :+: EffTail e1r) ef ~> Effectful u f (e2 :+: e1r) ef
 raiseUnderH = transformAllH weakenUnder
 {-# INLINE raiseUnderH #-}
diff --git a/heftia/src/Control/Hefty.hs b/heftia/src/Control/Hefty.hs
index fa59d92..dcf7aa9 100644
--- a/heftia/src/Control/Hefty.hs
+++ b/heftia/src/Control/Hefty.hs
@@ -7,9 +7,7 @@
 module Control.Hefty where
 
 import Control.Applicative (Alternative)
-import Control.Effect.Class (type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, type (:+:))
-import Control.Freer (Freer, InsClass, interpretFreer, liftIns)
+import Control.Freer (InsClass)
 import Control.Monad (MonadPlus)
 import Control.Monad.Base (MonadBase)
 import Control.Monad.IO.Class (MonadIO)
@@ -46,36 +44,3 @@ overHefty ::
     Hefty f' e' b
 overHefty f = Hefty . f . unHefty
 {-# INLINE overHefty #-}
-
-interpretRecRWith ::
-    forall r l f c.
-    Freer c f =>
-    ((Hefty f (l :+: r) ~> Hefty f l) -> l (Hefty f (l :+: r)) ~> l (Hefty f l)) ->
-    ((Hefty f (l :+: r) ~> Hefty f l) -> r (Hefty f (l :+: r)) ~> Hefty f l) ->
-    Hefty f (l :+: r) ~> Hefty f l
-interpretRecRWith f i =
-    overHefty $
-        interpretFreer $
-            caseH
-                (liftIns . f int)
-                (unHefty . i int)
-  where
-    int :: Hefty f (l :+: r) ~> Hefty f l
-    int = interpretRecRWith f i
-    {-# INLINE int #-}
-
-interpretRecR ::
-    forall r l f c.
-    (Freer c f, HFunctor l, HFunctor r) =>
-    (r (Hefty f l) ~> Hefty f l) ->
-    Hefty f (l :+: r) ~> Hefty f l
-interpretRecR i =
-    overHefty $
-        interpretFreer $
-            caseH
-                (liftIns . hfmapInt)
-                (unHefty . i . hfmapInt)
-  where
-    hfmapInt :: HFunctor e => e (Hefty f (l :+: r)) ~> e (Hefty f l)
-    hfmapInt = hfmap $ interpretRecR i
-    {-# INLINE hfmapInt #-}
diff --git a/heftia/src/Control/Hefty/SFunctor.hs b/heftia/src/Control/Hefty/SFunctor.hs
deleted file mode 100644
index bdbf37e..0000000
--- a/heftia/src/Control/Hefty/SFunctor.hs
+++ /dev/null
@@ -1,158 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
-
-module Control.Hefty.SFunctor where
-
-import Control.Effect.Class (LiftIns (LiftIns), NopS, unliftIns, type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
-import Control.Freer (Freer, interpretFreer, liftIns, transformFreer)
-import Control.Hefty (Hefty (Hefty), SigClass, overHefty, unHefty)
-import Data.Kind (Type)
-
-class HyperFunctor (h :: SigClass -> Type -> Type) where
-    hyfmap :: (e (h e) ~> e' (h e')) -> h e ~> h e'
-
-instance Freer c f => HyperFunctor (Hefty f) where
-    hyfmap f = Hefty . transformFreer f . unHefty
-    {-# INLINE hyfmap #-}
-
-class SFunctor (e :: SigClass) where
-    sfmap ::
-        (HyperFunctor h, SFunctor e1, SFunctor e2) =>
-        (forall ex. SFunctor ex => h (ex :+: e1) ~> h (ex :+: e2)) ->
-        e (h e1) ~> e (h e2)
-
-interpretRecRWithSFunctor ::
-    forall r l f c.
-    (Freer c f, SFunctor l, SFunctor r) =>
-    (forall ex. SFunctor ex => r (Hefty f (ex :+: l)) ~> Hefty f (ex :+: l)) ->
-    Hefty f (l :+: r) ~> Hefty f l
-interpretRecRWithSFunctor i =
-    overHefty $
-        interpretFreer $
-            caseH
-                (liftIns . sfmap int)
-                ( unHefty
-                    . absurdHyperFunctorL
-                    . i
-                    . sfmap (hyshfmap (caseH Inl (Inr . Inr)) . int)
-                )
-  where
-    int :: SFunctor ex' => Hefty f (ex' :+: (l :+: r)) ~> Hefty f (ex' :+: l)
-    int =
-        interpretRecRWithSFunctor (hyshfmap assocRSumH . i . shysfmap assocLSumH)
-            . hyshfmap assocLSumH
-
-hyshfmap ::
-    forall e1 e2 h.
-    ( HyperFunctor h
-    , SFunctor e1
-    , SFunctor e2
-    ) =>
-    (forall ex. e1 (h ex) ~> e2 (h ex)) ->
-    h e1 ~> h e2
-hyshfmap f = hyfmap $ shysfmap f . f
-{-# INLINE hyshfmap #-}
-
-shysfmap ::
-    forall e e1 e2 h.
-    ( HyperFunctor h
-    , SFunctor e
-    , SFunctor e1
-    , SFunctor e2
-    ) =>
-    (forall ex. e1 (h ex) ~> e2 (h ex)) ->
-    e (h e1) ~> e (h e2)
-shysfmap f = sfmap $ hyshfmap $ caseH Inl (Inr . f)
-{-# INLINE shysfmap #-}
-
-hysfmap ::
-    forall e e' h.
-    (HyperFunctor h, SFunctor e, SFunctor e') =>
-    (forall f. e f ~> e' f) ->
-    h e ~> h e'
-hysfmap f = hyfmap $ f . sfmap (rightHyperFunctor f)
-{-# INLINE hysfmap #-}
-
-rightHyperFunctor ::
-    forall l r r' h.
-    (HyperFunctor h, SFunctor l, SFunctor r, SFunctor r') =>
-    (forall ex. r (h (ex :+: r')) ~> r' (h (ex :+: r'))) ->
-    h (l :+: r) ~> h (l :+: r')
-rightHyperFunctor f =
-    hyfmap $ caseH (Inl . sfmapR f) (Inr . f . sfmapR f)
-
-sfmapR ::
-    forall e l r r' h.
-    (HyperFunctor h, SFunctor e, SFunctor l, SFunctor r, SFunctor r') =>
-    (forall ex. r (h (ex :+: r')) ~> r' (h (ex :+: r'))) ->
-    e (h (l :+: r)) ~> e (h (l :+: r'))
-sfmapR f =
-    sfmap $
-        assocHyperFunctorR
-            . rightHyperFunctor f
-            . assocHyperFunctorL
-
-assocHyperFunctorL ::
-    forall e1 e2 e3 h.
-    (HyperFunctor h, SFunctor e1, SFunctor e2, SFunctor e3) =>
-    h (e1 :+: (e2 :+: e3)) ~> h ((e1 :+: e2) :+: e3)
-assocHyperFunctorL = hyshfmap assocLSumH
-
-assocHyperFunctorR ::
-    forall e1 e2 e3 h.
-    (HyperFunctor h, SFunctor e1, SFunctor e2, SFunctor e3) =>
-    h ((e1 :+: e2) :+: e3) ~> h (e1 :+: (e2 :+: e3))
-assocHyperFunctorR = hyshfmap assocRSumH
-
-instance SFunctor (LiftIns e) where
-    sfmap _ = LiftIns . unliftIns
-    {-# INLINE sfmap #-}
-
-instance
-    (SFunctor e1, SFunctor e2) =>
-    SFunctor (e1 :+: e2)
-    where
-    sfmap f = caseH (Inl . sfmap f) (Inr . sfmap f)
-    {-# INLINE sfmap #-}
-
-newtype ViaHFunctor (e :: SigClass) f a = ViaHFunctor {unViaHFunctor :: e f a}
-    deriving (HFunctor)
-
-instance HFunctor e => SFunctor (ViaHFunctor e) where
-    sfmap f = hfmap $ absurdHyperFunctorL . f . weakenHyperFunctorL
-    {-# INLINE sfmap #-}
-
-absurdHyperFunctorL ::
-    forall e h.
-    (HyperFunctor h, SFunctor e) =>
-    h (NopS :+: e) ~> h e
-absurdHyperFunctorL = hysfmap $ caseH (\case {}) id
-{-# INLINE absurdHyperFunctorL #-}
-
-weakenHyperFunctorL ::
-    forall l r h.
-    (HyperFunctor h, SFunctor l, SFunctor r) =>
-    h r ~> h (l :+: r)
-weakenHyperFunctorL = hysfmap Inr
-{-# INLINE weakenHyperFunctorL #-}
-
-assocLSumH :: (e1 :+: (e2 :+: e3)) f ~> ((e1 :+: e2) :+: e3) f
-assocLSumH = caseH (Inl . Inl) (caseH (Inl . Inr) Inr)
-
-assocRSumH :: ((e1 :+: e2) :+: e3) f ~> (e1 :+: (e2 :+: e3)) f
-assocRSumH = caseH (caseH Inl (Inr . Inl)) (Inr . Inr)
-
-data ((e :: SigClass) +# (f :: Type -> Type)) (a :: Type) where
-    HyperFunctorPlusT :: h (e :+: r) a -> (e +# h r) a
-
-deriving stock instance Functor (h (e :+: r)) => Functor (e +# h r)
-deriving stock instance Foldable (h (e :+: r)) => Foldable (e +# h r)
-deriving stock instance Traversable (h (e :+: r)) => Traversable (e +# h r)
-
-instance SFunctor e => SFunctor ((+#) e) where
-    sfmap f (HyperFunctorPlusT a) = HyperFunctorPlusT $ f a
-    {-# INLINE sfmap #-}
diff --git a/heftia/src/Control/Monad/Freer/Tree.hs b/heftia/src/Control/Monad/Freer/Tree.hs
index d62fea3..ea5c459 100644
--- a/heftia/src/Control/Monad/Freer/Tree.hs
+++ b/heftia/src/Control/Monad/Freer/Tree.hs
@@ -61,8 +61,6 @@ interpretTreeK i (FreerTree m) =
                         (i e)
                         ((`runCont` runIdentity . k) . interpretTreeK i . FreerTree . f)
 
--- ContT \k -> f k \k' e -> Identity $ runCont (i e) (runIdentity . k')
-
 instance Freer Monad FreerTree where
     liftIns = liftInsTree
     interpretFreer = interpretTree
diff --git a/heftia/src/Data/Free/Sum.hs b/heftia/src/Data/Free/Sum.hs
index 52fedd9..7b4b5f9 100644
--- a/heftia/src/Data/Free/Sum.hs
+++ b/heftia/src/Data/Free/Sum.hs
@@ -4,7 +4,6 @@
 
 {- |
 Copyright   :  (c) 2023 Yamada Ryo
-               (c) 2023 Casper Bach Poulsen and Cas van der Rest
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
 Stability   :  experimental