diff --git a/Control/Invertible/BiArrow.hs b/Control/Invertible/BiArrow.hs
--- a/Control/Invertible/BiArrow.hs
+++ b/Control/Invertible/BiArrow.hs
@@ -14,6 +14,7 @@
   , (>>^^)
   , (<<^^)
   , (^^<<)
+  , BiKleisli
   ) where
 
 import Prelude hiding ((.))
@@ -106,6 +107,9 @@
   invert (f :<->: g) = g :<->: f
 
 instance SemigroupoidArrowA => BiArrow' (Bijection a)
+
+-- |Bidirectional 'Control.Arrow.Kleisli' monad arrow transformer.
+type BiKleisli m = Bijection (Kleisli m)
 
 #ifdef VERSION_semigroupoids
 instance (Semigroupoid a, Arrow a) => BiArrow (Semigroupoid.Iso a) where
diff --git a/Control/Invertible/Functor.hs b/Control/Invertible/Functor.hs
--- a/Control/Invertible/Functor.hs
+++ b/Control/Invertible/Functor.hs
@@ -5,12 +5,17 @@
 -- 
 -- > import qualified Control.Invertible.Functor as Inv
 --
-{-# LANGUAGE CPP, Safe, TypeOperators, FlexibleInstances #-}
+{-# LANGUAGE CPP, TypeOperators, FlexibleInstances #-}
+#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
+{-# LANGUAGE Safe #-}
+#endif
 module Control.Invertible.Functor
   ( Functor(..)
+  , fmapDefault
   , (<$>)
   ) where
 
+import qualified Prelude
 import Prelude hiding ((.), Functor(..), (<$>))
 import Control.Arrow (Arrow)
 import Control.Category ((.))
@@ -26,6 +31,10 @@
 -- |An invariant version of 'Data.Functor.Functor', equivalent to 'Data.Functor.Inviarant.Invariant'.
 class Functor f where
   fmap :: a <-> b -> f a -> f b
+
+-- |Default invertible 'Functor' implementation for simple non-invertible 'Prelude.Functor's.
+fmapDefault :: Prelude.Functor f => a <-> b -> f a -> f b
+fmapDefault (f :<->: _) x = f Prelude.<$> x
 
 -- |An infix synnonym for 'fmap'.
 (<$>) :: Functor f => a <-> b -> f a -> f b
diff --git a/Control/Invertible/MonadArrow.hs b/Control/Invertible/MonadArrow.hs
--- a/Control/Invertible/MonadArrow.hs
+++ b/Control/Invertible/MonadArrow.hs
@@ -1,12 +1,26 @@
 -- |
 -- A symmetric version of the Kleisli monad transformer arrow.
--- BiKleisli provides this Kleisli-like arrow over bijections.
+-- This admits three isomorphic 'MonadBijection' types:
 --
+-- * @'MonadArrow' ('<->') m a b@
+-- * @'Bijection' ('MonadFunction' m) a b@
+-- * @m a '<->' m b@
+--
 -- The Alimarine paper just calls it \"MoT\" for Monad Transformer.
-{-# LANGUAGE CPP, Safe, TupleSections, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE CPP, TupleSections, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeOperators #-}
+#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
+{-# LANGUAGE Safe #-}
+#endif
 module Control.Invertible.MonadArrow
   ( MonadArrow(..)
-  , BiKleisli
+  , MonadFunction
+  , MonadBijection
+  , MonadBijection'
+  , MonadBijection''
+  , monadBijection
+  , monadBijection'
   ) where
 
 import Prelude hiding (id, (.))
@@ -20,13 +34,26 @@
 #endif
 
 import Data.Invertible.Bijection
+import Data.Invertible.TH
 import Control.Invertible.BiArrow
 
 -- |Bidirectional 'Control.Arrow.Kleisli'-like monad arrow transformer.
 newtype MonadArrow a m b c = MonadArrow { runMonadArrow :: a (m b) (m c) }
 
--- |A MonadArrow over bijections.
-type BiKleisli m a b = MonadArrow (<->) m a b
+-- |Specialization of 'MonadArrow' to function arrows.
+type MonadFunction = MonadArrow (->)
+
+type MonadBijection m = MonadArrow (<->) m
+type MonadBijection' m = Bijection (MonadFunction m)
+type MonadBijection'' m a b = m a <-> m b
+
+-- |Convert between isomorphic representations of 'MonadBijection's.
+monadBijection :: MonadBijection' m a b <-> MonadBijection m a b
+monadBijection = [biCase|MonadArrow f :<->: MonadArrow g <-> (MonadArrow (f :<->: g))|]
+
+-- |Convert between isomorphic representations of 'MonadBijection's.
+monadBijection' :: MonadBijection'' m a b <-> MonadBijection' m a b
+monadBijection' = [biCase|f :<->: g <-> MonadArrow f :<->: MonadArrow g|]
 
 instance Category a => Category (MonadArrow a m) where
   id = MonadArrow id
diff --git a/Control/Invertible/Monoidal.hs b/Control/Invertible/Monoidal.hs
--- a/Control/Invertible/Monoidal.hs
+++ b/Control/Invertible/Monoidal.hs
@@ -2,13 +2,20 @@
 -- Invariant monoidal functors.
 -- 
 -- This roughly corresponds to "Control.Applicative", but exposes a non-overlapping API so can be imported unqualified.  It does, however, use operators similar to those provided by contravariant.
-{-# LANGUAGE CPP, Safe, TypeOperators, FlexibleInstances #-}
+{-# LANGUAGE CPP, TypeOperators, FlexibleInstances #-}
+#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
+{-# LANGUAGE Safe #-}
+#endif
 module Control.Invertible.Monoidal
-  ( -- * Functor
-    (>$<)
+  ( Bijection(..)
+  , I.biCase
+    -- * Functor
+  , (>$<)
   , (>$), ($<)
   -- * Monoidal
   , Monoidal(..)
+  , unitDefault
+  , pairADefault
   , (>*), (*<)
   -- ** Tuple combinators
   , liftI2
@@ -23,6 +30,7 @@
   , (>>>>*<)
   , (>>*<<)
   , pureI
+  , constI
   , sequenceI_
   , mapI_
   , forI_
@@ -30,6 +38,7 @@
   , mapMaybeI
   -- * MonoidalAlt
   , MonoidalAlt(..)
+  , eitherADefault
   , (>|), (|<)
   , optionalI
   , defaulting
@@ -40,7 +49,10 @@
   ) where
 
 import Prelude
+import Control.Applicative (liftA2, Alternative, (<|>))
 import Control.Arrow ((&&&), (***))
+import Control.Monad.Trans.Maybe (MaybeT(..))
+import Data.Void (Void)
 
 import Data.Invertible.Bijection
 import qualified Data.Invertible as I
@@ -69,6 +81,14 @@
   -- |Merge two functors into a tuple, analogous to @'Control.Applicative.liftA2' (,)@. (Sometimes known as @**@.)
   (>*<) :: f a -> f b -> f (a, b)
 
+-- |Default 'unit' implementation for non-invertible 'Applicative's.
+unitDefault :: Applicative f => f ()
+unitDefault = pure ()
+
+-- |Default '>*< implementation for non-invertible 'Applicative's.
+pairADefault :: Applicative f => f a -> f b -> f (a, b)
+pairADefault = liftA2 (,)
+
 -- |Sequence actions, discarding/inhabiting the unit value of the second argument.
 (>*) :: Monoidal f => f a -> f () -> f a
 (>*) = liftI2 I.fst
@@ -123,6 +143,10 @@
 pureI :: Monoidal f => a -> f a
 pureI a = I.const a >$< unit
 
+-- |Supply a constant value to a monoidal and ignore whatever is produced.
+constI :: Monoidal f => a -> f a -> f ()
+constI a = (>$<) $ I.invert $ I.const a
+
 -- |Sequence (like 'Data.Foldable.sequenceA_') a list of monoidals, ignoring (@'I.const' ()@) all the results.
 sequenceI_ :: (Foldable t, Monoidal f) => t (f ()) -> f ()
 sequenceI_ = foldr (*<) unit
@@ -147,9 +171,15 @@
 
 -- |Monoidal functors that allow choice.
 class Monoidal f => MonoidalAlt f where
+  -- |An always-failing (and thus impossible) value.
+  zero :: f Void
   -- |Associative binary choice.
   (>|<) :: f a -> f b -> f (Either a b)
 
+-- |Default '>|<' implementation for non-invertible 'Alternative's.
+eitherADefault :: Alternative f => f a -> f b -> f (Either a b)
+eitherADefault a b = Left <$> a <|> Right <$> b
+
 -- |Assymetric (and therefore probably not bijective) version of '>|<' that returns whichever action succeeds but always uses the left one on inputs.
 (>|) :: MonoidalAlt f => f a -> f a -> f a
 a >| b = (either id id :<->: Left) >$< (a >|< b)
@@ -160,7 +190,7 @@
 
 infixl 3 >|, >|<, |<
 
--- |Analogous to 'Control.Applicative.optional'.
+-- |Analogous to 'Control.Applicative.optional': always succeeds.
 optionalI :: MonoidalAlt f => f a -> f (Maybe a)
 optionalI f = I.lft >$< (f >|< unit)
 
@@ -201,3 +231,22 @@
   unit = I.id
   -- |Uses the 'Monoid' instance to combine '()'s.
   (ua :<->: au) >*< (ub :<->: bu) = ua &&& ub :<->: uncurry mappend . (au *** bu)
+
+instance I.Functor m => I.Functor (MaybeT m) where
+  fmap f (MaybeT m) = MaybeT $ I.fmap (I.bifmap f) m
+
+instance Monoidal m => Monoidal (MaybeT m) where
+  unit = MaybeT $ I.invert I.fromJust >$< unit
+  MaybeT f >*< MaybeT g = MaybeT
+    $ (uncurry pairADefault :<->: maybe (Nothing, Nothing) (Just *** Just))
+    >$< (f >*< g)
+
+instance Monoidal m => MonoidalAlt (MaybeT m) where
+  zero = MaybeT $ I.const Nothing >$< unit
+  MaybeT f >|< MaybeT g = MaybeT
+    $ (uncurry eitherADefault :<->: ue)
+    >$< (f >*< g)
+    where
+    ue Nothing = (Nothing, Nothing)
+    ue (Just (Left a)) = (Just a, Nothing)
+    ue (Just (Right b)) = (Nothing, Just b)
diff --git a/Control/Invertible/Monoidal/Free.hs b/Control/Invertible/Monoidal/Free.hs
--- a/Control/Invertible/Monoidal/Free.hs
+++ b/Control/Invertible/Monoidal/Free.hs
@@ -1,7 +1,11 @@
-{-# LANGUAGE Safe, GADTs, RankNTypes, TupleSections, TypeOperators, QuasiQuotes #-}
 -- |
 -- A vague analog of free monads for invariant monoidals.
 -- This can provide a simple basis for things like invertible parsers.
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs, RankNTypes, TupleSections, TypeOperators, QuasiQuotes #-}
+#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
+{-# LANGUAGE Safe #-}
+#endif
 module Control.Invertible.Monoidal.Free
   ( Free(..)
   , showsFree
@@ -23,6 +27,7 @@
 import Control.Monad.Trans.State (StateT(..))
 import Data.Functor.Classes (Show1, showsPrec1)
 import Data.Monoid ((<>), Alt(..))
+import Data.Void (Void, absurd)
 
 import Control.Invertible.Monoidal
 import qualified Data.Invertible as I
@@ -30,6 +35,7 @@
 -- |Produce a 'MonoidalAlt' out of any type constructor, simply by converting each monoidal operation into a constructor.
 -- Although a version more analogous to a free monad could be defined for instances of 'I.Functor' and restricted to 'Monoidal', including the Yoneda transform makes this the more general case.
 data Free f a where
+  Void :: Free f Void
   Empty :: Free f ()
   Free :: !(f a) -> Free f a
   Join :: Free f a -> Free f b -> Free f (a, b)
@@ -45,10 +51,12 @@
   (>*<) = Join
 
 instance MonoidalAlt (Free f) where
+  zero = Void
   (>|<) = Choose
 
 -- |Construct a string representation of a 'Free' structure, given a way to show any @f a@.
 showsPrecFree :: (forall a' . f a' -> ShowS) -> Int -> Free f a -> ShowS
+showsPrecFree _ _ Void = showString "Void"
 showsPrecFree _ _ Empty = showString "Empty"
 showsPrecFree fs d (Free f) = showParen (d > 10)
   $ showString "Free "
@@ -78,6 +86,7 @@
 
 -- |Transform the type constructor within a 'Free'.
 mapFree :: (forall a' . f a' -> m a') -> Free f a -> Free m a
+mapFree _ Void = Void
 mapFree _ Empty = Empty
 mapFree t (Transform f p) = Transform f $ mapFree t p
 mapFree t (Join p q) = Join (mapFree t p) (mapFree t q)
@@ -86,6 +95,7 @@
 
 -- |Given a way to extract a @b@ from any @f a@, use a 'Free' applied to a value to produce a @b@ by converting '>*<' to '<>'.
 foldFree :: Monoid b => (forall a' . f a' -> a' -> b) -> Free f a -> a -> b
+foldFree _ Void a = absurd a
 foldFree _ Empty () = mempty
 foldFree t (Transform f p) a = foldFree t p $ I.biFrom f a
 foldFree t (Join p q) (a, b) = foldFree t p a <> foldFree t q b
@@ -99,6 +109,7 @@
 
 -- |Evaluate a 'Free' into an underlying 'Alternative', by evaluating '>|<' with '<|>'.
 runFree :: Alternative f => Free f a -> f a
+runFree Void = empty
 runFree Empty = pure ()
 runFree (Transform f p) = I.biTo f <$> runFree p
 runFree (Join p q) = (,) <$> runFree p <*> runFree q
diff --git a/Control/Invertible/Monoidal/HList.hs b/Control/Invertible/Monoidal/HList.hs
deleted file mode 100644
--- a/Control/Invertible/Monoidal/HList.hs
+++ /dev/null
@@ -1,35 +0,0 @@
--- |
--- Combine monoidal functors into HLists.
-{-# LANGUAGE TypeOperators, DataKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TypeFamilies, UndecidableInstances #-}
-module Control.Invertible.Monoidal.HList
-  ( hConsI
-  , (>:*<)
-  , HSequenceI(..)
-  ) where
-
-import Prelude hiding (Functor(..), (<$>), fst, snd, id)
-import qualified Data.HList as HL
-
-import Data.Invertible.HList
-import Control.Invertible.Monoidal
-
--- |'HL.HCons' two monoidal functors.
-hConsI :: Monoidal f => f a -> f (HL.HList l) -> f (HL.HList (a ': l))
-hConsI = liftI2 hCons
-
--- |Infix alias for 'hConsI'.
-(>:*<) :: Monoidal f => f a -> f (HL.HList l) -> f (HL.HList (a ': l))
-(>:*<) = hConsI
-
-infixr 4 >:*<
-
--- |A monoidal version of 'HL.HSequence': a heteogeneous version of 'sequenceMaybesI'.
-class (Monoidal m, HL.SameLength a b) => HSequenceI m a b | a -> b, m b -> a where
-  hSequenceI :: HL.HList a -> m (HL.HList b)
-
-instance Monoidal m => HSequenceI m '[] '[] where
-  hSequenceI _ = pureI HL.HNil
-
-instance (m1 ~ m, Monoidal m, HSequenceI m as bs) => HSequenceI m (m1 a ': as) (a ': bs) where
-  hSequenceI (HL.HCons a b) = a >:*< hSequenceI b
-
diff --git a/Data/Invertible.hs b/Data/Invertible.hs
--- a/Data/Invertible.hs
+++ b/Data/Invertible.hs
@@ -7,7 +7,10 @@
 -- 
 -- > import qualified Data.Invertible as Inv
 --
+{-# LANGUAGE CPP #-}
+#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
 {-# LANGUAGE Safe #-}
+#endif
 module Data.Invertible
   ( module Data.Invertible.Bijection
   , module Data.Invertible.TH
diff --git a/Data/Invertible/HList.hs b/Data/Invertible/HList.hs
deleted file mode 100644
--- a/Data/Invertible/HList.hs
+++ /dev/null
@@ -1,36 +0,0 @@
--- |
--- Bidirectional version of "Data.HList.HList".
-{-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators, FlexibleContexts #-}
-module Data.Invertible.HList
-  ( hCons
-  , hReverse
-  , hReverse_
-  , hAppend
-  , hZip
-  ) where
-
-import qualified Data.HList as HL
-import Data.Proxy (Proxy(..))
-
-import Data.Invertible.Bijection
-import Data.Invertible.TH
-
--- |(De)construct an list from a head and tail.
-hCons :: (a, HL.HList l) <-> HL.HList (a ': l)
-hCons = [biCase|(a, l) <-> HL.HCons a l|]
-
--- |'HL.hReverse' the order of a list.
-hReverse :: (HL.HReverse a b, HL.HReverse b a) => HL.HList a <-> HL.HList b
-hReverse = HL.hReverse :<->: HL.hReverse
-
--- |'HL.hReverse_' the order of a list.
-hReverse_ :: (HL.HRevApp a '[] b, HL.HRevApp b '[] a) => HL.HList a <-> HL.HList b
-hReverse_ = HL.hReverse_ :<->: HL.hReverse_
-
--- |'HL.hAppend' (concatenate) or split two lists.
-hAppend :: (HL.HAppendList a b, HL.HSplitAt n (HL.HAppendListR a b) a b) => (HL.HList a, HL.HList b) <-> HL.HList (HL.HAppendListR a b)
-hAppend = uncurry HL.hAppendList :<->: HL.hSplitAt Proxy
-
--- |'HL.hZip' two lists together.
-hZip :: HL.HZipList a b l => (HL.HList a, HL.HList b) <-> HL.HList l
-hZip = uncurry HL.hZipList :<->: HL.hUnzipList
diff --git a/Data/Invertible/Maybe.hs b/Data/Invertible/Maybe.hs
--- a/Data/Invertible/Maybe.hs
+++ b/Data/Invertible/Maybe.hs
@@ -7,6 +7,7 @@
   , listToMaybe
   , maybeToList
   , fromMaybe
+  , fromJust
   ) where
 
 import qualified Data.Maybe as M
@@ -42,3 +43,7 @@
 -- |Convert between 'Nothing' and a default value, or 'Just' and its value (not a true bijection).
 fromMaybe :: Eq a => a -> Maybe a <-> a
 fromMaybe d = M.fromMaybe d :<->: \a -> if a == d then Nothing else Just a
+
+-- |Convert between 'Just' and its value.
+fromJust :: Maybe a <-> a
+fromJust = M.fromJust :<->: Just
diff --git a/Data/Invertible/Monad.hs b/Data/Invertible/Monad.hs
--- a/Data/Invertible/Monad.hs
+++ b/Data/Invertible/Monad.hs
@@ -11,7 +11,7 @@
 
 import Data.Invertible.Bijection
 
--- |Bind two functions to create a 'Control.Invertible.MonadArrow.BiKleisli'-form bijection.
+-- |Bind two functions to create a "Control.Invertible.MonadArrow"-form bijection.
 bind :: Monad m => (a -> m b) -> (b -> m a) -> m a <-> m b
 bind f g = (f =<<) :<->: (g =<<)
 
@@ -21,7 +21,7 @@
 
 infix 2 =<<->>=
 
--- |Promote a bijection to a 'Control.Invertible.MonadArrow.BiKleisli'-form bijection.
--- (Equivalent to 'Data.Invertible.Functor.bifmap'.)
+-- |Promote a bijection to a "Control.Invertible.MonadArrow"-form bijection.
+-- (Equivalent to 'Data.Invertible.Functor.bifmap' and 'Control.Invertible.BiArrow.biarr'.)
 liftM :: Monad m => a <-> b -> m a <-> m b
 liftM (f :<->: g) = M.liftM f :<->: M.liftM g
diff --git a/Data/Invertible/Monoid.hs b/Data/Invertible/Monoid.hs
--- a/Data/Invertible/Monoid.hs
+++ b/Data/Invertible/Monoid.hs
@@ -1,5 +1,6 @@
 -- |
 -- Bidirectional transforms for "Data.Monoid".
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE Safe, TypeOperators, QuasiQuotes #-}
 module Data.Invertible.Monoid
   ( BiEndo(..)
@@ -32,6 +33,11 @@
 
 -- | The monoid of endomorphisms under composition.
 newtype BiEndo a = BiEndo { appBiEndo :: a <-> a }
+
+#if MIN_VERSION_base(4,11,0)
+instance Semigroup (BiEndo a) where
+  BiEndo f <> BiEndo g = BiEndo (f C.. g)
+#endif
 
 instance Monoid (BiEndo a) where
   mempty = BiEndo C.id
diff --git a/Data/Invertible/Prelude.hs b/Data/Invertible/Prelude.hs
--- a/Data/Invertible/Prelude.hs
+++ b/Data/Invertible/Prelude.hs
@@ -1,7 +1,11 @@
 -- |
 -- The bidirectional \"Prelude\", which re-exports various bijections similar to functions from "Prelude".
 -- Most \"un\"-functions are left out for obvious reasons.
-{-# LANGUAGE Safe, TypeOperators #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeOperators #-}
+#if !(defined(VERSION_semigroupoids) && MIN_VERSION_semigroupoids(5,2,2))
+{-# LANGUAGE Safe #-}
+#endif
 module Data.Invertible.Prelude
   ( (<->)
   , type (<->)
diff --git a/Data/Invertible/TH.hs b/Data/Invertible/TH.hs
--- a/Data/Invertible/TH.hs
+++ b/Data/Invertible/TH.hs
@@ -1,5 +1,6 @@
 -- |
 -- Convenient construction of bidirectional functions using case-like syntax.
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE TemplateHaskell, Trustworthy #-}
 module Data.Invertible.TH
   ( biCase
@@ -16,15 +17,27 @@
 import Language.Haskell.Meta.Parse (parsePat)
 import qualified Language.Haskell.TH as TH
 import Language.Haskell.TH.Quote (QuasiQuoter(..))
+#if MIN_VERSION_base(4,9,0)
+import Text.Read.Lex (isSymbolChar)
+#endif
 
 import Data.Invertible.Bijection
 
-split :: Eq a => [a] -> [a] -> [[a]]
+#if !MIN_VERSION_base(4,9,0)
+isSymbolChar :: Char -> Bool
+isSymbolChar = (`elem` "!#$%&*+./<=>?@\\^|-~:")
+#endif
+
+split :: String -> String -> [String]
 split _ [] = []
-split t s@(c:r)
-  | Just s' <- stripPrefix t s = [] : split t s'
-  | p:l <- split t r = (c:p):l
-  | otherwise = [s]
+split d (p:s)
+  | not (isSymbolChar p)
+  , Just (p':s') <- stripPrefix d s
+  , not (isSymbolChar p') = [p] : conshead p' (split d s')
+  | otherwise = conshead p $ split d s
+  where
+  conshead c [] = [[c]]
+  conshead c (h:t) = (c:h):t
 
 patToPat :: TH.Pat -> TH.Pat
 patToPat = ptp . gmapT pta where
@@ -36,9 +49,24 @@
 patToExp :: TH.Pat -> TH.Exp
 patToExp (TH.LitP l) = TH.LitE l
 patToExp (TH.VarP v) = TH.VarE v
-patToExp (TH.TupP l) = TH.TupE $ map patToExp l
-patToExp (TH.UnboxedTupP l) = TH.UnboxedTupE $ map patToExp l
-patToExp (TH.ConP c a) = foldl (\f -> TH.AppE f . patToExp) (TH.ConE c) a
+patToExp (TH.TupP l) = TH.TupE $ map (
+#if MIN_VERSION_template_haskell(2,16,0)
+  Just .
+#endif
+  patToExp) l
+patToExp (TH.UnboxedTupP l) = TH.UnboxedTupE $ map (
+#if MIN_VERSION_template_haskell(2,16,0)
+  Just .
+#endif
+  patToExp) l
+#if MIN_VERSION_template_haskell(2,12,0)
+patToExp (TH.UnboxedSumP p a n) = TH.UnboxedSumE (patToExp p) a n
+#endif
+patToExp (TH.ConP c
+#if MIN_VERSION_template_haskell(2,18,0)
+  _ -- [Type], probably should have to be empty
+#endif
+  a) = foldl (\f -> TH.AppE f . patToExp) (TH.ConE c) a
 patToExp (TH.InfixP l o r) = TH.InfixE (Just $ patToExp l) (TH.ConE o) (Just $ patToExp r)
 patToExp (TH.UInfixP l o r) = TH.UInfixE (patToExp l) (TH.ConE o) (patToExp r)
 patToExp (TH.ParensP p) = TH.ParensE $ patToExp p
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2016, Dylan Simon
+Copyright (c) 2016-2017, Dylan Simon
 
 All rights reserved.
 
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,12 @@
+Haskell bidirectional arrows, bijective functions, and invariant functors
+
+Representations and operations for bidirectional arrows (total isomorphisms: an
+arrow paired with its inverse).  Classes for invariant functors and monoidal
+functors.  Includes a number of useful bijections and operations, as well as
+interoperability with related packages.
+
+See also: semigroupoids, TypeCompose, lens, semi-iso, partial-isomorphisms, and
+Piso packages.
+
+Artem Alimarine, et al. There and Back Again: Arrows for Invertible
+  Programming. Haskell '05.
diff --git a/invertible.cabal b/invertible.cabal
--- a/invertible.cabal
+++ b/invertible.cabal
@@ -1,5 +1,5 @@
 name:                invertible
-version:             0.1.2
+version:             0.2.0.8
 synopsis:            bidirectional arrows, bijective functions, and invariant functors
 description:
   Representations and operations for bidirectional arrows (total isomorphisms: an
@@ -17,6 +17,7 @@
 build-type:          Simple
 cabal-version:       >=1.10
 tested-with:         GHC == 7.10.3, GHC == 8.0.1
+extra-source-files:  README
 
 source-repository head
   type: git
@@ -24,20 +25,32 @@
 
 flag arrows
   description: Support the arrows package
-flag HList
-  description: Support the HList package
+  manual: True
+  default: False
 flag invariant
   description: Support the invariant package
+  manual: True
+  default: True
 flag lens
   description: Support the lens package
+  manual: True
+  default: True
 flag partial-isomorphisms
   description: Support the partial-isomorphisms package
+  manual: True
+  default: True
 flag Piso
   description: Support the Piso package
+  manual: True
+  default: False
 flag semigroupoids
   description: Support the semigroupoids package
+  manual: True
+  default: True
 flag TypeCompose
   description: Support the TypeCompose package
+  manual: True
+  default: False
 
 library
   other-modules:
@@ -70,23 +83,19 @@
   build-depends:
     base >= 4.8 && <5,
     transformers,
-    haskell-src-meta == 0.6.*,
+    haskell-src-meta >= 0.6 && < 0.9,
     template-haskell == 2.*
   default-language:    Haskell2010
   ghc-options: -Wall
 
   if flag(arrows)
     build-depends: arrows
-  if flag(HList)
-    exposed-modules: Data.Invertible.HList
-    exposed-modules: Control.Invertible.Monoidal.HList
-    build-depends: HList == 0.4.*
   if flag(invariant)
     exposed-modules: Data.Invertible.Invariant
     build-depends: invariant
   if flag(lens)
     exposed-modules: Data.Invertible.Lens
-    build-depends: lens == 4.*
+    build-depends: lens >= 4 && < 6
   if flag(partial-isomorphisms)
     exposed-modules: Data.Invertible.PartialIsomorphism
     if impl(ghc >= 8)
@@ -110,6 +119,8 @@
   type: exitcode-stdio-1.0
   hs-source-dirs: test
   main-is: Main.hs
+  other-modules:
+    FreeMonoidal
   default-language: Haskell2010
   ghc-options: -Wall
   build-depends:
diff --git a/test/FreeMonoidal.hs b/test/FreeMonoidal.hs
new file mode 100644
--- /dev/null
+++ b/test/FreeMonoidal.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE CPP, GADTs, FlexibleContexts, FlexibleInstances, TypeOperators, TupleSections, ConstraintKinds, GeneralizedNewtypeDeriving, QuasiQuotes #-}
+module FreeMonoidal (tests) where
+
+import Control.Monad (join, guard)
+import Data.Functor.Classes (Show1(..))
+import Data.Maybe (isJust)
+import qualified Test.QuickCheck as Q
+import Unsafe.Coerce (unsafeCoerce)
+
+import Control.Invertible.Monoidal.Free
+import qualified Data.Invertible as I
+
+genTree :: [Q.Gen a] -> Q.Gen a
+genTree = Q.scale (max 0 . pred) . join . Q.growingElements
+
+newtype Const a b = Const a
+  deriving (Eq, Ord, Show, Q.Arbitrary)
+
+instance Functor (Const a) where
+  fmap _ (Const x) = Const x
+
+instance Show a => Show1 (Const a) where
+#if MIN_VERSION_base(4,9,0)
+  liftShowsPrec _ _ =
+#else
+  showsPrec1 =
+#endif
+    showsPrec
+
+data Tree a
+  = TreeEmpty
+  | TreeFree a
+  | TreeJoin !(Tree a, Tree a)
+  | TreeChoose !(Either (Tree a) (Tree a))
+  deriving (Eq, Show)
+
+instance Q.Arbitrary a => Q.Arbitrary (Tree a) where
+  arbitrary = genTree
+    [ return TreeEmpty
+    , TreeFree <$> Q.arbitrary
+    , TreeJoin <$> Q.arbitrary
+    , TreeChoose <$> Q.arbitrary
+    ]
+
+  shrink TreeEmpty = []
+  shrink (TreeFree x) = TreeEmpty : map TreeFree (Q.shrink x) 
+  shrink (TreeJoin (p, q)) =
+    [TreeEmpty, p, q] ++ map TreeJoin (Q.shrink (p, q))
+  shrink (TreeChoose (Left p)) =
+    [TreeEmpty, p] ++ map (TreeChoose . Left) (Q.shrink p)
+  shrink (TreeChoose (Right p)) =
+    [TreeEmpty, p] ++ map (TreeChoose . Right) (Q.shrink p)
+
+type FreeTree a = Free (Const a) (Tree a)
+
+emptyTree :: FreeTree a
+emptyTree = Transform (I.const TreeEmpty) Empty
+
+leaf :: a -> FreeTree a
+leaf = Free . Const
+
+unJoin :: (Tree a, Tree a) I.<-> Tree a
+unJoin = [I.biCase|t <-> TreeJoin t|]
+
+unChoose :: Either (Tree a) (Tree a) I.<-> Tree a
+unChoose = [I.biCase|t <-> TreeChoose t|]
+
+instance Q.Arbitrary a => Q.Arbitrary (FreeTree a) where
+  arbitrary = genTree
+    [ return emptyTree
+    , leaf <$> Q.arbitrary
+    , Transform unJoin   <$> (Join   <$> Q.arbitrary <*> Q.arbitrary)
+    , Transform unChoose <$> (Choose <$> Q.arbitrary <*> Q.arbitrary)
+    , Transform I.id <$> Q.arbitrary
+    ]
+
+  shrink (Free x) = map Free (Q.shrink x) 
+  shrink (Transform _ Empty) = []
+  shrink (Transform _ (Join p q)) =
+    [emptyTree, pt, qt] ++ map (Transform unJoin . uncurry Join) (Q.shrink (pt, qt)) where
+    pt = unsafeCoerce p :: FreeTree a
+    qt = unsafeCoerce q :: FreeTree a
+  shrink (Transform _ (Choose p q)) =
+    [emptyTree, pt, qt] ++ map (Transform unChoose . uncurry Choose) (Q.shrink (pt, qt)) where
+    pt = unsafeCoerce p :: FreeTree a
+    qt = unsafeCoerce q :: FreeTree a
+  shrink (Transform _ p) = [pt] where
+    pt = unsafeCoerce p :: FreeTree a
+
+type ShowFree f = (Functor f, Show1 f)
+
+ok :: Q.Property
+ok = Q.property True
+
+bad :: ShowFree f => Free f a -> Q.Property
+bad f = Q.counterexample (show f) False
+
+checkNoT :: ShowFree f => Free f a -> Q.Property
+checkNoT t@(Transform _ _) = bad t
+checkNoT (Join p q) = checkNoT p Q..&&. checkNoT q
+checkNoT (Choose p q) = checkNoT p Q..&&. checkNoT q
+checkNoT _ = ok
+
+checkTNF :: ShowFree f => Free f a -> Q.Property
+checkTNF (Transform _ p) = checkNoT p
+checkTNF p = checkNoT p
+
+joinDNF :: ShowFree f => Free f a -> Q.Property
+joinDNF t@(Transform _ _) = bad t
+joinDNF c@(Choose _ _) = bad c
+joinDNF (Join p q) = joinDNF p Q..&&. joinDNF q
+joinDNF _ = ok
+
+checkDNF :: ShowFree f => Free f a -> Q.Property
+checkDNF t@(Transform _ _) = bad t
+checkDNF (Choose p q) = checkDNF p Q..&&. checkDNF q
+checkDNF p = joinDNF p
+
+checkTDNF :: ShowFree f => Free f a -> Q.Property
+checkTDNF (Transform _ p) = checkDNF p
+checkTDNF p = checkDNF p
+
+produceParse :: FreeTree Int -> [Int] -> Q.Property
+produceParse f l = isJust p Q.==> check where
+  check = prod f r ++ t Q.=== l Q..&&. reverse t ++ prod (reverseFree f) r Q.=== reverse l
+  Just (r, t) = p
+  p = pars f l
+  pars = parseFree parse
+  parse (Const i) j = unsafeCoerce (TreeFree j) <$ guard (j >= i)
+  prod = produceFree produce
+  produce (Const _) x = case unsafeCoerce x of { ~(TreeFree j) -> j }
+
+joinSorted :: (Show a, Ord a) => Maybe a -> Free (Const a) b -> (Maybe a, Q.Property)
+joinSorted b (Join p q) = (qb, pr Q..&&. qr) where
+  (pb, pr) = joinSorted b p
+  (qb, qr) = joinSorted pb q
+joinSorted b (Free (Const x)) = (Just x, Q.counterexample (show x ++ " < " ++ show b) $ all (x >=) b)
+joinSorted b Empty = (b, ok)
+joinSorted b o = (b, bad o)
+
+chooseSorted :: (Show a, Ord a) => Free (Const a) b -> Q.Property
+chooseSorted t@(Transform _ _) = bad t
+chooseSorted (Choose p q) = chooseSorted p Q..&&. chooseSorted q
+chooseSorted p = snd $ joinSorted Nothing p
+
+checkSorted :: (Show a, Ord a) => Free (Const a) b -> Q.Property
+checkSorted (Transform _ p) = chooseSorted p
+checkSorted p = chooseSorted p
+
+compareConst :: Ord a => Const a b -> Const a c -> Ordering
+compareConst (Const x) (Const y) = compare x y
+
+tests :: Q.Property
+tests = Q.conjoin
+  [ Q.label "TNF" $ checkTNF . (freeTNF :: FreeTree Int -> FreeTree Int)
+  , Q.label "TDNF" $ checkTDNF . (freeTDNF :: FreeTree Int -> FreeTree Int)
+  , Q.label "parseProduce" $ produceParse
+  , Q.label "sort" $ checkSorted . (sortFreeTDNF compareConst :: FreeTree Int -> FreeTree Int)
+  ]