diff --git a/heftia/src/Control/Effect/Freer.hs b/heftia/src/Control/Effect/Freer.hs
index 6015485..6e0a07c 100644
--- a/heftia/src/Control/Effect/Freer.hs
+++ b/heftia/src/Control/Effect/Freer.hs
@@ -37,13 +37,34 @@ import Data.Free.Sum (SumUnion)
 import Data.Free.Union (
     IsMember,
     Member,
-    Union,
-    absurdUnion,
-    decomp,
-    inject,
-    project,
-    weakenL,
-    weakenR,
+    Union (
+        absurdUnion,
+        bundleUnion2,
+        bundleUnion3,
+        bundleUnion4,
+        decomp,
+        flipUnion,
+        flipUnion3,
+        flipUnionUnder,
+        inject,
+        inject0,
+        project,
+        rot3,
+        rot3',
+        unbundleUnion2,
+        unbundleUnion3,
+        unbundleUnion4,
+        weaken,
+        weaken2,
+        weaken2Under,
+        weaken2Under2,
+        weaken3,
+        weaken3Under,
+        weaken4,
+        weakenUnder,
+        weakenUnder2,
+        weakenUnder3
+    ),
  )
 import Data.Kind (Type)
 
@@ -133,7 +154,14 @@ reinterpret i a =
     freerEffects $ ($ runFreerEffects a) $ reinterpretFT \u ->
         case decomp u of
             Left e -> runFreerEffects $ i e
