diff --git a/Control/Category/FreeCartesian.hs b/Control/Category/FreeCartesian.hs
--- a/Control/Category/FreeCartesian.hs
+++ b/Control/Category/FreeCartesian.hs
@@ -32,7 +32,6 @@
   show x = showsPrec (-1) x ""
   showsPrec d = \case
     I -> showString "id"
-    E -> showString "ε"
     P1 -> showString "π₁"
     P2 -> showString "π₂"
     Embed s -> showString (show s)
@@ -47,7 +46,6 @@
     f :▵: g -> showParen True (showDbg 2 f . showString " ▵ " . showDbg 2 g)
     P2 -> showString "π₂"
     P1 -> showString "π₁"
-    E -> showString "ε"
 
 
 parens :: [Char] -> [Char]
@@ -58,7 +56,6 @@
   I -> I
   Embed g -> Embed (f g)
   a :.: b -> mapGenerators f a :.: mapGenerators f b
-  E -> E
   P1 -> P1
   P2 -> P2
   a :▵: b -> mapGenerators f a :▵: mapGenerators f b
@@ -75,7 +72,6 @@
          -> FreeCartesian k {-<-}con{->-} a (b ⊗ c)
   P1     :: {-<-}con b => {->-} FreeCartesian k {-<-}con{->-} (a ⊗ b) a
   P2     :: {-<-}con a => {->-} FreeCartesian k {-<-}con{->-} (a ⊗ b) b {-<-}
-  E      :: FreeCartesian k con a () {->-}
 
 assocRight :: (Cat k obj x y) -> (Cat k obj x y)
 assocRight (a :.: (assocRight -> (b :.: c))) = (a :.: b) :.: c
@@ -112,7 +108,6 @@
   (Embed φ) -> embed φ
   P1 -> exl
   P2 -> exr
-  E -> dis
   f :▵: g -> evalCartesian embed f ▵ evalCartesian embed g
   
 
@@ -136,6 +131,5 @@
 instance ({-<-}ProdObj con, con (), forall a b. (con a, con b) => con (a,b),{->-} Monoidal k) => Cartesian (FreeCartesian k {-<-}con{->-}) {-<-}where
   exl = P1
   exr = P2
-  dis = E
   dup = id :▵: id
   (▵) = (:▵:){->-}
diff --git a/Control/Category/Linear.hs b/Control/Category/Linear.hs
--- a/Control/Category/Linear.hs
+++ b/Control/Category/Linear.hs
@@ -21,7 +21,7 @@
 
 module Control.Category.Linear (
   -- Interface
-  type P, unit, split, merge,
+  type P, mkUnit, split, merge,
   -- pattern (:::),
   encode, decode, (!:),
   -- Helpers for cartesian categories
@@ -51,7 +51,8 @@
 
 type P :: (Type -> Type -> Type) -> Type -> Type -> Type
 
-unit     :: {-<-}forall k con r. (Obj k r, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)         => {->-}P k r ()
+ignore      :: (Monoidal k, {-<-} O3 k r a (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-}) => P k r () ⊸ P k r a ⊸ P k r a
+mkUnit     :: {-<-}forall k con a r. (Obj k r, Monoidal k, con (), con a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)     => {->-} P k r a ⊸ (P k r a , P k r ())
 split    :: {-<-}forall con a b r k. (O3 k r a b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}P k r (a ⊗ b) ⊸ (P k r a, P k r b)
 merge    :: {-<-}forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}(P k r a , P k r b) ⊸ P k r (a ⊗ b)
 encode   :: {-<-} O3 k r a b => {->-}  (a `k` b) -> (P k r a ⊸ P k r b)
@@ -69,7 +70,8 @@
 
   
 encode φ (Y f)    = Y (Embed φ ∘ f) -- put φ after f.
-unit              = Y dis
+mkUnit            = split ∘ (encode unitor)
+ignore f g        = encode unitor' (merge (g,f))
 split (Y f)       = (Y (exl ∘ f), Y (exr ∘ f)) 
 merge (Y f, Y g)  = Y (f ▵ g)
 
