diff --git a/coapplicative.cabal b/coapplicative.cabal
--- a/coapplicative.cabal
+++ b/coapplicative.cabal
@@ -20,20 +20,30 @@
 -- PVP summary:     +-+------- breaking API changes
 --                  | | +----- non-breaking API additions
 --                  | | | +--- code changes with no API change
-version:            0.1.0.0
+version:            0.2.0.0
 
 -- A short (one-line) description of the package.
-synopsis:           A dual to applicative: covariant functors which can split
+synopsis:           Dualizes Applicative: covariant functors which can split and extract.
 
 -- A longer description of the package.
-description:        Provides covariant oplax monoidal functors. These functors
-                    can be "split" and support pattern-matching while
-                    retaining the functorial context.
-                    Default instances are provided for CoApplicatives that
-                    agree with their Comonad instances,
-                    as well as a wrapper for (usually non-lawful)
-                    instances on any Comonad.
+description:        Provides Splittable and Coapplicative classes.
+                    Splittable functors are oplax monoidal functors over
+                    Either/Void and support pattern-matching that preserves
+                    the context.
+                    Coapplicatives support this while also having extraction/
+                    cocartesian costrength. Unlike the situation with cartesian
+                    strength, not all functors support this natively.
 
+                    Every Comonad can define an instance of Coapplicative,
+                    but these need not agree with duplication, and need
+                    not be unique due to the non-uniqueness of the costrength.
+
+                    Instances are provided when they are compatible with
+                    the existing Comonad instance.
+
+                    Credit to Chris McKinlay's profunctor-optics for informing
+                    the typeclass structure
+
 -- The license under which the package is released.
 license:            MIT
 
@@ -65,7 +75,7 @@
     import:           warnings
 
     -- Modules exported by the library.
-    exposed-modules:  Control.CoApplicative
+    exposed-modules:  Control.Coapplicative, Control.Coapplicative.Traced
 
     -- Modules included in this library but not exported.
     -- other-modules:
