diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,19 @@
 # Changelog for free-category
 
+## Version 0.0.4.0
+- hoistOp
+- Renamed `Control.Category.FreeEff` module as `Control.Category.FreeEffect`
+  and renamed top level terms:
+    - `EffCategory` type class to `EffectCategory`
+    - `FreeEffCat` to `EffCat`
+    - `FreeEffCat` constructor as `Effect` and `lift` as `effect`
+    - `liftCat` to `liftEffect`
+    - `foldNatLift` to `foldNatEffCat`
+- Show instance of 'Cat' and 'C' via 'ListTr' (GHC >= 806)
+- Performance optimisations: rewrite rules & inline pragmas
+- Export ListTr from Control.Category.Free
+- foldrL, foldlL and zipWithL
+
 ## Version 0.0.3.0
 - Efficient 'Cat' and 'Aff' based on real time queues with scheduling
 - Added Monoid instances 
@@ -15,5 +29,3 @@
 ## Version 0.0.1.0
 - free category (concrete and condensity transformed)
 - free arrows (concrete and condensity transformed)
-
-## Unreleased changes
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,21 +2,31 @@
 [![Maintainer: coot](https://img.shields.io/badge/maintainer-coot-lightgrey.svg)](http://github.com/coot)
 [![CircleCI](https://circleci.com/gh/coot/free-category/tree/master.svg?style=svg)](https://circleci.com/gh/coot/free-category/tree/master)
 
-This package contains efficient free categories. There are two presentations:
+This package contains efficient implementations of free categories. There are
+various representations available:
 
-* using realtime queues (C. Okasaki 'Pure Functional Data Structures')
-* using continuation passing style
+* real-time queues (C. Okasaki 'Pure Functional Data Structures')
+* type aligned lists
+* continuation passing style (Church encoding)
 
 Free arrows and free Kleisli categories are also included.
 
 Free categories are useful to model state machines in a simple yet type safe
-manner.  For that purpose `Kleisli` categroies are a very useful target which
-allows to include monadic computations.  This packge contains a useful
-generalisation of `Kliesli` categories captured by `EffCategory` class
-(effectful categories), and a (free) transformer which lifts a category to
-an effectful one.
+manner.  For that purpose `Kleisli` categories are a very useful target which
+allows to include monadic computations.  This package contains a useful
+generalisation of `Kliesli` categories captured by `EffectCategory` class
+(categories with effects), and a (free) transformer which lifts a category to
+a category with effects.
 
-## Some examples
+## Benchmarks
+
+Check performance characteristics of various representations:
+
+* [report-O0](/bench/report-O0.md)
+* [report-O1](/bench/report-O1.md)
+* [report-O2](/bench/report-O2.md)
+
+## Resources
 * [LoginStateMachine](https://github.com/coot/free-category/blob/master/examples/src/LoginStateMachine.hs):
   based on [State Machines All The Way
   Down](https://www.youtube.com/watch?v=xq7ZuSRgCR4) by Edwin Bradly, 2017 You
@@ -26,4 +36,4 @@
   using a simple GADT.
 * Another
   [example](https://github.com/coot/free-algebras/blob/master/examples/src/Control/Category/Free.hs).
-* [Blog post](https://coot.me/posts/kleisli-categories-and-free-monads.html) on Keleisli categories.
+* [Blog post](https://coot.me/posts/kleisli-categories-and-free-monads.html) on Kleisli categories.
diff --git a/bench/Main.hs b/bench/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/Main.hs
@@ -0,0 +1,187 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE GADTs #-}
+
+module Main where
+
+import Prelude hiding (id, (.))
+import Control.Category
+import Data.Foldable (foldl')
+
+import Control.Category.Free
+import Control.Category.Free.Internal
+
+import Criterion
+import Criterion.Main
+
+
+data Alg a b where
+    Add :: !Int -> Alg Int Int
+    Mul :: !Int -> Alg Int Int
+
+instance Show (Alg a b) where
+    show (Add i) = "Add " ++ show i
+    show (Mul i) = "Mul " ++ show i
+
+interpret :: Alg a b -> a -> b
+interpret (Add i) = (+i)
+interpret (Mul i) = (*i)
+
+-- foldr on outer and inner lists
+fromListR :: Category (f Alg) => (Int -> f Alg Int Int) -> [[Int]] -> f Alg Int Int
+fromListR f = foldr (\is c -> foldr (\i c' -> f i . c') id is . c) id
+
+-- foldr on outer and foldl on inner list
+fromListRL :: Category (f Alg) => (Int -> f Alg Int Int) -> [[Int]] -> f Alg Int Int
+fromListRL f = foldr (\is c -> foldl (\c' i -> c' . f i) id is . c) id
+
+-- foldl on outer and inner loop
+fromListL :: Category (f Alg) => (Int -> f Alg Int Int) -> [[Int]] -> f Alg Int Int
+fromListL f = foldl' (\c is -> c . foldl' (\c' i -> c' . f i) id is) id
+
+-- foldl on outer and foldr on inner loop
+fromListLR :: Category (f Alg) => (Int -> f Alg Int Int) -> [[Int]] -> f Alg Int Int
+fromListLR f = foldr (\is c -> foldl' (\c' i -> c' . f i) id is . c) id
+
+-- alternate foldl and foldr
+fromListM' :: Category (f Alg) => (Int -> f Alg Int Int) -> [Int] -> f Alg Int Int
+fromListM' f is = foldl' (\c (i, x) -> if x then c . f i
+                                            else f i . c)
+                  id (zip is (concat $ repeat [True, False]))
+
+-- alternate foldl and foldr
+fromListM :: Category (f Alg) => (Int -> f Alg Int Int) -> [[Int]] -> f Alg Int Int
+fromListM f iss = foldl' (\c (is, x) -> if x then c . fromListM' f is
+                                             else fromListM' f is . c)
+                        id (zip iss (concat $ repeat [True, False]))
+
+setupEnv100 :: [[Int]]
+setupEnv100 = replicate 100 [1..100]
+
+setupEnv250 :: [[Int]]
+setupEnv250 = replicate 250 [1..250]
+
+setupEnv500 :: [[Int]]
+setupEnv500 = replicate 500 [1..500]
+
+main :: IO ()
+main = defaultMain
+    [ env (pure setupEnv100) $ \ints -> bgroup "main"
+      [ bgroup "Queue 100"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListR (\i -> liftQ (Add i)) ints)
+        , bench "right left" $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListRL (\i -> liftQ (Add i)) ints)
+        , bench "left left " $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListL (\i -> liftQ (Add i)) ints)
+        , bench "left right" $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListLR (\i -> liftQ (Add i)) ints)
+        , bench "alternate " $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListM (\i -> liftQ (Add i)) ints)
+        ]
+
+      , bgroup "ListTr 100"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListR (\i -> liftL (Add i)) ints)
+        , bench "right left" $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListRL (\i -> liftL (Add i)) ints)
+        , bench "left left " $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListL (\i -> liftL (Add i)) ints)
+        , bench "left right" $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListLR (\i -> liftL (Add i)) ints)
+        , bench "alternate " $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListM (\i -> ConsTr (Add i) NilTr) ints)
+        ]
+
+      , bgroup "C 100"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatFree2 interpret c 0)
+              (fromListR ((\i -> C $ \k -> k (Add i))) ints)
+        , bench "right left" $
+            whnf
+              (\c -> foldNatFree2 interpret c 0)
+              (fromListRL ((\i -> C $ \k -> k (Add i))) ints)
+        , bench "left left" $
+            whnf
+              (\c -> foldNatFree2 interpret c 0)
+              (fromListL ((\i -> C $ \k -> k (Add i))) ints)
+        , bench "left right" $
+            whnf
+              (\c -> foldNatFree2 interpret c 0)
+              (fromListLR ((\i -> C $ \k -> k (Add i))) ints)
+        , bench "alternate" $
+            whnf
+              (\c -> foldNatFree2 interpret c 0)
+              (fromListM ((\i -> C $ \k -> k (Add i))) ints)
+        ]
+      ]
+    , env (pure setupEnv250) $ \ints -> bgroup "main"
+      [ bgroup "Queue 250"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListR (\i -> liftQ (Add i)) ints)
+        ]
+
+      , bgroup "ListTr 250"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListR (\i -> liftL (Add i)) ints)
+        ]
+
+      {--
+        - , bgroup "C 250"
+        -   [ bench "right right" $
+        -       whnf
+        -         (\c -> foldNatFree2 interpret c 0)
+        -         (fromListR ((\i -> C $ \k -> k (Add i))) ints)
+        -   ]
+        --}
+      ]
+    , env (pure setupEnv500) $ \ints -> bgroup "main"
+      [ bgroup "Queue 500"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatQ interpret c 0)
+              (fromListR (\i -> liftQ (Add i)) ints)
+        ]
+
+      , bgroup "ListTr 500"
+        [ bench "right right" $
+            whnf
+              (\c -> foldNatL interpret c 0)
+              (fromListR (\i -> liftL (Add i)) ints)
+        ]
+
+      {--
+        - , bgroup "C 500"
+        -   [ bench "right right" $
+        -       whnf
+        -         (\c -> foldNatFree2 interpret c 0)
+        -         (fromListR ((\i -> C $ \k -> k (Add i))) ints)
+        -   ]
+        --}
+      ]
+    ]
+
diff --git a/bench/report-O0.md b/bench/report-O0.md
new file mode 100644
--- /dev/null
+++ b/bench/report-O0.md
@@ -0,0 +1,126 @@
+```
+cabal run -O0 bench-cats  
+benchmarking main/Queue 100/right right
+time                 1.141 ms   (1.138 ms .. 1.143 ms)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 1.140 ms   (1.138 ms .. 1.143 ms)
+std dev              8.646 μs   (6.948 μs .. 11.22 μs)
+
+benchmarking main/Queue 100/right left
+time                 1.141 ms   (1.136 ms .. 1.147 ms)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 1.138 ms   (1.135 ms .. 1.142 ms)
+std dev              10.92 μs   (8.393 μs .. 15.79 μs)
+
+benchmarking main/Queue 100/left left 
+time                 1.142 ms   (1.139 ms .. 1.146 ms)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 1.142 ms   (1.138 ms .. 1.147 ms)
+std dev              14.64 μs   (11.59 μs .. 19.91 μs)
+
+benchmarking main/Queue 100/left right
+time                 1.141 ms   (1.136 ms .. 1.147 ms)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 1.141 ms   (1.137 ms .. 1.148 ms)
+std dev              16.67 μs   (9.879 μs .. 29.72 μs)
+
+benchmarking main/Queue 100/alternate 
+time                 1.164 ms   (1.153 ms .. 1.185 ms)
+                     0.983 R²   (0.951 R² .. 0.999 R²)
+mean                 1.188 ms   (1.159 ms .. 1.290 ms)
+std dev              158.9 μs   (71.22 μs .. 324.6 μs)
+variance introduced by outliers: 83% (severely inflated)
+
+benchmarking main/ListTr 100/right right
+time                 700.0 μs   (691.4 μs .. 706.7 μs)
+                     0.997 R²   (0.993 R² .. 0.999 R²)
+mean                 756.8 μs   (718.7 μs .. 906.9 μs)
+std dev              245.7 μs   (9.661 μs .. 523.4 μs)
+variance introduced by outliers: 97% (severely inflated)
+
+benchmarking main/ListTr 100/right left
+time                 756.6 μs   (717.7 μs .. 812.2 μs)
+                     0.980 R²   (0.959 R² .. 1.000 R²)
+mean                 719.7 μs   (710.8 μs .. 755.0 μs)
+std dev              48.82 μs   (9.722 μs .. 100.7 μs)
+variance introduced by outliers: 57% (severely inflated)
+
+benchmarking main/ListTr 100/left left 
+time                 767.3 μs   (723.7 μs .. 813.2 μs)
+                     0.983 R²   (0.968 R² .. 1.000 R²)
+mean                 733.7 μs   (723.2 μs .. 762.2 μs)
+std dev              51.61 μs   (22.86 μs .. 96.08 μs)
+variance introduced by outliers: 59% (severely inflated)
+
+benchmarking main/ListTr 100/left right
+time                 717.4 μs   (715.5 μs .. 719.9 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 718.1 μs   (716.1 μs .. 721.1 μs)
+std dev              7.838 μs   (5.645 μs .. 12.14 μs)
+
+benchmarking main/ListTr 100/alternate 
+time                 715.4 μs   (712.1 μs .. 720.6 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 715.6 μs   (713.4 μs .. 719.0 μs)
+std dev              8.725 μs   (6.633 μs .. 11.88 μs)
+
+benchmarking main/C 100/right right
+time                 899.4 μs   (894.7 μs .. 905.2 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 902.1 μs   (898.5 μs .. 906.9 μs)
+std dev              13.97 μs   (10.79 μs .. 19.73 μs)
+
+benchmarking main/C 100/right left
+time                 903.2 μs   (895.5 μs .. 911.5 μs)
+                     0.999 R²   (0.999 R² .. 1.000 R²)
+mean                 900.8 μs   (896.2 μs .. 909.6 μs)
+std dev              20.72 μs   (14.03 μs .. 33.73 μs)
+variance introduced by outliers: 13% (moderately inflated)
+
+benchmarking main/C 100/left left
+time                 1.213 ms   (1.199 ms .. 1.241 ms)
+                     0.982 R²   (0.955 R² .. 0.999 R²)
+mean                 1.236 ms   (1.204 ms .. 1.320 ms)
+std dev              159.4 μs   (51.06 μs .. 269.7 μs)
+variance introduced by outliers: 81% (severely inflated)
+
+benchmarking main/C 100/left right
+time                 898.3 μs   (854.1 μs .. 969.1 μs)
+                     0.970 R²   (0.951 R² .. 0.992 R²)
+mean                 925.6 μs   (903.9 μs .. 959.2 μs)
+std dev              89.03 μs   (60.65 μs .. 138.8 μs)
+variance introduced by outliers: 72% (severely inflated)
+
+benchmarking main/C 100/alternate
+time                 1.075 ms   (1.063 ms .. 1.093 ms)
+                     0.996 R²   (0.992 R² .. 0.999 R²)
+mean                 1.085 ms   (1.071 ms .. 1.109 ms)
+std dev              58.94 μs   (35.22 μs .. 85.70 μs)
+variance introduced by outliers: 43% (moderately inflated)
+
+benchmarking main/Queue 250/right right
+time                 8.210 ms   (8.158 ms .. 8.283 ms)
+                     1.000 R²   (0.999 R² .. 1.000 R²)
+mean                 8.104 ms   (8.050 ms .. 8.148 ms)
+std dev              141.8 μs   (100.5 μs .. 213.6 μs)
+
+benchmarking main/ListTr 250/right right
+time                 6.835 ms   (6.677 ms .. 7.059 ms)
+                     0.997 R²   (0.994 R² .. 1.000 R²)
+mean                 6.631 ms   (6.592 ms .. 6.697 ms)
+std dev              151.1 μs   (73.51 μs .. 274.0 μs)
+
+benchmarking main/Queue 500/right right
+time                 33.14 ms   (32.12 ms .. 34.38 ms)
+                     0.995 R²   (0.984 R² .. 0.999 R²)
+mean                 33.84 ms   (33.06 ms .. 34.85 ms)
+std dev              1.819 ms   (1.173 ms .. 2.736 ms)
+variance introduced by outliers: 18% (moderately inflated)
+
+benchmarking main/ListTr 500/right right
+time                 28.88 ms   (27.92 ms .. 30.42 ms)
+                     0.983 R²   (0.944 R² .. 0.999 R²)
+mean                 29.04 ms   (28.51 ms .. 30.34 ms)
+std dev              1.758 ms   (608.9 μs .. 3.384 ms)
+variance introduced by outliers: 21% (moderately inflated)
+```
diff --git a/bench/report-O1.md b/bench/report-O1.md
new file mode 100644
--- /dev/null
+++ b/bench/report-O1.md
@@ -0,0 +1,129 @@
+```
+cabal run -O1 bench-cats  
+benchmarking main/Queue 100/right right
+time                 344.2 μs   (337.1 μs .. 362.0 μs)
+                     0.974 R²   (0.923 R² .. 1.000 R²)
+mean                 346.8 μs   (338.8 μs .. 375.4 μs)
+std dev              47.04 μs   (4.662 μs .. 98.23 μs)
+variance introduced by outliers: 87% (severely inflated)
+
+benchmarking main/Queue 100/right left
+time                 334.1 μs   (333.3 μs .. 334.7 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 333.7 μs   (333.1 μs .. 334.3 μs)
+std dev              2.083 μs   (1.686 μs .. 2.609 μs)
+
+benchmarking main/Queue 100/left left 
+time                 336.6 μs   (334.3 μs .. 340.4 μs)
+                     0.997 R²   (0.991 R² .. 1.000 R²)
+mean                 339.0 μs   (335.2 μs .. 353.2 μs)
+std dev              20.23 μs   (6.119 μs .. 45.16 μs)
+variance introduced by outliers: 55% (severely inflated)
+
+benchmarking main/Queue 100/left right
+time                 334.4 μs   (333.9 μs .. 335.0 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 334.3 μs   (333.6 μs .. 335.3 μs)
+std dev              2.840 μs   (2.002 μs .. 4.592 μs)
+
+benchmarking main/Queue 100/alternate 
+time                 333.4 μs   (332.9 μs .. 334.1 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 334.1 μs   (333.5 μs .. 334.7 μs)
+std dev              1.989 μs   (1.597 μs .. 2.655 μs)
+
+benchmarking main/ListTr 100/right right
+time                 168.0 μs   (167.7 μs .. 168.3 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 168.4 μs   (168.1 μs .. 168.9 μs)
+std dev              1.328 μs   (905.4 ns .. 2.041 μs)
+
+benchmarking main/ListTr 100/right left
+time                 176.4 μs   (173.7 μs .. 180.5 μs)
+                     0.985 R²   (0.966 R² .. 0.999 R²)
+mean                 180.4 μs   (174.5 μs .. 191.0 μs)
+std dev              26.56 μs   (11.94 μs .. 40.58 μs)
+variance introduced by outliers: 90% (severely inflated)
+
+benchmarking main/ListTr 100/left left 
+time                 181.4 μs   (171.8 μs .. 200.9 μs)
+                     0.965 R²   (0.926 R² .. 1.000 R²)
+mean                 174.4 μs   (171.5 μs .. 188.0 μs)
+std dev              17.44 μs   (1.898 μs .. 39.71 μs)
+variance introduced by outliers: 80% (severely inflated)
+
+benchmarking main/ListTr 100/left right
+time                 171.7 μs   (170.3 μs .. 173.4 μs)
+                     0.999 R²   (0.999 R² .. 0.999 R²)
+mean                 175.3 μs   (173.9 μs .. 177.5 μs)
+std dev              5.737 μs   (3.819 μs .. 10.35 μs)
+variance introduced by outliers: 30% (moderately inflated)
+
+benchmarking main/ListTr 100/alternate 
+time                 172.2 μs   (169.5 μs .. 174.3 μs)
+                     0.999 R²   (0.999 R² .. 1.000 R²)
+mean                 170.3 μs   (169.6 μs .. 171.4 μs)
+std dev              2.847 μs   (2.192 μs .. 3.745 μs)
+
+benchmarking main/C 100/right right
+time                 741.9 μs   (720.1 μs .. 769.8 μs)
+                     0.996 R²   (0.993 R² .. 0.999 R²)
+mean                 738.5 μs   (733.4 μs .. 746.4 μs)
+std dev              21.90 μs   (14.74 μs .. 36.25 μs)
+variance introduced by outliers: 20% (moderately inflated)
+
+benchmarking main/C 100/right left
+time                 671.2 μs   (655.1 μs .. 693.1 μs)
+                     0.974 R²   (0.924 R² .. 0.999 R²)
+mean                 681.5 μs   (658.5 μs .. 777.3 μs)
+std dev              127.4 μs   (26.16 μs .. 280.5 μs)
+variance introduced by outliers: 92% (severely inflated)
+
+benchmarking main/C 100/left left
+time                 802.2 μs   (784.7 μs .. 824.5 μs)
+                     0.996 R²   (0.996 R² .. 0.998 R²)
+mean                 795.6 μs   (787.1 μs .. 805.5 μs)
+std dev              30.72 μs   (26.91 μs .. 35.57 μs)
+variance introduced by outliers: 29% (moderately inflated)
+
+benchmarking main/C 100/left right
+time                 657.8 μs   (650.4 μs .. 668.8 μs)
+                     0.998 R²   (0.997 R² .. 0.999 R²)
+mean                 656.8 μs   (649.6 μs .. 665.1 μs)
+std dev              26.63 μs   (20.92 μs .. 35.68 μs)
+variance introduced by outliers: 33% (moderately inflated)
+
+benchmarking main/C 100/alternate
+time                 1.065 ms   (1.053 ms .. 1.082 ms)
+                     0.997 R²   (0.994 R² .. 0.999 R²)
+mean                 1.074 ms   (1.061 ms .. 1.093 ms)
+std dev              53.90 μs   (39.80 μs .. 70.25 μs)
+variance introduced by outliers: 39% (moderately inflated)
+
+benchmarking main/Queue 250/right right
+time                 3.203 ms   (2.938 ms .. 3.591 ms)
+                     0.966 R²   (0.942 R² .. 0.998 R²)
+mean                 2.963 ms   (2.915 ms .. 3.067 ms)
+std dev              226.0 μs   (94.89 μs .. 422.7 μs)
+variance introduced by outliers: 52% (severely inflated)
+
+benchmarking main/ListTr 250/right right
+time                 3.265 ms   (3.231 ms .. 3.295 ms)
+                     0.999 R²   (0.999 R² .. 1.000 R²)
+mean                 3.261 ms   (3.239 ms .. 3.284 ms)
+std dev              71.15 μs   (57.97 μs .. 86.47 μs)
+
+benchmarking main/Queue 500/right right
+time                 11.72 ms   (11.47 ms .. 11.94 ms)
+                     0.997 R²   (0.996 R² .. 0.999 R²)
+mean                 11.95 ms   (11.79 ms .. 12.20 ms)
+std dev              521.0 μs   (333.3 μs .. 799.6 μs)
+variance introduced by outliers: 17% (moderately inflated)
+
+benchmarking main/ListTr 500/right right
+time                 17.55 ms   (15.86 ms .. 18.15 ms)
+                     0.956 R²   (0.839 R² .. 0.999 R²)
+mean                 18.91 ms   (18.14 ms .. 22.44 ms)
+std dev              3.166 ms   (347.5 μs .. 6.963 ms)
+variance introduced by outliers: 71% (severely inflated)
+```
diff --git a/bench/report-O2.md b/bench/report-O2.md
new file mode 100644
--- /dev/null
+++ b/bench/report-O2.md
@@ -0,0 +1,126 @@
+```
+cabal run -O2 bench-cats                                               
+benchmarking main/Queue 100/right right
+time                 341.9 μs   (341.2 μs .. 342.8 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 340.9 μs   (340.0 μs .. 341.9 μs)
+std dev              3.115 μs   (2.201 μs .. 4.603 μs)
+
+benchmarking main/Queue 100/right left
+time                 342.2 μs   (341.6 μs .. 342.8 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 341.5 μs   (340.9 μs .. 342.2 μs)
+std dev              2.108 μs   (1.700 μs .. 2.556 μs)
+
+benchmarking main/Queue 100/left left 
+time                 341.5 μs   (341.1 μs .. 342.2 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 341.9 μs   (341.2 μs .. 343.3 μs)
+std dev              3.117 μs   (1.865 μs .. 5.348 μs)
+
+benchmarking main/Queue 100/left right
+time                 344.0 μs   (342.7 μs .. 345.8 μs)
+                     1.000 R²   (0.999 R² .. 1.000 R²)
+mean                 344.5 μs   (343.2 μs .. 346.5 μs)
+std dev              5.442 μs   (4.365 μs .. 7.546 μs)
+
+benchmarking main/Queue 100/alternate 
+time                 359.1 μs   (343.2 μs .. 378.1 μs)
+                     0.989 R²   (0.979 R² .. 0.999 R²)
+mean                 347.1 μs   (343.3 μs .. 357.3 μs)
+std dev              19.80 μs   (10.27 μs .. 35.11 μs)
+variance introduced by outliers: 53% (severely inflated)
+
+benchmarking main/ListTr 100/right right
+time                 175.0 μs   (174.3 μs .. 176.0 μs)
+                     0.999 R²   (0.999 R² .. 1.000 R²)
+mean                 175.8 μs   (174.8 μs .. 178.3 μs)
+std dev              5.004 μs   (2.051 μs .. 9.617 μs)
+variance introduced by outliers: 24% (moderately inflated)
+
+benchmarking main/ListTr 100/right left
+time                 175.2 μs   (174.2 μs .. 176.4 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 175.3 μs   (174.6 μs .. 176.2 μs)
+std dev              2.866 μs   (2.014 μs .. 4.405 μs)
+
+benchmarking main/ListTr 100/left left 
+time                 178.8 μs   (175.7 μs .. 182.2 μs)
+                     0.998 R²   (0.998 R² .. 1.000 R²)
+mean                 177.0 μs   (175.6 μs .. 179.9 μs)
+std dev              6.350 μs   (3.620 μs .. 11.78 μs)
+variance introduced by outliers: 33% (moderately inflated)
+
+benchmarking main/ListTr 100/left right
+time                 174.2 μs   (173.3 μs .. 175.6 μs)
+                     0.999 R²   (0.998 R² .. 0.999 R²)
+mean                 180.9 μs   (178.4 μs .. 184.9 μs)
+std dev              10.83 μs   (7.423 μs .. 16.29 μs)
+variance introduced by outliers: 59% (severely inflated)
+
+benchmarking main/ListTr 100/alternate 
+time                 173.9 μs   (173.0 μs .. 175.0 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 173.5 μs   (173.0 μs .. 174.1 μs)
+std dev              1.951 μs   (1.514 μs .. 2.633 μs)
+
+benchmarking main/C 100/right right
+time                 798.5 μs   (792.7 μs .. 803.5 μs)
+                     1.000 R²   (0.999 R² .. 1.000 R²)
+mean                 797.5 μs   (793.5 μs .. 800.9 μs)
+std dev              11.98 μs   (9.948 μs .. 15.01 μs)
+
+benchmarking main/C 100/right left
+time                 679.3 μs   (670.8 μs .. 691.7 μs)
+                     0.998 R²   (0.997 R² .. 0.998 R²)
+mean                 686.6 μs   (678.4 μs .. 695.5 μs)
+std dev              27.59 μs   (25.17 μs .. 30.52 μs)
+variance introduced by outliers: 32% (moderately inflated)
+
+benchmarking main/C 100/left left
+time                 780.6 μs   (776.9 μs .. 783.9 μs)
+                     1.000 R²   (1.000 R² .. 1.000 R²)
+mean                 775.6 μs   (772.1 μs .. 778.7 μs)
+std dev              10.92 μs   (8.476 μs .. 15.08 μs)
+
+benchmarking main/C 100/left right
+time                 601.6 μs   (598.7 μs .. 604.4 μs)
+                     1.000 R²   (0.999 R² .. 1.000 R²)
+mean                 607.9 μs   (602.8 μs .. 616.0 μs)
+std dev              20.49 μs   (15.07 μs .. 26.09 μs)
+variance introduced by outliers: 25% (moderately inflated)
+
+benchmarking main/C 100/alternate
+time                 1.045 ms   (987.6 μs .. 1.161 ms)
+                     0.940 R²   (0.867 R² .. 0.999 R²)
+mean                 1.016 ms   (986.8 μs .. 1.107 ms)
+std dev              152.4 μs   (57.42 μs .. 296.9 μs)
+variance introduced by outliers: 86% (severely inflated)
+
+benchmarking main/Queue 250/right right
+time                 2.733 ms   (2.700 ms .. 2.764 ms)
+                     0.999 R²   (0.999 R² .. 1.000 R²)
+mean                 2.694 ms   (2.676 ms .. 2.710 ms)
+std dev              56.66 μs   (45.91 μs .. 76.23 μs)
+
+benchmarking main/ListTr 250/right right
+time                 3.356 ms   (3.175 ms .. 3.551 ms)
+                     0.979 R²   (0.968 R² .. 0.989 R²)
+mean                 3.425 ms   (3.315 ms .. 3.587 ms)
+std dev              422.6 μs   (296.3 μs .. 610.7 μs)
+variance introduced by outliers: 74% (severely inflated)
+
+benchmarking main/Queue 500/right right
+time                 11.27 ms   (10.84 ms .. 11.78 ms)
+                     0.985 R²   (0.973 R² .. 0.993 R²)
+mean                 12.36 ms   (11.94 ms .. 12.99 ms)
+std dev              1.344 ms   (995.0 μs .. 1.928 ms)
+variance introduced by outliers: 56% (severely inflated)
+
+benchmarking main/ListTr 500/right right
+time                 18.27 ms   (17.13 ms .. 19.35 ms)
+                     0.986 R²   (0.975 R² .. 0.998 R²)
+mean                 18.14 ms   (17.70 ms .. 18.98 ms)
+std dev              1.466 ms   (866.9 μs .. 2.203 ms)
+variance introduced by outliers: 35% (moderately inflated)
+```
diff --git a/free-category.cabal b/free-category.cabal
--- a/free-category.cabal
+++ b/free-category.cabal
@@ -1,5 +1,5 @@
 name:           free-category
