diff --git a/Control/Invertible/BiArrow.hs b/Control/Invertible/BiArrow.hs
--- a/Control/Invertible/BiArrow.hs
+++ b/Control/Invertible/BiArrow.hs
@@ -4,7 +4,7 @@
 --
 --  * Artem Alimarine, et al. /There and Back Again: Arrows for Invertible Programming/. Haskell '05. <http://citeseer.ist.psu.edu/alimarine05there.html>
 --
-{-# LANGUAGE CPP, Trustworthy #-}
+{-# LANGUAGE CPP, Trustworthy, TypeOperators #-}
 module Control.Invertible.BiArrow
   ( BiArrow(..)
   , BiArrow'
diff --git a/Control/Invertible/Functor.hs b/Control/Invertible/Functor.hs
--- a/Control/Invertible/Functor.hs
+++ b/Control/Invertible/Functor.hs
@@ -5,7 +5,7 @@
 -- 
 -- > import qualified Control.Invertible.Functor as Inv
 --
-{-# LANGUAGE CPP, Safe, FlexibleInstances #-}
+{-# LANGUAGE CPP, Safe, TypeOperators, FlexibleInstances #-}
 module Control.Invertible.Functor
   ( Functor(..)
   , (<$>)
diff --git a/Control/Invertible/Monoidal.hs b/Control/Invertible/Monoidal.hs
--- a/Control/Invertible/Monoidal.hs
+++ b/Control/Invertible/Monoidal.hs
@@ -2,10 +2,11 @@
 -- 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, FlexibleInstances #-}
+{-# LANGUAGE CPP, Safe, TypeOperators, FlexibleInstances #-}
 module Control.Invertible.Monoidal
   ( -- * Functor
     (>$<)
+  , (>$), ($<)
   -- * Monoidal
   , Monoidal(..)
   , (>*), (*<)
@@ -22,13 +23,20 @@
   , (>>>>*<)
   , (>>*<<)
   , pureI
+  , sequenceI_
+  , mapI_
+  , forI_
   , sequenceMaybesI
   , mapMaybeI
   -- * MonoidalAlt
   , MonoidalAlt(..)
-  , possible
+  , (>|), (|<)
+  , optionalI
   , defaulting
-  , while
+  , manyI
+  , msumIndex
+  , msumFirst, msumLast
+  , oneOfI
   ) where
 
 import Prelude
@@ -41,9 +49,18 @@
 (>$<) :: I.Functor f => a <-> b -> f a -> f b
 (>$<) = I.fmap
 
-infixl 4 >$<
+infixl 4 $<, >$<, >$
 
--- |Lax invariant monoidal functor.
+-- |Given a value an an invariant for that value, always provide that value and ignore the produced value.
+-- @'I.fmap' . flip 'I.consts' ()@
+(>$) :: I.Functor f => a -> f a -> f ()
+(>$) a = I.fmap $ I.consts a ()
+
+-- |@flip ('>$')@
+($<) :: I.Functor f => f a -> a -> f ()
+($<) = flip (>$)
+
+-- |Invariant monoidal functor.
 -- This roughly corresponds to 'Applicative', which, for covariant functors, is equivalent to a monoidal functor.
 -- Invariant functors, however, may admit a monoidal instance but not applicative.
 class I.Functor f => Monoidal f where
@@ -52,14 +69,14 @@
   -- |Merge two functors into a tuple, analogous to @'Control.Applicative.liftA2' (,)@. (Sometimes known as @**@.)
   (>*<) :: f a -> f b -> f (a, b)
 
--- | Sequence actions, discarding/inhabiting the unit value of the first argument.
-(*<) :: Monoidal f => f () -> f a -> f a
-(*<) = liftI2 I.snd
-
--- | Sequence actions, discarding/inhabiting the unit value of the second argument.
+-- |Sequence actions, discarding/inhabiting the unit value of the second argument.
 (>*) :: Monoidal f => f a -> f () -> f a
 (>*) = liftI2 I.fst
 
+-- |Sequence actions, discarding/inhabiting the unit value of the first argument.
+(*<) :: Monoidal f => f () -> f a -> f a
+(*<) = liftI2 I.snd
+
 infixl 4 >*, >*<, *<
 
 -- |Lift an (uncurried) bijection into a monoidal functor.
@@ -106,13 +123,25 @@
 pureI :: Monoidal f => a -> f a
 pureI a = I.const a >$< unit
 
--- |Sequence (like 'Control.Applicative.sequenceA') and filter (like 'Data.Maybe.catMaybes') a list of monoidals, producing the list of non-'Nothing' values.
+-- |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
+
+-- |Map each element to a monoidal and 'sequenceI_' the results.
+mapI_ :: (Foldable t, Monoidal f) => (a -> f ()) -> t a -> f ()
+mapI_ f = foldr ((*<) . f) unit
+
+-- |@flip 'mapI_'@
+forI_ :: (Foldable t, Monoidal f) => t a -> (a -> f ()) -> f ()
+forI_ = flip mapI_
+
+-- |Sequence (like 'Data.Traversable.sequenceA') and filter (like 'Data.Maybe.catMaybes') a list of monoidals, producing the list of non-'Nothing' values.
 -- Shorter input lists pad with 'Nothing's and longer ones are ignored.
 sequenceMaybesI :: Monoidal f => [f (Maybe a)] -> f [a]
 sequenceMaybesI [] = pureI []
 sequenceMaybesI (x:l) = liftI2 I.consMaybe x (sequenceMaybesI l)
 
--- |Map each element to a 'Maybe' monoidal and sequence the results (like 'Control.Applicative.traverse' and 'Data.Maybe.mapMaybe').
+-- |Map each element to a 'Maybe' monoidal and sequence the results (like 'Data.Traversable.traverse' and 'Data.Maybe.mapMaybe').
 mapMaybeI :: Monoidal f => (a -> f (Maybe b)) -> [a] -> f [b]
 mapMaybeI = (sequenceMaybesI .) . map
 
@@ -121,20 +150,52 @@
   -- |Associative binary choice.
   (>|<) :: f a -> f b -> f (Either a b)
 
-infixl 3 >|<
+-- |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)
 
+-- |Assymetric (and therefore probably not bijective) version of '>|<' that returns whichever action succeeds but always uses the right one on inputs.
+(|<) :: MonoidalAlt f => f a -> f a -> f a
+a |< b = (either id id :<->: Right) >$< (a >|< b)
+
+infixl 3 >|, >|<, |<
+
 -- |Analogous to 'Control.Applicative.optional'.
-possible :: MonoidalAlt f => f a -> f (Maybe a)
-possible f = I.lft >$< (f >|< unit)
+optionalI :: MonoidalAlt f => f a -> f (Maybe a)
+optionalI f = I.lft >$< (f >|< unit)
 
 -- |Return a default value if a monoidal functor fails, and only apply it to non-default values.
 defaulting :: (MonoidalAlt f, Eq a) => a -> f a -> f a
-defaulting a f = I.fromMaybe a >$< possible f
+defaulting a f = I.fromMaybe a >$< optionalI f
 
 -- |Repeatedly apply a monoidal functor until it fails.  Analogous to 'Control.Applicative.many'.
-while :: MonoidalAlt f => f a -> f [a]
-while f = I.cons >$< possible (f >*< while f)
+manyI :: MonoidalAlt f => f a -> f [a]
+manyI f = I.cons >$< optionalI (f >*< manyI f)
 
+-- |Try a list of monoidal actions in sequence, producing the index of the first successful action, and evaluating the action with the given index.
+msumIndex :: MonoidalAlt f => [f ()] -> f Int
+msumIndex [] = error "msumIndex: empty list"
+msumIndex [x]   = (       (\() -> 0)      :<->: which) >$< x where
+  which i = case compare i 0 of
+    LT -> error "msumIndex: negative index"
+    EQ -> ()
+    GT -> error "msumIndex: index too large"
+msumIndex (x:l) = (either (\() -> 0) succ :<->: which) >$< (x >|< msumIndex l) where
+  which i = case compare i 0 of
+    LT -> error "msumIndex: negative index"
+    EQ -> Left ()
+    GT -> Right (pred i)
+
+-- |Fold a structure with '>|' ('|<'), thus always applying the input to the first (last) item for generation.
+msumFirst, msumLast :: (MonoidalAlt f, Traversable t) => t (f a) -> f a
+msumFirst = foldr1 (>|)
+msumLast = foldl1 (|<)
+
+-- |Take a list of items and apply them to the action in sequence until one succeeds and return the cooresponding item; match the input with the list and apply the corresponding action (or produce an error if the input is not an element of the list).
+oneOfI :: (MonoidalAlt f, Eq a) => (a -> f ()) -> [a] -> f a
+oneOfI _ [] = error "oneOfI: empty list"
+oneOfI f [x] = ((\() -> x) I.:<->: (\y -> if x == y then () else error "oneOfI: invalid option")) >$< f x
+oneOfI f (x:l) = (I.fromMaybe x I.. I.rgt) >$< (f x >|< oneOfI f l)
 
 instance Monoidal (Bijection (->) ()) where
   unit = I.id
diff --git a/Control/Invertible/Monoidal/Free.hs b/Control/Invertible/Monoidal/Free.hs
new file mode 100644
--- /dev/null
+++ b/Control/Invertible/Monoidal/Free.hs
@@ -0,0 +1,192 @@
+{-# 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.
+module Control.Invertible.Monoidal.Free
+  ( Free(..)
+  , showsFree
+  , mapFree
+  , foldFree
+  , produceFree
+  , runFree
+  , parseFree
+  , reverseFree
+  , freeTNF
+  , freeTDNF
+  , sortFreeTDNF
+  ) where
+
+import Control.Applicative (Alternative(..))
+import Control.Arrow ((***), first, second, (+++), left, right)
+import Control.Monad (MonadPlus(..))
+import Control.Monad.Trans.Class (lift)
+import Control.Monad.Trans.State (StateT(..))
+import Data.Functor.Classes (Show1(..))
+import Data.Monoid ((<>), Alt(..))
+
+import Control.Invertible.Monoidal
+import qualified Data.Invertible as I
+
+-- |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
+  Empty :: Free f ()
+  Free :: !(f a) -> Free f a
+  Join :: Free f a -> Free f b -> Free f (a, b)
+  Choose :: Free f a -> Free f b -> Free f (Either a b)
+  Transform :: (a I.<-> b) -> Free f a -> Free f b
+
+instance I.Functor (Free f) where
+  fmap f (Transform g p) = Transform (f I.. g) p
+  fmap f p = Transform f p
+
+instance Monoidal (Free f) where
+  unit = Empty
+  (>*<) = Join
+
+instance MonoidalAlt (Free f) where
+  (>|<) = 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 _ _ Empty = showString "Empty"
+showsPrecFree fs d (Free f) = showParen (d > 10)
+  $ showString "Free "
+  . fs f
+showsPrecFree fs d (Join p q) = showParen (d > 10)
+  $ showString "Join "
+  . showsPrecFree fs 11 p . showChar ' '
+  . showsPrecFree fs 11 q
+showsPrecFree fs d (Choose p q) = showParen (d > 10)
+  $ showString "Choose "
+  . showsPrecFree fs 11 p . showChar ' '
+  . showsPrecFree fs 11 q
+showsPrecFree fs d (Transform _ p) = showParen (d > 10)
+  $ showString "Transform <bijection> "
+  . showsPrecFree fs 11 p
+
+-- |Construct a string representation of a 'Free' structure, given a way to show any @f a@.
+showsFree :: (forall a' . f a' -> ShowS) -> Free f a -> ShowS
+showsFree fs = showsPrecFree fs 0
+
+data Underscore = Underscore
+instance Show Underscore where
+  show Underscore = "_"
+
+instance (Functor f, Show1 f) => Show (Free f a) where
+  showsPrec = showsPrecFree (showsPrec1 11 . (Underscore <$))
+
+-- |Transform the type constructor within a 'Free'.
+mapFree :: (forall a' . f a' -> m a') -> Free f a -> Free m a
+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)
+mapFree t (Choose p q) = Choose (mapFree t p) (mapFree t q)
+mapFree t (Free x) = Free (t x)
+
+-- |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 _ 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
+foldFree t (Choose p _) (Left a) = foldFree t p a
+foldFree t (Choose _ p) (Right a) = foldFree t p a
+foldFree t (Free x) a = t x a
+
+-- |'foldFree' over Alternative rather than Monoid.
+produceFree :: Alternative m => (forall a' . f a' -> a' -> b) -> Free f a -> a -> m b
+produceFree t f = getAlt . foldFree (\x a -> Alt $ pure $ t x a) f
+
+-- |Evaluate a 'Free' into an underlying 'Alternative', by evaluating '>|<' with '<|>'.
+runFree :: Alternative f => Free f a -> f a
+runFree Empty = pure ()
+runFree (Transform f p) = I.biTo f <$> runFree p
+runFree (Join p q) = (,) <$> runFree p <*> runFree q
+runFree (Choose p q) = Left <$> runFree p <|> Right <$> runFree q
+runFree (Free x) = x
+
+-- |Uncons the current state, returning the head and keeping the tail, or fail if empty.
+-- (Parsec's 'Text.Parsec.Prim.Stream' class provides similar but more general functionality.)
+unconsState :: Alternative m => StateT [a] m a
+unconsState = StateT ucs where
+  ucs (a:l) = pure (a, l)
+  ucs [] = empty
+
+-- |Given a way to convert @b@ elements into any @f a@, use a 'Free' to parse a list of @b@ elements into a value.
+-- This just uses 'unconsState' with 'runFree', and is the inverse of 'produceFree', provided the given conversions are themselves inverses.
+parseFree :: MonadPlus m => (forall a' . f a' -> b -> m a') -> Free f a -> [b] -> m (a, [b])
+parseFree t = runStateT . runFree . mapFree (\x -> lift . t x =<< unconsState)
+
+-- |Flip the effective order of each '>*<' operation in a 'Free', so that processing is done in the reverse order.
+-- It probably goes without saying, but applying this to an infinite structure, such as those produced by 'manyI', will not terminate.
+reverseFree :: Free f a -> Free f a
+reverseFree (Transform f (Join p q)) = Transform (f I.. I.swap) $ Join (reverseFree q) (reverseFree p)
+reverseFree (Transform f p) = Transform f $ reverseFree p
+reverseFree (Join p q) = Transform I.swap $ Join (reverseFree q) (reverseFree p)
+reverseFree (Choose p q) = Choose (reverseFree p) (reverseFree q)
+reverseFree p = p
+
+chooseTNF :: Free f a -> Free f b -> Free f (Either a b)
+chooseTNF (Transform f p) (Transform g q) = (f +++ g) >$< chooseTNF p q
+chooseTNF (Transform f p) q = left f >$< chooseTNF p q
+chooseTNF p (Transform g q) = right g >$< chooseTNF p q
+chooseTNF p q = Choose p q
+
+joinTNF :: Free f a -> Free f b -> Free f (a, b)
+joinTNF (Transform f p) (Transform g q) = (f *** g) >$< joinTNF p q
+joinTNF (Transform f p) q = first f >$< joinTNF p q
+joinTNF p (Transform g q) = second g >$< joinTNF p q
+joinTNF p q = Join p q
+
+-- |Convert a 'Free' to Transform Normal Form: extract and merge all the 'Transform', if any, to a single 'Transform' at the top.
+freeTNF :: Free f a -> Free f a
+freeTNF (Transform f p) = f >$< freeTNF p
+freeTNF (Join p q) = joinTNF (freeTNF p) (freeTNF q)
+freeTNF (Choose p q) = chooseTNF (freeTNF p) (freeTNF q)
+freeTNF p = p
+
+joinTDNF :: Free f a -> Free f b -> Free f (a, b)
+joinTDNF (Transform f p) (Transform g q) = (f *** g) >$< joinTDNF p q
+joinTDNF (Transform f p) q = first f >$< joinTDNF p q
+joinTDNF p (Transform g q) = second g >$< joinTDNF p q
+joinTDNF (Choose pp pq) q = I.eitherFirst >$< chooseTNF (joinTDNF pp q) (joinTDNF pq q)
+joinTDNF p (Choose qp qq) = I.eitherSecond >$< chooseTNF (joinTDNF p qp) (joinTDNF p qq)
+joinTDNF p Empty = Transform (I.invert I.fst) $ p
+joinTDNF Empty q = Transform (I.invert I.snd) $ q
+joinTDNF p q = Join p q
+
+-- |Convert a 'Free' to Transform Disjunctive Normal Form: reorder the terms so thet at most one 'Transform' is on the outside, followed by 'Choose' terms, which are above all 'Join' terms', with 'Empty' and 'Free' as leaves.
+-- Since each 'Join' above a 'Choose' creates a duplicate 'Join' term, the complexity and result size can be exponential (just as with boolean logic DNF).
+freeTDNF :: Free f a -> Free f a
+freeTDNF (Transform f p) = f >$< freeTDNF p
+freeTDNF (Join p q) = joinTDNF (freeTDNF p) (freeTDNF q)
+freeTDNF (Choose p q) = chooseTNF (freeTDNF p) (freeTDNF q)
+freeTDNF p = p
+
+pivot :: (a,(b,c)) I.<-> ((a,b),c)
+pivot = [I.biCase|(a,(b,c)) <-> ((a,b),c)|]
+
+swap12 :: (a,(b,c)) I.<-> (b,(a,c))
+swap12 = [I.biCase|(a,(b,c)) <-> (b,(a,c))|]
+
+sortJoinTDNF :: (forall a' b' . f a' -> f b' -> Ordering) -> Free f a -> Free f b -> Free f (a, b)
+sortJoinTDNF cmp (Transform f p) (Transform g q) = (f *** g) >$< sortJoinTDNF cmp p q
+sortJoinTDNF cmp (Transform f p) q = first f >$< sortJoinTDNF cmp p q
+sortJoinTDNF cmp p (Transform f q) = second f >$< sortJoinTDNF cmp p q
+sortJoinTDNF cmp (Choose pp pq) q = I.eitherFirst >$< chooseTNF (sortJoinTDNF cmp pp q) (sortJoinTDNF cmp pq q)
+sortJoinTDNF cmp p (Choose qp qq) = I.eitherSecond >$< chooseTNF (sortJoinTDNF cmp p qp) (sortJoinTDNF cmp p qq)
+sortJoinTDNF cmp (Join p q) r = pivot >$< sortJoinTDNF cmp p (sortJoinTDNF cmp q r)
+sortJoinTDNF cmp p@(Free x) q@(Free y) | cmp x y == GT = I.swap >$< Join q p
+sortJoinTDNF cmp p@(Free x) (Join q@(Free y) r) | cmp x y == GT = swap12 >$< joinTDNF q (sortJoinTDNF cmp p r)
+sortJoinTDNF cmp Empty p = I.invert I.snd >$< sortFreeTDNF cmp p
+sortJoinTDNF cmp p Empty = I.invert I.fst >$< sortFreeTDNF cmp p
+sortJoinTDNF _ p q = Join p q
+
+-- |Equivalent to 'freeTDNF', but also sorts the terms within each 'Join' clause to conform to the given ordering.
+-- The resulting 'Join' trees will be right-linearized (@Join x (Join y (Join z ...))@ such that @x <= y@, @y <= z@, etc.
+-- THis performs a /O(n^2)/ bubble sort on the already exponential TDNF.
+sortFreeTDNF :: (forall a' b' . f a' -> f b' -> Ordering) -> Free f a -> Free f a
+sortFreeTDNF cmp (Transform f p) = f >$< sortFreeTDNF cmp p
+sortFreeTDNF cmp (Choose p q) = chooseTNF (sortFreeTDNF cmp p) (sortFreeTDNF cmp q)
+sortFreeTDNF cmp (Join p q) = sortJoinTDNF cmp p (sortFreeTDNF cmp q)
+sortFreeTDNF _ p = p
diff --git a/Control/Invertible/Monoidal/HList.hs b/Control/Invertible/Monoidal/HList.hs
--- a/Control/Invertible/Monoidal/HList.hs
+++ b/Control/Invertible/Monoidal/HList.hs
@@ -1,6 +1,6 @@
 -- |
 -- Combine monoidal functors into HLists.
-{-# LANGUAGE DataKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE TypeOperators, DataKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TypeFamilies, UndecidableInstances #-}
 module Control.Invertible.Monoidal.HList
   ( hConsI
   , (>:*<)
diff --git a/Data/Invertible.hs b/Data/Invertible.hs
--- a/Data/Invertible.hs
+++ b/Data/Invertible.hs
@@ -20,6 +20,7 @@
   , module Data.Invertible.Functor
   , module Data.Invertible.List
   , module Data.Invertible.Maybe
+  , module Data.Invertible.Monad
   , module Data.Invertible.Monoid
   , module Data.Invertible.Ord
   , module Data.Invertible.Tuple
@@ -38,6 +39,7 @@
 import Data.Invertible.Functor
 import Data.Invertible.List
 import Data.Invertible.Maybe
+import Data.Invertible.Monad
 import Data.Invertible.Monoid
 import Data.Invertible.Ord
 import Data.Invertible.Tuple
diff --git a/Data/Invertible/Bijection.hs b/Data/Invertible/Bijection.hs
--- a/Data/Invertible/Bijection.hs
+++ b/Data/Invertible/Bijection.hs
@@ -1,6 +1,6 @@
 -- |
 -- The base representation for bidirectional arrows (bijections).
-{-# LANGUAGE Trustworthy, KindSignatures, FlexibleInstances, CPP #-}
+{-# LANGUAGE Trustworthy, TypeOperators, KindSignatures, FlexibleInstances, CPP #-}
 module Data.Invertible.Bijection
   ( Bijection(..)
   , type (<->)
diff --git a/Data/Invertible/Bits.hs b/Data/Invertible/Bits.hs
--- a/Data/Invertible/Bits.hs
+++ b/Data/Invertible/Bits.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Bits".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators #-}
 module Data.Invertible.Bits
   ( complement
   ) where
diff --git a/Data/Invertible/Bool.hs b/Data/Invertible/Bool.hs
--- a/Data/Invertible/Bool.hs
+++ b/Data/Invertible/Bool.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Bool".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators #-}
 module Data.Invertible.Bool
   ( not
   ) where
diff --git a/Data/Invertible/Coerce.hs b/Data/Invertible/Coerce.hs
--- a/Data/Invertible/Coerce.hs
+++ b/Data/Invertible/Coerce.hs
@@ -1,5 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Coerce".
+{-# LANGUAGE TypeOperators #-}
 module Data.Invertible.Coerce
   ( coerce
   ) where
diff --git a/Data/Invertible/Complex.hs b/Data/Invertible/Complex.hs
--- a/Data/Invertible/Complex.hs
+++ b/Data/Invertible/Complex.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Complex".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, QuasiQuotes, TypeOperators #-}
 module Data.Invertible.Complex
   ( complex
   , polar
diff --git a/Data/Invertible/Either.hs b/Data/Invertible/Either.hs
--- a/Data/Invertible/Either.hs
+++ b/Data/Invertible/Either.hs
@@ -1,12 +1,15 @@
 -- |
 -- Bidirectional version of "Data.Either".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, QuasiQuotes, TypeOperators #-}
 module Data.Invertible.Either
   ( switch
   , isLeft
   , isRight
   , lft
   , rgt
+  , eitherFirst
+  , eitherSecond
+  , pivotEither
   ) where
 
 import Prelude
@@ -52,4 +55,29 @@
   [biCase|
     Left () <-> Nothing
     Right a <-> Just a
+  |]
+
+-- |Lift an either out of the first component of a tuple.
+eitherFirst :: Either (a, c) (b, c) <-> (Either a b, c)
+eitherFirst =
+  [biCase|
+    Left  (a, c) <-> (Left  a, c)
+    Right (b, c) <-> (Right b, c)
+  |]
+
+-- |Lift an either out of the second component of a tuple.
+eitherSecond :: Either (a, b) (a, c) <-> (a, Either b c)
+eitherSecond =
+  [biCase|
+    Left  (a, b) <-> (a, Left  b)
+    Right (a, c) <-> (a, Right c)
+  |]
+
+-- |Pivot nested either terms between right and left (lacking a standard 3-sum representation).
+pivotEither :: Either a (Either b c) <-> Either (Either a b) c
+pivotEither =
+  [biCase|
+    Left a <-> Left (Left a)
+    Right (Left a) <-> Left (Right a)
+    Right (Right a) <-> Right a
   |]
diff --git a/Data/Invertible/Enum.hs b/Data/Invertible/Enum.hs
new file mode 100644
--- /dev/null
+++ b/Data/Invertible/Enum.hs
@@ -0,0 +1,20 @@
+-- |
+-- Bidirectional versions of 'Enum' functions.
+{-# LANGUAGE Safe, TypeOperators #-}
+module Data.Invertible.Enum
+  ( enum
+  , succ
+  ) where
+
+import qualified Prelude
+import Prelude hiding (succ)
+
+import Data.Invertible.Bijection
+
+-- |Convert between an 'Int' and an 'Enum' with 'P.toEnum' and 'P.fromEnum'.
+enum :: Enum a => Int <-> a
+enum = toEnum :<->: fromEnum
+
+-- |Combine 'Prelude.succ' and 'pred'
+succ :: Enum a => a <-> a
+succ = Prelude.succ :<->: pred
diff --git a/Data/Invertible/Function.hs b/Data/Invertible/Function.hs
--- a/Data/Invertible/Function.hs
+++ b/Data/Invertible/Function.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Function".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators #-}
 module Data.Invertible.Function
   ( id
   , (.)
diff --git a/Data/Invertible/Functor.hs b/Data/Invertible/Functor.hs
--- a/Data/Invertible/Functor.hs
+++ b/Data/Invertible/Functor.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Functor".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, QuasiQuotes, TypeOperators #-}
 module Data.Invertible.Functor
   ( bifmap
   , identity
diff --git a/Data/Invertible/HList.hs b/Data/Invertible/HList.hs
--- a/Data/Invertible/HList.hs
+++ b/Data/Invertible/HList.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.HList.HList".
-{-# LANGUAGE DataKinds, FlexibleContexts #-}
+{-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators, FlexibleContexts #-}
 module Data.Invertible.HList
   ( hCons
   , hReverse
diff --git a/Data/Invertible/Invariant.hs b/Data/Invertible/Invariant.hs
--- a/Data/Invertible/Invariant.hs
+++ b/Data/Invertible/Invariant.hs
@@ -1,5 +1,6 @@
 -- |
 -- Use bijections on 'Invariant' functors from "Data.Functor.Invariant".
+{-# LANGUAGE TypeOperators #-}
 module Data.Invertible.Invariant
   ( invmap
   ) where
diff --git a/Data/Invertible/Lens.hs b/Data/Invertible/Lens.hs
--- a/Data/Invertible/Lens.hs
+++ b/Data/Invertible/Lens.hs
@@ -1,6 +1,6 @@
 -- |
 -- Convert bijections to and from lens isomorphisms in "Control.Lens.Iso".
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RankNTypes, TypeOperators #-}
 module Data.Invertible.Lens
   ( toIso
   , unIso
diff --git a/Data/Invertible/List.hs b/Data/Invertible/List.hs
--- a/Data/Invertible/List.hs
+++ b/Data/Invertible/List.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.List" and other operations over lists.
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, QuasiQuotes, TypeOperators #-}
 module Data.Invertible.List
   ( cons
   , uncons
@@ -9,6 +9,8 @@
   , map
   , reverse
   , transpose
+  , lookup
+  , index
   , zip
   , zip3
   , zip4
@@ -21,9 +23,10 @@
   , words
   ) where
 
-import Prelude hiding (map, reverse, zip, zip3, unzip, zipWith, lines, words)
+import Prelude hiding (map, reverse, lookup, zip, zip3, unzip, zipWith, lines, words)
 import Control.Arrow ((***))
 import qualified Data.List as L
+import Data.Tuple (swap)
 
 import Data.Invertible.Bijection
 import Data.Invertible.TH
@@ -64,6 +67,18 @@
 -- |'L.transpose' the rows and columns of its argument.
 transpose :: [[a]] <-> [[a]]
 transpose = involution L.transpose
+
+-- |Bi-directional 'L.lookup'.
+lookup :: (Eq a, Eq b) => [(a, b)] -> Maybe a <-> Maybe b
+lookup l = (flip L.lookup l =<<) :<->: (flip L.lookup (L.map swap l) =<<)
+
+-- |Combine 'L.elemIndex' and safe 'L.!!'.
+index :: Eq a => [a] -> Maybe a <-> Maybe Int
+index l = (flip L.elemIndex l =<<) :<->: (idx l =<<) where
+  idx _ i | i < 0 = Nothing
+  idx [] _ = Nothing
+  idx (x:_) 0 = Just x
+  idx (_:r) i = idx r $ pred i
 
 -- |'L.zip' two lists together.
 zip :: ([a], [b]) <-> [(a, b)]
diff --git a/Data/Invertible/Maybe.hs b/Data/Invertible/Maybe.hs
--- a/Data/Invertible/Maybe.hs
+++ b/Data/Invertible/Maybe.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Maybe".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators, QuasiQuotes #-}
 module Data.Invertible.Maybe
   ( isJust
   , isNothing
@@ -31,11 +31,11 @@
     Just () <-> False
   |]
 
--- |Convert between (the head of) a (singleton) list and 'Maybe' (see 'M.listToMaybe'). (@'Control.Invertible.BiArrow.inv' 'maybeToList'@)
+-- |Convert between (the head of) a (singleton) list and 'Maybe' (see 'M.listToMaybe'). (@'Control.Invertible.BiArrow.invert' 'maybeToList'@)
 listToMaybe :: [a] <-> Maybe a
 listToMaybe = M.listToMaybe :<->: M.maybeToList
 
--- |Convert between 'Maybe' and a (singleton) list (see 'M.maybeToList'). (@'Control.Invertible.BiArrow.inv' 'listToMaybe'@)
+-- |Convert between 'Maybe' and a (singleton) list (see 'M.maybeToList'). (@'Control.Invertible.BiArrow.invert' 'listToMaybe'@)
 maybeToList :: Maybe a <-> [a]
 maybeToList = invert listToMaybe
 
diff --git a/Data/Invertible/Monad.hs b/Data/Invertible/Monad.hs
new file mode 100644
--- /dev/null
+++ b/Data/Invertible/Monad.hs
@@ -0,0 +1,27 @@
+-- |
+-- Using bijections with monads.
+{-# LANGUAGE Safe, TypeOperators #-}
+module Data.Invertible.Monad
+  ( bind
+  , (=<<->>=)
+  , liftM
+  ) where
+
+import qualified Control.Monad as M
+
+import Data.Invertible.Bijection
+
+-- |Bind two functions to create a 'Control.Invertible.MonadArrow.BiKleisli'-form bijection.
+bind :: Monad m => (a -> m b) -> (b -> m a) -> m a <-> m b
+bind f g = (f =<<) :<->: (g =<<)
+
+-- |Crazy operator form of 'bind'.
+(=<<->>=) :: Monad m => (a -> m b) -> (b -> m a) -> m a <-> m b
+(=<<->>=) = bind
+
+infix 2 =<<->>=
+
+-- |Promote a bijection to a 'Control.Invertible.MonadArrow.BiKleisli'-form bijection.
+-- (Equivalent to 'Data.Invertible.Functor.bifmap'.)
+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,6 +1,6 @@
 -- |
 -- Bidirectional transforms for "Data.Monoid".
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators, QuasiQuotes #-}
 module Data.Invertible.Monoid
   ( BiEndo(..)
   , dual
diff --git a/Data/Invertible/Ord.hs b/Data/Invertible/Ord.hs
--- a/Data/Invertible/Ord.hs
+++ b/Data/Invertible/Ord.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional operations over 'Ordering'.
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators, QuasiQuotes #-}
 module Data.Invertible.Ord
   ( down
   ) where
diff --git a/Data/Invertible/PartialIsomorphism.hs b/Data/Invertible/PartialIsomorphism.hs
--- a/Data/Invertible/PartialIsomorphism.hs
+++ b/Data/Invertible/PartialIsomorphism.hs
@@ -1,5 +1,6 @@
 -- |
 -- Convert bijections to and from (total) 'P.Iso'.
+{-# LANGUAGE TypeOperators #-}
 module Data.Invertible.PartialIsomorphism
   ( toIso
   , fromIso
diff --git a/Data/Invertible/Piso.hs b/Data/Invertible/Piso.hs
--- a/Data/Invertible/Piso.hs
+++ b/Data/Invertible/Piso.hs
@@ -1,5 +1,6 @@
 -- |
 -- Convert bijections to and from (total) 'P.Piso'.
+{-# LANGUAGE TypeOperators #-}
 module Data.Invertible.Piso
   ( toPiso
   , fromPiso
diff --git a/Data/Invertible/Prelude.hs b/Data/Invertible/Prelude.hs
--- a/Data/Invertible/Prelude.hs
+++ b/Data/Invertible/Prelude.hs
@@ -1,18 +1,18 @@
 -- |
 -- The bidirectional \"Prelude\", which re-exports various bijections similar to functions from "Prelude".
 -- Most \"un\"-functions are left out for obvious reasons.
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators #-}
 module Data.Invertible.Prelude
   ( (<->)
   , type (<->)
 
-  , enum
-
   , const
   , flip
   , id
   , (.)
   , not
+  , enum
+  , succ
   , fst
   , snd
   , curry
@@ -30,17 +30,14 @@
   , words
   ) where
 
-import Prelude hiding (not, id, (.), const, flip, Functor(..), (<$>), fst, snd, curry, uncurry, map, reverse, zip, zip3, unzip, zipWith, lines, words)
+import Prelude hiding (not, id, (.), const, succ, flip, Functor(..), (<$>), fst, snd, curry, uncurry, map, reverse, zip, zip3, unzip, zipWith, lines, words)
 
 import Control.Invertible.BiArrow
 import Control.Invertible.Functor
 import Data.Invertible.Bijection
 import Data.Invertible.Bool
+import Data.Invertible.Enum
 import Data.Invertible.Function
 import Data.Invertible.Functor
 import Data.Invertible.Tuple
 import Data.Invertible.List
-
--- |Convert between an 'Int' and an 'Enum' with 'P.toEnum' and 'P.fromEnum'.
-enum :: Enum a => Int <-> a
-enum = toEnum :<->: fromEnum
diff --git a/Data/Invertible/Tuple.hs b/Data/Invertible/Tuple.hs
--- a/Data/Invertible/Tuple.hs
+++ b/Data/Invertible/Tuple.hs
@@ -1,6 +1,6 @@
 -- |
 -- Bidirectional version of "Data.Tuple" and other operations over nested tuples.
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Safe, TypeOperators, QuasiQuotes #-}
 module Data.Invertible.Tuple
   ( fst
   , snd
diff --git a/invertible.cabal b/invertible.cabal
--- a/invertible.cabal
+++ b/invertible.cabal
@@ -1,5 +1,5 @@
 name:                invertible
-version:             0.1
+version:             0.1.1
 synopsis:            bidirectional arrows, bijective functions, and invariant functors
 description:
   Representations and operations for bidirectional arrows (total isomorphisms: an
@@ -49,10 +49,12 @@
     Data.Invertible.Coerce
     Data.Invertible.Complex
     Data.Invertible.Either
+    Data.Invertible.Enum
     Data.Invertible.Function
     Data.Invertible.Functor
     Data.Invertible.List
     Data.Invertible.Maybe
+    Data.Invertible.Monad
     Data.Invertible.Monoid
     Data.Invertible.Ord
     Data.Invertible.Tuple
@@ -62,13 +64,14 @@
     Control.Invertible.MonadArrow
     Control.Invertible.Functor
     Control.Invertible.Monoidal
+    Control.Invertible.Monoidal.Free
 
   build-depends:
     base >= 4.8 && <5,
+    transformers,
     haskell-src-meta == 0.6.*,
     template-haskell == 2.*
   default-language:    Haskell2010
-  default-extensions: TypeOperators, QuasiQuotes
   ghc-options: -Wall
 
   if flag(arrows)
@@ -95,3 +98,15 @@
   if flag(TypeCompose)
     exposed-modules: Data.Invertible.TypeCompose
     build-depends: TypeCompose >= 0.3
+
+test-suite tests
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Main.hs
+  default-language: Haskell2010
+  ghc-options: -Wall
+  build-depends:
+    base,
+    transformers,
+    QuickCheck,
+    invertible
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 System.Exit (exitSuccess, exitFailure)
+import qualified Test.QuickCheck as Q
+import Test.QuickCheck.Test (isSuccess)
+
+import qualified FreeMonoidal
+
+tests :: Q.Property
+tests = FreeMonoidal.tests
+
+main :: IO ()
+main = do
+  r <- Q.quickCheckWithResult Q.stdArgs{ Q.maxSize = 27, Q.maxSuccess = 1000 } tests
+  if isSuccess r
+    then exitSuccess
+    else exitFailure