-            Right e -> liftInsT $ weakenR e
+            Right e -> liftInsT $ weaken e
+
+transformAll ::
+    (TransFreer c fr, Union u, Union u', c f) =>
+    (u es ~> u' es') ->
+    FreerEffects fr u es f ~> FreerEffects fr u' es' f
+transformAll f = overFreerEffects $ transformT f
+{-# INLINE transformAll #-}
 
 transform ::
     (TransFreer c fr, Union u, c f) =>
@@ -142,8 +170,8 @@ transform ::
 transform f a =
     freerEffects $ ($ runFreerEffects a) $ transformT \u ->
         case decomp u of
-            Left e -> weakenL $ f e
-            Right e -> weakenR e
+            Left e -> inject0 $ f e
+            Right e -> weaken e
 
 interpose ::
     forall e fr u es f c.
@@ -213,24 +241,160 @@ intercept f a =
             Just e -> inject $ f e
             Nothing -> u
 
-raiseUnder ::
-    forall e' e es fr u f c.
-    (TransFreer c fr, Union u, c f) =>
-    FreerEffects fr u (e ': es) f ~> FreerEffects fr u (e ': e' ': es) f
-raiseUnder a =
-    freerEffects
-        . ($ runFreerEffects a)
-        $ transformT \u -> case decomp u of
-            Left e -> weakenL e
-            Right e -> weakenR $ weakenR e
-
 raise ::
     forall e es fr u f c.
     (TransFreer c fr, Union u, c f) =>
     FreerEffects fr u es f ~> FreerEffects fr u (e ': es) f
-raise a = freerEffects . ($ runFreerEffects a) $ transformT weakenR
+raise = transformAll weaken
 {-# INLINE raise #-}
 
+raise2 ::
+    forall e1 e2 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': es) f
+raise2 = transformAll weaken2
+{-# INLINE raise2 #-}
+
+raise3 ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
+raise3 = transformAll weaken3
+{-# INLINE raise3 #-}
+
+raise4 ::
+    forall e1 e2 e3 e4 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u es f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
+raise4 = transformAll weaken4
+{-# INLINE raise4 #-}
+
+raiseUnder ::
+    forall e1 e2 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f
+raiseUnder = transformAll weakenUnder
+{-# INLINE raiseUnder #-}
+
+raiseUnder2 ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
+raiseUnder2 = transformAll weakenUnder2
+{-# INLINE raiseUnder2 #-}
+
+raiseUnder3 ::
+    forall e1 e2 e3 e4 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
+raiseUnder3 = transformAll weakenUnder3
+{-# INLINE raiseUnder3 #-}
+
+raise2Under ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
+raise2Under = transformAll weaken2Under
+{-# INLINE raise2Under #-}
+
+raise2Under2 ::
+    forall e1 e2 e3 e4 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
+raise2Under2 = transformAll weaken2Under2
+{-# INLINE raise2Under2 #-}
+
+raise3Under ::
+    forall e1 e2 e3 e4 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
+raise3Under = transformAll weaken3Under
+{-# INLINE raise3Under #-}
+
+flipFreer ::
+    forall e1 e2 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (e2 ': e1 ': es) f
+flipFreer = transformAll flipUnion
+{-# INLINE flipFreer #-}
+
+flipFreer3 ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e2 ': e1 ': es) f
+flipFreer3 = transformAll flipUnion3
+{-# INLINE flipFreer3 #-}
+
+flipFreerUnder ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e1 ': e3 ': e2 ': es) f
+flipFreerUnder = transformAll flipUnionUnder
+{-# INLINE flipFreerUnder #-}
+
+rotate3 ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e2 ': e3 ': e1 ': es) f
+rotate3 = transformAll rot3
+{-# INLINE rotate3 #-}
+
+rotate3' ::
+    forall e1 e2 e3 es fr u f c.
+    (TransFreer c fr, Union u, c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (e3 ': e1 ': e2 ': es) f
+rotate3' = transformAll rot3'
+{-# INLINE rotate3' #-}
+
+bundle2 ::
+    forall e1 e2 es fr u f c u'.
+    (TransFreer c fr, Union u, Union u', c f) =>
+    FreerEffects fr u (e1 ': e2 ': es) f ~> FreerEffects fr u (u' '[e1, e2] ': es) f
+bundle2 = transformAll bundleUnion2
+{-# INLINE bundle2 #-}
+
+bundle3 ::
+    forall e1 e2 e3 es fr u f c u'.
+    (TransFreer c fr, Union u, Union u', c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3] ': es) f
+bundle3 = transformAll bundleUnion3
+{-# INLINE bundle3 #-}
+
+bundle4 ::
+    forall e1 e2 e3 e4 es fr u f c u'.
+    (TransFreer c fr, Union u, Union u', c f) =>
+    FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f ~> FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f
+bundle4 = transformAll bundleUnion4
+{-# INLINE bundle4 #-}
+
+unbundle2 ::
+    forall e1 e2 es fr u f c u'.
+    (TransFreer c fr, Union u, Union u', c f) =>
+    FreerEffects fr u (u' '[e1, e2] ': es) f ~> FreerEffects fr u (e1 ': e2 ': es) f
+unbundle2 = transformAll unbundleUnion2
+{-# INLINE unbundle2 #-}
+
+unbundle3 ::
+    forall e1 e2 e3 es fr u f c u'.
+    (TransFreer c fr, Union u, Union u', c f) =>
+    FreerEffects fr u (u' '[e1, e2, e3] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': es) f
+unbundle3 = transformAll unbundleUnion3
+{-# INLINE unbundle3 #-}
+
+unbundle4 ::
+    forall e1 e2 e3 e4 es fr u f c u'.
+    (TransFreer c fr, Union u, Union u', c f) =>
+    FreerEffects fr u (u' '[e1, e2, e3, e4] ': es) f ~> FreerEffects fr u (e1 ': e2 ': e3 ': e4 ': es) f
+unbundle4 = transformAll unbundleUnion4
+{-# INLINE unbundle4 #-}
+
+overFreerEffects ::
+    (fr (u es) f a -> fr' (u' es') g b) ->
+    FreerEffects fr u es f a ->
+    FreerEffects fr' u' es' g b
+overFreerEffects f = freerEffects . f . runFreerEffects
+{-# INLINE overFreerEffects #-}
+
 interpreted :: (TransFreer c fr, c f, Union u) => FreerEffects fr u '[] f ~> f
 interpreted = runInterpretF absurdUnion . runFreerEffects
 {-# INLINE interpreted #-}
diff --git a/heftia/src/Control/Effect/Heftia.hs b/heftia/src/Control/Effect/Heftia.hs
index 02ab9a8..eaf84fa 100644
--- a/heftia/src/Control/Effect/Heftia.hs
+++ b/heftia/src/Control/Effect/Heftia.hs
@@ -33,6 +33,7 @@ import Control.Heftia.Trans (
     liftSigT,
     reelaborateHT,
     runElaborateH,
+    transformHT,
     translateT,
  )
 import Control.Monad (MonadPlus)
@@ -44,13 +45,34 @@ import Data.Hefty.Sum (SumUnionH)
 import Data.Hefty.Union (
     IsMemberH,
     MemberH,
-    UnionH,
-    absurdUnionH,
-    decompH,
-    injectH,
-    projectH,
-    weakenLH,
-    weakenRH,
+    UnionH (
+        absurdUnionH,
+        bundleUnion2H,
+        bundleUnion3H,
+        bundleUnion4H,
+        decompH,
+        flipUnion3H,
+        flipUnionH,
+        flipUnionUnderH,
+        inject0H,
+        injectH,
+        projectH,
+        rot3H,
+        rot3H',
+        unbundleUnion2H,
+        unbundleUnion3H,
+        unbundleUnion4H,
+        weaken2H,
+        weaken2Under2H,
+        weaken2UnderH,
+        weaken3H,
+        weaken3UnderH,
+        weaken4H,
+        weakenH,
+        weakenUnder2H,
+        weakenUnder3H,
+        weakenUnderH
+    ),
  )
 import Data.Kind (Type)
 
@@ -163,7 +185,20 @@ reinterpretH i a =
     heftiaEffects $ ($ runHeftiaEffects a) $ reelaborateHT \u ->
         case decompH u of
             Left e -> runHeftiaEffects $ i $ hfmap heftiaEffects e
-            Right e -> liftSigT $ weakenRH e
+            Right e -> liftSigT $ weakenH e
+
+transformAllH ::
+    ( TransHeftia c h
+    , UnionH u
+    , UnionH u'
+    , HFunctor (u es)
+    , HFunctor (u' es')
+    , c f
+    ) =>
+    (forall g. u es g ~> u' es' g) ->
+    HeftiaEffects h u es f ~> HeftiaEffects h u' es' f
+transformAllH f = overHeftiaEffects $ transformHT f
+{-# INLINE transformAllH #-}
 
 translate ::
     ( TransHeftia c h
@@ -179,8 +214,22 @@ translate ::
 translate f a =
     heftiaEffects $ ($ runHeftiaEffects a) $ translateT \u ->
         case decompH u of
-            Left e -> weakenLH $ hfmap runHeftiaEffects $ f $ hfmap heftiaEffects e
-            Right e -> weakenRH e
+            Left e -> inject0H $ hfmap runHeftiaEffects $ f $ hfmap heftiaEffects e
+            Right e -> weakenH e
+
+translateAll ::
+    ( TransHeftia c h
+    , UnionH u
+    , UnionH u'
+    , HFunctor (u es)
+    , HFunctor (u' es')
+    , c f
+    ) =>
+    (u es (HeftiaEffects h u' es' f) ~> u' es' (HeftiaEffects h u' es' f)) ->
+    HeftiaEffects h u es f ~> HeftiaEffects h u' es' f
+translateAll f =
+    overHeftiaEffects $ translateT (hfmap runHeftiaEffects . f . hfmap heftiaEffects)
+{-# INLINE translateAll #-}
 
 interposeH ::
     forall e h u es f c.
@@ -206,24 +255,280 @@ interceptH f a =
                 Just e -> injectH $ hfmap runHeftiaEffects $ f e
                 Nothing -> hfmap runHeftiaEffects u'
 
+raiseH ::
+    forall e hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u hs)
+    , HFunctor (u (e ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e ': hs) f
+raiseH = transformAllH weakenH
+{-# INLINE raiseH #-}
+
+raise2H ::
+    forall e1 e2 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u hs)
+    , HFunctor (u (e1 ': e2 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': hs) f
+raise2H = transformAllH weaken2H
+{-# INLINE raise2H #-}
+
+raise3H ::
+    forall e1 e2 e3 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u hs)
+    , HFunctor (u (e1 ': e2 ': e3 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f
+raise3H = transformAllH weaken3H
+{-# INLINE raise3H #-}
+
+raise4H ::
+    forall e1 e2 e3 e4 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u hs)
+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u hs f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
+raise4H = transformAllH weaken4H
+{-# INLINE raise4H #-}
+
 raiseUnderH ::
-    forall e' e es h u f c.
-    (TransHeftia c h, HFunctor (u (e : es)), HFunctor (u (e : e' : es)), UnionH u, c f) =>
-    HeftiaEffects h u (e ': es) f ~> HeftiaEffects h u (e ': e' ': es) f
-raiseUnderH a =
-    heftiaEffects
-        . ($ runHeftiaEffects a)
-        $ translateT \u -> case decompH u of
-            Left e -> weakenLH e
-            Right e -> weakenRH $ weakenRH e
+    forall e1 e2 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': hs))
+    , HFunctor (u (e1 ': e2 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': hs) f
+raiseUnderH = transformAllH weakenUnderH
+{-# INLINE raiseUnderH #-}
+
+raiseUnder2H ::
+    forall e1 e2 e3 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': hs))
+    , HFunctor (u (e1 ': e2 ': e3 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f
+raiseUnder2H = transformAllH weakenUnder2H
+{-# INLINE raiseUnder2H #-}
+
+raiseUnder3H ::
+    forall e1 e2 e3 e4 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': hs))
+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
+raiseUnder3H = transformAllH weakenUnder3H
+{-# INLINE raiseUnder3H #-}
+
+raise2UnderH ::
+    forall e1 e2 e3 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': hs))
+    , HFunctor (u (e1 ': e2 ': e3 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': hs) f
+raise2UnderH = transformAllH weaken2UnderH
+{-# INLINE raise2UnderH #-}
+
+raise2Under2H ::
+    forall e1 e2 e3 e4 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': hs))
+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
+raise2Under2H = transformAllH weaken2Under2H
+{-# INLINE raise2Under2H #-}
+
+raise3UnderH ::
+    forall e1 e2 e3 e4 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': hs))
+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': hs) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': hs) f
+raise3UnderH = transformAllH weaken3UnderH
+{-# INLINE raise3UnderH #-}
+
+flipHeftia ::
+    forall e1 e2 hs h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': hs))
+    , HFunctor (u (e2 ': e1 ': hs))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': hs) f ~> HeftiaEffects h u (e2 ': e1 ': hs) f
+flipHeftia = transformAllH flipUnionH
+{-# INLINE flipHeftia #-}
+
+flipHeftia3 ::
+    forall e1 e2 e3 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': es))
+    , HFunctor (u (e3 : e2 : e1 : es))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e2 ': e1 ': es) f
+flipHeftia3 = transformAllH flipUnion3H
+{-# INLINE flipHeftia3 #-}
+
+flipHeftiaUnder ::
+    forall e1 e2 e3 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': es))
+    , HFunctor (u (e1 : e3 : e2 : es))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e1 ': e3 ': e2 ': es) f
+flipHeftiaUnder = transformAllH flipUnionUnderH
+{-# INLINE flipHeftiaUnder #-}
+
+rotate3H ::
+    forall e1 e2 e3 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': es))
+    , HFunctor (u (e2 : e3 : e1 : es))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e2 ': e3 ': e1 ': es) f
+rotate3H = transformAllH rot3H
+{-# INLINE rotate3H #-}
+
+rotate3H' ::
+    forall e1 e2 e3 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': es))
+    , HFunctor (u (e3 : e1 : e2 : es))
+    , c f
+    , UnionH u
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (e3 ': e1 ': e2 ': es) f
+rotate3H' = transformAllH rot3H'
+{-# INLINE rotate3H' #-}
+
+bundle2H ::
+    forall u' e1 e2 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': es))
+    , HFunctor (u (u' '[e1, e2] ': es))
+    , c f
+    , UnionH u
+    , UnionH u'
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': es) f ~> HeftiaEffects h u (u' '[e1, e2] ': es) f
+bundle2H = transformAllH bundleUnion2H
+{-# INLINE bundle2H #-}
+
+bundle3H ::
+    forall u' e1 e2 e3 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': es))
+    , HFunctor (u (u' '[e1, e2, e3] : es))
+    , c f
+    , UnionH u
+    , UnionH u'
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': es) f ~> HeftiaEffects h u (u' '[e1, e2, e3] ': es) f
+bundle3H = transformAllH bundleUnion3H
+{-# INLINE bundle3H #-}
+
+bundle4H ::
+    forall u' e1 e2 e3 e4 es h u f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))
+    , HFunctor (u (u' '[e1, e2, e3, e4] : es))
+    , c f
+    , UnionH u
+    , UnionH u'
+    ) =>
+    HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f
+        ~> HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f
+bundle4H = transformAllH bundleUnion4H
+{-# INLINE bundle4H #-}
+
+unbundle2H ::
+    forall e1 e2 es h u u' f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': es))
+    , HFunctor (u (u' '[e1, e2] ': es))
+    , c f
+    , UnionH u
+    , UnionH u'
+    ) =>
+    HeftiaEffects h u (u' '[e1, e2] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': es) f
+unbundle2H = transformAllH unbundleUnion2H
+{-# INLINE unbundle2H #-}
+
+unbundle3H ::
+    forall e1 e2 e3 es h u u' f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': es))
+    , HFunctor (u (u' '[e1, e2, e3] ': es))
+    , c f
+    , UnionH u
+    , UnionH u'
+    ) =>
+    HeftiaEffects h u (u' '[e1, e2, e3] ': es) f ~> HeftiaEffects h u (e1 ': e2 ': e3 ': es) f
+unbundle3H = transformAllH unbundleUnion3H
+{-# INLINE unbundle3H #-}
+
+unbundle4H ::
+    forall e1 e2 e3 e4 es h u u' f c.
+    ( TransHeftia c h
+    , HFunctor (u (e1 ': e2 ': e3 ': e4 ': es))
+    , HFunctor (u (u' '[e1, e2, e3, e4] ': es))
+    , c f
+    , UnionH u
+    , UnionH u'
+    ) =>
+    HeftiaEffects h u (u' '[e1, e2, e3, e4] ': es) f
+        ~> HeftiaEffects h u (e1 ': e2 ': e3 ': e4 ': es) f
+unbundle4H = transformAllH unbundleUnion4H
+{-# INLINE unbundle4H #-}
 
 hoistHeftiaEffects ::
     (TransHeftia c h, HFunctor (u es), c f, c g) =>
     (f ~> g) ->
     HeftiaEffects h u es f ~> HeftiaEffects h u es g
-hoistHeftiaEffects f = heftiaEffects . hoistHeftia f . runHeftiaEffects
+hoistHeftiaEffects f = overHeftiaEffects $ hoistHeftia f
 {-# INLINE hoistHeftiaEffects #-}
 
+overHeftiaEffects ::
+    (h (u es) f a -> h' (u' es') g b) ->
+    HeftiaEffects h u es f a ->
+    HeftiaEffects h' u' es' g b
+overHeftiaEffects f = heftiaEffects . f . runHeftiaEffects
+{-# INLINE overHeftiaEffects #-}
+
 hoistInterpose ::
     forall e h u es fr u' es' f c c'.
     ( TransHeftia c h
diff --git a/heftia/src/Data/Free/Union.hs b/heftia/src/Data/Free/Union.hs
index b5394a6..c9466ae 100644
--- a/heftia/src/Data/Free/Union.hs
+++ b/heftia/src/Data/Free/Union.hs
@@ -4,13 +4,13 @@
 
 module Data.Free.Union where
 
-import Control.Effect.Class (Instruction)
+import Control.Effect.Class (Instruction, type (~>))
 import Data.Kind (Constraint)
 
 class Union (u :: [Instruction] -> Instruction) where
     type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint
 
-    inject :: HasMembership u f fs => f a -> u fs a
+    inject :: HasMembership u f fs => f ~> u fs
     project :: HasMembership u f fs => u fs a -> Maybe (f a)
 
     comp :: Either (f a) (u fs a) -> u (f ': fs) a
@@ -23,16 +23,101 @@ class Union (u :: [Instruction] -> Instruction) where
     (f |+|: g) u = case decomp u of
         Left x -> f x
         Right x -> g x
-
-    weakenL :: f a -> u (f ': fs) a
-    weakenL = comp . Left
-
-    weakenR :: u fs a -> u (f ': fs) a
-    weakenR = comp . Right
-
     {-# INLINE (|+|:) #-}
-    {-# INLINE weakenL #-}
-    {-# INLINE weakenR #-}
+
+    inject0 :: f ~> u (f ': fs)
+    inject0 = comp . Left
+    {-# INLINE inject0 #-}
+
+    injectUnder :: f2 ~> u (f1 ': f2 ': fs)
+    injectUnder = weaken . inject0
+    {-# INLINE injectUnder #-}
+
+    injectUnder2 :: f3 ~> u (f1 ': f2 ': f3 ': fs)
+    injectUnder2 = weaken2 . inject0
+    {-# INLINE injectUnder2 #-}
+
+    injectUnder3 :: f4 ~> u (f1 ': f2 ': f3 ': f4 ': fs)
+    injectUnder3 = weaken3 . inject0
+    {-# INLINE injectUnder3 #-}
+
+    weaken :: u fs a -> u (f ': fs) a
+    weaken = comp . Right
+    {-# INLINE weaken #-}
+
+    weaken2 :: u fs a -> u (f1 ': f2 ': fs) a
+    weaken2 = weaken . weaken
+    {-# INLINE weaken2 #-}
+
+    weaken3 :: u fs a -> u (f1 ': f2 ': f3 ': fs) a
+    weaken3 = weaken2 . weaken
+    {-# INLINE weaken3 #-}
+
+    weaken4 :: u fs a -> u (f1 ': f2 ': f3 ': f4 ': fs) a
+    weaken4 = weaken3 . weaken
+    {-# INLINE weaken4 #-}
+
+    weakenUnder :: u (f1 ': fs) ~> u (f1 ': f2 ': fs)
+    weakenUnder = inject0 |+|: weaken2
+
+    weakenUnder2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': fs)
+    weakenUnder2 = inject0 |+|: injectUnder |+|: weaken3
+
+    weakenUnder3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
+    weakenUnder3 = inject0 |+|: injectUnder |+|: injectUnder2 |+|: weaken4
+
+    weaken2Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': fs)
+    weaken2Under = inject0 |+|: weaken3
+
+    weaken2Under2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
+    weaken2Under2 = inject0 |+|: injectUnder |+|: weaken4
+
+    weaken3Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
+    weaken3Under = inject0 |+|: weaken4
+
+    flipUnion :: u (f1 ': f2 ': fs) ~> u (f2 ': f1 ': fs)
+    flipUnion = injectUnder |+|: inject0 |+|: weaken2
+
+    flipUnion3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f2 ': f1 ': fs)
+    flipUnion3 = injectUnder2 |+|: injectUnder |+|: inject0 |+|: weaken3
+
+    flipUnionUnder :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f3 ': f2 ': fs)
+    flipUnionUnder = inject0 |+|: injectUnder2 |+|: injectUnder |+|: weaken3
+
+    rot3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f2 ': f3 ': f1 ': fs)
+    rot3 = injectUnder2 |+|: inject0 |+|: injectUnder |+|: weaken3
+
+    rot3' :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f1 ': f2 ': fs)
+    rot3' = injectUnder |+|: injectUnder2 |+|: inject0 |+|: weaken3
+
+    bundleUnion2 :: Union u' => u (f1 ': f2 ': fs) ~> u (u' '[f1, f2] ': fs)
+    bundleUnion2 = inject0 . inject0 |+|: inject0 . injectUnder |+|: weaken
+
+    bundleUnion3 :: Union u' => u (f1 ': f2 ': f3 ': fs) ~> u (u' '[f1, f2, f3] ': fs)
+    bundleUnion3 =
+        (inject0 . inject0)
+            |+|: (inject0 . injectUnder)
+            |+|: (inject0 . injectUnder2)
+            |+|: weaken
+
+    bundleUnion4 :: Union u' => u (f1 ': f2 ': f3 ': f4 ': fs) ~> u (u' '[f1, f2, f3, f4] ': fs)
+    bundleUnion4 =
+        (inject0 . inject0)
+            |+|: (inject0 . injectUnder)
+            |+|: (inject0 . injectUnder2)
+            |+|: (inject0 . injectUnder3)
+            |+|: weaken
+
+    unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': f2 ': fs)
+    unbundleUnion2 = (inject0 |+|: injectUnder |+|: absurdUnion) |+|: weaken2
+
+    unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': f2 ': f3 ': fs)
+    unbundleUnion3 = (inject0 |+|: injectUnder |+|: injectUnder2 |+|: absurdUnion) |+|: weaken3
+
+    unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
+    unbundleUnion4 =
+        (inject0 |+|: injectUnder |+|: injectUnder2 |+|: injectUnder3 |+|: absurdUnion)
+            |+|: weaken4
 
 type family IsMember (f :: Instruction) fs where
     IsMember f (f ': fs) = 'True
diff --git a/heftia/src/Data/Hefty/Union.hs b/heftia/src/Data/Hefty/Union.hs
index f6f2aa2..cf77d64 100644
--- a/heftia/src/Data/Hefty/Union.hs
+++ b/heftia/src/Data/Hefty/Union.hs
@@ -6,13 +6,13 @@
 
 module Data.Hefty.Union where
 
-import Control.Effect.Class (Signature)
+import Control.Effect.Class (Signature, type (~>))
 import Data.Kind (Constraint)
 
 class UnionH (u :: [Signature] -> Signature) where
     type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint
 
-    injectH :: HasMembershipH u h hs => h f a -> u hs f a
+    injectH :: HasMembershipH u h hs => h f ~> u hs f
     projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)
 
     compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a
@@ -25,16 +25,106 @@ class UnionH (u :: [Signature] -> Signature) where
     (f |+: g) u = case decompH u of
         Left x -> f x
         Right x -> g x
-
-    weakenLH :: h f a -> u (h ': hs) f a
-    weakenLH = compH . Left
-
-    weakenRH :: u hs f a -> u (h ': hs) f a
-    weakenRH = compH . Right
-
     {-# INLINE (|+:) #-}
-    {-# INLINE weakenLH #-}
-    {-# INLINE weakenRH #-}
+
+    inject0H :: h f ~> u (h ': hs) f
+    inject0H = compH . Left
+    {-# INLINE inject0H #-}
+
+    injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f
+    injectUnderH = weakenH . inject0H
+    {-# INLINE injectUnderH #-}
+
+    injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f
+    injectUnder2H = weaken2H . inject0H
+    {-# INLINE injectUnder2H #-}
+
+    injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
+    injectUnder3H = weaken3H . inject0H
+    {-# INLINE injectUnder3H #-}
+
+    weakenH :: u hs f ~> u (h ': hs) f
+    weakenH = compH . Right
+    {-# INLINE weakenH #-}
+
+    weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f
+    weaken2H = weakenH . weakenH
+    {-# INLINE weaken2H #-}
+
+    weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f
+    weaken3H = weaken2H . weakenH
+    {-# INLINE weaken3H #-}
+
+    weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
+    weaken4H = weaken3H . weakenH
+    {-# INLINE weaken4H #-}
+
+    weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f
+    weakenUnderH = inject0H |+: weaken2H
+
+    weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
+    weakenUnder2H = inject0H |+: injectUnderH |+: weaken3H
+
+    weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
+    weakenUnder3H = inject0H |+: injectUnderH |+: injectUnder2H |+: weaken4H
+
+    weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
+    weaken2UnderH = inject0H |+: weaken3H
+
+    weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
+    weaken2Under2H = inject0H |+: injectUnderH |+: weaken4H
+
+    weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
+    weaken3UnderH = inject0H |+: weaken4H
+
+    flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f
+    flipUnionH = injectUnderH |+: inject0H |+: weaken2H
+
+    flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f
+    flipUnion3H = injectUnder2H |+: injectUnderH |+: inject0H |+: weaken3H
+
+    flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f
+    flipUnionUnderH = inject0H |+: injectUnder2H |+: injectUnderH |+: weaken3H
+
+    rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f
+    rot3H = injectUnder2H |+: inject0H |+: injectUnderH |+: weaken3H
+
+    rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f
+    rot3H' = injectUnderH |+: injectUnder2H |+: inject0H |+: weaken3H
+
+    bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f
+    bundleUnion2H = inject0H . inject0H |+: inject0H . injectUnderH |+: weakenH
+
+    bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f
+    bundleUnion3H =
+        (inject0H . inject0H)
+            |+: (inject0H . injectUnderH)
+            |+: (inject0H . injectUnder2H)
+            |+: weakenH
+
+    bundleUnion4H ::
+        UnionH u' =>
+        u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f
+    bundleUnion4H =
+        (inject0H . inject0H)
+            |+: (inject0H . injectUnderH)
+            |+: (inject0H . injectUnder2H)
+            |+: (inject0H . injectUnder3H)
+            |+: weakenH
+
+    unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f
+    unbundleUnion2H = (inject0H |+: injectUnderH |+: absurdUnionH) |+: weaken2H
+
+    unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
+    unbundleUnion3H = (inject0H |+: injectUnderH |+: injectUnder2H |+: absurdUnionH) |+: weaken3H
+
+    unbundleUnion4H ::
+        UnionH u' =>
+        u (u' '[h1, h2, h3, h4] ': hs) f
+            ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
+    unbundleUnion4H =
+        (inject0H |+: injectUnderH |+: injectUnder2H |+: injectUnder3H |+: absurdUnionH)
+            |+: weaken4H
 
 type family IsMemberH (h :: Signature) hs where
     IsMemberH h (h ': hs) = 'True