-version:        0.0.3.0
+version:        0.0.4.0
 synopsis:       Free category
 description:    Free categories
 category:       Algebra, Control, Monads, Category
@@ -15,7 +15,10 @@
 extra-source-files:
     ChangeLog.md
     README.md
-tested-with:    GHC==8.0.2, GHC==8.2.2, GHC==8.4.4, GHC==8.6.5
+    bench/report-O0.md
+    bench/report-O1.md
+    bench/report-O2.md
+tested-with:    GHC==8.0.2, GHC==8.2.2, GHC==8.4.4, GHC==8.6.5, GHC==8.8.1
 
 source-repository head
   type: git
@@ -26,18 +29,59 @@
       Control.Arrow.Free
       Control.Category.Free
       Control.Category.Free.Internal
-      Control.Category.FreeEff
+      Control.Category.FreeEffect
   other-modules:
       Paths_free_category
   hs-source-dirs:
       src
   build-depends:
       base          >= 4.9 && <5
-    , free-algebras >= 0.0.7.0
+    , free-algebras >= 0.0.8.0
   ghc-options:
     -Wall
     -fwarn-incomplete-record-updates
     -fwarn-incomplete-uni-patterns
     -fwarn-redundant-constraints
     -fwarn-deprecations
+  default-language: Haskell2010
+
+test-suite test-cats
+  type:
+      exitcode-stdio-1.0
+  hs-source-dirs:
+      test
+  main-is:
+      Main.hs
+  other-modules:
+      Test.Cat
+      Test.Queue
+  build-depends:
+      base
+    , QuickCheck
+    , tasty-quickcheck
+    , tasty
+    , free-algebras
+
+    , free-category
+  ghc-options:
+    -Wall
+    -fwarn-incomplete-record-updates
+    -fwarn-incomplete-uni-patterns
+    -fno-ignore-asserts
+    -fwarn-deprecations
+  default-language: Haskell2010
+
+benchmark bench-cats
+  hs-source-dirs:
+      bench
+  main-is:
+      Main.hs
+  type:
+      exitcode-stdio-1.0
+  build-depends:
+      base
+    , free-category
+    , criterion
+  ghc-options:
+    -rtsopts
   default-language: Haskell2010