@@ -83,8 +85,6 @@
 -- If the underlying category is cartesian, we have additionally:
 
 
-ignore      :: (Monoidal k, {-<-} O3 k r a (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-}) => P k r () ⊸ P k r a ⊸ P k r a
-ignore f g  = encode unitor' (merge (g,f))
   
 copy  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-} ) => P k r a ⊸ P k r (a ⊗ a)
 copy  = encode dup
@@ -119,16 +119,14 @@
 -- 1. push abstract morphisms (E, X) into the already processed part
 -- 2. turn f ▵ g into a Merge
 
-expose  ::  {-<-}(ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => {->-}Cat cat {-<-}con{->-} a b ->
-            (  forall x. {-<-}con (Prod x) =>{->-} FreeSMC cat {-<-}con{->-} (Prod x) b ->
-               Merge cat {-<-}con{->-} a x -> k) -> k
+expose  ::  (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => {->-}Cat cat {-<-}con{->-} a b ->
+            (  forall x. con (Prod x) => FreeSMC cat con (Prod x) b -> Merge cat con a x -> k) -> k
 expose (f1 :▵: f2) k      =  expose f1 $ \g1 fs1 ->
                              expose f2 $ \g2 fs2 ->
                              appendSorted fs1 fs2 $ \g fs ->
                              k ((g1 × g2) ∘ g) fs
 expose (Embed ϕ :<: f) k  =  expose f $ \g fs ->
                              k (SMC.Embed ϕ ∘ g) fs
-expose (E :<: _) k        = k id Nil
 expose x k                = k unitor' (x :+ Nil)
 
 -- | Merge L/R pair
@@ -140,10 +138,10 @@
 -- already maximally exposed. So we do not handle the base cases here.
 
 -- If R :<: f is the first in the order, then L :<: f also exists;
--- and it should be first, so the case (R :<: f) :+ (L :<: g) must be rejected.
+-- and it should be first, so the case (R :<: f) :+ (L :<: f) isn't a possible merge.
 reduceStep ((P1 :<: f₁) :+ (P2 :<: f₂) :+ rest) k
   | EQ <- compareMorphisms f₁ f₂ =
-  expose f₁               $ \g f' -> -- expose any merge
+  expose f₁               $ \g f' -> -- expose any fork (▵) in f₁
   appendSorted f' rest    $ \g' rest' -> -- insert the exposed stuff in a sorted way
   k (assoc ∘ (g × id) ∘ g') rest'
 reduceStep (f :+ rest) k =
@@ -220,7 +218,6 @@
 compareAtoms :: (con a, con b, con c) => Cat cat con a b -> Cat cat con a c -> Order b c
 compareAtoms P1 P1 = EQ
 compareAtoms P2 P2 = EQ
-compareAtoms E E = EQ
 compareAtoms (Embed _) (Embed _) = unsafeCoerce EQ -- Same source -> same Atoms
 compareAtoms (f :▵: g) (f' :▵: g') = case compareMorphisms f f' of
   LT -> LT
@@ -235,7 +232,5 @@
 compareAtoms _ P2 = GT
 compareAtoms (Embed _) _ = LT
 compareAtoms _ (Embed _) = GT
-compareAtoms E _ = LT
-compareAtoms _ E = GT
 compareAtoms f g = error ("compareAtoms:\n" ++ showDbg 0 f "\n" ++ showDbg 0 g "" )
 
diff --git a/linear-smc.cabal b/linear-smc.cabal
--- a/linear-smc.cabal
+++ b/linear-smc.cabal
@@ -1,6 +1,6 @@
 Cabal-Version:  3.0
 name:           linear-smc
-version:        1.1.1
+version:        2.0.1
 category:       control
 synopsis:       Build SMC morphisms using linear types
 description:
@@ -16,7 +16,7 @@
 license-file:   LICENSE
 author:         Jean-Philippe Bernardy
 maintainer:     jeanphilippe.bernardy@gmail.com
-tested-with:    GHC==9.0.1
+tested-with:    GHC==9.0.2
 build-type:     Simple
 
 library