diff --git a/src/Control/CoApplicative.hs b/src/Control/CoApplicative.hs
deleted file mode 100644
--- a/src/Control/CoApplicative.hs
+++ /dev/null
@@ -1,197 +0,0 @@
-{-# LANGUAGE DeriveFunctor, TypeOperators, FlexibleContexts, UndecidableInstances #-}
-
--- | Provides CoApplicative typeclass and instances.
-module Control.CoApplicative (CoApplicative(..), CoAppComonad(..)) where
-
-import Control.Comonad
-import Control.Comonad.Trans.Env
-import Data.Void
-import Data.Functor.Identity (Identity(..))
-import Data.List.NonEmpty
-import Data.Maybe (mapMaybe)
-import Data.Bifunctor
-import Data.Functor.Sum
-import Data.Coerce
-import GHC.Generics
-
-leftToMaybe :: Either a b -> Maybe a
-leftToMaybe (Left x) = Just x
-leftToMaybe (Right _) = Nothing
-rightToMaybe :: Either a b -> Maybe b
-rightToMaybe (Left _) = Nothing
-rightToMaybe (Right x) = Just x
-
--- | An opmonoidal functor over the cocartesian structure
--- of Either and Void.
---
--- Laws include associativity, and compatibility with fmap
--- (which implies identity laws)
---
--- either id split . split = either split id . split . fmap reassoc
--- where reassoc is the unique total function of type (Either a (Either b c)) -> Either (Either a b) c
--- split . fmap (either f g) = either (fmap f) (fmap g) . split
--- split . fmap Left = Left
--- split . fmap Right = Right
---
--- Every Comonad is a CoApplicative, but not always in a compatible way
--- with the Comonad structure.
--- In particular, duplicate must distribute with split:
---
--- bimap duplicate duplicate (split wab) = split (fmap split (duplicate wab))
---
-class Functor f => CoApplicative f where
-  nonempty :: f Void -> Void
-  split :: f (Either a b) -> Either (f a) (f b)
-
-  -- | Filter Maybe through the data-structure along Just,
-  -- discarding the context of Nothing values
-  --
-  -- The default implementation biases towards the Left
-  splitMaybe :: f (Maybe a) -> Maybe (f a)
-  splitMaybe = leftToMaybe . split . fmap maybeToLeft
-    where
-      maybeToLeft (Just x) = Left x
-      maybeToLeft Nothing = Right ()
-
-  -- | Zip a list through the data-structure,
-  -- discarding the context of nil values.
-  -- I.e. each position in the resulting
-  -- list will "collect" the corresponding f a
-  splitList :: f [a] -> [f a]
-  splitList = roll . maybe Nothing (Just . dorec) . splitMaybe . fmap unroll
-    {- TODO: make this fuse? At least on its output -}
-    where
-      dorec was = (fmap fst was, splitList $ fmap snd was)
-
-      unroll :: [b] -> Maybe (b, [b])
-      unroll [] = Nothing
-      unroll (x : xs) = Just (x, xs)
-      roll :: Maybe (b, [b]) -> [b]
-      roll Nothing = []
-      roll (Just (x, xs)) = x : xs
-
-instance CoApplicative Identity where
-  nonempty (Identity v) = v
-  split (Identity (Left x)) = Left (Identity x)
--- This is compatible
-  split (Identity (Right y)) = Right (Identity y)
-
--- | Filters out elements which do not match the head.
-instance CoApplicative NonEmpty where
-  nonempty (v :| _) = v
-  split (Left x :| rest) = Left (x :| mapMaybe leftToMaybe rest)
-  split (Right x :| rest) = Right (x :| mapMaybe rightToMaybe rest)
-
-instance (CoApplicative f, CoApplicative g) => CoApplicative (Sum f g) where
-  nonempty (InL fv) = nonempty fv
-  nonempty (InR gv) = nonempty gv
-  split (InL fe) = bimap InL InL (split fe)
-  split (InR ge) = bimap InR InR (split ge)
-  splitMaybe (InL fm) = InL <$> (splitMaybe fm)
-  splitMaybe (InR gm) = InR <$> (splitMaybe gm)
-  splitList (InL fxs) = InL <$> (splitList fxs)
-  splitList (InR gxs) = InR <$> (splitList gxs)
-
-instance CoApplicative ((,) a) where
-  nonempty (_, v) = v
-  split (a, Left x) = Left (a, x)
-  split (a, Right y) = Right (a, y)
-
-instance CoApplicative ((,,) a b) where
-  nonempty (_, _, v) = v
-  split (a, b, Left x) = Left (a, b, x)
-  split (a, b, Right y) = Right (a, b, y)
-
-instance CoApplicative ((,,,) a b c) where
-  nonempty (_, _, _, v) = v
-  split (a, b, c, Left x) = Left (a, b, c, x)
-  split (a, b, c, Right y) = Right (a, b, c, y)
-
-instance CoApplicative ((,,,,) a b c d) where
-  nonempty (_, _, _, _, v) = v
-  split (a, b, c, d, Left x) = Left (a, b, c, d, x)
-  split (a, b, c, d, Right y) = Right (a, b, c, d, y)
-
-instance CoApplicative ((,,,,,) a b c d e) where
-  nonempty (_, _, _, _, _, v) = v
-  split (a, b, c, d, e, Left x) = Left (a, b, c, d, e, x)
-  split (a, b, c, d, e, Right y) = Right (a, b, c, d, e, y)
-
-instance CoApplicative ((,,,,,,) a b c d e f) where
-  nonempty (_, _, _, _, _, _, v) = v
-  split (a, b, c, d, e, f, Left x) = Left (a, b, c, d, e, f, x)
-  split (a, b, c, d, e, f, Right y) = Right (a, b, c, d, e, f, y)
-
-instance CoApplicative w => CoApplicative (EnvT e w) where
-  nonempty (EnvT _ wv) = nonempty wv
-  split (EnvT e we) = bimap (EnvT e) (EnvT e) (split we)
-  splitMaybe (EnvT e wm) = EnvT e <$> splitMaybe wm
-  splitList (EnvT e wxs) = EnvT e <$> splitList wxs
-
-instance CoApplicative f => CoApplicative (M1 i c f) where
-  nonempty (M1 fv) = nonempty fv
-  split (M1 fab) = coerce (split fab)
-  splitMaybe (M1 fa) = M1 <$> splitMaybe fa
-  splitList (M1 fxs) = M1 <$> splitList fxs
-
--- identical to Sum
-instance (CoApplicative f, CoApplicative g) => CoApplicative (f :+: g) where
-  nonempty (L1 fv) = nonempty fv
-  nonempty (R1 gv) = nonempty gv
-  split (L1 fe) = bimap L1 L1 (split fe)
-  split (R1 ge) = bimap R1 R1 (split ge)
-  splitMaybe (L1 fm) = L1 <$> (splitMaybe fm)
-  splitMaybe (R1 gm) = R1 <$> (splitMaybe gm)
-  splitList (L1 fxs) = L1 <$> (splitList fxs)
-  splitList (R1 gxs) = R1 <$> (splitList gxs)
-
-instance (CoApplicative f, CoApplicative g) => CoApplicative (f :.: g) where
-  nonempty (Comp1 fgv) = nonempty (nonempty <$> fgv)
-  split (Comp1 fgab) =
-    coerce $
-    split (fmap split fgab)
-  splitMaybe (Comp1 fga) = fmap Comp1 $ splitMaybe $ fmap splitMaybe fga
-  splitList (Comp1 fgxs) = fmap Comp1 $ splitList $ fmap splitList fgxs
-
-instance CoApplicative Par1 where
-  nonempty (Par1 v) = v
-  split (Par1 (Left a)) = Left (Par1 a)
-  split (Par1 (Right a)) = Right (Par1 a)
-  splitMaybe (Par1 m) = Par1 <$> m
-  splitList (Par1 xs) = Par1 <$> xs
-
-instance CoApplicative f => CoApplicative (Rec1 f) where
-  nonempty (Rec1 fv) = nonempty fv
-  split (Rec1 fab) = coerce (split fab)
-  splitMaybe (Rec1 fa) = coerce $ splitMaybe fa
-  splitList (Rec1 fxs) = coerce $ splitList fxs
-
-instance (Generic1 f, CoApplicative (Rep1 f)) => CoApplicative (Generically1 f) where
-  nonempty (Generically1 fa) = nonempty (from1 fa)
-  split (Generically1 fab) =
-    bimap (Generically1 . to1) (Generically1 . to1)
-    (split (from1 fab))
-  splitMaybe (Generically1 fa) = fmap Generically1 $ fmap to1 $ splitMaybe $ from1 fa
-  splitList (Generically1 fxs) = fmap Generically1 $ fmap to1 $ splitList $ from1 fxs
-
--- | There is a derivable instance for any Comonad,
--- but this will not be compatible with context shifts for most instances.
--- 
--- In the context of pattern-matching, this means that reaching the same branch
--- two different ways may result in conflicting views of the surrounding context.
--- (only the context which lands on the same side of the branch is consistent)
-newtype CoAppComonad w a = CoAppComonad { runCoAppComonad :: w a } deriving (Functor)
-
-instance Comonad w => CoApplicative (CoAppComonad w) where
-  nonempty (CoAppComonad wv) = extract wv
-  split (CoAppComonad wab) =
-    case extract wab of
-      Left x -> Left (CoAppComonad $ fmap (either id (const x)) wab)
-      Right y -> Right (CoAppComonad $ fmap (either (const y) id) wab)
-
-instance Comonad w => Comonad (CoAppComonad w) where
-  extract = extract . runCoAppComonad
-  {- coerce gets blocked by unknown roles sadly -}
-  duplicate (CoAppComonad wa) = CoAppComonad (fmap CoAppComonad (duplicate wa))
-
-
diff --git a/src/Control/Coapplicative.hs b/src/Control/Coapplicative.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Coapplicative.hs
@@ -0,0 +1,317 @@
+{-# LANGUAGE DeriveFunctor, TypeOperators, FlexibleContexts, UndecidableInstances #-}
+
+-- | Provides Coapplicative typeclass and instances.
+module Control.Coapplicative (Splittable(..), Coapplicative(..), ComonadCoapp(..)) where
+
+import Control.Coapplicative.Traced
+import Control.Comonad
+import Control.Comonad.Env
+import Control.Comonad.Traced hiding (Sum)
+import Data.Void
+import Data.Functor.Identity (Identity(..))
+import Data.List.NonEmpty
+import Data.Maybe (mapMaybe)
+import Data.Bifunctor
+import Data.Functor.Sum
+import Data.Coerce
+import GHC.Generics
+
+leftToMaybe :: Either a b -> Maybe a
+leftToMaybe (Left x) = Just x
+leftToMaybe (Right _) = Nothing
+rightToMaybe :: Either a b -> Maybe b
+rightToMaybe (Left _) = Nothing
+rightToMaybe (Right x) = Just x
+
+-- | An opmonoidal functor over the cocartesian structure
+-- of Either and Void.
+--
+-- Laws include associativity, and compatibility with fmap
+-- (which implies identity laws)
+--
+-- > reassoc . bimap id split . split = bimap split id . split . fmap reassoc
+-- where reassoc is the unique total function of type @(Either a (Either b c)) -> Either (Either a b) c@
+--
+-- > split . fmap (either f g) = bimap (fmap f) (fmap g) . split
+-- > split . fmap Left = Left
+-- > split . fmap Right = Right
+--
+-- Comonads should ensure that their Splittable instance agrees with
+-- their Comonad instance:
+--
+-- > bimap extract extract . split = extract
+-- > bimap duplicate duplicate . split = fmap split . split . duplicate
+class Functor f => Splittable f where
+  nonempty :: f Void -> Void
+  split :: f (Either a b) -> Either (f a) (f b)
+  {-# MINIMAL nonempty, split #-}
+
+  -- | Filter Maybe through the data-structure along Just,
+  -- discarding the context of Nothing values
+  --
+  -- The default implementation biases towards the Left
+  splitMaybe :: f (Maybe a) -> Maybe (f a)
+  splitMaybe = leftToMaybe . split . fmap maybeToLeft
+    where
+      maybeToLeft (Just x) = Left x
+      maybeToLeft Nothing = Right ()
+
+  -- | Zip a list through the data-structure,
+  -- discarding the context of nil values.
+  -- I.e. each position in the resulting
+  -- list will "collect" the corresponding f a context
+  splitList :: f [a] -> [f a]
+  splitList = roll . maybe Nothing (Just . dorec) . splitMaybe . fmap unroll
+    {- TODO: make this fuse? At least on its output -}
+    where
+      dorec was = (fmap fst was, splitList $ fmap snd was)
+
+      unroll :: [b] -> Maybe (b, [b])
+      unroll [] = Nothing
+      unroll (x : xs) = Just (x, xs)
+      roll :: Maybe (b, [b]) -> [b]
+      roll Nothing = []
+      roll (Just (x, xs)) = x : xs
+
+
+-- | A Coapplicative has both a cocartesian costrength and is Splittable.
+-- This differs from Applicatives because the cartesian strength in Haskell
+-- is implicit and unique for every Functor.
+--
+-- Similarly to Splittable, every Comonad can be made into a Coapplicative,
+-- but not always in a way that is compatible with duplicate.
+-- The lack of a unique costrength breaks the dualization.
+--
+-- copure and costrength are inter-derivable for Splittable functors.
+class Splittable f => Coapplicative f where
+  costrength :: f (Either a b) -> Either a (f b)
+  costrength = bimap copure id . split
+  copure :: f a -> a
+  copure = either id (absurd . nonempty) . costrength . fmap Left
+  {-# MINIMAL costrength | copure #-}
+
+instance Splittable Identity where
+  nonempty (Identity v) = v
+  split (Identity (Left x)) = Left (Identity x)
+-- This is compatible
+  split (Identity (Right y)) = Right (Identity y)
+instance Coapplicative Identity where
+  costrength (Identity (Left x)) = Left x
+  costrength (Identity (Right y)) = Right (Identity y)
+  copure = runIdentity
+
+-- | Filters out elements which do not match the head.
+instance Splittable NonEmpty where
+  nonempty (v :| _) = v
+  split (Left x :| rest) = Left (x :| mapMaybe leftToMaybe rest)
+  split (Right x :| rest) = Right (x :| mapMaybe rightToMaybe rest)
+instance Coapplicative NonEmpty where
+  costrength (Left x :| _) = Left x
+  costrength (Right y :| rest) = Right (y :| mapMaybe rightToMaybe rest)
+  copure = extract
+
+instance (Splittable f, Splittable g) => Splittable (Sum f g) where
+  nonempty (InL fv) = nonempty fv
+  nonempty (InR gv) = nonempty gv
+  split (InL fe) = bimap InL InL (split fe)
+  split (InR ge) = bimap InR InR (split ge)
+  splitMaybe (InL fm) = InL <$> (splitMaybe fm)
+  splitMaybe (InR gm) = InR <$> (splitMaybe gm)
+  splitList (InL fxs) = InL <$> (splitList fxs)
+  splitList (InR gxs) = InR <$> (splitList gxs)
+instance (Coapplicative f, Coapplicative g) => Coapplicative (Sum f g) where
+  costrength (InL fe) = bimap id InL $ costrength fe
+  costrength (InR ge) = bimap id InR $ costrength ge
+  copure (InL fx) = copure fx
+  copure (InR gx) = copure gx
+
+instance Splittable ((,) a) where
+  nonempty (_, v) = v
+  split (a, Left x) = Left (a, x)
+  split (a, Right y) = Right (a, y)
+instance Coapplicative ((,) a) where
+  costrength (_, Left x) = Left x
+  costrength (a, Right y) = Right (a, y)
+  copure (_, x) = x
+
+instance Splittable ((,,) a b) where
+  nonempty (_, _, v) = v
+  split (a, b, Left x) = Left (a, b, x)
+  split (a, b, Right y) = Right (a, b, y)
+instance Coapplicative ((,,) a b) where
+  costrength (_, _, Left x) = Left x
+  costrength (a, b, Right y) = Right (a, b, y)
+  copure (_, _, x) = x
+
+instance Splittable ((,,,) a b c) where
+  nonempty (_, _, _, v) = v
+  split (a, b, c, Left x) = Left (a, b, c, x)
+  split (a, b, c, Right y) = Right (a, b, c, y)
+instance Coapplicative ((,,,) a b c) where
+  costrength (_, _, _, Left x) = Left x
+  costrength (a, b, c, Right y) = Right (a, b, c, y)
+  copure (_, _, _, x) = x
+
+instance Splittable ((,,,,) a b c d) where
+  nonempty (_, _, _, _, v) = v
+  split (a, b, c, d, Left x) = Left (a, b, c, d, x)
+  split (a, b, c, d, Right y) = Right (a, b, c, d, y)
+instance Coapplicative ((,,,,) a b c d) where
+  costrength (_, _, _, _, Left x) = Left x
+  costrength (a, b, c, d, Right y) = Right (a, b, c, d, y)
+  copure (_, _, _, _, x) = x
+
+instance Splittable ((,,,,,) a b c d e) where
+  nonempty (_, _, _, _, _, v) = v
+  split (a, b, c, d, e, Left x) = Left (a, b, c, d, e, x)
+  split (a, b, c, d, e, Right y) = Right (a, b, c, d, e, y)
+instance Coapplicative ((,,,,,) a b c d e) where
+  costrength (_, _, _, _, _, Left x) = Left x
+  costrength (a, b, c, d, e, Right y) = Right (a, b, c, d, e, y)
+  copure (_, _, _, _, _, x) = x
+
+instance Splittable ((,,,,,,) a b c d e f) where
+  nonempty (_, _, _, _, _, _, v) = v
+  split (a, b, c, d, e, f, Left x) = Left (a, b, c, d, e, f, x)
+  split (a, b, c, d, e, f, Right y) = Right (a, b, c, d, e, f, y)
+instance Coapplicative ((,,,,,,) a b c d e f) where
+  costrength (_, _, _, _, _, _, Left x) = Left x
+  costrength (a, b, c, d, e, f, Right y) = Right (a, b, c, d, e, f, y)
+  copure (_, _, _, _, _, _, x) = x
+
+instance Splittable w => Splittable (EnvT e w) where
+  nonempty (EnvT _ wv) = nonempty wv
+  split (EnvT e we) = bimap (EnvT e) (EnvT e) (split we)
+  splitMaybe (EnvT e wm) = EnvT e <$> splitMaybe wm
+  splitList (EnvT e wxs) = EnvT e <$> splitList wxs
+instance Coapplicative w => Coapplicative (EnvT e w) where
+  costrength (EnvT e wx) = bimap id (EnvT e) $ costrength wx
+  copure (EnvT _ wx) = copure wx
+
+-- | In order to have a consistent view of the context, we must be able
+-- to replace non-matching parts of the context in a consistent way.
+--
+-- Largely no Monoid can satisfy this, but this instance is provided because
+-- it exists, and because it is a non-trivial law-abiding instance
+-- which is not filtering a zipper.
+--
+-- Creating non-law-abiding TinyGroup instances will allow for this instance
+-- to be used in a way which is not quite compatible with the Comonad instance.
+instance (Splittable w, TinyGroup m) => Splittable (TracedT m w) where
+  nonempty = nonempty . fmap (\t -> t mempty) . runTracedT
+  split = coerce . split . fmap splitCyclic . runTracedT
+    where
+      -- This is somewhat overkill now
+      splitCyclic :: TinyGroup m => (m -> Either a b) -> Either (m -> a) (m -> b)
+      splitCyclic t =
+        case t mempty of
+          Left _ -> Left findLefts
+          Right _ -> Right findRights
+        where
+          -- These terminate because generator will eventually
+          -- cover the entire group, and by the calling condition
+          -- we know that at least one element will eventually
+          -- be found on the correct side of the Either
+          findLefts i =
+            case t i of
+              Left x -> x
+              Right _ -> findLefts (i <> generator)
+          findRights i =
+            case t i of
+              Left _ -> findRights (i <> generator)
+              Right x -> x
+instance (Coapplicative w, TinyGroup m) => Coapplicative (TracedT m w) where
+  copure (TracedT wa) = copure (($ mempty) <$> wa)
+
+instance Splittable f => Splittable (M1 i c f) where
+  nonempty (M1 fv) = nonempty fv
+  split (M1 fab) = coerce (split fab)
+  splitMaybe (M1 fa) = M1 <$> splitMaybe fa
+  splitList (M1 fxs) = M1 <$> splitList fxs
+instance Coapplicative f => Coapplicative (M1 i c f) where
+  copure (M1 fa) = copure fa
+
+-- identical to Sum
+instance (Splittable f, Splittable g) => Splittable (f :+: g) where
+  nonempty (L1 fv) = nonempty fv
+  nonempty (R1 gv) = nonempty gv
+  split (L1 fe) = bimap L1 L1 (split fe)
+  split (R1 ge) = bimap R1 R1 (split ge)
+  splitMaybe (L1 fm) = L1 <$> (splitMaybe fm)
+  splitMaybe (R1 gm) = R1 <$> (splitMaybe gm)
+  splitList (L1 fxs) = L1 <$> (splitList fxs)
+  splitList (R1 gxs) = R1 <$> (splitList gxs)
+instance (Coapplicative f, Coapplicative g) => Coapplicative (f :+: g) where
+  copure (L1 fa) = copure fa
+  copure (R1 ga) = copure ga
+  costrength (L1 fa) = bimap id L1 $ costrength fa
+  costrength (R1 ga) = bimap id R1 $ costrength ga
+
+instance (Splittable f, Splittable g) => Splittable (f :.: g) where
+  nonempty (Comp1 fgv) = nonempty (nonempty <$> fgv)
+  split (Comp1 fgab) =
+    coerce $
+    split (fmap split fgab)
+  splitMaybe (Comp1 fga) = fmap Comp1 $ splitMaybe $ fmap splitMaybe fga
+  splitList (Comp1 fgxs) = fmap Comp1 $ splitList $ fmap splitList fgxs
+instance (Coapplicative f, Coapplicative g) => Coapplicative (f :.: g) where
+  copure (Comp1 fgx) = copure $ copure <$> fgx
+  costrength (Comp1 fgx) =
+    coerce $ costrength $ fmap costrength fgx
+
+instance Splittable Par1 where
+  nonempty (Par1 v) = v
+  split (Par1 (Left a)) = Left (Par1 a)
+  split (Par1 (Right a)) = Right (Par1 a)
+  splitMaybe (Par1 m) = Par1 <$> m
+  splitList (Par1 xs) = Par1 <$> xs
+instance Coapplicative Par1 where
+  copure (Par1 x) = x
+
+instance Splittable f => Splittable (Rec1 f) where
+  nonempty (Rec1 fv) = nonempty fv
+  split (Rec1 fab) = coerce (split fab)
+  splitMaybe (Rec1 fa) = coerce $ splitMaybe fa
+  splitList (Rec1 fxs) = coerce $ splitList fxs
+instance Coapplicative f => Coapplicative (Rec1 f) where
+  copure (Rec1 fx) = copure fx
+  costrength (Rec1 fx) = coerce $ costrength fx
+
+instance (Generic1 f, Splittable (Rep1 f)) => Splittable (Generically1 f) where
+  nonempty (Generically1 fa) = nonempty (from1 fa)
+  split (Generically1 fab) =
+    bimap (Generically1 . to1) (Generically1 . to1)
+    (split (from1 fab))
+  splitMaybe (Generically1 fa) = fmap Generically1 $ fmap to1 $ splitMaybe $ from1 fa
+  splitList (Generically1 fxs) = fmap Generically1 $ fmap to1 $ splitList $ from1 fxs
+instance (Generic1 f, Coapplicative (Rep1 f)) => Coapplicative (Generically1 f) where
+  copure (Generically1 fx) = copure (from1 fx)
+  costrength (Generically1 fx) = bimap id (Generically1 . to1) $ costrength $ from1 fx
+
+-- | There is a derivable instance for any Comonad,
+-- but this will not be compatible with context shifts for most instances.
+-- 
+-- In the context of pattern-matching, this means that reaching the same branch
+-- two different ways may result in conflicting views of the surrounding context.
+-- (only the context which lands on the same side of the branch is consistent)
+newtype ComonadCoapp w a = ComonadCoapp { runComonadCoapp :: w a } deriving (Functor)
+
+instance Comonad w => Splittable (ComonadCoapp w) where
+  nonempty (ComonadCoapp wv) = extract wv
+  split (ComonadCoapp wab) =
+    case extract wab of
+      Left x -> Left (ComonadCoapp $ fmap (either id (const x)) wab)
+      Right y -> Right (ComonadCoapp $ fmap (either (const y) id) wab)
+instance Comonad w => Coapplicative (ComonadCoapp w) where
+  copure (ComonadCoapp wx) = extract wx
+  costrength (ComonadCoapp wab) =
+    case extract wab of
+      Left x -> Left x
+      Right y -> Right (ComonadCoapp $ fmap (either (const y) id) wab)
+
+instance Comonad w => Comonad (ComonadCoapp w) where
+  extract = extract . runComonadCoapp
+  {- coerce gets blocked by unknown roles sadly -}
+  duplicate (ComonadCoapp wa) = ComonadCoapp (fmap ComonadCoapp (duplicate wa))
+
+
diff --git a/src/Control/Coapplicative/Traced.hs b/src/Control/Coapplicative/Traced.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Coapplicative/Traced.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+-- | This module includes the TinyCyclic typeclass,
+-- which is used for the Coapplciative instance of Traced
+-- (although that instance is in the main module Control.Coapplicative)
+module Control.Coapplicative.Traced (TinyGroup(..)) where
+
+import Data.Bits (Xor(..))
+
+-- | Traced has only a single non-trivial way to make a Coapplicative
+-- instance which agrees with Comonad's duplicate
+--
+-- Specifically, the Monoid must be either trivial or equivalent to Z2
+-- That is to say, it must be a group and every element must be equal
+-- to the generator or equal to mempty
+--
+-- This typeclass is provided so that it is possible to supply other
+-- instances which are not law-abiding
+class Monoid m => TinyGroup m where
+  generator :: m
+
+instance TinyGroup () where
+  generator = ()
+
+instance TinyGroup (Xor Bool) where
+  generator = Xor True
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,15 +1,20 @@
 {-# LANGUAGE DeriveAnyClass, DeriveGeneric, DeriveFunctor, DerivingStrategies, DerivingVia #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
 
 module Main (main) where
 
 import GHC.Generics
-import Control.CoApplicative
+import Control.Coapplicative
+import Control.Coapplicative.Traced
 import Data.List.NonEmpty
+import Data.Functor.Classes (Eq1(..), Show1(..))
 import Data.Functor.Sum
 import Data.Functor.Identity
 import Control.Comonad
+import Control.Comonad.Traced hiding (Sum)
 import Data.Bifunctor
+import Data.Bits (Xor(..))
 
 import Hedgehog
 import qualified Hedgehog.Gen as Gen
@@ -21,36 +26,171 @@
   | C (NonEmpty a)
   | D (Int, String, a)
   deriving stock (Generic, Generic1, Functor, Show)
-  deriving CoApplicative via (Generically1 Ex)
+  deriving (Splittable, Coapplicative) via (Generically1 Ex)
+instance Eq1 Ex where
+  liftEq e x y =
+    case (x, y) of
+      (A fx, A fy) -> liftEq e fx fy
+      (B x, B y) -> e x y
+      (C xs, C ys) -> liftEq e xs ys
+      (D (i1, s1, x), D (i2, s2, y)) ->
+        i1 == i2 && s1 == s2 && e x y
+      _ -> False
+instance Eq a => Eq (Ex a) where
+  (==) = liftEq (==)
+instance Show1 Ex where
+  liftShowsPrec showA shows i ex _ = "TODO Show1 Ex"
 
 testCompiles :: IO ()
-testCompiles = print (split (B x))
+testCompiles = do
+  print (split (B x))
  where
   x :: Either Int Bool
   x = Left 4
 
 someInt :: Gen Int
-someInt = Gen.int $ Range.constant 0 10
+someInt = Gen.int $ Range.constant 0 9
 
 someInt2 :: Gen Int
-someInt2 = Gen.int $ Range.constant 11 20
+someInt2 = Gen.int $ Range.constant 10 19
 
 someInt3 :: Gen Int
-someInt3 = Gen.int $ Range.constant 21 30
+someInt3 = Gen.int $ Range.constant 20 29
 
+genEx :: Gen a -> Gen (Ex a)
+genEx ga =
+  -- doesn't matter
+  let genString = Gen.string (Range.constant 0 5) Gen.binit in
+  Gen.choice [
+    A <$> (Gen.choice [pure (InL . Identity), pure (InR . Identity)] <*> ga),
+    B <$> ga,
+    C <$> Gen.nonEmpty (Range.constant 0 20) ga,
+    D <$> ((,,) <$> someInt <*> genString <*> ga)
+  ]
+
 prop_nonEmptyDupSplit :: Property
 prop_nonEmptyDupSplit = property $ do
-  xs <- forAll $ Gen.nonEmpty (Range.linear 1 20) $ Gen.either someInt someInt
+  xs <- forAll $ Gen.nonEmpty (Range.linear 0 20) $ Gen.either someInt someInt
   bimap duplicate duplicate (split xs) === split (fmap split (duplicate xs))
 
+
+-- TODO use a newtype instead so we can verify all properties easily;
+-- mechanized though so lower priority
+prop_tracedXorDupSplit :: Property
+prop_tracedXorDupSplit = property $ do
+  i <- forAll $ Gen.either someInt someInt
+  j <- forAll $ Gen.either someInt2 someInt2
+  let toFn (i, j) b =
+        case b of
+          Xor False -> i
+          Xor True -> j
+      toFn' = traced . toFn
+      fromFn (TracedT (Identity f)) = (f $ Xor False, f $ Xor True)
+      fromFn' = fromFn . fmap fromFn
+      fromFns = bimap fromFn' fromFn'
+
+      f :: Traced (Xor Bool) (Either Int Int)
+      f = toFn' (i, j)
+  annotate $ show $ fromFn' $ duplicate f
+  fromFns (bimap duplicate duplicate (split f)) ===
+    fromFns (split (fmap split (duplicate f)))
+
+-- Use only when we find something that isn't a comonad :)
+pred_validSplit :: (Splittable f, Eq1 f, Show1 f) => (forall a. Gen a -> Gen (f a)) -> Property
+pred_validSplit gen = property $ do
+  xs <- forAll $ gen (Gen.either someInt someInt2)
+  let left :: a -> Either a Bool
+      left = Left
+      right :: a -> Either Bool a
+      right = Right
+  split (left <$> xs) === Left xs
+  split (right <$> xs) === Right xs
+  f <- (*) <$> forAll someInt
+  g <- (+) <$> forAll someInt
+
+  bimap (fmap f) (fmap g) (split xs) === split (bimap f g <$> xs)
+
+pred_validComonadCoapplicative :: (Coapplicative w, Comonad w, Eq1 w, Show1 w)
+                               => (forall a. Gen a -> Gen (w a)) -> Property
+pred_validComonadCoapplicative gen = property $ do
+  xs <- forAll $ gen (Gen.either someInt someInt2)
+  -- copy-paste to not regen
+  let left :: a -> Either a Bool
+      left = Left
+      right :: a -> Either Bool a
+      right = Right
+  split (left <$> xs) === Left xs
+  split (right <$> xs) === Right xs
+  f <- (*) <$> forAll someInt
+  g <- (+) <$> forAll someInt
+
+  bimap (fmap f) (fmap g) (split xs) === split (bimap f g <$> xs)
+
+  -- nonempty laws are trivial
+  bimap extract extract (split xs) === extract xs
+  bimap duplicate duplicate (split xs) === split (fmap split (duplicate xs))
+
+  copure xs === extract xs
+  bimap copure id (split xs) === costrength xs
+  (costrength . fmap costrength) (duplicate xs) ===
+    bimap id duplicate (costrength xs)
+
+
+{-
+data Z3 = Z0 | Z1 | Z2
+instance Semigroup Z3 where
+  Z0 <> x = x
+  x <> Z0 = x
+  Z1 <> Z1 = Z2
+  Z1 <> Z2 = Z0
+  Z2 <> Z1 = Z0
+  Z2 <> Z2 = Z1
+
+instance Monoid Z3 where
+  mempty = Z0
+
+instance FinCyclic Z3 where
+  generator = Z1
+
+prop_tracedDupSplit :: Property
+prop_tracedDupSplit = property $ do
+  i <- forAll $ Gen.either someInt someInt
+  j <- forAll $ Gen.either someInt2 someInt2
+  k <- forAll $ Gen.either someInt3 someInt3
+
+  let toFn (i, j, k) z3 =
+        case z3 of
+          Z0 -> i
+          Z1 -> j
+          Z2 -> k
+      toFn' = traced . toFn
+      fromFn :: Traced Z3 a -> (a, a, a)
+      fromFn (TracedT (Identity f)) = (f Z0, f Z1, f Z2)
+      fromFn' :: Traced Z3 (Traced Z3 a) -> ((a, a, a), (a, a, a), (a, a, a))
+      fromFn' = fromFn . fmap fromFn
+      fromFns :: Either (Traced Z3 (Traced Z3 a)) (Traced Z3 (Traced Z3 a)) ->
+                 Either ((a, a, a), (a, a, a), (a, a, a))
+                        ((a, a, a), (a, a, a), (a, a, a))
+      fromFns = bimap fromFn' fromFn'
+
+      f :: Traced Z3 (Either Int Int)
+      f = toFn' (i, j, k)
+  annotate $ show $ fromFn' $ duplicate f
+  fromFns (bimap duplicate duplicate (split f)) ===
+    fromFns (split (fmap split (duplicate f)))
+    -}
+
 testProps :: IO Bool
 testProps =
+  let genNE = Gen.nonEmpty (Range.linear 1 20) in
   checkParallel $ Group "Properties" [
-      ("nonempty_dup_split", prop_nonEmptyDupSplit)
+      ("traced_xor_dup_split", prop_tracedXorDupSplit),
+      ("nonempty_valid", pred_validComonadCoapplicative genNE),
+      ("generics_split", pred_validSplit genEx)
     ]
 
 main :: IO ()
 main = do
-  testCompiles
+  let _ = testCompiles
   _ <- testProps
   pure ()