diff --git a/src/Control/Arrow/Free.hs b/src/Control/Arrow/Free.hs
--- a/src/Control/Arrow/Free.hs
+++ b/src/Control/Arrow/Free.hs
@@ -41,7 +41,7 @@
   ( AlgebraType0
   , AlgebraType
   , FreeAlgebra2 (..)
-  , proof
+  , Proof (..)
   , wrapFree2
   , foldFree2
   , hoistFree2
@@ -63,7 +63,7 @@
 mapArr :: f b c
        -> Arr f a b
        -> Arr f a c
-mapArr bc ac = Cons bc emptyQ . ac
+mapArr bc ac = Cons bc nilQ . ac
 
 foldArr :: forall f arr a b.
            Arrow arr
@@ -71,7 +71,7 @@
         -> Arr f a b
         -> arr a b
 foldArr _   Id = id
-foldArr fun (Cons bc ab) = fun bc . foldQ (foldNatFree2 fun) ab
+foldArr fun (Cons bc ab) = fun bc . foldNatQ (foldNatFree2 fun) ab
 foldArr fun (Arr f g)    = arr f  . foldNatFree2 fun g
 foldArr fun (Prod f g)   = foldNatFree2 fun f &&& foldNatFree2 fun g
 
@@ -79,7 +79,7 @@
   id = Id
   Id         . f  = f
   f          . Id = f
-  (Cons f g)  . h  = Cons f (g `snoc` h)
+  (Cons f g) . h  = Cons f (g `snocQ` h)
   (Arr f g)  . h  = Arr f (g . h)
   (Prod f g) . h  = Prod (f . h) (g . h)
 
@@ -103,14 +103,14 @@
 type instance AlgebraType  Arr c = Arrow c
 
 instance FreeAlgebra2 Arr where
-  liftFree2 = \fab -> Cons fab emptyQ
+  liftFree2 = \fab -> Cons fab nilQ
   {-# INLINE liftFree2 #-}
 
   foldNatFree2 = foldArr
   {-# INLINE foldNatFree2 #-}
 
-  codom2  = proof
-  forget2 = proof
+  codom2  = Proof
+  forget2 = Proof
 
 --
 -- Free arrows using CSP style
@@ -166,5 +166,5 @@
   foldNatFree2 fun (A f) = f fun
   {-# INLINE foldNatFree2 #-}
 
-  codom2  = proof
-  forget2 = proof
+  codom2  = Proof
+  forget2 = Proof
diff --git a/src/Control/Category/Free.hs b/src/Control/Category/Free.hs
--- a/src/Control/Category/Free.hs
+++ b/src/Control/Category/Free.hs
@@ -1,13 +1,19 @@
-{-# LANGUAGE BangPatterns       #-}
-{-# LANGUAGE CPP                #-}
-{-# LANGUAGE GADTs              #-}
-{-# LANGUAGE FlexibleInstances  #-}
-{-# LANGUAGE PatternSynonyms    #-}
-{-# LANGUAGE PolyKinds          #-}
-{-# LANGUAGE RankNTypes         #-}
-{-# LANGUAGE TypeOperators      #-}
-{-# LANGUAGE TypeFamilies       #-}
-{-# LANGUAGE ViewPatterns       #-}
+{-# LANGUAGE BangPatterns          #-}
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE ViewPatterns          #-}
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
 
 {-# OPTIONS_HADDOCK show-extensions #-}
 
@@ -20,23 +26,43 @@
 #endif
 
 module Control.Category.Free
-    ( -- * Free category
-      Cat (Id)
-    , arrCat
-    , mapCat
-    , foldCat
+    ( -- * Real time Queue
+      Queue (ConsQ, NilQ)
+    , consQ
+    , snocQ
+    , unconsQ
+    , liftQ
+    , foldNatQ
+    , foldrQ
+    , foldlQ
+    , zipWithQ
+
+      -- * Type alligned list
+    , ListTr (..)
+    , liftL
+    , foldNatL
+    , foldlL
+    , foldrL
+    , zipWithL
+
       -- * Free category (CPS style)
     , C (..)
+    , liftC
+    , consC
+    , foldNatC
     , toC
     , fromC
-      -- * Oposite category
+
+      -- * Opposite category
     , Op (..)
+    , hoistOp
 
       -- * Free interface re-exports
     , FreeAlgebra2 (..)
     , wrapFree2
     , foldFree2
     , hoistFree2
+    , hoistFreeH2
     , joinFree2
     , bindFree2
     )
@@ -45,17 +71,17 @@
 import           Prelude hiding (id, concat, (.))
 import           Control.Category (Category (..))
 import           Control.Algebra.Free2
-  ( AlgebraType0
-  , AlgebraType
-  , FreeAlgebra2 (..)
-  , proof
-  , wrapFree2
-  , foldFree2
-  , hoistFree2
-  , hoistFreeH2
-  , joinFree2
-  , bindFree2
-  )
+                  ( AlgebraType0
+                  , AlgebraType
+                  , FreeAlgebra2 (..)
+                  , Proof (..)
+                  , wrapFree2
+                  , foldFree2
+                  , hoistFree2
+                  , hoistFreeH2
+                  , joinFree2
+                  , bindFree2
+                  )
 import           Control.Arrow (Arrow (..), ArrowZero (..), ArrowChoice (..))
 #if __GLASGOW_HASKELL__ < 804
 import           Data.Monoid (Monoid (..))
@@ -63,106 +89,9 @@
 #endif
 
 import           Control.Category.Free.Internal
---
--- Free categories based on real time queues; Ideas after E.Kmett's guanxi
--- project.
---
 
--- | Efficient encoding of a category for which morphism composition has
--- @O\(1\)@ complexity and fold is linear in the number of transitions.
--- 
-data Cat (f :: k -> k -> *) a b where
-    Id   :: Cat f a a 
-    Cat  :: forall f a b c.
-            f b c
-         -> Queue (Cat f) a b
-         -> Cat f a c 
 
--- | Smart constructor for embeding spanning transitions into 'Cat', the same
--- as @'liftFree2' \@'Cat'@.  It is like 'arr' for 'Arrows'.
 --
-arrCat :: forall (f :: k -> k -> *) a b.
-         f a b
-      -> Cat f a b
-arrCat fab = Cat fab emptyQ
-
--- | Smart constructor 'mapCat' for morphisms of @'Cat' f@ category.
---
-mapCat :: forall (f :: k -> k -> *) a b c.
-           f b c
-        -> Cat f a b
-        -> Cat f a c
-mapCat fbc cab = arrCat fbc . cab
-
--- | Right fold of 'Cat' into a category, the same as @'foldNatFree2' \@'Cat'@.
---
--- /complexity/: @O\(n\) where @n@ is number of transition embedded in 'Cat'.
-foldCat :: forall f c a b.
-           Category c
-        => (forall x y. f x y -> c x y)
-        -> Cat f a b
-        -> c a b
-foldCat _nat Id = id
-foldCat nat (Cat tr queue) =
-    case queue of
-      NilQ            -> nat tr
-      ConsQ Id queue' -> nat tr . foldQ (foldCat nat) queue'
-      ConsQ c  queue' -> nat tr . foldCat nat c . foldQ (foldCat nat) queue'
-
--- TODO: implement foldl; it might require different representation.  Function
--- composition is applied from right to left, so it should be more efficient.
-
--- | /complexity/ of composition @('.')@: @O\(1\)@ (worst case)
-instance Category (Cat f) where
-    id = Id
-
-    Id . f  = f
-    f  . Id = f
-    Cat f q . h = Cat f (q `snoc` h)
-
-type instance AlgebraType0 Cat f = ()
-type instance AlgebraType  Cat c = Category c
-
--- | /complexity/ of 'foldNatFree2': @O\(n\)@ where @n@ is number of
--- transitions embeded in 'Cat'.
---
-instance FreeAlgebra2 Cat where
-  liftFree2 = arrCat
-  {-# INLINE liftFree2 #-}
-
-  foldNatFree2 = foldCat
-  {-# INLINE foldNatFree2 #-}
-
-  codom2  = proof
-  forget2 = proof
-
-instance Arrow f => Arrow (Cat f) where
-    arr = arrCat . arr
-    Cat tr queue *** Cat tr' queue' = Cat (tr *** tr') (zipWithQ (***) queue queue')
-    Cat tr queue *** Id             = Cat (tr *** arr id) (zipWithQ (***) queue NilQ)
-    Id           *** Cat tr' queue' = Cat (arr id *** tr') (zipWithQ (***) NilQ queue')
-    Id           *** Id             = Cat (arr id *** arr id) NilQ
-
-instance ArrowZero f => ArrowZero (Cat f) where
-    zeroArrow = arrCat zeroArrow
-
-instance ArrowChoice f => ArrowChoice (Cat f) where
-    Cat fxb cax +++ Cat fyb cay
-                         = Cat (fxb +++ fyb) (zipWithQ (+++) cax cay)
-    Cat fxb cax +++ Id   = Cat (fxb +++ arr id) (zipWithQ (+++) cax NilQ)
-    Id +++ (Cat fxb cax) = Cat (arr id +++ fxb) (zipWithQ (+++) NilQ cax)
-    Id +++ Id            = Id
-
-instance Semigroup (Cat f o o) where
-    f <> g = f . g
-
-instance Monoid (Cat f o o) where
-    mempty = Id
-#if __GLASGOW_HASKELL__ < 804
-    mappend = (<>)
-#endif
-
---
 -- CPS style free categories
 --
 
@@ -170,56 +99,115 @@
 -- CPS style encoded free category; one can use @'FreeAlgebra2'@ class
 -- instance:
 --
--- prop> liftFree2    @C :: f a b -> C f a b
--- prop> foldNatFree2 @C :: Category d => (forall x y. f x y -> d x y) -> C f a b -> d a b
+-- > liftFree2    @C :: f a b -> C f a b
+-- > foldNatFree2 @C :: Category d
+-- >                 => (forall x y. f x y -> d x y)
+-- >                 -> C f a b -> d a b
+--
 newtype C f a b
   = C { runC :: forall r. Category r
              => (forall x y. f x y -> r x y)
              -> r a b
       }
 
-instance Category (C f) where
-  id = C (const id)
-  C bc . C ab = C $ \k -> bc k . ab k
+composeC :: C f y z -> C f x y -> C f x z
+composeC (C g) (C f) = C $ \k -> g k . f k
+{-# INLINE [1] composeC #-}
 
 -- |
--- Isomorphism from @'Cat'@ to @'C'@, which is a specialisation of
+-- Isomorphism from @'ListTr'@ to @'C'@, which is a specialisation of
 -- @'hoistFreeH2'@.
 toC :: ListTr f a b -> C f a b
 toC = hoistFreeH2
 {-# INLINE toC #-}
 
 -- |
--- Inverse of @'fromC'@, which also is a specialisatin of @'hoistFreeH2'@.
+-- Inverse of @'fromC'@, which also is a specialisation of @'hoistFreeH2'@.
 fromC :: C f a b -> ListTr f a b
 fromC = hoistFreeH2
 {-# INLINE fromC #-}
 
+liftC :: forall (f :: k -> k -> *) a b.
+         f a b
+      -> C f a b
+liftC = \f -> C $ \k -> k f
+{-# INLINE [1] liftC #-}
+
+consC :: forall (f :: k -> k -> *) a b c.
+         f b c
+      -> C f a b
+      -> C f a c
+consC bc ab = liftC bc `composeC` ab
+{-# INLINE [1] consC #-}
+
+foldNatC :: forall (f :: k -> k -> *) c a b.
+            Category c
+         => (forall x y. f x y -> c x y)
+         -> C f a b
+         -> c a b
+foldNatC nat (C f) = f nat
+{-# INLINE [1] foldNatC #-}
+
+{-# RULES
+
+"foldNatC/consC"
+  forall (f :: f (v :: k) (w :: k))
+         (q :: C f (u :: k) (v :: k))
+         (nat :: forall (x :: k) (y :: k). f x y -> c x y).
+  foldNatC nat (consC f q) = nat f . foldNatC nat q
+
+"foldNatC/liftC"
+  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
+         (g :: f v w)
+         (h :: C f u v).
+  foldNatC nat (liftC g `composeC` h) = nat g . foldNatC nat h
+
+#-}
+
+instance Category (C f) where
+  id  = C (const id)
+  (.) = composeC
+
+#if __GLASGOW_HASKELL__ >= 806
+-- | Show instance via 'ListTr'
+--
+instance (forall x y. Show (f x y)) => Show (C f a b) where
+    show c = show (hoistFreeH2 c :: ListTr f a b)
+#else
+-- | Blind show instance via 'ListTr'
+--
+instance Show (C f a b) where
+    show c = show (hoistFreeH2 c :: ListTr f a b)
+#endif
+
 type instance AlgebraType0 C f = ()
 type instance AlgebraType  C c = Category c
 
 instance FreeAlgebra2 C where
-  liftFree2 = \fab -> C $ \k -> k fab
+  liftFree2    = liftC
   {-# INLINE liftFree2 #-}
-
-  foldNatFree2 fun (C f) = f fun
+  foldNatFree2 = foldNatC
   {-# INLINE foldNatFree2 #-}
 
-  codom2  = proof
-  forget2 = proof
+  codom2  = Proof
+  forget2 = Proof
 
 instance Arrow f => Arrow (C f) where
   arr ab = C $ \k -> k (arr ab)
+  {-# INLINE arr #-}
+
   C c1 *** C c2  = C $ \k -> k (c1 id *** c2 id)
+  {-# INLINE (***) #-}
 
 instance ArrowZero f => ArrowZero (C f) where
   zeroArrow = C $ \k -> k zeroArrow
 
 instance ArrowChoice f => ArrowChoice (C f) where
   C c1 +++ C c2  = C $ \k -> k (c1 id +++ c2 id)
+  {-# INLINE (+++) #-}
 
 instance Semigroup (C f o o) where
-  f <> g = f . g
+  f <> g = f `composeC` g
 
 instance Monoid (C f o o) where
   mempty = id
diff --git a/src/Control/Category/Free/Internal.hs b/src/Control/Category/Free/Internal.hs
--- a/src/Control/Category/Free/Internal.hs
+++ b/src/Control/Category/Free/Internal.hs
@@ -1,16 +1,21 @@
-{-# LANGUAGE CPP               #-}
-{-# LANGUAGE GADTs             #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternSynonyms   #-}
-{-# LANGUAGE PolyKinds         #-}
-{-# LANGUAGE RankNTypes        #-}
-{-# LANGUAGE TypeFamilies      #-}
-{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE ViewPatterns          #-}
 
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
+
 {-# OPTIONS_HADDOCK show-extensions #-}
 
 #if __GLASGOW_HASKELL__ <= 802
--- ghc802 does not infer that 'cons' is used when using a bidirectional
+-- ghc802 does not infer that 'consQ' is used when using a bidirectional
 -- pattern
 {-# OPTIONS_GHC -Wno-unused-top-binds    #-}
 -- the 'complete' pragma was introduced in ghc804
@@ -23,13 +28,27 @@
 --
 module Control.Category.Free.Internal
   ( Op (..)
+  , hoistOp
+
   , ListTr (..)
+  , liftL
+  , foldNatL
+  , lengthListTr
+  , foldrL
+  , foldlL
+  , zipWithL
+
   , Queue (NilQ, ConsQ)
-  , emptyQ
-  , cons
-  , uncons
-  , snoc
-  , foldQ
+  , liftQ
+  , nilQ
+  , consQ
+  , ViewL (..)
+  , unconsQ
+  , snocQ
+  , foldNatQ
+  , foldrQ
+  , foldlQ
+  , hoistQ
   , zipWithQ
   ) where
 
@@ -45,14 +64,26 @@
 import           Control.Algebra.Free2 ( AlgebraType0
                                        , AlgebraType
                                        , FreeAlgebra2 (..)
-                                       , proof
+                                       , Proof (..)
                                        )
 
 -- | Oposite categoy in which arrows from @a@ to @b@ are represented by arrows
 -- from @b@ to @a@ in the original category.
 --
 newtype Op (f :: k -> k -> *) (a :: k) (b :: k) = Op { runOp :: f b a }
+  deriving Show
 
+-- | 'Op' is an endo-functor of the category of categories.
+--
+hoistOp :: forall (f :: k -> k -> *)
+                  (g :: k -> k -> *)
+                  a b.
+           (forall x y. f x y -> g x y)
+        -> Op f a b
+        -> Op g a b
+hoistOp nat (Op ba) = Op (nat ba)
+{-# INLINE hoistOp #-}
+
 instance Category f => Category (Op f) where
     id = Op id
     Op f . Op g = Op (g . f)
@@ -66,25 +97,150 @@
     mappend = (<>)
 #endif
 
--- |
--- Free category encoded as a recursive data type, in a simlar way as
--- @'Control.Monad.Free.Free'@.  You can use @'FreeAlgebra2'@ class instance:
+
 --
--- prop> liftFree2    @Cat :: f a b -> Cat f ab
--- prop> foldNatFree2 @Cat :: Category d => (forall x y. f x y -> d x y) -> Cat f a b -> d a b
+-- Type aligned list 'ListTr'
 --
+
+
+-- | Simple representation of a free category by using type aligned
+-- lists.  This is not a surprise as free monoids can be represented by
+-- lists (up to laziness)
+--
+-- 'ListTr' has @'FreeAlgebra2'@ class instance:
+--
+-- > liftFree2    @ListTr :: f a b -> ListTr f ab
+-- > foldNatFree2 @ListTr :: Category d
+-- >                      => (forall x y. f x y -> d x y)
+-- >                      -> ListTr f a b
+-- >                      -> d a b
+--
 -- The same performance concerns that apply to @'Control.Monad.Free.Free'@
 -- apply to this encoding of a free category.
 --
+-- Note that even though this is a naive version, it behaves quite well in
+-- simple benchmarks and quite stable regardless of the level of optimisations.
+--
 data ListTr :: (k -> k -> *) -> k -> k -> * where
   NilTr  :: ListTr f a a
   ConsTr :: f b c -> ListTr f a b -> ListTr f a c
 
+lengthListTr :: ListTr f a b -> Int
+lengthListTr NilTr = 0
+lengthListTr (ConsTr _ xs) = 1 + lengthListTr xs
+
+composeL :: forall (f :: k -> k -> *) x y z.
+            ListTr f y z
+         -> ListTr f x y
+         -> ListTr f x z
+composeL (ConsTr x xs) ys = ConsTr x (xs . ys)
+composeL NilTr         ys = ys
+{-# INLINE [1] composeL #-}
+
+liftL :: forall (f :: k -> k -> *) x y.
+         f x y -> ListTr f x y
+liftL f = ConsTr f NilTr
+{-# INLINE [1] liftL #-}
+
+foldNatL :: forall (f :: k -> k -> *) c a b.
+            Category c
+         => (forall x y. f x y -> c x y)
+         -> ListTr f a b
+         -> c a b
+foldNatL _   NilTr     = id
+foldNatL fun (ConsTr bc ab) = fun bc . foldNatFree2 fun ab
+{-# INLINE [1] foldNatL #-}
+
+{-# RULES
+
+"foldNatL/ConsTr"
+  forall (f :: f (v :: k) (w :: k))
+         (q :: ListTr f (u :: k) (v :: k))
+         (nat :: forall (x :: k) (y :: k). f x y -> c x y).
+  foldNatL nat (ConsTr f q) = nat f . foldNatL nat q
+
+"foldNatL/NilTr"  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y).
+                  foldNatL nat NilTr = id
+
+"foldNatL/liftL"
+  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
+         (g :: f v w)
+         (h :: ListTr f u v).
+    foldNatL nat (liftL g `composeL` h) = nat g . foldNatL nat h
+
+#-}
+
+-- | 'foldr' of a 'ListTr'
+--
+foldrL :: forall (f :: k -> k -> *) c a b d.
+          (forall x y z. f y z -> c x y -> c x z)
+       -> c a b
+       -> ListTr f b d
+       -> c a d
+foldrL _nat ab NilTr          = ab
+foldrL  nat ab (ConsTr xd bx) = nat xd (foldrL nat ab bx)
+{-# INLINE [1] foldrL #-}
+
+-- | 'foldl' of a 'ListTr'
+--
+-- TODO: make it strict, like 'foldl''.
+--
+foldlL :: forall (f :: k -> k -> *) c a b d.
+          (forall x y z. c y z -> f x y -> c x z)
+       -> c b d
+       -> ListTr f a b
+       -> c a d
+foldlL _nat bd NilTr          = bd
+foldlL  nat bd (ConsTr xb ax) = foldlL nat (nat bd xb) ax
+
+zipWithL :: forall f g a b a' b'.
+        Category f
+     => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y'))
+     -> ListTr f a  b
+     -> ListTr f a' b'
+     -> ListTr f (g a a') (g b b')
+zipWithL fn queueA queueB = case (queueA, queueB) of
+    (NilTr, NilTr) -> NilTr
+    (NilTr, ConsTr trB' queueB') -> ConsTr (id   `fn` trB') (zipWithL fn NilTr    queueB')
+    (ConsTr trA' queueA', NilTr) -> ConsTr (trA' `fn` id)   (zipWithL fn queueA' NilTr)
+    (ConsTr trA' queueA', ConsTr trB' queueB')
+                                 -> ConsTr (trA' `fn` trB') (zipWithL fn queueA' queueB')
+
+#if __GLASGOW_HASKELL__ >= 806
+instance (forall (x :: k) (y :: k). Show (f x y)) => Show (ListTr f a b) where
+    show NilTr         = "NilTr"
+    show (ConsTr x xs) = "ConsTr " ++ show x ++ " " ++ show xs
+#else
+instance Show (ListTr f a b) where
+    show NilTr         = "NilTr"
+    show (ConsTr _ xs) = "ConsTr _ " ++ show xs
+#endif
+
 instance Category (ListTr f) where
-  id = NilTr
-  NilTr    . ys = ys
-  (ConsTr x xs) . ys = ConsTr x (xs . ys)
+  id  = NilTr
+  (.) = composeL
 
+type instance AlgebraType0 ListTr f = ()
+type instance AlgebraType  ListTr c = Category c
+
+instance FreeAlgebra2 ListTr where
+  liftFree2    = liftL
+  {-# INLINE liftFree2 #-}
+  foldNatFree2 = foldNatL
+  {-# INLINE foldNatFree2 #-}
+
+  codom2  = Proof
+  forget2 = Proof
+
+instance Semigroup (ListTr f o o) where
+  f <> g = g . f
+
+instance Monoid (ListTr f o o) where
+  mempty = NilTr
+#if __GLASGOW_HASKELL__ < 804
+  mappend = (<>)
+#endif
+
 instance Arrow f => Arrow (ListTr f) where
   arr ab                          = arr ab `ConsTr` NilTr
 
@@ -104,99 +260,163 @@
   NilTr +++ (ConsTr fxb cax) = (arr id +++ fxb) `ConsTr` (NilTr +++ cax)
   NilTr +++ NilTr            = NilTr
 
-instance Semigroup (ListTr f o o) where
-  f <> g = g . f
 
-instance Monoid (ListTr f o o) where
-  mempty = NilTr
-#if __GLASGOW_HASKELL__ < 804
-  mappend = (<>)
-#endif
-
-type instance AlgebraType0 ListTr f = ()
-type instance AlgebraType  ListTr c = Category c
-
-instance FreeAlgebra2 ListTr where
-  liftFree2 = \fab -> ConsTr fab NilTr
-  {-# INLINE liftFree2 #-}
-
-  foldNatFree2 _   NilTr     = id
-  foldNatFree2 fun (ConsTr bc ab) = fun bc . foldNatFree2 fun ab
-  {-# INLINE foldNatFree2 #-}
-
-  codom2  = proof
-  forget2 = proof
+--
+-- Type aligned real time 'Queue'
+--
 
 
 -- | Type alligned real time queues; Based on `Purely Functinal Data Structures`
--- C.Okasaki.
+-- C.Okasaki.  This the most reliably behaved implementation of free categories
+-- in this package.
 --
--- Upper bounds of `cons`, `snoc`, `uncons` are @O\(1\)@ (worst case).
+-- Upper bounds of `consQ`, `snocQ`, `unconsQ` are @O\(1\)@ (worst case).
 --
--- Invariant: sum of lengths of two last least is equal the length of the first
--- one.
+-- Internal invariant: sum of lengths of two last least is equal the length of
+-- the first one.
 --
 data Queue (f :: k -> k -> *) (a :: k) (b :: k) where
     Queue :: forall f a c b x.
-             !(ListTr f b c)
+               ListTr f      b c
           -> !(ListTr (Op f) b a)
-          -> !(ListTr f b x)
+          ->   ListTr f      b x
           -> Queue f a c
 
-emptyQ :: Queue (f :: k -> k -> *) a a
-emptyQ = Queue NilTr NilTr NilTr
+pattern ConsQ :: f b c -> Queue f a b -> Queue f a c
+pattern ConsQ a as <- (unconsQ -> a :< as) where
+    ConsQ = consQ
 
-cons :: forall (f :: k -> k -> *) a b c.
-        f b c
-     -> Queue f a b
-     -> Queue f a c
-cons fbc (Queue f r s) = Queue (ConsTr fbc f) r (ConsTr undefined s)
+pattern NilQ :: () => a ~ b => Queue f a b
+pattern NilQ <- (unconsQ -> EmptyL) where
+    NilQ = nilQ
 
+#if __GLASGOW_HASKELL__ > 802
+{-# complete NilQ, ConsQ #-}
+#endif
+
+composeQ :: forall (f :: k -> k -> *) x y z.
+            Queue f y z
+         -> Queue f x y
+         -> Queue f x z
+composeQ (ConsQ f q1) q2 = ConsQ f (q1 . q2)
+composeQ NilQ         q2 = q2
+{-# INLINE [1] composeQ #-}
+
+nilQ :: Queue (f :: k -> k -> *) a a
+nilQ = Queue NilTr NilTr NilTr
+{-# INLINE [1] nilQ #-}
+
+consQ :: forall (f :: k -> k -> *) a b c.
+         f b c
+      -> Queue f a b
+      -> Queue f a c
+consQ bc (Queue f r s) = Queue (ConsTr bc f) r (ConsTr undefined s)
+{-# INLINE [1] consQ #-}
+
 data ViewL f a b where
     EmptyL :: ViewL f a a
     (:<)   :: f b c -> Queue f a b -> ViewL f a c
 
 -- | 'uncons' a 'Queue', complexity: @O\(1\)@
 --
-uncons :: Queue f a b
-       -> ViewL f a b
-uncons (Queue NilTr NilTr _)                = EmptyL
-uncons (Queue (ConsTr tr f) r (ConsTr _ s)) = tr :< exec f r s
-uncons _                                    = error "Queue.uncons: invariant violation"
+unconsQ :: Queue f a b
+        -> ViewL f a b
+unconsQ (Queue NilTr NilTr _)     = EmptyL
+unconsQ (Queue (ConsTr tr f) r s) = tr :< exec f r s
+unconsQ _                         = error "Queue.uncons: invariant violation"
+{-# INLINE unconsQ #-}
 
-snoc :: forall (f :: k -> k -> *) a b c.
-        Queue f b c
-     -> f a b
-     -> Queue f a c
-snoc (Queue f r s) g = exec f (ConsTr (Op g) r) s
+snocQ :: forall (f :: k -> k -> *) a b c.
+         Queue f b c
+      -> f a b
+      -> Queue f a c
+snocQ (Queue f r s) g = exec f (ConsTr (Op g) r) s
+{-# INLINE snocQ #-}
 
-pattern ConsQ :: f b c -> Queue f a b -> Queue f a c
-pattern ConsQ a as <- (uncons -> a :< as) where
-    ConsQ = cons
+-- | 'foldr' of a 'Queue'
+--
+foldrQ :: forall (f :: k -> k -> *) c a b d.
+          (forall x y z. f y z -> c x y -> c x z)
+       -> c a b
+       -> Queue f b d
+       -> c a d
+foldrQ _nat ab NilQ          = ab
+foldrQ  nat ab (ConsQ xd bx) = nat xd (foldrQ nat ab bx)
+{-# INLINE [1] foldrQ #-}
 
-pattern NilQ :: () => a ~ b => Queue f a b
-pattern NilQ <- (uncons -> EmptyL) where
-    NilQ = emptyQ
+{-# RULES
 
-#if __GLASGOW_HASKELL__ > 802
-{-# complete NilQ, ConsQ #-}
-#endif
+"foldrQ/consQ/nilQ"
+  foldrQ consQ nilQ = id
 
--- | Efficient fold of a queue into a category.
+"foldrQ/single"
+  forall (nat :: forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
+         (t :: f (v :: k) (w :: k))
+         (nil :: c (u :: k) (v :: k)).
+  foldrQ nat nil (consQ t nilQ) = nat t nil
+
+"foldrQ/nilQ"
+  forall (nat :: forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
+         (nil :: c (u :: k) (v :: k)).
+  foldrQ nat nil nilQ = nil
+
+"foldrQ/consQ"
+  forall (f :: Queue f (x :: k) (y :: k))
+         (g :: Queue f (y :: k) (z :: k)).
+  foldrQ consQ f g = g . f
+
+#-}
+
+liftQ :: forall (f :: k -> k -> *) a b.
+         f a b -> Queue f a b
+liftQ = \fab -> ConsQ fab NilQ
+{-# INLINE [1] liftQ #-}
+
+-- | Efficient fold of a queue into a category, analogous to 'foldM'.
 --
 -- /complexity/ @O\(n\)@
 --
-foldQ :: forall (f :: k -> k -> *) c a b.
-         Category c
-      => (forall x y. f x y -> c x y)
-      -> Queue f a b
-      -> c a b
-foldQ nat queue = case queue of
-    NilQ            -> id
-    ConsQ tr queue' -> nat tr . foldQ nat queue'
+foldNatQ :: forall (f :: k -> k -> *) c a b.
+            Category c
+         => (forall x y. f x y -> c x y)
+         -> Queue f a b
+         -> c a b
+foldNatQ nat = foldrQ (\f c -> nat f . c) id
+{-# INLINE [1] foldNatQ #-}
 
+{-# RULES
+
+"foldNatQ/consQ" forall (f :: f (v :: k) (w :: k))
+                        (q :: Queue f (u :: k) (v :: k))
+                        (nat :: forall (x :: k) (y :: k). f x y -> c x y).
+                 foldNatQ nat (consQ f q) = nat f . foldNatQ nat q
+
+"foldNatQ/nilQ"  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y).
+                 foldNatQ nat nilQ = id
+
+
+"foldNatC/liftQ"
+  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
+         (g :: f v w)
+         (h :: Queue f u v).
+  foldNatQ nat (liftQ g `composeQ` h) = nat g . foldNatQ nat h
+
+#-}
+
+-- | 'foldl' of a 'Queue'
+--
+-- TODO: make it strict, like 'foldl''.
+--
+foldlQ :: forall (f :: k -> k -> *) c a b d.
+          (forall x y z. c y z -> f x y -> c x z)
+       -> c b d
+       -> Queue f a b
+       -> c a d
+foldlQ _nat bd NilQ          = bd
+foldlQ  nat bd (ConsQ xb ax) = foldlQ nat (nat bd xb) ax
+
 zipWithQ :: forall f g a b a' b'.
-        Arrow f
+        Category f
      => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y'))
      -> Queue f a  b
      -> Queue f a' b'
@@ -209,12 +429,112 @@
                                -> ConsQ (trA' `fn` trB') (zipWithQ fn queueA' queueB')
 
 
+-- | 'Queue' is an endo-functor on the category of graphs (or category of
+-- categories), thus one can hoist the transitions using a natural
+-- transformation.  This in analogy to @'map' :: (a -> b) -> [a] -> [b]@.
+--
+hoistQ :: forall (f :: k -> k -> *)
+                 (g :: k -> k -> *)
+                 a  b.
+          (forall x y. f x y -> g x y)
+       -> Queue f a b
+       -> Queue g a b
+hoistQ nat q = case q of
+    NilQ        -> NilQ
+    ConsQ tr q' -> ConsQ (nat tr) (hoistQ nat q')
+{-# INLINE [1] hoistQ #-}
 
+{-# RULES
+
+"hoistQ/foldNatQ"
+  forall (nat1 :: forall (x :: k) (y :: k). f x y -> g x y)
+         (nat  :: forall (x :: k) (y :: k). g x y -> h x y)
+         (q    :: Queue f x y).
+  foldNatQ nat (hoistQ nat1 q) = foldNatQ (nat . nat1) q
+
+"hoistQ/hoistQ"
+  forall (nat1 :: forall (x :: k) (y :: k). f x y -> g x y)
+         (nat  :: forall (x :: k) (y :: k). g x y -> h x y)
+         (q    :: Queue f x y).
+    hoistQ nat (hoistQ nat1 q) = hoistQ (nat . nat1) q
+
+#-}
+
+#if __GLASGOW_HASKELL__ >= 806
+instance (forall (x :: k) (y :: k). Show (f x y))
+      => Show (Queue f a b) where
+    show (Queue f r s) =
+        "Queue ("
+        ++ show f
+        ++ ") ("
+        ++ show r
+        ++ ") "
+        ++ show (lengthListTr s)
+#else
+instance Show (Queue f r s) where
+    show (Queue f r s) =
+        "Queue "
+      ++ show (lengthListTr f)
+      ++ " "
+      ++ show (lengthListTr r)
+      ++ " "
+      ++ show (lengthListTr s)
+#endif
+
+instance Category (Queue f) where
+    id  = NilQ
+    (.) = composeQ
+
+type instance AlgebraType0 Queue f = ()
+type instance AlgebraType  Queue c = Category c
+
+instance FreeAlgebra2 Queue where
+  liftFree2    = liftQ
+  {-# INLINE liftFree2 #-}
+  foldNatFree2 = foldNatQ
+  {-# INLINE foldNatFree2 #-}
+
+  codom2  = Proof
+  forget2 = Proof
+
+instance Semigroup (Queue f o o) where
+  f <> g = g `composeQ` f
+
+instance Monoid (Queue f o o) where
+  mempty = NilQ
+#if __GLASGOW_HASKELL__ < 804
+  mappend = (<>)
+#endif
+
+instance Arrow f => Arrow (Queue f) where
+  arr ab = arr ab `ConsQ` NilQ
+
+  (ConsQ fxb cax) *** (ConsQ fyb cay)
+                           = (fxb *** fyb)    `ConsQ` (cax *** cay)
+  (ConsQ fxb cax) *** NilQ = (fxb *** arr id) `ConsQ` (cax *** NilQ)
+  NilQ *** (ConsQ fxb cax) = (arr id *** fxb) `ConsQ` (NilQ *** cax)
+  NilQ *** NilQ            = NilQ
+
+instance ArrowZero f => ArrowZero (Queue f) where
+  zeroArrow = zeroArrow `ConsQ` NilQ
+
+instance ArrowChoice f => ArrowChoice (Queue f) where
+  (ConsQ fxb cax) +++ (ConsQ fyb cay)
+                           = (fxb +++ fyb)    `ConsQ` (cax +++ cay)
+  (ConsQ fxb cax) +++ NilQ = (fxb +++ arr id) `ConsQ` (cax +++ NilQ)
+  NilQ +++ (ConsQ fxb cax) = (arr id +++ fxb) `ConsQ` (NilQ +++ cax)
+  NilQ +++ NilQ            = NilQ
+
+--
+-- Internal API
+--
+
 exec :: ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
 exec xs ys (ConsTr _ t) = Queue xs ys t
 exec xs ys NilTr        = Queue xs' NilTr xs'
   where
     xs' = rotate xs ys NilTr
+{-# INLINABLE exec #-}
 
 rotate :: ListTr f c d -> ListTr (Op f) c b -> ListTr f a b -> ListTr f a d
 rotate NilTr         (ConsTr (Op f) NilTr) a = ConsTr f a
diff --git a/src/Control/Category/FreeEff.hs b/src/Control/Category/FreeEff.hs
deleted file mode 100644
--- a/src/Control/Category/FreeEff.hs
+++ /dev/null
@@ -1,89 +0,0 @@
-{-# LANGUAGE GADTs                  #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE PolyKinds              #-}
-{-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE TypeFamilies           #-}
-
-{-# OPTIONS_HADDOCK show-extensions #-}
-
-module Control.Category.FreeEff
-  ( EffCategory (..)
-  , FreeEffCat (..)
-  , liftCat
-  , foldNatLift
-  , liftKleisli
-  ) where
-
-import Prelude hiding (id, (.))
-
-import Control.Arrow (Kleisli (..))
-import Control.Category (Category (..))
-import Data.Functor.Identity (Identity (..))
-
-import Control.Category.Free (Cat)
-import Control.Algebra.Free2 (FreeAlgebra2 (..))
-import Data.Algebra.Free (AlgebraType, AlgebraType0, proof)
-
-
--- | Categories which can lift monadic actions, i.e. effectful categories.
---
-class Category c => EffCategory c m | c -> m where
-  lift :: m (c a b) -> c a b
-
-instance Monad m => EffCategory (Kleisli m) m where
-  lift m = Kleisli (\a -> m >>= \(Kleisli f) -> f a)
-
-instance EffCategory (->) Identity where
-  lift = runIdentity
-
--- | Category transformer, which adds @'EffCategory'@ instance to the
--- underlying base category.
---
-data FreeEffCat :: (* -> *) -> (k -> k -> *) -> k -> k -> * where
-  Base :: c a b -> FreeEffCat m c a b
-  Lift :: m (FreeEffCat m c a b) -> FreeEffCat m c a b
-
-instance (Functor m, Category c) => Category (FreeEffCat m c) where
-  id = Base id
-  Base f  . Base g  = Base $ f . g
-  f       . Lift mg = Lift $ (f .) <$> mg
-  Lift mf . g       = Lift $ (. g) <$> mf
-
-instance (Functor m, Category c) => EffCategory (FreeEffCat m c) m where
-  lift = Lift
-
-type instance AlgebraType0 (FreeEffCat m) c = (Monad m, Category c)
-type instance AlgebraType  (FreeEffCat m) c  = EffCategory c m
-instance Monad m => FreeAlgebra2 (FreeEffCat m) where
-  liftFree2    = Base
-  foldNatFree2 nat (Base cab)  = nat cab
-  foldNatFree2 nat (Lift mcab) = lift $ foldNatFree2 nat <$> mcab
-
-  codom2  = proof
-  forget2 = proof
-
--- | Wrap a transition into a free category @'Cat'@ and then in
--- @'FreeEffCat'@
---
--- prop> liftCat tr = Base (tr :.: Id)
---
-liftCat :: Monad m => tr a b -> FreeEffCat m (Cat tr) a b
-liftCat = liftFree2 . liftFree2
-
--- | Fold @'FreeLifing'@ category based on a free category @'Cat' tr@ using
--- a functor @tr x y -> c x y@.
---
-foldNatLift
-  :: (Monad m, EffCategory c m)
-  => (forall x y. tr x y -> c x y)
-  -> FreeEffCat m (Cat tr) a b
-  -> c a b
-foldNatLift nat = foldNatFree2 (foldNatFree2 nat)
-
--- |  Functor from @'->'@ category to @'Kleisli' m@.  If @m@ is @Identity@ then
--- it will respect @'lift'@ i.e. @liftKleisli (lift ar) = lift (liftKleisli <$>
--- ar).
---
-liftKleisli :: Applicative m => (a -> b) -> Kleisli m a b
-liftKleisli f = Kleisli (pure . f)
diff --git a/src/Control/Category/FreeEffect.hs b/src/Control/Category/FreeEffect.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/FreeEffect.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE TypeFamilies           #-}
+
+{-# OPTIONS_HADDOCK show-extensions #-}
+
+module Control.Category.FreeEffect
+  ( EffectCategory (..)
+  , EffCat (..)
+  , liftEffect
+  , foldNatEffCat
+  , liftKleisli
+  ) where
+
+import Prelude hiding (id, (.))
+
+import Control.Arrow (Kleisli (..))
+import Control.Category (Category (..))
+import Data.Functor.Identity (Identity (..))
+
+import Control.Algebra.Free2 (FreeAlgebra2 (..))
+import Data.Algebra.Free (AlgebraType, AlgebraType0, Proof (..))
+
+
+-- | Categories which can lift monadic actions, i.e. effectful categories.
+--
+class Category c => EffectCategory c m | c -> m where
+  effect :: m (c a b) -> c a b
+
+instance Monad m => EffectCategory (Kleisli m) m where
+  effect m = Kleisli (\a -> m >>= \(Kleisli f) -> f a)
+
+instance EffectCategory (->) Identity where
+  effect = runIdentity
+
+-- | Category transformer, which adds @'EffectCategory'@ instance to the
+-- underlying base category.
+--
+data EffCat :: (* -> *) -> (k -> k -> *) -> k -> k -> * where
+  Base   :: c a b -> EffCat m c a b
+  Effect :: m (EffCat m c a b) -> EffCat m c a b
+
+instance (Functor m, Category c) => Category (EffCat m c) where
+  id = Base id
+  Base f    . Base g    = Base   $ f . g
+  f         . Effect mg = Effect $ (f .) <$> mg
+  Effect mf . g         = Effect $ (. g) <$> mf
+
+instance (Functor m, Category c) => EffectCategory (EffCat m c) m where
+  effect = Effect
+
+type instance AlgebraType0 (EffCat m) c = (Monad m, Category c)
+type instance AlgebraType  (EffCat m) c  = EffectCategory c m
+instance Monad m => FreeAlgebra2 (EffCat m) where
+  liftFree2    = Base
+  foldNatFree2 nat (Base cab)    = nat cab
+  foldNatFree2 nat (Effect mcab) = effect $ foldNatFree2 nat <$> mcab
+
+  codom2  = Proof
+  forget2 = Proof
+
+-- | Wrap a transition into @'EffCat' cat@ for any free category 'cat' (e.g.
+-- 'Cat').
+--
+liftEffect :: ( Monad m
+              , FreeAlgebra2 cat
+              , AlgebraType0 cat tr
+              , Category    (cat tr)
+              )
+           => tr a b -> EffCat m (cat tr) a b
+liftEffect = liftFree2 . liftFree2
+
+-- | Fold @'FreeLifing'@ category based on a free category @'cat' tr@ (e.g.
+-- @'Cat' tr@) using a functor @tr x y -> c x y@.
+--
+foldNatEffCat
+  :: ( Monad m
+     , FreeAlgebra2 cat
+     , AlgebraType  cat c
+     , AlgebraType0 cat tr
+     , Category    (cat tr)
+     , EffectCategory c m
+     )
+  => (forall x y. tr x y -> c x y)
+  -> EffCat m (cat tr) a b
+  -> c a b
+foldNatEffCat nat = foldNatFree2 (foldNatFree2 nat)
+
+-- |  Functor from @(->)@ category to @'Kleisli' m@.  If @m@ is 'Identity' then
+-- it will respect 'effect' i.e.
+-- @'liftKleisli' ('effect' ar) = 'effect' ('liftKleisli' \<$\> ar)@.
+--
+liftKleisli :: Applicative m => (a -> b) -> Kleisli m a b
+liftKleisli f = Kleisli (pure . f)
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,17 @@
+module Main (main) where
+
+import           Test.Tasty
+
+import qualified Test.Queue
+import qualified Test.Cat
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests =
+  testGroup "free-categories"
+    -- data structures
+  [ Test.Queue.tests
+  , Test.Cat.tests
+  ]
diff --git a/test/Test/Cat.hs b/test/Test/Cat.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Cat.hs
@@ -0,0 +1,410 @@
+{-# LANGUAGE CPP                   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TupleSections         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Cat (tests) where
+
+import           Prelude hiding ((.), id)
+import           Control.Category
+import           Data.Function (on)
+#if __GLASGOW_HASKELL__ < 804
+import           Data.Monoid (Monoid (..))
+import           Data.Semigroup (Semigroup (..))
+#endif
+import           Text.Show.Functions ()
+import           Numeric.Natural (Natural)
+
+import           Control.Algebra.Free2
+import           Control.Category.Free
+
+import           Test.QuickCheck
+import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.QuickCheck (testProperty)
+
+tests :: TestTree
+tests =
+  testGroup "Control.Category.Free"
+  [ testProperty "Queue" prop_Queue
+  , testProperty "C"     prop_C
+  , testGroup "Category laws"
+    [ testProperty "ListTr id"            prop_id_ListTr
+    , testProperty "ListTr associativity" prop_associativity_ListTr
+    , testProperty "Queue id"            prop_id_Queue
+    , testProperty "Queue associativity" prop_associativity_Queue
+    , testProperty "C id"                 prop_id_C
+    , testProperty "C associativity"      prop_associativity_C
+    ]
+  , testGroup "foldFree2 and foldMap"
+    [ testProperty "foldFree ListTr" prop_foldListTr
+    , testProperty "foldFree Queue"  prop_foldQueue
+    , testProperty "foldFree C"      prop_foldC
+    ]
+  ]
+
+
+data Tr a b where
+    -- Num transition
+    NumTr       :: Num a => (a -> a) -> Tr a a
+    FromInteger :: Num b => Tr Integer b
+
+    -- Integral transition
+    ToInteger  :: Integral a => Tr a Integer
+
+
+interpretTr :: Tr a b -> a -> b
+interpretTr (NumTr f)   = f
+interpretTr FromInteger = fromInteger
+interpretTr ToInteger   = toInteger
+
+
+instance (Show a, Show b) => Show (Tr a b) where
+    show (NumTr f)   = "NumTr " ++ show f
+    show FromInteger = "FromInteger"
+    show ToInteger   = "ToInteger"
+
+
+data SomeNumTr f a where
+    SomeNumTr :: Num a
+              => f Tr a a
+              -> SomeNumTr f a
+
+instance Show (f Tr a a) => Show (SomeNumTr f a) where
+      show (SomeNumTr f) = "SomeNumTr " ++ show f
+
+
+data SomeIntegralTr f a where
+    SomeIntegralTr :: Integral a
+                   => f Tr a a
+                   -> SomeIntegralTr f a
+
+instance Show (f Tr a a) => Show (SomeIntegralTr f a) where
+      show (SomeIntegralTr f) = "SomeIntegralTr " ++ show f
+
+
+-- A 'fromIntegral' transition in any free category @f@.
+fromIntegralTr :: ( Integral a
+                  , Num b
+                  , Category     (f Tr)
+                  , AlgebraType0 f Tr
+                  , FreeAlgebra2 f
+                  ) => f Tr a b
+fromIntegralTr = liftFree2 FromInteger . liftFree2 ToInteger
+
+
+data Sing a where
+    SInt     :: Sing Int
+    SInteger :: Sing Integer
+    SNatural :: Sing Natural
+
+instance Show (Sing a) where
+    show SInt     = "SInt"
+    show SInteger = "SInteger"
+    show SNatural = "SNatural"
+
+data AnySing where
+    AnySing :: Eq a => Sing a -> AnySing
+
+instance Eq AnySing where
+    AnySing SInt     == AnySing SInt     = True
+    AnySing SInteger == AnySing SInteger = True
+    AnySing SNatural == AnySing SNatural = True
+    _                == _                = False
+
+instance Show AnySing where
+    show (AnySing sing) = show sing
+
+instance Arbitrary AnySing where
+    arbitrary = oneof
+      [ pure $ AnySing SInt
+      , pure $ AnySing SInteger
+      , pure $ AnySing SNatural
+      ]
+
+
+instance Arbitrary Natural where
+    arbitrary =
+      fromIntegral . getPositive <$> (arbitrary :: Gen (Positive Integer))
+
+instance CoArbitrary Natural where
+    coarbitrary a = variant (fromIntegral a :: Int)
+
+data AnyListTr b where
+    AnyListTr :: Eq c => ListTr Tr b c -> Sing c -> AnyListTr b
+
+
+genNextTr :: Sing b
+          -> Gen (AnyListTr b)
+genNextTr b = do
+    AnySing c <- arbitrary
+    case (b, c) of
+      (SInt, SInt) ->
+        (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
+      (SInteger, SInteger) ->
+        (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
+      (SNatural, SNatural) ->
+        (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
+
+      (SInt, SInteger) ->
+        pure $ AnyListTr fromIntegralTr c
+      (SInt, SNatural) ->
+        pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c
+      (SInteger, SInt) ->
+        pure $ AnyListTr fromIntegralTr c
+      (SNatural, SInt) ->
+        pure $ AnyListTr fromIntegralTr c
+      (SNatural, SInteger) ->
+        pure $ AnyListTr fromIntegralTr c
+      (SInteger, SNatural) ->
+        pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c
+
+
+data ArbListTr where
+    ArbListTr :: Eq b => ListTr Tr a b -> Sing a -> Sing b -> ArbListTr
+
+#if __GLASGOW_HASKELL__ >= 806
+instance (forall x y. Show (Tr x y)) => Show ArbListTr where
+    show (ArbListTr listTr a b) =
+         "ArbListTr "
+      ++ show a
+      ++ " -> "
+      ++ show b
+      ++ " "
+      ++ show listTr
+#else
+instance Show ArbListTr where
+    show (ArbListTr _listTr a b) =
+         "ArbListTr "
+      ++ show a
+      ++ " -> "
+      ++ show b
+#endif
+
+instance Arbitrary ArbListTr where
+    arbitrary = sized $ \n -> do
+        k <- choose (0, n)
+        AnySing a <- arbitrary
+        go k a (AnyListTr NilTr a)
+      where
+        go 0 a (AnyListTr ab b) = pure $ ArbListTr ab a b
+        go n a (AnyListTr ab b) = do
+          AnyListTr bc c <- genNextTr b
+          -- (.) can be used as (++) for ListTr
+          go (n - 1) a $ AnyListTr (bc . ab) c
+
+
+--
+-- test 'Cat' and 'C' treating 'ListTr' as a model to compare to.
+--
+prop_Queue, prop_C
+    :: Blind ArbListTr -> Bool
+
+
+prop_Queue (Blind (ArbListTr listTr SInt _)) =
+      foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
+    ==
+      foldNatFree2 interpretTr listTr 0
+prop_Queue (Blind (ArbListTr listTr SInteger _)) =
+      foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
+    ==
+      foldNatFree2 interpretTr listTr 0
+prop_Queue (Blind (ArbListTr listTr SNatural _)) =
+      foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
+    ==
+      foldNatFree2 interpretTr listTr 0
+
+
+prop_C (Blind (ArbListTr listTr SInt _)) =
+      foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
+    ==
+      foldNatFree2 interpretTr listTr 0
+prop_C (Blind (ArbListTr listTr SInteger _)) =
+      foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
+    ==
+      foldNatFree2 interpretTr listTr 0
+prop_C (Blind (ArbListTr listTr SNatural _)) =
+      foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
+    ==
+      foldNatFree2 interpretTr listTr 0
+
+--
+-- Test Category Laws
+-- @
+--  f . id == f == id . f
+--  f . g . h == (f . g) . h
+-- @
+--
+
+prop_id :: Category c
+        => (c a b -> c a b -> Bool)
+        -> c a b
+        -> Bool
+prop_id eqCat f = eqCat (f . id) f && eqCat (id . f) f
+
+prop_associativity :: Category c
+                   => (c x w -> c x w -> Bool)
+                   -> c z w -> c y z -> c x y
+                   -> Bool
+prop_associativity eqCat f g h =
+    (f . g . h) `eqCat` ((f . g) . h)
+
+
+-- | Integers form commutative monoid, and thus a category (a groupoid to be
+-- precise) with a single object.
+--
+data IntCat (a :: ()) (b :: ()) where
+     IntCat :: Int -> IntCat a a
+
+instance Show (IntCat a b) where
+    show (IntCat i) = "IntCat " ++ show i
+
+instance Eq (IntCat a b) where
+    IntCat i  == IntCat j = i == j
+
+instance Category IntCat where
+    id = IntCat 0
+    IntCat a . IntCat b = IntCat (a + b)
+
+instance Semigroup (IntCat '() '()) where
+    IntCat a <> IntCat b = IntCat (a + b)
+
+instance Monoid (IntCat '() '()) where
+    mempty = IntCat 0
+#if __GLASGOW_HASKELL__ < 804
+    mappend = (<>)
+#endif
+
+instance Arbitrary (IntCat '() '()) where
+    arbitrary = IntCat <$> arbitrary
+
+fromList :: forall (a :: k) m f.
+            ( FreeAlgebra2 m
+            , AlgebraType0 m f
+            , Category    (m f)
+            ) => [f a a] -> m f a a
+fromList [] = id
+fromList (f : fs) = liftFree2 f . fromList fs
+
+toList :: ( FreeAlgebra2 m
+          , AlgebraType0 m IntCat
+          , AlgebraType  m (ListTr IntCat)
+          )
+       => m IntCat '() '()
+       -> [IntCat '() '()]
+toList c = go (hoistFreeH2 c)
+  where
+    go :: ListTr IntCat '() '() -> [IntCat '() '()]
+    go NilTr = []
+    go (ConsTr tr@IntCat{} xs) = tr : go xs
+
+--
+-- 'C' category laws
+--
+
+newtype ArbIntC = ArbIntC (C IntCat '() '())
+
+instance Show ArbIntC where
+    show (ArbIntC c) = show c
+
+instance Arbitrary ArbIntC where
+    arbitrary = ArbIntC . fromList <$> arbitrary
+    shrink (ArbIntC c) =
+      map (ArbIntC . fromList)
+          $ shrinkList (const [])
+          $ toList c
+
+prop_id_C :: ArbIntC -> Bool
+prop_id_C (ArbIntC f) =
+    prop_id (on (==) toList) f
+
+prop_associativity_C
+    :: ArbIntC -> ArbIntC -> ArbIntC
+    -> Bool
+prop_associativity_C (ArbIntC f0)
+                     (ArbIntC f1)
+                     (ArbIntC f2) =
+      prop_associativity (on (==) toList) f0 f1 f2
+
+--
+-- 'Queue' category laws
+--
+
+newtype ArbIntQueue = ArbIntQueue (Queue IntCat '() '())
+
+instance Show ArbIntQueue where
+    show (ArbIntQueue f) = show (toList f)
+
+instance Arbitrary ArbIntQueue where
+    arbitrary = ArbIntQueue . fromList <$> arbitrary
+    shrink (ArbIntQueue c) =
+      map (ArbIntQueue . fromList)
+          $ shrinkList (const [])
+          $ toList c
+
+prop_id_Queue :: ArbIntQueue -> Bool
+prop_id_Queue (ArbIntQueue f) =
+    prop_id (on (==) toList) f
+
+prop_associativity_Queue
+    :: ArbIntQueue -> ArbIntQueue -> ArbIntQueue
+    -> Bool
+prop_associativity_Queue (ArbIntQueue f0)
+                         (ArbIntQueue f1)
+                         (ArbIntQueue f2) =
+      prop_associativity (on (==) toList) f0 f1 f2
+
+--
+-- 'ListTr' category laws
+--
+
+newtype ArbIntListTr = ArbIntListTr (ListTr IntCat '() '())
+
+instance Show ArbIntListTr where
+    show (ArbIntListTr f) = show (toList f)
+
+instance Arbitrary ArbIntListTr where
+    arbitrary = ArbIntListTr . fromList <$> arbitrary
+    shrink (ArbIntListTr c) =
+      map (ArbIntListTr . fromList)
+          $ shrinkList (const [])
+          $ toList c
+
+prop_id_ListTr :: ArbIntListTr -> Bool
+prop_id_ListTr (ArbIntListTr f) =
+    prop_id (on (==) toList) f
+
+prop_associativity_ListTr
+    :: ArbIntListTr -> ArbIntListTr -> ArbIntListTr
+    -> Bool
+prop_associativity_ListTr (ArbIntListTr f0)
+                          (ArbIntListTr f1)
+                          (ArbIntListTr f2) =
+      prop_associativity (on (==) toList) f0 f1 f2
+
+
+--
+-- Compatibility between 'foldFree2' and 'foldMap' for 'IntCat'
+--
+
+prop_foldListTr :: ArbIntListTr -> Bool
+prop_foldListTr (ArbIntListTr f)
+    = foldFree2 f == foldMap id (toList f)
+
+prop_foldQueue :: ArbIntQueue -> Bool
+prop_foldQueue (ArbIntQueue f)
+    = foldFree2 f == foldMap id (toList f)
+
+prop_foldC :: (Blind ArbIntC) -> Bool
+prop_foldC (Blind (ArbIntC f))
+    = foldFree2 f == foldMap id (toList f)
diff --git a/test/Test/Queue.hs b/test/Test/Queue.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Queue.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+
+module Test.Queue (tests) where
+
+import           Prelude hiding ((.), id)
+import           Text.Show.Functions ()
+
+import           Control.Category.Free.Internal
+
+import           Test.QuickCheck
+import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.QuickCheck (testProperty)
+
+tests :: TestTree
+tests =
+  testGroup "Queue"
+  [ testProperty "consQ"   prop_consQ
+  , testProperty "unconsQ" prop_unconsQ
+  , testProperty "snocQ"   prop_snocQ
+  , testProperty "foldrQ"  (prop_foldr @Int)
+  , testProperty "foldrQ"  (prop_foldl @Int)
+  ]
+
+data K = K
+
+data Tr (a :: K) (b :: K) where
+    A :: Int -> Tr 'K 'K
+
+instance Eq (Tr 'K 'K) where
+    A i == A j = i == j
+
+instance Show (Tr a b) where
+    show (A i) = "A " ++ show i
+
+instance Arbitrary (Tr 'K 'K) where
+    arbitrary = A <$> arbitrary
+
+
+toList :: Queue Tr 'K 'K -> [Tr 'K 'K]
+toList q = case q of
+    ConsQ a@A{} as -> a : toList as
+    _              -> []
+
+
+fromList :: [Tr 'K 'K] -> Queue Tr 'K 'K
+fromList []              = NilQ
+fromList (a : as) = ConsQ a (fromList as)
+
+
+instance Arbitrary (Queue Tr 'K 'K) where
+    arbitrary = fromList <$> arbitrary
+    shrink q  = map fromList $ shrinkList (const []) (toList q)
+
+
+prop_unconsQ :: Queue Tr 'K 'K -> Bool
+prop_unconsQ q = case (q, toList q) of
+    (ConsQ a@A{} _, a' : _) -> a == a'
+    (NilQ, []) -> True
+    _          -> False
+
+
+prop_consQ :: Tr 'K 'K -> Queue Tr 'K 'K -> Bool
+prop_consQ a@A{} q = case consQ a q of
+    ConsQ a'@A{} _ -> a' == a'
+    _              -> False
+
+
+prop_snocQ :: Tr 'K 'K -> Queue Tr 'K 'K -> Bool
+prop_snocQ a@A{} q = last (toList (q `snocQ` a)) == a
+
+
+data TrA a (x :: K) (y :: K) where
+    TrA :: a -> TrA a 'K 'K
+
+instance Show a => Show (TrA a 'K 'K) where
+    show (TrA a) = "TrA " ++ show a
+
+instance Eq a => Eq (TrA a k k) where
+    TrA a == TrA b = a == b
+
+instance Arbitrary a => Arbitrary (TrA a 'K 'K) where
+    arbitrary = TrA <$> arbitrary
+    shrink (TrA a) = map TrA (shrink a)
+
+
+prop_foldr :: forall a.
+              Eq a
+           => (Int -> a -> a)
+           -> TrA a 'K 'K
+           -> Queue Tr 'K 'K
+           -> Bool
+prop_foldr f a q = foldrQ g a q == foldr g a (toList q)
+  where
+    g :: Tr y z-> TrA a x y -> TrA a x z
+    g (A i) (TrA j) = TrA (f i j)
+
+
+prop_foldl :: forall a.
+              Eq a
+           => (a -> Int -> a)
+           -> TrA a 'K 'K
+           -> Queue Tr 'K 'K
+           -> Bool
+prop_foldl f a q = foldlQ g a q == foldl g a (toList q)
+  where
+    g :: TrA a y z-> Tr x y -> TrA a x z
+    g (TrA j) (A i) = TrA (f j i)