diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,26 @@
-# Revision history for possibly-can
+# Revision history for smash
 
-## 0.1.0.0 -- YYYY-mm-dd
+## 0.1.3 -- 2022-04-03
+
+* Update `base` bounds to allow GHC 9.2.x
+
+## 0.1.2
+
+* Add Monad Transformers for `Can`, `Wedge`, and `Smash` ([#25](https://github.com/emilypi/smash/pull/25))
+* Add Safe haskell pragmas
+* Add instances for all functor classes.
+* Add instances for `MonadZip`
+* Add nice pointfree definitions for some functions ([#24](https://github.com/emilypi/smash/pull/24), thanks @subttle!)
+* Add unfolds to the Api.
+* Add template haskell `Lift` instance ([#20](https://github.com/emilypi/smash/pull/20), thanks @gergoerdi!)
+* Fixes for various haddock problems (thank you @lemastero and @L7R7!)
+* Bump base to exclude 8.2.x
+
+## 0.1.1
+
+* Add `NFData`, `Binary` instances
+* CPP to extend to 8.2.2 without warnings
+
+## 0.1.0.0
 
 * First version. Released on an unsuspecting world.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,1 +1,45 @@
-# Smash-core: smash products in Hask
+# smash: Combinators for Maybe types
+
+[![Build Status](https://travis-ci.com/emilypi/smash.svg?branch=master)](https://travis-ci.com/emilypi/smash)
+[![Hackage](https://img.shields.io/hackage/v/smash.svg)](https://hackage.haskell.org/package/smash)
+
+This package consists of 3 interesting datatypes and their respective monad transformers:
+
+ - [Wedge](https://hackage.haskell.org/package/smash/docs/Data-Wedge.html): Isomorphic to `Maybe (Either a b)`. The `Wedge` datatype represents the coproduct in the category Hask\* of pointed Hask types, called a [wedge sum](https://ncatlab.org/nlab/show/wedge+sum). One can derive this type as follows:
+
+    ```haskell
+    Either (Maybe a) (Maybe b)
+    ~ (1 + a) + (1 + b)
+    -- units are the same via pushout
+    ~ 1 + a + b
+    ~ Maybe (Either a b)
+    ~ Wedge a b
+    ```
+
+ - [Can](https://hackage.haskell.org/package/smash/docs/Data-Can.html): Isomorphic to `Maybe (These a b)`. The `Can` datatype represents the product in Hask\*. One can derive this as follows:
+
+    ```haskell
+    (Maybe a, Maybe a)
+    ~ (1 + a) * (1 + b)
+    -- products distribute over coproducts
+    ~ 1 + b + a + a*b
+    -- coproducts are associative
+    ~ 1 + (b + a + a*b)
+    ~ 1 + These a b
+    ~ Maybe (These a b)
+    ~ Can a b
+    ```
+
+ - [Smash](https://hackage.haskell.org/package/smash/docs/Data-Smash.html): Isomorphic to `Maybe (a,b)`. The `Smash` datatype represents a special type of product, a
+[smash product](https://ncatlab.org/nlab/show/smash+product), in the category Hask\*.  The smash product is a symmetric, monoidal tensor in Hask* that is the quotient of `Can` over `Wedge`. It can be derived as follows:
+
+    ```haskell
+    Can a b / Wedge a b
+    ~ 1 + a + b + a*b / 1 + a + b
+    -- reassoc coproduct
+    ~ (1 + a + b) + a*b / 1 + a + b
+    -- def. of quotient: (1 + a + b) ~ 1
+    ~ 1 + a * b
+    ~ Maybe (a,b)
+    ~ Smash a b
+    ```
diff --git a/smash.cabal b/smash.cabal
--- a/smash.cabal
+++ b/smash.cabal
@@ -1,71 +1,50 @@
-cabal-version:       2.0
-
-
-name:                smash
-version:             0.1.0.0
-synopsis:            Smash products - like 'These', but with a unit!
+cabal-version:      2.0
+name:               smash
+version:            0.1.3
+synopsis:           Combinators for Maybe types
 description:
   Smash products are like the 'These' datatype, only with a unit. You can
   think of this type as isomorphic to 'Maybe (These a b)'.
 
-homepage:            https://github.com/emilypi/smash
-bug-reports:         https://github.com/emilypi/smash/issues
-license:             BSD3
-license-file:        LICENSE
-author:              Emily Pillmore
-maintainer:          emilypi@cohomolo.gy
-copyright:           (c) 2020 Emily Pillmore <emilypi@cohomolo.gy>
-category:            Data
-build-type:          Simple
+homepage:           https://github.com/emilypi/smash
+bug-reports:        https://github.com/emilypi/smash/issues
+license:            BSD3
+license-file:       LICENSE
+author:             Emily Pillmore
+maintainer:         emilypi@cohomolo.gy
+copyright:          (c) 2020-2022 Emily Pillmore <emilypi@cohomolo.gy>
+category:           Data
+build-type:         Simple
 extra-source-files:
   CHANGELOG.md
   README.md
 
 tested-with:
-  GHC ==8.2.2 || ==8.4.3 || ==8.4.4 || ==8.6.3 || ==8.6.5 || ==8.8.3 || ==8.10.1
-
+  GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.2
 
 source-repository head
   type:     git
   location: https://github.com/emilypi/smash.git
 
-
-flag ghc-flags
-  description: Generate .ghc.flags files during compilation
-  manual:      True
-  default:     False
-
-flag perf-flags
-  description: Performance tuning flags
-  manual:      True
-  default:     False
-
 library
-  exposed-modules:     Data.Can
-                     , Data.Smash
-                     , Data.Wedge
-  -- other-modules:
-  -- other-extensions:
-  build-depends:       base >=4.10 && <5.0
-                     , bifunctors
-                     , hashable
-
-  hs-source-dirs:      src
-  default-language:    Haskell2010
-  ghc-options:         -Wall
-
-  if flag(ghc-flags)
-    build-tool-depends: hsinspect:hsinspect
-    build-depends: ghcflags
-    ghc-options: -fplugin GhcFlags.Plugin
-
-  if flag(perf-flags)
-    ghc-options: -ddump-simpl -ddump-to-file
+  exposed-modules:
+    Control.Monad.Trans.Can
+    Control.Monad.Trans.Smash
+    Control.Monad.Trans.Wedge
+    Data.Can
+    Data.Smash
+    Data.Wedge
 
+  other-modules:    Data.Smash.Internal
+  build-depends:
+      base             >=4.12 && <4.17
+    , bifunctors       ^>=5.5
+    , binary           ^>=0.8
+    , deepseq          ^>=1.4
+    , hashable         ^>=1.3
+    , mtl
+    , template-haskell >=2.2 && < 3.0
 
-test-suite tasty
-  default-language:    Haskell2010
-  type:                exitcode-stdio-1.0
-  hs-source-dirs:      test
-  main-is:             MyLibTest.hs
-  build-depends:       base >=4.10 && <5.0
+  hs-source-dirs:   src
+  default-language: Haskell2010
+  ghc-options:      -Wall
diff --git a/src/Control/Monad/Trans/Can.hs b/src/Control/Monad/Trans/Can.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Can.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# language Safe #-}
+-- |
+-- Module       : Control.Monad.Trans.Can
+-- Copyright    : (c) 2020-2022 Emily Pillmore
+-- License      : BSD-3-Clause
+--
+-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>
+-- Stability    : Experimental
+-- Portability  : Non-portable
+--
+-- This module contains utilities for the monad transformer
+-- for the pointed product.
+--
+module Control.Monad.Trans.Can
+( -- * Monad Transformer
+  CanT(..)
+  -- ** Combinators
+, mapCanT
+) where
+
+
+import Data.Can
+import Control.Applicative (liftA2)
+import Control.Monad.Writer
+import Control.Monad.Reader
+import Control.Monad.State.Class
+import Control.Monad.Except
+import Control.Monad.RWS
+
+-- | A monad transformer for the pointed product,
+-- parameterized by:
+--
+--   * @a@ - the value on the left
+--   * @b@ - the value on the right
+--   * @m@ - The monad over a pointed product (see: 'Can').
+--
+-- This monad transformer is similar to 'TheseT',
+-- except with the possibility of an empty unital value.
+--
+newtype CanT a m b = CanT { runCanT :: m (Can a b) }
+
+-- | Map both the left and right values and output of a computation using
+-- the given function.
+--
+-- * @'runCanT' ('mapCanT' f m) = f . 'runCanT' m@
+--
+mapCanT :: (m (Can a b) -> n (Can c d)) -> CanT a m b -> CanT c n d
+mapCanT f = CanT . f . runCanT
+
+instance Functor f => Functor (CanT a f) where
+  fmap f = CanT . fmap (fmap f) . runCanT
+
+instance (Semigroup a, Applicative f) => Applicative (CanT a f) where
+  pure = CanT . pure . pure
+  CanT f <*> CanT a = CanT $ liftA2 (<*>) f a
+
+instance (Semigroup a, Monad m) => Monad (CanT a m) where
+  return = pure
+
+  CanT m >>= k = CanT $ do
+    c <- m
+    case c of
+      Eno a -> runCanT $ k a
+      Two a b -> do
+        c' <- runCanT $ k b
+        return $ case c' of
+          Eno b' -> Two a b'
+          Two a' b' -> Two (a <> a') b'
+          _ -> c'
+      One a -> return $ One a
+      Non -> return Non
+
+instance (Semigroup a, MonadWriter w m) => MonadWriter w (CanT a m) where
+  tell = lift . tell
+
+  listen (CanT m) = CanT $ go <$> listen m where
+    go (c,w) = case c of
+      Non -> Non
+      One a -> One a
+      Eno b -> Eno (b,w)
+      Two a b -> Two a (b, w)
+
+  pass (CanT m) = CanT $ pass (go <$> m) where -- collect $200.
+    go = \case
+      Non -> (Non, id)
+      One a -> (One a, id)
+      Eno (a,f) -> (Eno a, f)
+      Two w (a,f) -> (Two w a, f)
+
+
+instance (Semigroup a, MonadReader r m) => MonadReader r (CanT a m) where
+  ask = lift ask
+  local f (CanT m) = CanT (local f m)
+
+instance (MonadState s m, Semigroup t) => MonadState s (CanT t m) where
+  get = lift get
+  put = lift . put
+
+instance (Semigroup t, MonadRWS r w s m) => MonadRWS r w s (CanT t m)
+
+instance MonadTrans (CanT a) where
+  lift = CanT . fmap Eno
+
+instance (MonadError e m, Semigroup e) => MonadError e (CanT e m) where
+  throwError = lift . throwError
+  catchError (CanT m) f = CanT $ catchError m (runCanT . f)
diff --git a/src/Control/Monad/Trans/Smash.hs b/src/Control/Monad/Trans/Smash.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Smash.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# language Safe #-}
+-- |
+-- Module       : Control.Monad.Trans.Smash
+-- Copyright    : (c) 2020-2022 Emily Pillmore
+-- License      : BSD-3-Clause
+--
+-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>
+-- Stability    : Experimental
+-- Portability  : Non-portable
+--
+-- This module contains utilities for the monad transformer
+-- for the smash product.
+--
+module Control.Monad.Trans.Smash
+( -- * Monad transformer
+  SmashT(..)
+  -- ** Combinators
+, mapSmashT
+) where
+
+
+import Data.Smash
+
+import Control.Applicative (liftA2)
+import Control.Monad.Writer
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.RWS
+
+
+-- | A monad transformer for the smash product,
+-- parameterized by:
+--
+--   * @a@ - the value on the left
+--   * @b@ - the value on the right
+--   * @m@ - The monad over a pointed product (see: 'Smash').
+--
+newtype SmashT a m b = SmashT { runSmashT :: m (Smash a b) }
+
+-- | Map both the left and right values and output of a computation using
+-- the given function.
+--
+-- * @'runSmashT' ('mapSmashT' f m) = f . 'runSmashT' m@
+--
+mapSmashT :: (m (Smash a b) -> n (Smash c d)) -> SmashT a m b -> SmashT c n d
+mapSmashT f = SmashT . f . runSmashT
+
+instance Functor f => Functor (SmashT a f) where
+  fmap f = SmashT . fmap (fmap f) . runSmashT
+
+instance (Monoid a, Applicative f) => Applicative (SmashT a f) where
+  pure = SmashT . pure . pure
+  SmashT f <*> SmashT a = SmashT $ liftA2 (<*>) f a
+
+instance (Monoid a, Monad m) => Monad (SmashT a m) where
+  return = pure
+
+  SmashT m >>= k = SmashT $ do
+    c <- m
+    case c of
+      Smash a b -> do
+        c' <- runSmashT $ k b
+        return $ case c' of
+          Nada -> Nada
+          Smash a' b' -> Smash (a <> a') b'
+      Nada -> return Nada
+
+instance (Monoid a, MonadReader r m) => MonadReader r (SmashT a m) where
+  ask = lift ask
+  local f (SmashT m) = SmashT $ local f m
+
+instance (Monoid a, MonadWriter w m) => MonadWriter w (SmashT a m) where
+  tell = lift . tell
+
+  listen (SmashT m) = SmashT $ go <$> listen m where
+    go (c,w) = case c of
+      Nada -> Nada
+      Smash a b -> Smash a (b, w)
+
+  pass (SmashT m) = SmashT $ pass (go <$> m) where
+    go = \case
+      Nada -> (Nada, id)
+      Smash t (a, f) -> (Smash t a, f)
+
+instance (Monoid t, MonadState s m) => MonadState s (SmashT t m) where
+  get = lift get
+  put = lift . put
+
+instance (Monoid t, MonadRWS r w s m) => MonadRWS r w s (SmashT t m)
+
+instance Monoid a => MonadTrans (SmashT a) where
+  lift = SmashT . fmap (Smash mempty)
diff --git a/src/Control/Monad/Trans/Wedge.hs b/src/Control/Monad/Trans/Wedge.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Wedge.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# language Safe #-}
+-- |
+-- Module       : Control.Monad.Trans.Wedge
+-- Copyright    : (c) 2020-2022 Emily Pillmore
+-- License      : BSD-3-Clause
+--
+-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>
+-- Stability    : Experimental
+-- Portability  : Non-portable
+--
+-- This module contains utilities for the monad transformer
+-- for the pointed coproduct.
+--
+module Control.Monad.Trans.Wedge
+( -- * Monad transformer
+  WedgeT(..)
+  -- ** Combinators
+, mapWedgeT
+) where
+
+
+import Data.Wedge
+import Control.Applicative (liftA2)
+import Control.Monad.Writer
+import Control.Monad.Reader
+import Control.Monad.State.Class
+import Control.Monad.Except
+import Control.Monad.RWS
+
+-- | A monad transformer for the pointed product,
+-- parameterized by:
+--
+--   * @a@ - the value on the left
+--   * @b@ - the value on the right
+--   * @m@ - The monad over a pointed coproduct (see: 'Wedge').
+--
+-- This monad transformer is similar to 'ExceptT',
+-- except with the possibility of an empty unital value.
+--
+newtype WedgeT a m b = WedgeT { runWedgeT :: m (Wedge a b) }
+
+-- | Map both the left and right values and output of a computation using
+-- the given function.
+--
+-- * @'runWedgeT' ('mapWedgeT' f m) = f . 'runWedgeT' m@
+--
+mapWedgeT :: (m (Wedge a b) -> n (Wedge c d)) -> WedgeT a m b -> WedgeT c n d
+mapWedgeT f = WedgeT . f . runWedgeT
+
+
+instance Functor f => Functor (WedgeT a f) where
+  fmap f = WedgeT . fmap (fmap f) . runWedgeT
+
+instance (Semigroup a, Applicative f) => Applicative (WedgeT a f) where
+  pure = WedgeT . pure . pure
+  WedgeT f <*> WedgeT a = WedgeT $ liftA2 (<*>) f a
+
+instance (Semigroup a, Monad m) => Monad (WedgeT a m) where
+  return = pure
+
+  WedgeT m >>= k = WedgeT $ do
+    c <- m
+    case c of
+      Nowhere -> return Nowhere
+      Here a -> return $ Here a
+      There a -> runWedgeT $ k a
+
+instance (MonadReader r m, Semigroup t) => MonadReader r (WedgeT t m) where
+  ask = lift ask
+  local f (WedgeT m) = WedgeT $ local f m
+
+instance (MonadWriter w m, Semigroup t) => MonadWriter w (WedgeT t m) where
+  tell = lift . tell
+
+  listen (WedgeT m) = WedgeT $ go <$> listen m where
+    go = \case
+      (Nowhere, _) -> Nowhere
+      (Here t, _) -> Here t
+      (There a, w) -> There (a, w)
+
+  pass (WedgeT m) = WedgeT $ pass (go <$> m) where
+    go = \case
+     Nowhere -> (Nowhere, id)
+     Here w -> (Here w, id)
+     There (a,f) -> (There a, f)
+
+instance (MonadState s m, Semigroup t) => MonadState s (WedgeT t m) where
+  get = lift get
+  put = lift . put
+
+instance (Semigroup t, MonadRWS r w s m) => MonadRWS r w s (WedgeT t m)
+
+instance MonadTrans (WedgeT a) where
+  lift = WedgeT . fmap There
+
+instance (MonadError e m, Semigroup e) => MonadError e (WedgeT e m) where
+  throwError e = WedgeT $ Here <$> throwError e
+  catchError (WedgeT m) f = WedgeT $ catchError m (runWedgeT . f)
diff --git a/src/Data/Can.hs b/src/Data/Can.hs
--- a/src/Data/Can.hs
+++ b/src/Data/Can.hs
@@ -1,25 +1,33 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE Safe #-}
 -- |
 -- Module       : Data.Can
--- Copyright    : (c) 2020 Emily Pillmore
+-- Copyright    : (c) 2020-2022 Emily Pillmore
 -- License      : BSD-3-Clause
 --
 -- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>
 -- Stability    : Experimental
--- Portability  : portable
+-- Portability  : CPP, RankNTypes, TypeApplications
 --
 -- This module contains the definition for the 'Can' datatype. In
 -- practice, this type is isomorphic to 'Maybe' 'These' - the type with
 -- two possibly non-exclusive values and an empty case.
+--
 module Data.Can
 ( -- * Datatypes
   -- $general
   Can(..)
+  -- ** Type synonyms
+, type (⊗)
   -- * Combinators
 , canFst
 , canSnd
@@ -29,11 +37,20 @@
 , isNon
   -- ** Eliminators
 , can
-  -- * Folding
+, canWithMerge
+, canEach
+, canEachA
+  -- * Folding and Unfolding
 , foldOnes
 , foldEnos
 , foldTwos
 , gatherCans
+, unfoldr
+, unfoldrM
+, iterateUntil
+, iterateUntilM
+, accumUntil
+, accumUntilM
   -- * Filtering
 , ones
 , enos
@@ -50,6 +67,7 @@
 , partitionAll
 , partitionEithers
 , mapCans
+, eqCan
   -- * Distributivity
 , distributeCan
 , codistributeCan
@@ -61,25 +79,43 @@
 ) where
 
 
-import Control.Applicative (Alternative(..))
+import Control.Applicative (Alternative(..), liftA2)
+import Control.DeepSeq
+import Control.Monad.Zip
+import Control.Monad
 
-import Data.Bifunctor
+import Data.Biapplicative
 import Data.Bifoldable
+import Data.Binary (Binary(..))
 import Data.Bitraversable
 import Data.Data
 import qualified Data.Either as E
+import Data.Functor.Classes
+import Data.Functor.Contravariant (Equivalence(..))
 import Data.Foldable
+import Data.Functor.Identity
 import Data.Hashable
+import Data.Hashable.Lifted
 
 import GHC.Generics
+import GHC.Read
 
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Data.Smash.Internal
+
+import Text.Read hiding (get)
+
+
+
+
 {- $general
 
 Categorically, the 'Can' datatype represents the
 <https://ncatlab.org/nlab/show/pointed+object#limits_and_colimits pointed product>
 in the category Hask* of pointed Hask types. The category Hask* consists of
 Hask types affixed with a dedicated base point of an object along with the object - i.e. @'Maybe' a@ in Hask. Hence, the product is
-@(1 + a) * (1 + b) ~ 1 + a + b + a*b@, or @'Maybe' ('Either' ('Either' a b) (a,b))@ in Hask. Pictorially, you can visualize
+@(1 + a) * (1 + b) ~ 1 + a + b + a*b@, or @'Maybe' ('These' a b)@ in Hask. Pictorially, you can visualize
 this as:
 
 
@@ -98,7 +134,7 @@
 coproduct in Hask*, called 'Wedge'. Namely, facts about currying
 @Can a b -> c ~ a -> b -> c@ and distributivity over 'Wedge'
 along with other facts about its associativity, commutativity, and
-any other analogy with '(,)' that you can think of.
+any other analogy with @(',')@ that you can think of.
 -}
 
 
@@ -112,8 +148,13 @@
     ( Eq, Ord, Read, Show
     , Generic, Generic1
     , Typeable, Data
+    , TH.Lift
     )
 
+-- | A type operator synonym for 'Can'
+--
+type a ⊗ b = Can a b
+
 -- -------------------------------------------------------------------- --
 -- Eliminators
 
@@ -135,11 +176,56 @@
 can _ _ g _ (Eno b) = g b
 can _ _ _ h (Two a b) = h a b
 
+-- | Case elimination for the 'Can' datatype, with uniform behaviour.
+--
+canWithMerge
+    :: c
+      -- ^ default value to supply for the 'Non' case
+    -> (a -> c)
+      -- ^ eliminator for the 'One' case
+    -> (b -> c)
+      -- ^ eliminator for the 'Eno' case
+    -> (c -> c -> c)
+      -- ^ merger for the 'Two' case
+    -> Can a b
+    -> c
+canWithMerge c _ _ _ Non = c
+canWithMerge _ f _ _ (One a) = f a
+canWithMerge _ _ g _ (Eno b) = g b
+canWithMerge _ f g m (Two a b) = m (f a) (g b)
+
+-- | Case elimination for the 'Can' datatype, with uniform behaviour over a
+-- 'Monoid' result.
+--
+canEach
+    :: Monoid c
+    => (a -> c)
+      -- ^ eliminator for the 'One' case
+    -> (b -> c)
+      -- ^ eliminator for the 'Eno' case
+    -> Can a b
+    -> c
+canEach f g = canWithMerge mempty f g (<>)
+
+-- | Case elimination for the 'Can' datatype, with uniform behaviour over a
+-- 'Monoid' result in the context of an 'Applicative'.
+--
+canEachA
+    :: Applicative m
+    => Monoid c
+    => (a -> m c)
+      -- ^ eliminator for the 'One' case
+    -> (b -> m c)
+      -- ^ eliminator for the 'Eno' case
+    -> Can a b
+    -> m c
+canEachA f g = canWithMerge (pure mempty) f g (liftA2 (<>))
+
 -- -------------------------------------------------------------------- --
 -- Combinators
 
 -- | Project the left value of a 'Can' datatype. This is analogous
--- to 'fst' for '(,)'.
+-- to 'fst' for @(',')@.
 --
 canFst :: Can a b -> Maybe a
 canFst = \case
@@ -148,7 +234,7 @@
   _ -> Nothing
 
 -- | Project the right value of a 'Can' datatype. This is analogous
--- to 'snd' for '(,)'.
+-- to 'snd' for @(',')@.
 --
 canSnd :: Can a b -> Maybe b
 canSnd = \case
@@ -283,6 +369,79 @@
 gatherCans (Eno bs) = fmap Eno bs
 gatherCans (Two as bs) = zipWith Two as bs
 
+-- | Unfold from right to left into a pointed product. For a variant
+-- that accumulates in the seed instead of just updating with a
+-- new value, see 'accumUntil' and 'accumUntilM'.
+--
+unfoldr :: Alternative f => (b -> Can a b) -> b -> f a
+unfoldr f = runIdentity . unfoldrM (pure . f)
+
+-- | Unfold from right to left into a monadic computation over a pointed product
+--
+unfoldrM :: (Monad m, Alternative f) => (b -> m (Can a b)) -> b -> m (f a)
+unfoldrM f b = f b >>= \case
+    Non -> pure empty
+    One a -> (pure a <|>) <$> unfoldrM f b
+    Eno b' -> unfoldrM f b'
+    Two a b' -> (pure a <|>) <$> unfoldrM f b'
+
+-- | Iterate on a seed, accumulating a result. See 'iterateUntilM' for
+-- more details.
+--
+iterateUntil :: Alternative f => (b -> Can a b) -> b -> f a
+iterateUntil f = runIdentity . iterateUntilM (pure . f)
+
+-- | Iterate on a seed, which may result in one of four scenarios:
+--
+--   1. The function yields a @Non@ value, which terminates the
+--      iteration.
+--
+--   2. The function yields a @One@ value.
+--
+--   3. The function yields a @Eno@ value, which changes the seed
+--      and iteration continues with the new seed.
+--
+--   4. The function yields the @a@ value of a @Two@ case.
+--
+iterateUntilM
+    :: Monad m
+    => Alternative f
+    => (b -> m (Can a b))
+    -> b
+    -> m (f a)
+iterateUntilM f b = f b >>= \case
+    Non -> pure empty
+    One a -> pure (pure a)
+    Eno b' -> iterateUntilM f b'
+    Two a _ -> pure (pure a)
+
+-- | Iterate on a seed, accumulating values and monoidally
+-- updating the seed with each update.
+--
+accumUntil
+    :: Alternative f
+    => Monoid b
+    => (b -> Can a b)
+    -> f a
+accumUntil f = runIdentity (accumUntilM (pure . f))
+
+-- | Iterate on a seed, accumulating values and monoidally
+-- updating a seed within a monad.
+--
+accumUntilM
+    :: Monad m
+    => Alternative f
+    => Monoid b
+    => (b -> m (Can a b))
+    -> m (f a)
+accumUntilM f = go mempty
+  where
+    go b = f b >>= \case
+      Non -> pure empty
+      One a -> (pure a <|>) <$> go b
+      Eno b' -> go (b' `mappend` b)
+      Two a b' -> (pure a <|>) <$> go (b' `mappend` b)
+
 -- -------------------------------------------------------------------- --
 -- Partitioning
 
@@ -312,11 +471,10 @@
 -- their parts.
 --
 partitionCans
-    :: forall f t a b
-    . ( Foldable t
-      , Alternative f
-      )
-    => t (Can a b) -> (f a, f b)
+    :: Alternative f
+    => Foldable t
+    => t (Can a b)
+    -> (f a, f b)
 partitionCans = foldr go (empty, empty)
   where
     go Non acc = acc
@@ -325,44 +483,40 @@
     go (Two a b) (as, bs) = (pure a <|> as, pure b <|> bs)
 
 -- | Partition a structure by mapping its contents into 'Can's,
--- and folding over '(<|>)'.
+-- and folding over @('<|>')@.
 --
 mapCans
-    :: forall f t a b c
-    . ( Alternative f
-      , Traversable t
-      )
+    :: Traversable t
+    => Alternative f
     => (a -> Can b c)
     -> t a
     -> (f b, f c)
 mapCans f = partitionCans . fmap f
 
+-- | Equivalence relation formed by grouping of equal 'Can' constructors.
+--
+eqCan :: Equivalence (Can a b)
+eqCan = Equivalence equivalence
+  where
+    equivalence :: Can a b -> Can a b -> Bool
+    equivalence Non       Non       = True
+    equivalence (One   _) (One   _) = True
+    equivalence (Eno   _) (Eno   _) = True
+    equivalence (Two _ _) (Two _ _) = True
+    equivalence _         _         = False
+
 -- -------------------------------------------------------------------- --
 -- Distributivity
 
 -- | Distribute a 'Can' value over a product.
 --
 distributeCan :: Can (a,b) c -> (Can a c, Can b c)
-distributeCan = \case
-    Non -> (Non, Non)
-    One (a,b) -> (One a, One b)
-    Eno c -> (Eno c, Eno c)
-    Two (a,b) c -> (Two a c, Two b c)
+distributeCan = unzipFirst
 
 -- | Codistribute a coproduct over a 'Can' value.
 --
 codistributeCan :: Either (Can a c) (Can b c) -> Can (Either a b) c
-codistributeCan = \case
-    Left ac -> case ac of
-      Non -> Non
-      One a -> One (Left a)
-      Eno c -> Eno c
-      Two a c -> Two (Left a) c
-    Right bc -> case bc of
-      Non -> Non
-      One b -> One (Right b)
-      Eno c -> Eno c
-      Two b c -> Two (Right b) c
+codistributeCan = undecideFirst
 
 -- -------------------------------------------------------------------- --
 -- Associativity
@@ -407,18 +561,14 @@
 -- | Swap the positions of values in a 'Can'.
 --
 swapCan :: Can a b -> Can b a
-swapCan = \case
-    Non -> Non
-    One a -> Eno a
-    Eno b -> One b
-    Two a b -> Two b a
+swapCan = can Non Eno One (flip Two)
 
 -- -------------------------------------------------------------------- --
 -- Curry & Uncurry
 
 -- | Curry a function from a 'Can' to a 'Maybe' value, resulting in a
 -- function of curried 'Maybe' values. This is analogous to currying
--- for '(->)'.
+-- for @('->')@.
 --
 canCurry :: (Can a b -> Maybe c) -> Maybe a -> Maybe b -> Maybe c
 canCurry k ma mb = case (ma, mb) of
@@ -429,7 +579,7 @@
 
 -- | "Uncurry" a function from a 'Can' to a 'Maybe' value, resulting in a
 -- function of curried 'Maybe' values. This is analogous to uncurrying
--- for '(->)'.
+-- for @('->')@.
 --
 canUncurry :: (Maybe a -> Maybe b -> Maybe c) -> Can a b -> Maybe c
 canUncurry k = \case
@@ -439,9 +589,82 @@
     Two a b -> k (Just a) (Just b)
 
 -- -------------------------------------------------------------------- --
--- Std instances
+-- Functor class instances
 
+instance Eq a => Eq1 (Can a) where
+  liftEq = liftEq2 (==)
 
+instance Eq2 Can where
+  liftEq2 _ _ Non Non = True
+  liftEq2 f _ (One a) (One c) = f a c
+  liftEq2 _ g (Eno b) (Eno d) = g b d
+  liftEq2 f g (Two a b) (Two c d) = f a c && g b d
+  liftEq2 _ _ _ _ = False
+
+instance Ord a => Ord1 (Can a) where
+  liftCompare = liftCompare2 compare
+
+instance Ord2 Can where
+  liftCompare2 _ _ Non Non = EQ
+  liftCompare2 _ _ Non _ = LT
+  liftCompare2 _ _ _ Non = GT
+  liftCompare2 f _ (One a) (One c) = f a c
+  liftCompare2 _ g (Eno b) (Eno d) = g b d
+  liftCompare2 f g (Two a b) (Two c d) = f a c <> g b d
+  liftCompare2 _ _ One{} _ = LT
+  liftCompare2 _ _ _ One{} = GT
+  liftCompare2 _ _ _ Two{} = LT
+  liftCompare2 _ _ Two{} _ = GT
+
+instance Show a => Show1 (Can a) where
+  liftShowsPrec = liftShowsPrec2 showsPrec showList
+
+instance Show2 Can where
+  liftShowsPrec2 _ _ _ _ _ Non = showString "Non"
+  liftShowsPrec2 f _ _ _ d (One a) = showsUnaryWith f "One" d a
+  liftShowsPrec2 _ _ g _ d (Eno b) = showsUnaryWith g "Eno" d b
+  liftShowsPrec2 f _ g _ d (Two a b) = showsBinaryWith f g "Two" d a b
+
+instance Read a => Read1 (Can a) where
+  liftReadsPrec = liftReadsPrec2 readsPrec readList
+
+instance Read2 Can where
+  liftReadPrec2 rpa _ rpb _ = nonP <|> oneP <|> enoP <|> twoP
+    where
+      nonP = Non <$ expectP (Ident "Non")
+      oneP = readData $ readUnaryWith rpa "One" One
+      enoP = readData $ readUnaryWith rpb "Eno" Eno
+      twoP = readData $ readBinaryWith rpa rpb "Two" Two
+
+instance NFData a => NFData1 (Can a) where
+  liftRnf = liftRnf2 rnf
+
+instance NFData2 Can where
+  liftRnf2 f g = \case
+    Non -> ()
+    One a -> f a
+    Eno b -> g b
+    Two a b -> f a `seq` g b
+
+instance Hashable a => Hashable1 (Can a) where
+  liftHashWithSalt = liftHashWithSalt2 hashWithSalt
+
+instance Hashable2 Can where
+  liftHashWithSalt2 f g salt = \case
+    Non -> salt `hashWithSalt` (0 :: Int) `hashWithSalt` ()
+    One a -> salt `hashWithSalt` (1 :: Int) `f` a
+    Eno b -> salt `hashWithSalt` (2 :: Int) `g` b
+    Two a b -> (salt `hashWithSalt` (3 :: Int) `f` a) `g` b
+
+-- -------------------------------------------------------------------- --
+-- Normal instances
+
+instance (NFData a, NFData b) => NFData (Can a b) where
+    rnf Non = ()
+    rnf (One a) = rnf a
+    rnf (Eno b) = rnf b
+    rnf (Two a b) = rnf a `seq` rnf b
+
 instance (Hashable a, Hashable b) => Hashable (Can a b)
 
 instance Functor (Can a) where
@@ -504,7 +727,39 @@
 
 instance (Semigroup a, Semigroup b) => Monoid (Can a b) where
   mempty = Non
+  mappend = (<>)
 
+instance (Binary a, Binary b) => Binary (Can a b) where
+  put Non = put @Int 0
+  put (One a) = put @Int 1 >> put a
+  put (Eno b) = put @Int 2 >> put b
+  put (Two a b) = put @Int 3 >> put a >> put b
+
+  get = get @Int >>= \case
+    0 -> pure Non
+    1 -> One <$> get
+    2 -> Eno <$> get
+    3 -> Two <$> get <*> get
+    _ -> fail "Invalid Can index"
+
+instance Semigroup a => MonadZip (Can a) where
+  mzipWith f a b = f <$> a <*> b
+
+instance Semigroup a => Alternative (Can a) where
+  empty = Non
+  Non <|> c = c
+  c <|> Non = c
+  One a <|> One b = One (a <> b)
+  One a <|> Eno b = Two a b
+  One a <|> Two b c = Two (a <> b) c
+  Eno a <|> One b = Two b a
+  Eno _ <|> c = c
+  Two a b <|> One c = Two (a <> c) b
+  Two a _ <|> Eno b = Two a b
+  Two a _ <|> Two b c = Two (a <> b) c
+
+instance Semigroup a => MonadPlus (Can a)
+
 -- -------------------------------------------------------------------- --
 -- Bifunctors
 
@@ -515,12 +770,24 @@
     Eno b -> Eno (g b)
     Two a b -> Two (f a) (g b)
 
+instance Biapplicative Can where
+  bipure = Two
+
+  One f <<*>> One a = One (f a)
+  One f <<*>> Two a _ = One (f a)
+  Eno g <<*>> Eno b = Eno (g b)
+  Eno g <<*>> Two _ b = Eno (g b)
+  Two f _ <<*>> One a = One (f a)
+  Two _ g <<*>> Eno b = Eno (g b)
+  Two f g <<*>> Two a b = Two (f a) (g b)
+  _ <<*>> _ = Non
+
 instance Bifoldable Can where
   bifoldMap f g = \case
     Non -> mempty
     One a -> f a
     Eno b -> g b
-    Two a b -> f a <> g b
+    Two a b -> f a `mappend` g b
 
 instance Bitraversable Can where
   bitraverse f g = \case
diff --git a/src/Data/Smash.hs b/src/Data/Smash.hs
--- a/src/Data/Smash.hs
+++ b/src/Data/Smash.hs
@@ -1,25 +1,32 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE Safe #-}
 -- |
 -- Module       : Data.Smash
--- Copyright    : (c) 2020 Emily Pillmore
+-- Copyright    : (c) 2020-2022 Emily Pillmore
 -- License      : BSD-3-Clause
 --
 -- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>
 -- Stability    : Experimental
--- Portability  : portable
+-- Portability  : CPP, RankNTypes, TypeApplications
 --
 -- This module contains the definition for the 'Smash' datatype. In
--- practice, this type is isomorphic to 'Maybe (a,b)' - the type with
+-- practice, this type is isomorphic to @'Maybe' (a,b)@ - the type with
 -- two possibly non-exclusive values and an empty case.
+--
 module Data.Smash
 ( -- * Datatypes
   -- $general
   Smash(..)
+  -- ** Type synonyms
+, type (⨳)
   -- * Combinators
 , toSmash
 , fromSmash
@@ -29,17 +36,26 @@
 , hulkSmash
 , isSmash
 , isNada
+, smashDiag
+, smashDiag'
   -- ** Eliminators
 , smash
   -- * Filtering
 , smashes
 , filterNadas
-  -- * Folding
+  -- * Folding and Unfolding
 , foldSmashes
 , gatherSmashes
+, unfoldr
+, unfoldrM
+, iterateUntil
+, iterateUntilM
+, accumUntil
+, accumUntilM
   -- * Partitioning
 , partitionSmashes
 , mapSmashes
+, eqSmash
   -- * Currying & Uncurrying
 , smashCurry
 , smashUncurry
@@ -59,22 +75,38 @@
 
 
 import Control.Applicative (Alternative(..))
-import Data.Bifunctor
+import Control.DeepSeq
+import Control.Monad.Zip
+
+import Data.Biapplicative
 import Data.Bifoldable
+import Data.Binary (Binary(..))
 import Data.Bitraversable
 import Data.Can (Can(..), can)
 import Data.Data
+import Data.Functor.Classes
+import Data.Functor.Contravariant (Equivalence(..))
+import Data.Functor.Identity
 import Data.Hashable
 import Data.Wedge (Wedge(..))
 
 import GHC.Generics
+import GHC.Read
 
+import Text.Read hiding (get)
+
+import Data.Smash.Internal
+import qualified Language.Haskell.TH.Syntax as TH
+import Control.Monad
+import Data.Hashable.Lifted
+
+
 {- $general
 
 Categorically, the 'Smash' datatype represents a special type of product, a
 <https://ncatlab.org/nlab/show/smash+product smash product>, in the category Hask*
 of pointed Hask types. The category Hask* consists of Hask types affixed with
-a dedicated base point - i.e. all objects look like 'Maybe a'. The smash product is a symmetric, monoidal tensor in Hask* that plays
+a dedicated base point - i.e. all objects look like @'Maybe' a@. The smash product is a symmetric, monoidal tensor in Hask* that plays
 nicely with the product, 'Can', and coproduct, 'Wedge'. Pictorially,
 these datatypes look like this:
 
@@ -113,7 +145,7 @@
 
 -- | The 'Smash' data type represents A value which has either an
 -- empty case, or two values. The result is a type, 'Smash a b', which is
--- isomorphic to 'Maybe (a,b)'.
+-- isomorphic to @'Maybe' (a,b)@.
 --
 -- Categorically, the smash product (the quotient of a pointed product by
 -- a wedge sum) has interesting properties. It forms a closed
@@ -125,22 +157,25 @@
     ( Eq, Ord, Read, Show
     , Generic, Generic1
     , Typeable, Data
+    , TH.Lift
     )
 
+-- | A type operator synonym for 'Smash'
+--
+type a ⨳ b = Smash a b
+
 -- -------------------------------------------------------------------- --
 -- Combinators
 
 -- | Convert a 'Maybe' value into a 'Smash' value
 --
 toSmash :: Maybe (a,b) -> Smash a b
-toSmash Nothing = Nada
-toSmash (Just (a,b)) = Smash a b
+toSmash = maybe Nada (uncurry Smash)
 
 -- | Convert a 'Smash' value into a 'Maybe' value
 --
 fromSmash :: Smash a b -> Maybe (a,b)
-fromSmash Nada = Nothing
-fromSmash (Smash a b) = Just (a,b)
+fromSmash = smash Nothing (curry Just)
 
 -- | Smash product of pointed type modulo its wedge
 --
@@ -157,14 +192,14 @@
   There d -> Smash a d
 
 -- | Project the left value of a 'Smash' datatype. This is analogous
--- to 'fst' for '(,)'.
+-- to 'fst' for @(',')@.
 --
 smashFst :: Smash a b -> Maybe a
 smashFst Nada = Nothing
 smashFst (Smash a _) = Just a
 
 -- | Project the right value of a 'Smash' datatype. This is analogous
--- to 'snd' for '(,)'.
+-- to 'snd' for @(',')@.
 --
 smashSnd :: Smash a b -> Maybe b
 smashSnd Nada = Nothing
@@ -181,6 +216,19 @@
 isSmash :: Smash a b -> Bool
 isSmash = not . isNada
 
+-- | Create a smash product of self-similar values from a pointed object.
+--
+-- This is the diagonal morphism in Hask*.
+--
+smashDiag :: Maybe a -> Smash a a
+smashDiag Nothing = Nada
+smashDiag (Just a) = Smash a a
+
+-- | See: 'smashDiag'. This is always a 'Smash' value.
+--
+smashDiag' :: a -> Smash a a
+smashDiag' a = Smash a a
+
 -- -------------------------------------------------------------------- --
 -- Eliminators
 
@@ -214,7 +262,7 @@
 -- Folding
 
 -- | Fold over the 'Smash' case of a 'Foldable' of 'Smash' products by
--- some accumulatig function.
+-- some accumulating function.
 --
 foldSmashes
     :: Foldable f
@@ -235,6 +283,66 @@
 gatherSmashes (Smash as bs) = zipWith Smash as bs
 gatherSmashes _ = []
 
+-- | Unfold from right to left into a smash product
+--
+unfoldr :: Alternative f => (b -> Smash a b) -> b -> f a
+unfoldr f = runIdentity . unfoldrM (pure . f)
+
+-- | Unfold from right to left into a monadic computation over a smash product
+--
+unfoldrM :: (Monad m, Alternative f) => (b -> m (Smash a b)) -> b -> m (f a)
+unfoldrM f b = f b >>= \case
+    Nada -> pure empty
+    Smash a b' -> (pure a <|>) <$> unfoldrM f b'
+
+-- | Iterate on a seed, accumulating a result. See 'iterateUntilM' for
+-- more details.
+--
+iterateUntil :: Alternative f => (b -> Smash a b) -> b -> f a
+iterateUntil f = runIdentity . iterateUntilM (pure . f)
+
+-- | Iterate on a seed, which may result in one of two scenarios:
+--
+--   1. The function yields a @Nada@ value, which terminates the
+--      iteration.
+--
+--   2. The function yields a @Smash@ value.
+--
+iterateUntilM
+    :: Monad m
+    => Alternative f
+    => (b -> m (Smash a b))
+    -> b
+    -> m (f a)
+iterateUntilM f b = f b >>= \case
+    Nada -> pure empty
+    Smash a _ -> pure (pure a)
+
+-- | Iterate on a seed, accumulating values and monoidally
+-- updating the seed with each update.
+--
+accumUntil
+    :: Alternative f
+    => Monoid b
+    => (b -> Smash a b)
+    -> f a
+accumUntil f = runIdentity (accumUntilM (pure . f))
+
+-- | Iterate on a seed, accumulating values and monoidally
+-- updating a seed within a monad.
+--
+accumUntilM
+    :: Monad m
+    => Alternative f
+    => Monoid b
+    => (b -> m (Smash a b))
+    -> m (f a)
+accumUntilM f = go mempty
+  where
+    go b = f b >>= \case
+      Nada -> pure empty
+      Smash a b' -> (pure a <|>) <$> go (b' `mappend` b)
+
 -- -------------------------------------------------------------------- --
 -- Partitioning
 
@@ -242,10 +350,8 @@
 -- their parts.
 --
 partitionSmashes
-    :: forall f t a b
-    . ( Foldable t
-      , Alternative f
-      )
+    :: Alternative f
+    => Foldable t
     => t (Smash a b) -> (f a, f b)
 partitionSmashes = foldr go (empty, empty)
   where
@@ -253,30 +359,38 @@
     go (Smash a b) (as, bs) = (pure a <|> as, pure b <|> bs)
 
 -- | Partition a structure by mapping its contents into 'Smash's,
--- and folding over '(<|>)'.
+-- and folding over @('<|>')@.
 --
 mapSmashes
-    :: forall f t a b c
-    . ( Alternative f
-      , Traversable t
-      )
+    :: Alternative f
+    => Traversable t
     => (a -> Smash b c)
     -> t a
     -> (f b, f c)
 mapSmashes f = partitionSmashes . fmap f
 
+-- | Equivalence relation formed by grouping of equal 'Smash' constructors.
+--
+eqSmash :: Equivalence (Smash a b)
+eqSmash = Equivalence equivalence
+  where
+    equivalence :: Smash a b -> Smash a b -> Bool
+    equivalence Nada        Nada        = True
+    equivalence (Smash _ _) (Smash _ _) = True
+    equivalence _           _           = False
+
 -- -------------------------------------------------------------------- --
 -- Currying & Uncurrying
 
 -- | "Curry" a map from a smash product to a pointed type. This is analogous
--- to 'curry' for '(->)'.
+-- to 'curry' for @('->')@.
 --
 smashCurry :: (Smash a b -> Maybe c) -> Maybe a -> Maybe b -> Maybe c
 smashCurry f (Just a) (Just b) = f (Smash a b)
 smashCurry _ _ _ = Nothing
 
 -- | "Uncurry" a map of pointed types to a map of a smash product to a pointed type.
--- This is analogous to 'uncurry' for '(->)'.
+-- This is analogous to 'uncurry' for @('->')@.
 --
 smashUncurry :: (Maybe a -> Maybe b -> Maybe c) -> Smash a b -> Maybe c
 smashUncurry _ Nada = Nothing
@@ -305,8 +419,7 @@
 -- | Distribute a 'Smash' of a pair into a pair of 'Smash's
 --
 pairSmash :: Smash (a,b) c -> (Smash a c, Smash b c)
-pairSmash Nada = (Nada, Nada)
-pairSmash (Smash (a,b) c) = (Smash a c, Smash b c)
+pairSmash = unzipFirst
 
 -- | Distribute a 'Smash' of a pair into a pair of 'Smash's
 --
@@ -324,7 +437,7 @@
   Eno b -> Eno (Smash b c)
   Two a b -> Two (Smash a c) (Smash b c)
 
--- | Unistribute a 'Can' of 'Smash's into a 'Smash' of 'Can's.
+-- | Undistribute a 'Can' of 'Smash's into a 'Smash' of 'Can's.
 --
 unpairSmashCan :: Can (Smash a c) (Smash b c) -> Smash (Can a b) c
 unpairSmashCan cc = case cc of
@@ -351,16 +464,67 @@
 -- -------------------------------------------------------------------- --
 -- Symmetry
 
--- | Swap the positions of values in a 'Smash a b' to form a 'Smash b a'.
+-- | Swap the positions of values in a @'Smash' a b@ to form a @'Smash' b a@.
 --
 swapSmash :: Smash a b -> Smash b a
-swapSmash Nada = Nada
-swapSmash (Smash a b) = Smash b a
+swapSmash = smash Nada (flip Smash)
 
 -- -------------------------------------------------------------------- --
--- Std instances
+-- Functor class instances
 
+instance Eq a => Eq1 (Smash a) where
+  liftEq = liftEq2 (==)
 
+instance Eq2 Smash where
+  liftEq2 _ _ Nada Nada = True
+  liftEq2 _ _ Nada _ = False
+  liftEq2 _ _ _ Nada = False
+  liftEq2 f g (Smash a b) (Smash c d) = f a c && g b d
+
+instance Ord a => Ord1 (Smash a) where
+  liftCompare = liftCompare2 compare
+
+instance Ord2 Smash where
+  liftCompare2 _ _ Nada Nada = EQ
+  liftCompare2 _ _ Nada _ = LT
+  liftCompare2 _ _ _ Nada = GT
+  liftCompare2 f g (Smash a b) (Smash c d) = f a c <> g b d
+
+instance Show a => Show1 (Smash a) where
+  liftShowsPrec = liftShowsPrec2 showsPrec showList
+
+instance Show2 Smash where
+  liftShowsPrec2 _ _ _ _ _ Nada = showString "Nada"
+  liftShowsPrec2 f _ g _ d (Smash a b) = showsBinaryWith f g "Smash" d a b
+
+instance Read a => Read1 (Smash a) where
+  liftReadsPrec = liftReadsPrec2 readsPrec readList
+
+instance Read2 Smash where
+  liftReadPrec2 rpa _ rpb _ = nadaP <|> smashP
+    where
+      nadaP = Nada <$ expectP (Ident "Nada")
+      smashP = readData $ readBinaryWith rpa rpb "Smash" Smash
+
+instance NFData a => NFData1 (Smash a) where
+  liftRnf = liftRnf2 rnf
+
+instance NFData2 Smash where
+  liftRnf2 f g = \case
+    Nada -> ()
+    Smash a b -> f a `seq` g b
+
+instance Hashable a => Hashable1 (Smash a) where
+  liftHashWithSalt = liftHashWithSalt2 hashWithSalt
+
+instance Hashable2 Smash where
+  liftHashWithSalt2 f g salt = \case
+    Nada -> salt `hashWithSalt` (0 :: Int) `hashWithSalt` ()
+    Smash a b -> (salt `hashWithSalt` (1 :: Int) `f` a) `g` b
+
+-- -------------------------------------------------------------------- --
+-- Std instances
+
 instance (Hashable a, Hashable b) => Hashable (Smash a b)
 
 instance Functor (Smash a) where
@@ -383,6 +547,9 @@
     Nada -> Nada
     Smash c d -> Smash (a <> c) d
 
+instance Monoid a => MonadZip (Smash a) where
+  mzipWith f a b = f <$> a <*> b
+
 instance (Semigroup a, Semigroup b) => Semigroup (Smash a b) where
   Nada <> b = b
   a <> Nada = a
@@ -390,7 +557,29 @@
 
 instance (Semigroup a, Semigroup b) => Monoid (Smash a b) where
   mempty = Nada
+  mappend = (<>)
 
+instance (NFData a, NFData b) => NFData (Smash a b) where
+  rnf Nada = ()
+  rnf (Smash a b) = rnf a `seq` rnf b
+
+instance (Binary a, Binary b) => Binary (Smash a b) where
+  put Nada = put @Int 0
+  put (Smash a b) = put @Int 1 >> put a >> put b
+
+  get = get @Int >>= \case
+    0 -> pure Nada
+    1 -> Smash <$> get <*> get
+    _ -> fail "Invalid Smash index"
+
+instance Monoid a => Alternative (Smash a) where
+  empty = Nada
+  Nada <|> c = c
+  c <|> Nada = c
+  Smash a _ <|> Smash c d = Smash (a <> c) d
+
+instance Monoid a => MonadPlus (Smash a)
+
 -- -------------------------------------------------------------------- --
 -- Bifunctors
 
@@ -399,10 +588,16 @@
     Nada -> Nada
     Smash a b -> Smash (f a) (g b)
 
+instance Biapplicative Smash where
+  bipure = Smash
+
+  Smash f g <<*>> Smash a b = Smash (f a) (g b)
+  _ <<*>> _ = Nada
+
 instance Bifoldable Smash where
   bifoldMap f g = \case
     Nada -> mempty
-    Smash a b -> f a <> g b
+    Smash a b -> f a `mappend` g b
 
 instance Bitraversable Smash where
   bitraverse f g = \case
diff --git a/src/Data/Smash/Internal.hs b/src/Data/Smash/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Smash/Internal.hs
@@ -0,0 +1,27 @@
+{-# language Safe #-}
+-- |
+-- Module       : Data.Smash.Internal
+-- Copyright    : (c) 2020-2022 Emily Pillmore
+-- License      : BSD-3-Clause
+--
+-- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>,
+--                Asad Saeeduddin <https://github.com/masaeedu>
+-- Stability    : Experimental
+-- Portability  : non-portable
+--
+-- This module contains utilities for distributing and codistributing
+-- bifunctors over monoidal actions.
+--
+module Data.Smash.Internal
+( unzipFirst
+, undecideFirst
+) where
+
+import Data.Bifunctor
+
+unzipFirst :: Bifunctor f => f (a, b) c -> (f a c, f b c)
+unzipFirst fabc = (first fst fabc, first snd fabc)
+
+undecideFirst :: Bifunctor f => Either (f a c) (f b c) -> f (Either a b) c
+undecideFirst (Left fac) = first Left fac
+undecideFirst (Right fbc) = first Right fbc
diff --git a/src/Data/Wedge.hs b/src/Data/Wedge.hs
--- a/src/Data/Wedge.hs
+++ b/src/Data/Wedge.hs
@@ -1,25 +1,32 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Safe #-}
 -- |
 -- Module       : Data.Wedge
--- Copyright    : (c) 2020 Emily Pillmore
+-- Copyright    : (c) 2020-2022 Emily Pillmore
 -- License      : BSD-3-Clause
 --
 -- Maintainer   : Emily Pillmore <emilypi@cohomolo.gy>
 -- Stability    : Experimental
--- Portability  : portable
+-- Portability  : CPP, RankNTypes, TypeApplications
 --
 -- This module contains the definition for the 'Wedge' datatype. In
--- practice, this type is isomorphic to 'Maybe (Either a b)' - the type with
+-- practice, this type is isomorphic to @'Maybe' ('Either' a b)@ - the type with
 -- two possibly non-exclusive values and an empty case.
+--
 module Data.Wedge
 ( -- * Datatypes
   -- $general
   Wedge(..)
+  -- ** Type synonyms
+, type (∨)
   -- * Combinators
 , quotWedge
 , wedgeLeft
@@ -37,13 +44,20 @@
 , filterHeres
 , filterTheres
 , filterNowheres
-  -- ** Folding
+  -- ** Folding and Unfolding
 , foldHeres
 , foldTheres
 , gatherWedges
+, unfoldr
+, unfoldrM
+, iterateUntil
+, iterateUntilM
+, accumUntil
+, accumUntilM
   -- ** Partitioning
 , partitionWedges
 , mapWedges
+, eqWedge
   -- ** Distributivity
 , distributeWedge
 , codistributeWedge
@@ -56,58 +70,80 @@
 
 
 import Control.Applicative (Alternative(..))
+import Control.DeepSeq
+import Control.Monad.Zip
 
 import Data.Bifunctor
 import Data.Bifoldable
+import Data.Binary (Binary(..))
 import Data.Bitraversable
 import Data.Data
+import Data.Functor.Classes
+import Data.Functor.Contravariant (Equivalence(..))
+import Data.Functor.Identity
 import Data.Hashable
 
 import GHC.Generics
+import GHC.Read
 
+import qualified Language.Haskell.TH.Syntax as TH
+
+import Text.Read hiding (get)
+
+import Data.Smash.Internal
+import Control.Monad
+import Data.Hashable.Lifted
+
+
 {- $general
 
 Categorically, the 'Wedge' datatype represents the coproduct (like, 'Either')
 in the category Hask* of pointed Hask types, called a <https://ncatlab.org/nlab/show/wedge+sum wedge sum>.
 The category Hask* consists of Hask types affixed with
 a dedicated base point along with an object. In Hask, this is
-equivalent to `1 + a`, also known as 'Maybe a'. Because we can conflate
-basepoints of different types (there is only one @Nothing@ type), the wedge sum is
-can be viewed as the type `1 + a + b`, or `Maybe (Either a b)` in Hask.
+equivalent to @1 + a@, also known as @'Maybe' a@. Because we can conflate
+basepoints of different types (there is only one @Nothing@ type), the wedge sum
+can be viewed as the type @1 + a + b@, or @'Maybe' ('Either' a b)@ in Hask.
+
 Pictorially, one can visualize this as:
 
 
 @
 'Wedge':
-                a
-                |
-Nowhere +-------+
-                |
-                b
+                  a
+                  |
+'Nowhere' +-------+
+                  |
+                  b
 @
 
 
 The fact that we can think about 'Wedge' as a coproduct gives us
 some reasoning power about how a 'Wedge' will interact with the
 product in Hask*, called 'Can'. Namely, we know that a product of a type and a
-coproduct, `a * (b + c)`, is equivalent to `(a + b) * (a + c)`. Additioally,
+coproduct, @a * (b + c)@, is equivalent to @(a * b) + (a * c)@. Additionally,
 we may derive other facts about its associativity, distributivity, commutativity, and
-any more. As an exercise, think of soemthing `Either` can do. Now do it with 'Wedge'!
+many more. As an exercise, think of something 'Either' can do. Now do it with 'Wedge'!
 
 -}
 
 -- | The 'Wedge' data type represents values with two exclusive
 -- possibilities, and an empty case. This is a coproduct of pointed
 -- types - i.e. of 'Maybe' values. The result is a type, 'Wedge a b',
--- which is isomorphic to 'Maybe (Either a b)'.
+-- which is isomorphic to @'Maybe' ('Either' a b)@.
 --
 data Wedge a b = Nowhere | Here a | There b
   deriving
     ( Eq, Ord, Read, Show
     , Generic, Generic1
     , Typeable, Data
+    , TH.Lift
     )
 
+-- | A type operator synonym for 'Wedge'.
+--
+type a ∨ b = Wedge a b
+
 -- -------------------------------------------------------------------- --
 -- Eliminators
 
@@ -129,24 +165,20 @@
 -- | Given two possible pointed types, produce a 'Wedge' by
 -- considering the left case, the right case, and mapping their
 -- 'Nothing' cases to 'Nowhere'. This is a pushout of pointed
--- types `A <- * -> B`.
+-- types @A <- * -> B@.
 --
 quotWedge :: Either (Maybe a) (Maybe b) -> Wedge a b
-quotWedge (Left a) = maybe Nowhere Here a
-quotWedge (Right b) = maybe Nowhere There b
+quotWedge = either (maybe Nowhere Here) (maybe Nowhere There)
 
--- | Convert a 'Wedge a b' into a 'Maybe (Either a b)' value.
+-- | Convert a 'Wedge a b' into a @'Maybe' ('Either' a b)@ value.
 --
 fromWedge :: Wedge a b -> Maybe (Either a b)
-fromWedge Nowhere = Nothing
-fromWedge (Here a) = Just (Left a)
-fromWedge (There b) = Just (Right b)
+fromWedge = wedge Nothing (Just . Left) (Just . Right)
 
--- | Convert a 'Maybe (Either a b)' value into a 'Wedge'
+-- | Convert a @'Maybe' ('Either' a b)@ value into a 'Wedge'
 --
 toWedge :: Maybe (Either a b) -> Wedge a b
-toWedge Nothing = Nowhere
-toWedge (Just e) = either Here There e
+toWedge = maybe Nowhere (either Here There)
 
 -- | Inject a 'Maybe' value into the 'Here' case of a 'Wedge',
 -- or 'Nowhere' if the empty case is given. This is analogous to the
@@ -260,6 +292,74 @@
 gatherWedges (Here as) = fmap Here as
 gatherWedges (There bs) = fmap There bs
 
+-- | Unfold from right to left into a wedge product. For a variant
+-- that accumulates in the seed instead of just updating with a
+-- new value, see 'accumUntil' and 'accumUntilM'.
+--
+unfoldr :: Alternative f => (b -> Wedge a b) -> b -> f a
+unfoldr f = runIdentity . unfoldrM (pure . f)
+
+-- | Unfold from right to left into a monadic computation over a wedge product
+--
+unfoldrM :: (Monad m, Alternative f) => (b -> m (Wedge a b)) -> b -> m (f a)
+unfoldrM f b = f b >>= \case
+    Nowhere -> pure empty
+    Here a -> (pure a <|>) <$> unfoldrM f b
+    There b' -> unfoldrM f b'
+
+-- | Iterate on a seed, accumulating a result. See 'iterateUntilM' for
+-- more details.
+--
+iterateUntil :: Alternative f => (b -> Wedge a b) -> b -> f a
+iterateUntil f = runIdentity . iterateUntilM (pure . f)
+
+-- | Iterate on a seed, which may result in one of three scenarios:
+--
+--   1. The function yields a @Nowhere@ value, which terminates the
+--      iteration.
+--
+--   2. The function yields a @Here@ value.
+--
+--   3. The function yields a @There@ value, which changes the seed
+--      and iteration continues with the new seed.
+--
+iterateUntilM
+    :: Monad m
+    => Alternative f
+    => (b -> m (Wedge a b))
+    -> b
+    -> m (f a)
+iterateUntilM f b = f b >>= \case
+    Nowhere -> pure empty
+    Here a -> pure (pure a)
+    There b' -> iterateUntilM f b'
+
+-- | Iterate on a seed, accumulating values and monoidally
+-- updating the seed with each update.
+--
+accumUntil
+    :: Alternative f
+    => Monoid b
+    => (b -> Wedge a b)
+    -> f a
+accumUntil f = runIdentity (accumUntilM (pure . f))
+
+-- | Iterate on a seed, accumulating values and monoidally
+-- updating a seed within a monad.
+--
+accumUntilM
+    :: Monad m
+    => Alternative f
+    => Monoid b
+    => (b -> m (Wedge a b))
+    -> m (f a)
+accumUntilM f = go mempty
+  where
+    go b = f b >>= \case
+      Nowhere -> pure empty
+      Here a -> (pure a <|>) <$> go b
+      There b' -> go (b' `mappend` b)
+
 -- -------------------------------------------------------------------- --
 -- Partitioning
 
@@ -267,10 +367,8 @@
 -- their parts.
 --
 partitionWedges
-    :: forall f t a b
-    . ( Foldable t
-      , Alternative f
-      )
+    :: Alternative f
+    => Foldable t
     => t (Wedge a b) -> (f a, f b)
 partitionWedges = foldr go (empty, empty)
   where
@@ -279,18 +377,27 @@
     go (There b) (as, bs) = (as, pure b <|> bs)
 
 -- | Partition a structure by mapping its contents into 'Wedge's,
--- and folding over '(<|>)'.
+-- and folding over @('<|>')@.
 --
 mapWedges
-    :: forall f t a b c
-    . ( Alternative f
-      , Traversable t
-      )
+    :: Traversable t
+    => Alternative f
     => (a -> Wedge b c)
     -> t a
     -> (f b, f c)
 mapWedges f = partitionWedges . fmap f
 
+-- | Equivalence relation formed by grouping of equal 'Wedge' constructors.
+--
+eqWedge :: Equivalence (Wedge a b)
+eqWedge = Equivalence equivalence
+  where
+    equivalence :: Wedge a b -> Wedge a b -> Bool
+    equivalence Nowhere   Nowhere   = True
+    equivalence (Here  _) (Here  _) = True
+    equivalence (There _) (There _) = True
+    equivalence _         _         = False
+
 -- -------------------------------------------------------------------- --
 -- Associativity
 
@@ -322,23 +429,12 @@
 -- | Distribute a 'Wedge' over a product.
 --
 distributeWedge :: Wedge (a,b) c -> (Wedge a c, Wedge b c)
-distributeWedge = \case
-  Nowhere -> (Nowhere, Nowhere)
-  Here (a,b) -> (Here a, Here b)
-  There c -> (There c, There c)
+distributeWedge = unzipFirst
 
--- | Codistribute 'Wedge's over a coproduct
+-- | Codistribute 'Wedge's over a coproduct.
 --
 codistributeWedge :: Either (Wedge a c) (Wedge b c) -> Wedge (Either a b) c
-codistributeWedge = \case
-  Left w -> case w of
-    Nowhere -> Nowhere
-    Here a -> Here (Left a)
-    There c -> There c
-  Right w -> case w of
-    Nowhere -> Nowhere
-    Here b -> Here (Right b)
-    There c -> There c
+codistributeWedge = undecideFirst
 
 -- -------------------------------------------------------------------- --
 -- Symmetry
@@ -346,12 +442,69 @@
 -- | Swap the positions of the @a@'s and the @b@'s in a 'Wedge'.
 --
 swapWedge :: Wedge a b -> Wedge b a
-swapWedge = \case
-  Nowhere -> Nowhere
-  Here a -> There a
-  There b -> Here b
+swapWedge = wedge Nowhere There Here
 
 -- -------------------------------------------------------------------- --
+-- Functor class instances
+
+instance Eq a => Eq1 (Wedge a) where
+  liftEq = liftEq2 (==)
+
+instance Eq2 Wedge where
+  liftEq2 _ _ Nowhere Nowhere = True
+  liftEq2 f _ (Here a) (Here c) = f a c
+  liftEq2 _ g (There b) (There d) = g b d
+  liftEq2 _ _ _ _ = False
+
+instance Ord a => Ord1 (Wedge a) where
+  liftCompare = liftCompare2 compare
+
+instance Ord2 Wedge where
+  liftCompare2 _ _ Nowhere Nowhere = EQ
+  liftCompare2 _ _ Nowhere _ = LT
+  liftCompare2 _ _ _ Nowhere = GT
+  liftCompare2 f _ (Here a) (Here c) = f a c
+  liftCompare2 _ _ Here{} There{} = LT
+  liftCompare2 _ _ There{} Here{} = GT
+  liftCompare2 _ g (There b) (There d) = g b d
+
+instance Show a => Show1 (Wedge a) where
+  liftShowsPrec = liftShowsPrec2 showsPrec showList
+
+instance Show2 Wedge where
+  liftShowsPrec2 _ _ _ _ _ Nowhere = showString "Nowhere"
+  liftShowsPrec2 f _ _ _ d (Here a) = showsUnaryWith f "Here" d a
+  liftShowsPrec2 _ _ g _ d (There b) = showsUnaryWith g "There" d b
+
+instance Read a => Read1 (Wedge a) where
+  liftReadsPrec = liftReadsPrec2 readsPrec readList
+
+instance Read2 Wedge where
+  liftReadPrec2 rpa _ rpb _ = nowhereP <|> hereP <|> thereP
+    where
+      nowhereP = Nowhere <$ expectP (Ident "Nowhere")
+      hereP = readData $ readUnaryWith rpa "Here" Here
+      thereP = readData $ readUnaryWith rpb "There" There
+
+instance Hashable a => Hashable1 (Wedge a) where
+  liftHashWithSalt = liftHashWithSalt2 hashWithSalt
+
+instance Hashable2 Wedge where
+  liftHashWithSalt2 f g salt = \case
+    Nowhere -> salt `hashWithSalt` (0 :: Int) `hashWithSalt` ()
+    Here a -> salt `hashWithSalt` (1 :: Int) `f` a
+    There b -> salt `hashWithSalt` (2 :: Int) `g` b
+
+instance NFData a => NFData1 (Wedge a) where
+  liftRnf = liftRnf2 rnf
+
+instance NFData2 Wedge where
+  liftRnf2 f g = \case
+    Nowhere -> ()
+    Here a -> f a
+    There b -> g b
+
+-- -------------------------------------------------------------------- --
 -- Std instances
 
 instance (Hashable a, Hashable b) => Hashable (Wedge a b)
@@ -372,7 +525,7 @@
     Here a -> pure (Here a)
     There b -> There <$> f b
 
-instance Semigroup a => Applicative (Wedge a) where
+instance Applicative (Wedge a) where
   pure = There
 
   _ <*> Nowhere = Nowhere
@@ -381,7 +534,7 @@
   There _ <*> Here b = Here b
   There f <*> There a = There (f a)
 
-instance Semigroup a => Monad (Wedge a) where
+instance Monad (Wedge a) where
   return = pure
   (>>) = (*>)
 
@@ -399,6 +552,37 @@
 
 instance (Semigroup a, Semigroup b) => Monoid (Wedge a b) where
   mempty = Nowhere
+  mappend = (<>)
+
+instance (NFData a, NFData b) => NFData (Wedge a b) where
+    rnf Nowhere = ()
+    rnf (Here a) = rnf a
+    rnf (There b) = rnf b
+
+instance (Binary a, Binary b) => Binary (Wedge a b) where
+  put Nowhere = put @Int 0
+  put (Here a) = put @Int 1 >> put a
+  put (There b) = put @Int 2 >> put b
+
+  get = get @Int >>= \case
+    0 -> pure Nowhere
+    1 -> Here <$> get
+    2 -> There <$> get
+    _ -> fail "Invalid Wedge index"
+
+instance Semigroup a => MonadZip (Wedge a) where
+  mzipWith f a b = f <$> a <*> b
+
+instance Monoid a => Alternative (Wedge a) where
+  empty = Nowhere
+  Nowhere <|> c = c
+  c <|> Nowhere = c
+  Here a <|> Here b = Here (a <> b)
+  Here _ <|> There b = There b
+  There a <|> Here _ = There a
+  There _ <|> There b = There b
+
+instance Monoid a => MonadPlus (Wedge a)
 
 -- -------------------------------------------------------------------- --
 -- Bifunctors
diff --git a/test/MyLibTest.hs b/test/MyLibTest.hs
deleted file mode 100644
--- a/test/MyLibTest.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module Main (main) where
-
-main :: IO ()
-main = putStrLn "Test suite not yet implemented."