diff --git a/Control/Category/Constrained.hs b/Control/Category/Constrained.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Constrained.hs
@@ -0,0 +1,247 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE LinearTypes #-}
+
+module Control.Category.Constrained where
+
+import Prelude hiding ((.),id)
+import Data.Kind
+import Data.Constraint
+import Data.Type.Equality
+
+
+type O2 k a b = (Obj k a, Obj k b)
+type O3 k a b c =
+  (Obj k a, Obj k b, Obj k c)
+type O4 k a b c d =
+  (Obj k a, Obj k b, Obj k c, Obj k d)
+
+type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where
+  All c '[] = ()
+  All c (x ': xs) = (c x, All c xs)
+  
+
+class Trivial a
+instance Trivial a
+
+instance ProdObj Trivial where
+  prodobj = Dict
+  objprod = Dict
+  objunit = Dict
+
+
+class Category k where
+  type Obj k :: Type -> Constraint {-<-}
+  type Obj k = Trivial {->-}
+  id   :: Obj k a => a `k` a
+  (∘)  ::   (Obj k a, Obj k b, Obj k c) =>
+             (b `k` c) -> (a `k` b) -> a `k` c
+
+infixl 8 .
+infixl 8 ∘
+
+(.) :: (Category k, O3 k a b c) => k b c -> k a b -> k a c
+(.) = (∘)
+
+class ProdObj con where
+  prodobj :: (con a, con b) => Dict (con (a⊗b))
+  objprod :: forall z a b. (z ~ (a⊗b), con z) => Dict (con a, con b)
+  objunit :: Dict (con ())
+
+objProd :: forall k a b z. (z ~ (a⊗b), Obj k z, Monoidal k) => Dict (Obj k a, Obj k b)
+objProd = objprod
+
+prodObj ::  forall k a b. (Monoidal k, Obj k a, Obj k b) => Dict (Obj k (a⊗b))
+prodObj = prodobj
+
+unitObj ::  forall k. (Monoidal k) => Dict (Obj k ())
+unitObj = objunit
+
+
+infixr 0 //
+(//) :: Dict c -> (c => k) -> k
+Dict // k = k
+
+type a ⊗ b = (a,b)
+infixr 7 ⊗
+
+
+class ({-<-}ProdObj (Obj k),{->-}Category k) => Monoidal k where
+  (×)      :: {-<-}(Obj k a, Obj k b, Obj k c, Obj k d) =>{->-} (a `k` b) -> (c `k` d) -> (a ⊗ c) `k` (b ⊗ d)
+  swap     :: {-<-}(Obj k a, Obj k b) =>{->-} (a ⊗ b) `k` (b ⊗ a)
+  assoc    :: {-<-}(Obj k a, Obj k b, Obj k c) =>{->-} ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))
+  assoc'   :: {-<-}(Obj k a, Obj k b, Obj k c) =>{->-} (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)
+  unitor   :: {-<-}(Obj k a) =>{->-} a `k` (a ⊗ ())
+  unitor'  :: {-<-}(Obj k a) =>{->-} (a ⊗ ()) `k` a
+
+class Monoidal k => Cartesian k where
+  exl   ::  {-<-} forall a b. O2 k a b                     => {->-}   (a ⊗ b) `k` a
+  exr   ::  {-<-} forall a b. O2 k a b                     => {->-}   (a ⊗ b) `k` b
+  dis   ::  {-<-} forall a.   Obj k a                      => {->-}   a `k` ()
+  dup   ::  {-<-} (Obj k a, Obj k (a⊗a))                   => {->-}   a `k` (a ⊗ a)
+  (▵)   ::  {-<-} forall a b c. (Obj k a,Obj k b, Obj k c) => {->-}   (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)
+
+  {-<-}
+  {-# MINIMAL exl,exr,dup | exl,exr,(▵) | dis,dup | dis,(▵) #-}
+  dis = disDefault
+  dup = id ▵ id
+  exl = exlDefault
+  exr = exrDefault
+  (▵) = (▵!)
+  {->-}
+
+disDefault :: forall k a. (Cartesian k, Obj k a) =>  a `k` ()
+disDefault = exr . unitor
+     \\ prodObj @k @a @()
+     \\ unitObj @k
+
+exlDefault :: forall k a b. (Cartesian k, O2 k a b) =>  (a ⊗ b) `k` a
+exlDefault = unitor' . (id × dis)
+          \\ prodObj @k @a @b
+          \\ prodObj @k @a @()
+          \\ unitObj @k
+
+exrDefault :: forall k a b. (Cartesian k, O2 k a b) =>  (a ⊗ b) `k` b
+exrDefault = unitor' ∘ swap ∘ (dis × id)
+          \\ prodObj @k @a @b
+          \\ prodObj @k @b @()
+          \\ prodObj @k @() @b
+          \\ unitObj @k
+
+(▵!) :: forall k a b c. (Cartesian k, O3 k a b c) =>   (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)
+f ▵! g = (f × g) . dup
+          \\ prodObj @k @a @a
+          \\ prodObj @k @b @c
+
+cartesianCross :: (Obj k (b1 ⊗ b2), Obj k b3, Obj k c, Obj k b1,
+                     Obj k b2, Cartesian k) =>
+                    k b1 b3 -> k b2 c -> k (b1 ⊗ b2) (b3 ⊗ c)
+cartesianCross a b = (a . exl) ▵ (b . exr)
+cartesianUnitor :: forall a k. (Obj k a, Obj k (), Cartesian k) => a `k` (a ⊗ ())
+cartesianUnitor = id ▵ dis
+
+cartesianUnitor' :: forall a k. (Obj k a, Obj k (), Cartesian k) => (a ⊗ ()) `k` a
+cartesianUnitor' = exl
+
+cartesianSwap :: forall a b k. (Obj k a, Obj k b, Cartesian k) => (a ⊗ b) `k` (b ⊗ a)
+cartesianSwap = exr ▵ exl
+     \\ prodObj @k @a @b
+
+cartesianAssoc :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))
+cartesianAssoc = (exl . exl) ▵ ((exr . exl) ▵ exr)
+     \\ prodObj @k @(a,b) @c
+     \\ prodObj @k @a @b
+     \\ prodObj @k @b @c
+
+cartesianAssoc' :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)
+cartesianAssoc' = (exl ▵ (exl . exr)) ▵ (exr . exr)
+     \\ prodObj @k @a @(b,c)
+     \\ prodObj @k @a @b
+     \\ prodObj @k @b @c
+
+
+
+class Monoidal k => CoCartesian k where
+  inl   :: {-<-} O2 k a b                                 => {->-} a `k` (a ⊗ b)
+  inr   :: {-<-} O2 k a b                                 => {->-} b `k` (a ⊗ b)
+  new   :: {-<-} forall a. (Obj k a)                      => {->-} () `k` a
+  jam   :: {-<-} Obj k a                                  => {->-} (a⊗a) `k` a
+  (▿)   :: {-<-} forall a b c. (Obj k a,Obj k b, Obj k c) => {->-} (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a
+
+  {-<-}
+  jam = id ▿ id
+  new = newDefault
+  (▿) = (▿!)
+  {->-}
+
+jamDefault :: (Obj k a, CoCartesian k) => (a⊗a) `k` a
+jamDefault = id ▿ id
+
+newDefault :: forall k a. (Obj k a, CoCartesian k) => () `k` a
+newDefault = unitor' . inr
+        \\ prodObj @k @a @()
+        \\ unitObj @k
+
+(▿!) ::  forall k a b c. (O3 k a b c, CoCartesian k) => (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a
+f ▿! g = jam . (f × g)
+            \\ prodObj @k @a @a
+            \\ prodObj @k @b @c
+
+transp :: forall a b c d k con . (con ~ Obj k, Monoidal k, O4 k a b c d, (forall α β. (con α, con β) => con (α,β)))
+       => ((a,b) ⊗ (c,d)) `k` ((a,c) ⊗ (b,d))
+transp = assoc' . (id × (assoc . (swap × id) . assoc')) . assoc
+
+-- -- Poor man's infix arrows.
+-- -- http://haskell.1045720.n5.nabble.com/Type-operators-in-GHC-td5154978i20.html
+-- type a - (c :: * -> * -> *) = c a
+-- type c > b                  = c b
+
+-- infix 2 -
+-- infix 1 >
+
+
+class Cartesian k => Closed k where
+  -- expObj' :: forall a b. SObj k a -> SObj k b -> SObj k (a -> b)
+  apply :: O2 k a b => ((a -> b) ⊗ a) `k`  b
+  curry :: O3 k a b c => ((a ⊗ b) `k` c) -> (a `k` (b -> c))
+
+
+class Invertible k where
+  dual :: (a `k` b) -> b `k` a
+
+type Hopf k = (Cartesian k, CoCartesian k)
+  -- (laws unstated as usual...)
+  -- jam . dup = id
+  -- etc.
+
+instance Category (FUN x) where
+  id = \x -> x
+  f ∘ g = \x -> f (g x)
+
+instance Monoidal (FUN m) where
+  (f × g) (a,b) = (f a, g b)
+  assoc ((x,y),z) = (x,(y,z)) 
+  assoc' (x,(y,z)) = ((x,y),z)  
+  swap (x,y) = (y,x)
+  unitor = (,())
+  unitor' (x,()) = x
+
+instance Cartesian (->) where
+  exl = fst
+  exr = snd
+  (f ▵ g) x = (f x, g x)
+  dup x = (x,x)
+
+instance Closed (->) where
+  apply (f,x) = f x
+  curry = Prelude.curry
+
+type Comparator k = forall a b b'. k a b -> k a b' -> Maybe (b :~: b')
+
+class Category k => HasCompare k where
+  compareMorphs :: Comparator k
+
+-- | Equality-witnessing order type
+data Order a b where
+  LT, GT :: Order a b
+  EQ :: Order a a
diff --git a/Control/Category/FreeCartesian.hs b/Control/Category/FreeCartesian.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/FreeCartesian.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE LinearTypes #-}
+
+module Control.Category.FreeCartesian where
+
+import Prelude hiding ((.),id,curry)
+import Control.Category.Constrained
+import Data.Kind
+
+instance (forall x y. (con x, con y) => Show (k x y)) => Show  (Cat k con a b) where
+  show x = showsPrec (-1) x ""
+  showsPrec d = \case
+    I -> showString "id"
+    E -> showString "ε"
+    P1 -> showString "π₁"
+    P2 -> showString "π₂"
+    Embed s -> showString (show s)
+    f :.: g -> showParen (d >  0) (showsPrec 0 f . showString " ∘ " . showsPrec 0 g)
+    f :▵: g -> showParen (d > -1) (showsPrec 2 f . showString " ▵ " . showsPrec 2 g)
+
+showDbg :: Int -> Cat k con a b -> ShowS
+showDbg d = \case
+    Embed _ -> showString "?"
+    I -> showString "id"
+    f :.: g -> showParen (d /= 0) (showDbg 0 f . showString " ∘ " . showDbg 0 g)
+    f :▵: g -> showParen True (showDbg 2 f . showString " ▵ " . showDbg 2 g)
+    P2 -> showString "π₂"
+    P1 -> showString "π₁"
+    E -> showString "ε"
+
+
+parens :: [Char] -> [Char]
+parens x = "(" <> x <> ")"
+
+mapGenerators :: (con a, con b) => (forall x y. (con x, con y) => k x y -> k' x y) -> Cat k con a b -> Cat k' con a b
+mapGenerators f = \case
+  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
+  x -> error (showDbg 0 x " (Free.mapGenerators)")
+
+type Cat = FreeCartesian
+
+data FreeCartesian k {-<-} (con :: Type -> Constraint) {->-} a b where
+  I      :: FreeCartesian k {-<-}con{->-} a a
+  (:.:)  :: {-<-}con b => {->-} FreeCartesian k {-<-}con{->-} b c -> FreeCartesian k {-<-}con{->-} a b
+         -> FreeCartesian k {-<-}con{->-} a c
+  Embed  :: {-<-}(con a, con b) => {->-}k a b -> FreeCartesian k {-<-}con{->-} a b
+  (:▵:)  :: {-<-}(con a, con b, con c) => {->-}FreeCartesian k {-<-}con {->-}a b -> FreeCartesian k {-<-}con{->-} a c
+         -> 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
+assocRight x = x
+
+rightView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
+rightView (assocRight -> (a :.: b)) = a :.: b
+rightView x = I :.: x
+
+assocLeft :: (Cat k obj x y) -> (Cat k obj x y)
+assocLeft ((assocLeft -> (a :.: b)) :.: c) = a :.: (b :.: c)
+assocLeft x = x
+
+leftView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
+leftView (assocLeft -> (a :.: b)) = a :.: b
+leftView x = x :.: I
+
+pattern (:>:) ::  (obj x, obj y) => (obj b)  => Cat k obj b y -> Cat k obj x b -> Cat k obj x y
+pattern f :>: g <- (rightView -> f :.: g)
+  where f :>: g = f . g
+
+pattern (:<:) ::  (obj x, obj y) => (obj b) => (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y
+pattern f :<: g <- (leftView -> f :.: g)
+  where f :<: g = f . g
+
+evalCartesian :: forall k a b con f.
+              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
+               con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
+              (forall α β. (con α, con β) => k α β -> f α β)  ->
+              Cat k (Obj k) a b -> f a b
+evalCartesian embed = \case
+  I -> id
+  (f :.: g) -> evalCartesian embed f . evalCartesian embed g
+  (Embed φ) -> embed φ
+  P1 -> exl
+  P2 -> exr
+  E -> dis
+  f :▵: g -> evalCartesian embed f ▵ evalCartesian embed g
+  
+
+instance Category (Cat k con) where
+  type Obj (Cat k con) = con
+  id = I
+  I ∘ x = x
+  x ∘ I = x
+  P1 ∘ (f :▵: _) = f
+  P2 ∘ (_ :▵: g) = g
+  x ∘ y = x :.: y
+ 
+
+instance ({-<-}ProdObj con, con (), forall a b. (con a, con b) => con (a,b), {->-}Monoidal k) =>  Monoidal (FreeCartesian k {-<-}con{->-}) {-<-}where
+  f × g = cartesianCross f g
+  assoc = cartesianAssoc
+  assoc' = cartesianAssoc'
+  swap = cartesianSwap
+  unitor = cartesianUnitor
+  unitor' = cartesianUnitor'{->-}
+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/FreeSMC.hs b/Control/Category/FreeSMC.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/FreeSMC.hs
@@ -0,0 +1,418 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Control.Category.FreeSMC where
+
+import Prelude hiding ((.),id,curry)
+import Control.Category.Constrained
+import Data.Monoid
+import Data.Kind
+import Data.Type.Equality
+
+data Sho a b = Sho {fromSho :: Int -> ShowS}
+
+instance Show (Sho a b) where
+  showsPrec d (Sho f) = f d
+
+shoCon :: String -> Sho a b
+shoCon name = Sho $ \_ -> showString name
+
+instance Category Sho where
+  type Obj Sho = Trivial
+  id = shoCon "id"
+  Sho f ∘ Sho g = Sho $ \d -> showParen (d /= 0) (f 0 . showString " ∘ " . g 0)
+
+instance Monoidal Sho where
+  swap = shoCon "swap"
+  assoc = shoCon "assoc"
+  assoc' = shoCon "assoc'"
+  unitor = shoCon "unitor"
+  unitor' = shoCon "unitor'"
+  Sho f × Sho g = Sho $ \d -> showParen (d /= 0) (f 2 . showString " × " . g 2)
+
+instance Cartesian Sho where
+  dis = shoCon "dis"
+  dup = shoCon "dup"
+  exl = shoCon "exl"
+  exr = shoCon "exr"
+  Sho f ▵ Sho g = Sho $ \d -> showParen (d /= 0) (f 2 . showString " ▵ " . g 2)
+
+class HasShow k where
+  toShow :: k a b -> Sho a b
+
+instance HasShow Sho where
+  toShow = id
+
+
+instance (forall x y. (con x, con y) => Show (k x y)) => Show  (Cat k con a b) where
+  show x = showsPrec (-1) x ""
+  showsPrec d = \case
+    I -> showString "id"
+    S -> showString "swap"
+    A  -> showString "assoc"
+    A' -> showString "assoc'"
+    U a -> {-showString "[" .-} fromSho (evalUnitor (trivializeUnitor a)) 0 {-. showString "]"-}
+    U' a -> {-showString "[" .-} fromSho (evalUnitor' (trivializeUnitor a)) 0 {-. showString "]"-}
+    X s -> showString (show s)
+    f :.: g -> showParen (d >  0) (showsPrec 0 f . showString " ∘ " . showsPrec 0 g)
+    f :×: g -> showParen (d > -1) (showsPrec 2 f . showString " × " . showsPrec 2 g)
+
+
+showDbg :: Int -> Cat k con a b -> ShowS
+showDbg d = \case
+    X _ -> showString "?"
+
+    I -> showString "id"
+    f :.: g -> showParen (d /= 0) (showDbg 0 f . showString " ∘ " . showDbg 0 g)
+
+    f :×: g -> showParen True (showDbg 2 f . showString " × " . showDbg 2 g)
+    S -> showString "σ"
+    A  -> showString "α"
+    A' -> showString "α'"
+    U _ -> showString "ρ"
+    U' a  -> showString ("ρ'(" ++ show a ++ ")")
+
+
+
+parens :: [Char] -> [Char]
+parens x = "("<> x <>")"
+
+mapGenerators :: (con a, con b) => (forall x y. (con x, con y) => k x y -> k' x y) -> Cat k con a b -> Cat k' con a b
+mapGenerators f = \case
+  X g -> X (f g)
+
+  I -> I
+  a :.: b -> mapGenerators f a :.: mapGenerators f b
+
+  a :×: b -> mapGenerators f a :×: mapGenerators f b
+  A -> A
+  A' -> A'
+  S -> S
+  U x -> U x
+  U' x -> U' x
+
+  x -> error (showDbg 0 x " (Free.mapGenerators)")
+
+
+instance Show (Unitor con a b) where
+  show UL = "⟨"
+  show UR = "⟩"
+  show (IL a) = "⟨" ++ show a
+  show (IR a) = "⟩" ++ show a
+data Unitor con a b where
+  UL :: Unitor con a ((),a)
+  UR :: Unitor con a (a,())
+  IL :: (con a, con b, con c) => Unitor con a b -> Unitor con (a,c) (b,c)
+  IR :: (con a, con b, con c) => Unitor con a b -> Unitor con (c,a) (c,b)
+
+compareUnitors :: Unitor con a b -> Unitor con a b' -> Maybe (b :~: b')
+compareUnitors UL UL = Just Refl
+compareUnitors UR UR = Just Refl
+compareUnitors (IL a) (IL b) = case compareUnitors a b of Nothing -> Nothing; Just Refl -> Just Refl
+compareUnitors (IR a) (IR b) = case compareUnitors a b of Nothing -> Nothing; Just Refl -> Just Refl
+compareUnitors _ _ = Nothing
+
+trivializeUnitor :: Unitor con a b -> Unitor Trivial a b
+trivializeUnitor UL = UL
+trivializeUnitor UR = UR
+trivializeUnitor (IL f) = IL (trivializeUnitor f)
+trivializeUnitor (IR f) = IR (trivializeUnitor f)
+
+commuteUnitors :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
+                  con a, con b) => Unitor con c b -> Unitor con a b -> Cat cat con a c
+commuteUnitors UL UL = id
+commuteUnitors UL UR = id
+commuteUnitors UR UR = id
+commuteUnitors UR UL = id
+commuteUnitors (IL a) (IL b) = (commuteUnitors a b × id)
+commuteUnitors (IR a) (IR b) = (id × commuteUnitors a b)
+commuteUnitors (IR a) (IL b) = (U (IL b)) .  (U' (IR a))
+commuteUnitors (IL a) (IR b) = (U (IR b)) .  (U' (IL a))
+commuteUnitors UL (IR a) = U a . U' UL
+commuteUnitors UR (IL a) = U a . U' UR
+commuteUnitors (IR a) UL = U UL . U' a
+commuteUnitors (IL a) UR = U UR . U' a
+
+
+data Cat k (con :: Type -> Constraint) a b where
+  A :: (con a, con b, con c) => Cat k con ((a,b),c) (a,(b,c))
+  A' :: (con a, con b, con c) => Cat k con (a,(b,c)) ((a,b),c)
+  S ::  (con a, con b) => Cat k con (a,b) (b,a) 
+  Embed :: (con a, con b) => k a b -> Cat k con a b
+  I :: Cat k con a a
+  U :: Unitor con a b -> Cat k con a b
+  U' :: Unitor con b a -> Cat k con a b
+
+  (:.:) :: con b => (Cat k con b c) -> (Cat k con a b) -> (Cat k con a c)
+  (:×:) :: (con a, con b, con c, con d) => (Cat k con a b) -> (Cat k con c d) -> (Cat k con (a ⊗ c) (b ⊗ d))
+
+
+instance Invertible (Cat k con) where
+  dual :: Cat k con a b -> Cat k con b a
+  dual = \case
+    I -> I
+    f :×: g -> dual f :×: dual g
+    f :.: g -> dual g :.: dual f
+    S -> S
+    A -> A'
+    A' -> A
+
+assocRight :: (Cat k obj x y) -> (Cat k obj x y)
+assocRight (a :.: (assocRight -> (b :.: c))) = (a :.: b) :.: c
+assocRight x = x
+
+rightView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
+rightView (assocRight -> (a :.: b)) = a :.: b
+rightView x = I :.: x
+
+assocLeft :: (Cat k obj x y) -> (Cat k obj x y)
+assocLeft ((assocLeft -> (a :.: b)) :.: c) = a :.: (b :.: c)
+assocLeft x = x
+
+leftView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
+leftView (assocLeft -> (a :.: b)) = a :.: b
+leftView x = x :.: I
+
+pattern (:>:) ::  (obj x, obj y) => (obj b)  =>  (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y
+pattern f :>: g <- (rightView -> f :.: g)
+  where f :>: g = f . g
+
+pattern (:<:) ::  (obj x, obj y) => (obj b) => (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y
+pattern f :<: g <- (leftView -> f :.: g)
+  where f :<: g = f . g
+
+-- pattern Uncurry :: (obj a1, obj a2, obj c, obj (a1×a2)) => Cat k obj a1  (a2 -> c) -> Cat k obj (a1 × a2)  c
+-- pattern Uncurry f <- Apply :<: (f :×: I)
+
+
+
+evalM :: forall k a b con.
+              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
+               con ~ Obj k, Monoidal k, Obj k a, Obj k b) => Cat k (Obj k) a b -> (k a b)
+evalM I          = id
+evalM (f :×: g)  = evalM f × evalM g
+evalM (f :.: g)  = evalM f . evalM g
+evalM A          = assoc
+evalM A'         = assoc'
+evalM S          = swap
+evalM (U u)      = evalUnitor u
+evalM (U' u)     = evalUnitor' u
+evalM (Embed ϕ)  = ϕ
+
+evalCartesian :: forall k a b con.
+              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
+               con ~ Obj k, Cartesian k, Obj k a, Obj k b) => Cat k (Obj k) a b -> (k a b)
+evalCartesian = \case
+  I -> id
+  (f :×: g) -> evalCartesian f × evalCartesian g
+  (f :.: g) -> evalCartesian f . evalCartesian g
+  (X ϕ) -> ϕ
+  A -> assoc
+  A' -> assoc'
+  S -> swap
+  (U u) -> evalUnitor u
+  (U' u) -> evalUnitor' u
+
+
+evalUnitor :: forall k a b con.
+              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
+               con ~ Obj k, Monoidal k, Obj k a, Obj k b)
+           => Unitor (Obj k) a b -> (k a b)
+evalUnitor UR = unitor
+evalUnitor UL = swap . unitor
+evalUnitor (IL x) = (evalUnitor x × id)
+evalUnitor (IR x) = (id × evalUnitor x)
+
+evalUnitor' :: forall k a b con.
+              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
+               con ~ Obj k, Monoidal k, Obj k a, Obj k b)
+           => Unitor (Obj k) b a -> (k a b)
+evalUnitor' UR = unitor'
+evalUnitor' UL = unitor' . swap
+evalUnitor' (IL x) = (evalUnitor' x × id)
+evalUnitor' (IR x) = (id × evalUnitor' x)
+-- eval Dup = dup
+-- eval Apply = apply
+-- eval (Curry f) = curry (eval f)
+---------------------------
+-- Cat k obj - instances
+
+
+pattern X :: forall (k :: Type -> Type -> Type) (con :: Type -> Constraint) a b. () => (con a, con b) => k a b -> Cat k con a b
+pattern X x = Embed x
+
+instance Category (Cat k con) where
+  type Obj (Cat k con) = con
+  id = I
+  I ∘ x = x
+  x ∘ I = x
+  x ∘ y = x :.: y
+
+instance (ProdObj con, forall a b. (con a, con b) => con (a,b)) =>  Monoidal (Cat k con) where
+  I × I = I
+  U' a × I = U' (IL a)
+  I × U' a = U' (IR a)
+  f × g = f :×: g
+  assoc =  A
+  assoc' = A'
+  swap = S
+  unitor = U UR
+  unitor' = U' UR
+
+
+type Composer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> (Cat k con a c)
+type PartialComposer k con = forall a b c. (con a, con b, con c) => Cat k con b c -> Cat k con a b  -> Alt Maybe (Cat k con a c)
+type ProtoSimplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => Composer k con -> PartialComposer k con
+type Simplifier k con = (con (), ProdObj con, forall a b. (con a, con b) => con (a,b)) => forall a b. (con a, con b) =>  (Cat k con a b) -> (Cat k con a b)
+
+monoidalSimplify :: (con (), ProdObj con, forall α β. (con α, con β) => con (α,β)) => (con a, con b) => Cat k con a b -> Cat k con a b
+monoidalSimplify = mkSimplifier (\x -> monoidalRules x)
+
+monoidalRules :: forall k con. ProtoSimplifier k con
+monoidalRules  (.) = \ x y -> Alt (after x y) where
+  after :: (con a, con b, con c) => Cat k con b c -> Cat k con a b -> Maybe (Cat k con a c)
+
+  -- obvious simplifications
+  S `after` S = Just id
+  A' `after` A = Just id
+  A `after` A' = Just id
+
+  -- commute (or cancel) unitors
+  U' x `after` U y = Just (commuteUnitors x y)
+
+  -- push swaps to the right
+  S `after` (f :×: g) = Just ((g × f) . S)
+
+  -- swap individual strands
+  S `after` A = Just (assoc' . (id × swap) . assoc . (swap × id))
+  S `after` A' = Just (assoc . (swap × id) . assoc' . (id × swap))
+  A  `after` S = Just ((id × swap) . assoc  . (swap × id) . assoc')
+  A' `after` S = Just ((swap × id) . assoc'  . (id × swap ) . assoc)
+
+  -- push U' through S
+  U' UR `after` S = Just (U' UL)
+  U' UL `after` S = Just (U' UR)
+  U' (IL a) `after` S = Just (swap . U' (IR a))
+  U' (IR a) `after` S = Just (swap . U' (IL a))
+
+  -- push U' into ×
+  U' UR `after` ((f :×: I) :<: h) = Just (f . U' UR  . h)
+  U' (IL a) `after` ((f :×: g) :<: h) = Just (((U' a . f) × g)  . h )
+  U' (IR a) `after` ((f :×: g) :<: h) = Just ((f × (U' a . g))  . h )
+
+  -- push U' through A'
+  U' UR `after` A' = Just (id × U' UR)
+  U' (IR a) `after` A' = Just (A' . (id × (id × U' a)))
+  U' (IL (IR a)) `after` A' = Just (A' . (id × (U' a × id)) )
+  U' (IL UR) `after` A' = Just (id × U' UL )
+  U' (IL UL)     `after` A' = Just (U' UL)
+  U' (IL (IL a)) `after` A' = Just (A' . (U' a × id))
+
+  -- push U' through A
+  U' UL          `after` A = Just (U' UL × id)
+  U' (IL a)      `after` A = Just (A . ((U' a × id) × id))
+  U' (IR (IL a)) `after` A = Just (A . ((id × U' a) × id))
+  U' (IR UL)     `after` A = Just (U' UR × id)
+  U' (IR UR)     `after` A = Just (U' UR)
+  U' (IR (IR a)) `after` A = Just (A . (id × U' a))
+
+  -- compose strands 
+  (f :×: g) `after` (h :×: i) = Just ((f . h) × (g . i))
+
+
+  -- failing the above, extract unitors
+  ((f :>: U' a) :×: g) `after` h = Just ((f×g) . U' (IL a) . h )
+  (f :×: (g :>: U' a)) `after` h = Just ((f × g) . U' (IR a) . h)
+
+  h `after` ((f :>: U' a) :×: g) = Just (h . (f × g) . U' (IL a) )
+  h `after` (f :×: (g :>: U' a)) = Just (h . (f × g) . U' (IR a) )
+
+
+  -- extract unitors from ▵:
+  -- h `after` ((U a :<: f) :▵: g) = Just (h . U (IL a) . (f ▵ g)  )
+  -- h `after` (f :▵: (U a :<: g )) = Just (h . U (IR a) . (f ▵ g) )
+
+  _ `after` _ = Nothing
+
+
+neverEqual :: Comparator k
+neverEqual _ _ = Nothing
+
+
+
+
+{-
+
+closedCartesianRules :: forall k con. ProtoSimplifier k con
+closedCartesianRules (.) = \ x y -> Alt (after x y) where
+  after :: (con a, con b, con c) => Cat k con b  c -> Cat k con a b  -> Maybe (Cat k con a c)
+  
+  -- Incomplete support for apply/curry simplifier
+  Apply `after` (Curry f :×: I) = Just f
+  -- Apply `after` (Curry (g :>: R) :▵: f) = Just (g . f)
+  _ `after` _ = Nothing
+-}
+mkSimplifier :: forall k con. ProtoSimplifier k con -> Simplifier k con
+mkSimplifier protoAfter = simplify where
+   (...) :: Composer k con
+   I ... g  = g -- g is already normal.
+   f ... I  = f -- f is already normal.
+   (f :>: g) ... (h :<: i) = case getAlt (g `after` h) of
+     Nothing -> (f :>: g) :.: (h :<: i) -- no reaction.  both subterms are normal. so we're done.
+     Just j -> f ... j ... i --- reaction :: we must recurse. ("After" must return a normal term; j.)
+   f ... g = f :.: g
+   after :: PartialComposer k con
+   after = protoAfter (...)
+
+   simplify :: (con a, con b) => Cat k con a b -> Cat k con a b
+   -- simplify (Curry f) = Curry (simplify f)
+   simplify (f :×: g) = simplify f × simplify g
+   simplify (f :.: g) = simplify f ... simplify g
+   simplify x = x
+
+
+toDup :: (ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con b) => Cat k con a b -> Cat k con a b
+toDup = \case
+  I -> I
+  (f :×: g) -> toDup f × toDup g
+  (f :.: g) -> toDup f . toDup g
+  X ϕ -> X ϕ
+  A -> A
+  A' -> A'
+  S -> S
+  (U u) -> U u
+  (U' u) -> U' u
+
+
+toE :: (ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con b) => Cat k con a b -> Cat k con a b
+toE = \case
+  I -> I
+  (f :×: g) -> toE f × toE g
+  (f :.: g) -> toE f . toE g
+  X ϕ -> X ϕ
+  A -> A
+  A' -> A'
+  S -> S
+  (U u) -> U u
+  (U' u) -> U' u
+
diff --git a/Control/Category/Linear.hs b/Control/Category/Linear.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Linear.hs
@@ -0,0 +1,235 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
+
+module Control.Category.Linear (
+  -- Interface
+  type P, unit, split, merge, pattern (:::),
+  encode, decode, reduce, (!:),
+  -- Helpers for cartesian categories
+  ignore, copy, discard
+) where
+
+
+import Data.Kind (Type)
+
+import Prelude hiding ((.),id,curry,LT,GT,EQ)
+import Control.Category.Constrained
+import Control.Category.FreeCartesian as Cartesian
+import Unsafe.Coerce
+import qualified Control.Category.FreeSMC as SMC
+
+
+
+pattern (:::) :: forall con (k :: Type -> Type -> Type) r a b.
+                   (Obj k r, Obj k a, Obj k b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) =>
+                   P k r a ⊸ P k r b ⊸ P k r (a, b)
+pattern x ::: y <- (split @con -> (x,y))
+  where x ::: y = merge @con (x,y)
+
+infixr ::: -- GHC does not always see this change. rm -r dist/dante. T_T (ghc 8.8.4)
+
+
+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 ()
+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)
+decode   :: {-<-} forall a b k con. (con (), con ~ Obj k, Monoidal k, con a, con b, (forall α β. (con α, con β) => con (α,β))) => {->-} (forall r. {-<-}Obj k r =>{->-} P k r a ⊸ P k r b) -> (a `k` b)
+
+(!:) :: 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)
+x !: y = merge (x,y)
+
+
+data P k r a     where
+  Y :: FreeCartesian k {-<-} (Obj k) {->-} r a -> P k r a
+fromP :: P k r a -> FreeCartesian k {-<-} (Obj k) {->-} r a
+fromP (Y f) = f
+
+  
+encode φ (Y f)    = Y (Embed φ ∘ f) -- put φ after f.
+unit              = Y dis
+split (Y f)       = (Y (exl ∘ f), Y (exr ∘ f)) 
+merge (Y f, Y g)  = Y (f ▵ g)
+
+
+decode f          = SMC.evalM (reduce (extract f))
+extract           :: {-<-} (Obj k a, Obj k b) => {->-} (forall r. {-<-} Obj k r => {->-} P k r a ⊸ P k r b) -> FreeCartesian k {-<-} (Obj k) {->-} a b
+extract f         = fromP (f (Y id))
+
+
+---------------------------------------------------------------------
+-- 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
+discard  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k, con () {->-} ) => P k r a ⊸ P k r ()
+discard  = encode dis
+
+
+
+
+
+
+type FreeSMC = SMC.Cat
+
+-- haskell-src-exts does not like the ' before constructors. It does not honour extensions either.
+type Null = '[]
+type Cons x xs = x ': xs
+
+type family Prod (xs :: [Type])  where
+  Prod Null = ()
+  Prod (Cons x ys) = x ⊗ Prod ys
+
+
+data Merge k {-<-}con{->-} a xs where
+  (:+)   :: {-<-}(con x, con (Prod xs)) => {->-}FreeCartesian k {-<-}con{->-} a x -> Merge k {-<-}con{->-} a xs
+         -> Merge k {-<-}con{->-}  a (Cons x xs)
+  Nil    :: Merge k {-<-}con{->-} a Null
+
+infixr :+
+
+
+-- | expose does two things:
+-- 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 (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
+
+reduceStep  ::  {-<-}(ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con (Prod xs)) =>{->-} Merge cat {-<-}con{->-} a xs ->
+                (  forall zs. {-<-}con (Prod zs) => {->-}FreeSMC cat {-<-}con{->-} (Prod zs) (Prod xs)  ->
+                  Merge cat {-<-}con{->-} a zs -> k) -> k
+-- There exists at least one pair of the form L :<: f and R :<: f if
+-- 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.
+reduceStep ((P1 :<: f₁) :+ (P2 :<: f₂) :+ rest) k
+  | EQ <- compareMorphisms f₁ f₂ =
+  expose f₁               $ \g f' -> -- expose any merge
+  appendSorted f' rest    $ \g' rest' -> -- insert the exposed stuff in a sorted way
+  k (assoc ∘ (g × id) ∘ g') rest'
+reduceStep (f :+ rest) k =
+  reduceStep rest                    $ \g rest' ->
+  appendSorted (f :+ Nil) rest'  $ \g' rest'' ->
+  k ((unitor' × g) ∘ g') rest''
+  
+appendSorted  :: {-<-}(ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con (Prod xs), con (Prod ys)) => {->-} Merge cat {-<-}con{->-} a xs -> Merge cat {-<-}con{->-} a ys ->
+                 (  forall zs. {-<-}con(Prod zs)=> {->-}FreeSMC cat {-<-}con{->-}  (Prod zs)
+                                                                                   (Prod xs ⊗ Prod ys)  ->
+                    Merge cat{-<-}con{->-} a zs -> k) -> k
+appendSorted  Nil        ys         k = k (swap ∘  unitor)  ys
+appendSorted  xs         Nil        k = k          unitor   xs
+appendSorted  (x :+ xs)  (y :+ ys)  k =
+  case compareMorphisms x y of
+    GT  ->   appendSorted (x :+ xs) ys $ \a zs ->
+             k (assoc ∘ (swap × id) ∘  assoc' ∘ (id × a))  (y :+ zs)
+    _   ->   appendSorted xs (y :+ ys) $ \a zs ->
+             k (                       assoc' ∘ (id × a))  (x :+ zs)
+
+-- | intermediate result
+data R cat con a b where
+  St :: con (Prod b)
+    => FreeSMC k con (Prod b) c -- already processed part (SMC here)
+    -> Merge k con a b -- maximally exposed and sorted merge tree (see 'expose' below)
+    -> R k con a c
+
+-- | Perform 1 reduction step, assumes input is already maximally exposed and sorted. 
+reductionStep :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => R cat con a b -> R cat con a b
+reductionStep (St r1 (f :+ Nil)) = expose f $ \ready m -> St (r1 . unitor . ready) m  -- single morphism to analyse
+reductionStep (St r1 m) = reduceStep m $ \r2 m' -> St (r1 . r2) m' -- L/R pair to find and reduce
+
+-- | Perform all reduction steps and return intermediate states
+reductionSteps  :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), 
+               con a, con b) => R cat con a b -> [R cat con a b]
+reductionSteps st@(St _ (I :+ Nil)) = [st] -- done!
+reductionSteps st = st : reductionSteps (reductionStep st)
+
+freeToR :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
+           con x) => Cat k con a x -> R k con a x
+freeToR f = St unitor' (f :+ Nil)
+
+rToFree :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b)
+        => R cat con a b -> FreeSMC cat con a b
+rToFree (St done (I :+ Nil)) = done . unitor
+
+reduce  :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
+             con a, con b) => Cartesian.Cat cat con a b -> FreeSMC cat con a b
+reduce = rToFree . last . reductionSteps . freeToR
+
+-- Invariant: same source!
+compareMorphisms :: (con a, con b, con c) => Cat cat con a b -> Cat cat con a c -> Order b c
+compareMorphisms I I = EQ
+compareMorphisms I _ = LT
+compareMorphisms _ I = GT
+compareMorphisms (f Cartesian.:>: g) (f' Cartesian.:>: g') =
+  case compareAtoms g g' of
+    LT -> LT
+    GT -> GT
+    EQ -> compareMorphisms f f'
+
+-- Invariant: same source!
+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
+  GT -> GT
+  EQ -> case compareMorphisms g g' of
+    LT -> LT
+    GT -> GT
+    EQ -> EQ
+compareAtoms (P1) (_) = LT
+compareAtoms (_) (P1) = GT
+compareAtoms (P2) (_) = LT
+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/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,166 @@
+
+                   GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+  This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+  0. Additional Definitions.
+
+  As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+  "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+  An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+  A "Combined Work" is a work produced by combining or linking an
+Application with the Library.  The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+  The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+  The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+  1. Exception to Section 3 of the GNU GPL.
+
+  You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+  2. Conveying Modified Versions.
+
+  If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+   a) under this License, provided that you make a good faith effort to
+   ensure that, in the event an Application does not supply the
+   function or data, the facility still operates, and performs
+   whatever part of its purpose remains meaningful, or
+
+   b) under the GNU GPL, with none of the additional permissions of
+   this License applicable to that copy.
+
+  3. Object Code Incorporating Material from Library Header Files.
+
+  The object code form of an Application may incorporate material from
+a header file that is part of the Library.  You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+   a) Give prominent notice with each copy of the object code that the
+   Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the object code with a copy of the GNU GPL and this license
+   document.
+
+  4. Combined Works.
+
+  You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+   a) Give prominent notice with each copy of the Combined Work that
+   the Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the Combined Work with a copy of the GNU GPL and this license
+   document.
+
+   c) For a Combined Work that displays copyright notices during
+   execution, include the copyright notice for the Library among
+   these notices, as well as a reference directing the user to the
+   copies of the GNU GPL and this license document.
+
+   d) Do one of the following:
+
+       0) Convey the Minimal Corresponding Source under the terms of this
+       License, and the Corresponding Application Code in a form
+       suitable for, and under terms that permit, the user to
+       recombine or relink the Application with a modified version of
+       the Linked Version to produce a modified Combined Work, in the
+       manner specified by section 6 of the GNU GPL for conveying
+       Corresponding Source.
+
+       1) Use a suitable shared library mechanism for linking with the
+       Library.  A suitable mechanism is one that (a) uses at run time
+       a copy of the Library already present on the user's computer
+       system, and (b) will operate properly with a modified version
+       of the Library that is interface-compatible with the Linked
+       Version.
+
+   e) Provide Installation Information, but only if you would otherwise
+   be required to provide such information under section 6 of the
+   GNU GPL, and only to the extent that such information is
+   necessary to install and execute a modified version of the
+   Combined Work produced by recombining or relinking the
+   Application with a modified version of the Linked Version. (If
+   you use option 4d0, the Installation Information must accompany
+   the Minimal Corresponding Source and Corresponding Application
+   Code. If you use option 4d1, you must provide the Installation
+   Information in the manner specified by section 6 of the GNU GPL
+   for conveying Corresponding Source.)
+
+  5. Combined Libraries.
+
+  You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+   a) Accompany the combined library with a copy of the same work based
+   on the Library, uncombined with any other library facilities,
+   conveyed under the terms of this License.
+
+   b) Give prominent notice with the combined library that part of it
+   is a work based on the Library, and explaining where to find the
+   accompanying uncombined form of the same work.
+
+  6. Revised Versions of the GNU Lesser General Public License.
+
+  The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+  Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+  If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.
diff --git a/examples/Unitary.hs b/examples/Unitary.hs
new file mode 100644
--- /dev/null
+++ b/examples/Unitary.hs
@@ -0,0 +1,254 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE LinearTypes #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
+
+import Control.Category.Constrained
+import Control.Category.Linear
+
+import Data.Complex
+import Data.List (transpose, intercalate)
+import Data.Constraint
+import Control.Monad
+import System.Exit (exitFailure)
+import Prelude hiding (id,(.),not)
+import Data.Array
+import Numeric
+
+type COMPLEX = Complex Double
+
+
+data U a b = U {fromM :: Array (a,b) COMPLEX}
+
+class (Bounded a, Ix a, Eq a) => Finite a where
+  inhabitants :: [a]
+  subFinite :: forall c b. (Finite (c ⊗ b), a ~ (c ⊗ b)) => Dict (Finite c, Finite b)
+instance Finite () where
+  inhabitants = [()]
+  subFinite = error "Finite ()"
+instance Finite Bool where
+  inhabitants = inhabitants'
+  subFinite = error "Finite Bool"
+
+inhabitants' :: forall a. (Bounded a, Enum a) => [a]
+inhabitants' = [minBound..maxBound]
+
+pad :: Int -> String -> String
+pad n xs = replicate (n - length xs) ' ' ++ xs
+
+padAll :: [String] -> [String]
+padAll xs = map (pad m) xs
+  where m = maximum (map length xs)
+
+showMat :: [[String]] -> String
+showMat = unlines . map (intercalate "  ") . transpose . map padAll . transpose 
+
+showCOMPLEX :: RealFloat a => Complex a -> String
+showCOMPLEX (x :+ y) =  (showFFloat (Just 1) x  . showString "+i" . showFFloat (Just 1) y ) ""
+
+instance (Finite a, Finite b) => Show (a `U` b) where
+  show (U f) = showMat [[showCOMPLEX (f ! (i,j))  | i <- inhabitants] | j <- inhabitants]
+
+
+instance (Finite a, Finite b) => Finite (a,b) where
+  inhabitants = [(x,y) | x <- inhabitants, y <- inhabitants]
+  subFinite = Dict
+
+instance ProdObj Finite where
+  prodobj = Dict
+  objprod = subFinite
+  objunit = Dict
+
+summation :: (Num a, Finite t) => (t -> a) -> a
+summation f = sum [f x | x <- inhabitants]
+
+tabulate :: (Finite a, Finite b) => (a -> b -> COMPLEX) -> a `U` b
+tabulate f = U (  array (  (minBound,minBound),
+                           (maxBound,maxBound))
+                    [((i,j),f i j) | i <- inhabitants, j <- inhabitants])
+
+instance Category U where
+  type Obj U = Finite
+  id = tabulate delta   -- identity matrix
+  U g ∘ U f = tabulate (\i j ->  summation
+                                 (\k -> f!(i,k)  *  g!(k,j)))   -- matrix multiplication
+
+instance Monoidal U where
+  U f × U g = tabulate (\(a,c) (b,d) -> f ! (a,b) * g ! (c,d)) -- kroneckerProduct
+  unitor = tabulate (\x (y,()) -> delta x y)
+  unitor' = tabulate (\(y,()) x -> delta x y)
+  assoc = tabulate  (\  ((x,y),z) (x',(y',z')) ->
+                        delta ((x,y),z) ((x',y'),z'))
+  assoc' = tabulate  (\  (x',(y',z')) ((x,y),z) ->
+                         delta ((x,y),z) ((x',y'),z'))
+  swap = tabulate $ \(x,y) (y',x') -> delta (x,y) (x',y')
+ 
+-- This is indeed a tensor product.
+-- Assume z with two untangled parts: z[(i,k)] = x[i] + y[k]
+-- Consider: ((f×g) · z) (j,l)
+-- = ∑i ∑k (f×g)(j,l)(i,k) z[i,k]
+-- = ∑i ∑k f(j,i) * g(l,k) * (x[i] + y[k])
+-- = ∑i ∑k f(j,i) * g(l,k) * x[i]    +   ∑i ∑k f(j,i) * g(l,k) * y[k]
+-- = ∑i  f(j,i) * x[i] * ∑k g(l,k)   +   ∑k g(l,k) * y[k] * ∑i f(j,i)
+-- = ∑i  f(j,i) * x[i] *    1        +   ∑k g(l,k) * y[k] *     1
+-- =  (f · x)(j)                     +   (g · y)(l)
+
+
+-- instance Cartesian (U) where
+--   dup = tabulate $ \i (j,k) -> if i==j && i==k then one else 0
+--   exl = tabulate $ \(i,_) k -> if i==k then 1 else 0
+--   exr = tabulate $ \(_,i) k -> if i==k then 1 else 0
+
+-- instance CoCartesian (U) where
+--   jam = tabulate $ \(j,k) i -> if i==j && i==k then 1 else 0
+--   inl = tabulate $ \k (i,_) -> if i==k then 1 else 0
+--   inr = tabulate $ \k (_,i) -> if i==k then 1 else 0
+
+-- instance Frobenius COMPLEX (U) where
+--   scale c = tabulate $ \i j -> c * delta i j
+
+
+
+vsq2 :: COMPLEX
+vsq2 = 1 / sqrt 2
+
+-- Hadamard (H) gate
+h :: Finite r => P U r Bool ⊸ P U r Bool
+h = encode (tabulate m) where
+  m :: Bool -> Bool -> COMPLEX
+  m True True = -vsq2
+  m _ _       =  vsq2
+
+
+decoded_h :: U Bool Bool
+decoded_h = decode h
+
+-- >>> decoded_h
+-- 0.7071067811865475 :+ 0.0       0.7071067811865475 :+ 0.0
+-- 0.7071067811865475 :+ 0.0 (-0.7071067811865475) :+ (-0.0)
+
+i :: COMPLEX
+i = 0 :+ 1
+
+t :: Finite r => P (U) r Bool ⊸ P (U) r Bool
+t = encode (tabulate m) where
+  m :: Bool -> Bool -> COMPLEX
+  m True True = exp (i*pi/4)
+  m False False = 1
+  m _ _       =  0
+
+hermitianConjugate :: (Finite a, Finite b) => b `U` a -> a `U` b 
+hermitianConjugate (U f) =  tabulate (\i j -> conjugate (f ! (j,i)))
+
+conjugateTranspose :: {-<-}(Finite a, Finite b) =>{->-} U b a -> U a b
+conjugateTranspose = hermitianConjugate 
+
+-- Lets' not show the type; it works also for M matrices.
+
+invert :: {-<-} (Finite a, Finite b) => {->-} (forall s. {-<-} Finite s => {->-} P U s a ⊸ P U s b) -> (forall r. {-<-} Finite r => {->-} P U r b ⊸ P U r a)
+invert f = encode (conjugateTranspose (decode f))
+
+t' :: Finite r => P U r Bool ⊸ P U r Bool
+t' = invert t
+
+t'decoded :: U Bool Bool
+t'decoded = decode t'
+
+-- >>> t'decoded
+-- 1.0 :+ (-0.0)                                0.0 :+ (-0.0)
+-- 0.0 :+ (-0.0)  0.7071067811865476 :+ (-0.7071067811865475)
+
+ctrl :: Finite a =>  (forall r. Finite r => P (U) r a ⊸ P (U) r a) ->
+                     (forall r. Finite r => P (U) r Bool ⊸ P (U) r a ⊸ P (U) r (Bool,a))
+ctrl f x y = encode (ctrlMat (decode f)) (x !: y)
+
+ctrlMat :: Finite a => U a a -> U (Bool,a) (Bool,a)
+ctrlMat (U f) = tabulate (\(cIn,x) (cOut,y) ->
+        case (cIn,cOut) of
+          (True,True) -> f!(x,y) -- if the control is active, transform using f
+          (False,False) -> delta x y -- otherwise identity 
+          _ -> 0) -- never transform the control
+
+
+delta :: (Eq a) => a -> a -> COMPLEX
+delta x y = if x == y then 1 else 0
+
+
+not :: Finite r => P (U) r Bool ⊸ P (U) r Bool
+not = encode ((tabulate $ \x y -> 1 - delta x y))
+
+(&) ::  a ⊸ (a ⊸ b) ⊸ b
+x & f = f x
+
+ctrlneg' :: U (Bool,Bool) (Bool,Bool)
+ctrlneg' = decode (\p -> split p & \(x,y) -> ctrl not x y)
+
+-- >>> ctrlneg'
+-- 1.0 :+ 0.0  0.0 :+ 0.0  0.0 :+ 0.0  0.0 :+ 0.0
+-- 0.0 :+ 0.0  1.0 :+ 0.0  0.0 :+ 0.0  0.0 :+ 0.0
+-- 0.0 :+ 0.0  0.0 :+ 0.0  0.0 :+ 0.0  1.0 :+ 0.0
+-- 0.0 :+ 0.0  0.0 :+ 0.0  1.0 :+ 0.0  0.0 :+ 0.0
+
+
+
+
+second :: (t ⊸ b) ⊸ (a, t) ⊸ (a, b)
+second f (x,y) = (x,f y)
+
+first :: (t ⊸ b) ⊸ (t, a) ⊸ (b, a)
+first f (x,y) = (f x,y)
+
+
+toffoli2 :: (Obj k r, Obj k (b, b), Obj k b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) =>
+                (P k r b ⊸ P k r b)
+                -> (P k r b ⊸ P k r b)
+                -> (P k r b ⊸ P k r b)
+                -> (P k r b ⊸ P k r b ⊸ (P k r (b,b)))
+                -> ((P k r b, P k r b), P k r b)
+                ⊸ P k r ((b, b), b)
+
+toffoli2 {-<-} hadam tGate tInv cnot {->-}  ((c1,c2),x) =
+   cnot c1          (hadam    x)   & split & \(c1,x)  ->
+   cnot c2          (tInv     x)   & split & \(c2,x)  ->
+   cnot c1          (tGate    x)   & split & \(c1,x)  ->
+   cnot c2          (tInv     x)   & split & \(c2,x)  ->
+   cnot c2          (tGate    c1)  & split & \(c2,y)  ->
+   (cnot (tGate c2) (tInv y)) !: (hadam (tGate x))
+  
+toffU :: Finite r => P U r ((Bool, Bool), Bool) ⊸ P (U) r ((Bool, Bool), Bool)
+toffU = toffoli2 h t t' (ctrl not) . first split . split
+
+
+toffoli'' :: U ((Bool, Bool), Bool) ((Bool, Bool), Bool)
+toffoli'' = decode toffU
+
+result :: String
+result = "1.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0   0.0+i0.0   0.0+i0.0\n\
+         \0.0+i0.0  1.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0   0.0+i0.0   0.0+i0.0\n\
+         \0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  1.0+i0.0  0.0+i0.0   0.0+i0.0   0.0+i0.0\n\
+         \0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  1.0+i0.0   0.0+i0.0   0.0+i0.0\n\
+         \0.0+i0.0  0.0+i0.0  1.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0   0.0+i0.0   0.0+i0.0\n\
+         \0.0+i0.0  0.0+i0.0  0.0+i0.0  1.0+i0.0  0.0+i0.0  0.0+i0.0   0.0+i0.0   0.0+i0.0\n\
+         \0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0   0.0+i0.0  1.0+i-0.0\n\
+         \0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  0.0+i0.0  1.0+i-0.0   0.0+i0.0\n"
+
+main :: IO ()
+main = unless (show (toffoli'') == result) exitFailure
+
+-- Local Variables:
+-- dante-target: "test-unitary"
+-- End:
diff --git a/linear-smc.cabal b/linear-smc.cabal
new file mode 100644
--- /dev/null
+++ b/linear-smc.cabal
@@ -0,0 +1,42 @@
+Cabal-Version:  3.0
+name:           linear-smc
+version:        1.0.0
+category:       control
+synopsis:       Build SMC morphisms using linear types
+description:
+  A number of domain specific languages, such as circuits or
+  data-science workflows, are best expressed as diagrams of boxes
+  connected by wires.
+  A faithful abstraction of box-and-wires is Symmetric Monoidal Categories (SMCs)
+  This library
+  allows one to program SMCs with linear functions instead of SMC
+  combinators. This is done without resorting to template haskell or compiler plugins.
+  The rationale, design and implementation of this library is provided by the paper  "Evaluating Linear Functions to Symmetric Monoidal Categories", by Jean-Philippe Bernardy and Arnaud Spiwack, appearing at Haskell Symposium 2021.
+license:        LGPL-3.0-or-later
+license-file:   LICENSE
+author:         Jean-Philippe Bernardy
+maintainer:     jeanphilippe.bernardy@gmail.com
+tested-with:    GHC==9.0.1
+build-type:     Simple
+
+library
+  build-depends:       base >=4.13 && < 666
+  build-depends: constraints
+
+  default-language: Haskell2010
+  exposed-modules:
+    Control.Category.Constrained
+    Control.Category.Linear
+  other-modules:
+    Control.Category.FreeSMC
+    Control.Category.FreeCartesian
+    
+
+Test-Suite test-unitary
+  build-depends: constraints
+  build-depends: array
+  default-language: Haskell2010
+  type:       exitcode-stdio-1.0
+  main-is:    examples/Unitary.hs
+  build-depends: base
+