diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,57 @@
 Changelog
 =========
 
+Version 0.2.0.0
+---------------
+
+*November 11, 2019*
+
+<https://github.com/mstksg/functor-combinators/releases/tag/v0.2.0.0>
+
+*   Major restructuring of the hbifunctor-based classes. `Data.HBifunctor.Associative`
+    and `Data.HBifunctor.Tensor` are more or less completely rewritten; the
+    typeclasses are restructured in order to more properly reflect the math
+    that motivates them.  See the updated type classes to see what methods
+    ended up where.
+
+    However, much of the external API that is independent of the underlying
+    abstraction is effectively unchanged (`biget`, etc.)
+
+    For the most part, the migration would involve:
+
+    *   `SF`, `MF` are now `NonEmptyBy` and `ListBy`, respectively.
+    *   `-SF` and `-MF` as suffixes for function names now become `-NE` and
+        `-LB`.
+
+*   Restructuring of `Interpret`: It now takes an extra type parameter, the
+    type to interpret into.  This makes it more consistent with the new `MonoidIn`
+    and `SemigroupIn`.  Most of the external API should be effectively
+    unchanged.
+
+    For the most part, the migration would only affect people who *write*
+    instances of `Interpret`.  Instead of
+
+    ```haskell
+    instance Interpret MyType where
+        type C MyType = Monad
+    ```
+
+    you would write:
+
+    ```haskell
+    instance Monad f => Interpret MyType f where
+    ```
+
+
+Version 0.1.1.1
+---------------
+
+*July 13, 2019*
+
+<https://github.com/mstksg/functor-combinators/releases/tag/v0.1.1.1>
+
+*   Moved to *trivial-constraints-0.6.0.0*
+
 Version 0.1.1.0
 ---------------
 
diff --git a/functor-combinators.cabal b/functor-combinators.cabal
--- a/functor-combinators.cabal
+++ b/functor-combinators.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: fe8311fa4240fa72d0cf9023f7b1410f94e3b6bbee3bb8ba0164ecf28d7265d0
+-- hash: 6adc855dec7f54345b5714740988109de58bf4e1fc0b788594bb77e11f29974e
 
 name:           functor-combinators
-version:        0.1.1.1
+version:        0.2.0.0
 synopsis:       Tools for functor combinator-based program design
 description:    Tools for working with /functor combinators/: types that take functors (or
                 other indexed types) and returns a new functor that "enhances" or "mixes"
@@ -65,6 +65,7 @@
       Data.HFunctor.Internal
   hs-source-dirs:
       src
+  default-extensions: AllowAmbiguousTypes ConstraintKinds DataKinds DefaultSignatures DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies EmptyCase ExistentialQuantification ExplicitNamespaces FlexibleContexts FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving InstanceSigs KindSignatures LambdaCase MultiParamTypeClasses OverloadedStrings PatternSynonyms QuantifiedConstraints RankNTypes ScopedTypeVariables StandaloneDeriving TemplateHaskell TupleSections TypeApplications TypeFamilies TypeInType TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
   ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns
   build-depends:
       base >=4.12 && <5
@@ -85,7 +86,7 @@
     , tagged
     , these
     , transformers
-    , trivial-constraint >=0.6
+    , trivial-constraint >=0.5
     , vinyl
   default-language: Haskell2010
 
@@ -99,6 +100,7 @@
       Paths_functor_combinators
   hs-source-dirs:
       test
+  default-extensions: AllowAmbiguousTypes ConstraintKinds DataKinds DefaultSignatures DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies EmptyCase ExistentialQuantification ExplicitNamespaces FlexibleContexts FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving InstanceSigs KindSignatures LambdaCase MultiParamTypeClasses OverloadedStrings PatternSynonyms QuantifiedConstraints RankNTypes ScopedTypeVariables StandaloneDeriving TemplateHaskell TupleSections TypeApplications TypeFamilies TypeInType TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
   ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.12 && <5
diff --git a/src/Control/Applicative/ListF.hs b/src/Control/Applicative/ListF.hs
--- a/src/Control/Applicative/ListF.hs
+++ b/src/Control/Applicative/ListF.hs
@@ -1,14 +1,3 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable     #-}
-{-# LANGUAGE DeriveFunctor      #-}
-{-# LANGUAGE DeriveGeneric      #-}
-{-# LANGUAGE DeriveTraversable  #-}
-{-# LANGUAGE LambdaCase         #-}
-{-# LANGUAGE PatternSynonyms    #-}
-{-# LANGUAGE TemplateHaskell    #-}
-{-# LANGUAGE TypeOperators      #-}
-{-# LANGUAGE ViewPatterns       #-}
-
 -- |
 -- Module      : Control.Applicative.ListF
 -- Copyright   : (c) Justin Le 2019
diff --git a/src/Control/Applicative/Step.hs b/src/Control/Applicative/Step.hs
--- a/src/Control/Applicative/Step.hs
+++ b/src/Control/Applicative/Step.hs
@@ -1,22 +1,4 @@
-{-# LANGUAGE AllowAmbiguousTypes        #-}
-{-# LANGUAGE DeriveDataTypeable         #-}
-{-# LANGUAGE DeriveFoldable             #-}
-{-# LANGUAGE DeriveFunctor              #-}
-{-# LANGUAGE DeriveGeneric              #-}
-{-# LANGUAGE DeriveTraversable          #-}
-{-# LANGUAGE EmptyCase                  #-}
-{-# LANGUAGE EmptyDataDeriving          #-}
-{-# LANGUAGE ExistentialQuantification  #-}
-{-# LANGUAGE FlexibleInstances          #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE PolyKinds                  #-}
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE TemplateHaskell            #-}
-{-# LANGUAGE TypeApplications           #-}
-{-# LANGUAGE TypeInType                 #-}
-{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE EmptyDataDeriving #-}
 
 -- |
 -- Module      : Control.Applicative.Step
diff --git a/src/Control/Monad/Freer/Church.hs b/src/Control/Monad/Freer/Church.hs
--- a/src/Control/Monad/Freer/Church.hs
+++ b/src/Control/Monad/Freer/Church.hs
@@ -1,17 +1,3 @@
-{-# LANGUAGE EmptyCase                 #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleInstances         #-}
-{-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE KindSignatures            #-}
-{-# LANGUAGE LambdaCase                #-}
-{-# LANGUAGE MultiParamTypeClasses     #-}
-{-# LANGUAGE PatternSynonyms           #-}
-{-# LANGUAGE RankNTypes                #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
-{-# LANGUAGE TypeApplications          #-}
-{-# LANGUAGE TypeOperators             #-}
-{-# LANGUAGE ViewPatterns              #-}
-
 -- |
 -- Module      : Control.Monad.Freer.Church
 -- Copyright   : (c) Justin Le 2019
diff --git a/src/Control/Natural/IsoF.hs b/src/Control/Natural/IsoF.hs
--- a/src/Control/Natural/IsoF.hs
+++ b/src/Control/Natural/IsoF.hs
@@ -1,8 +1,3 @@
-{-# LANGUAGE DeriveFunctor      #-}
-{-# LANGUAGE ExplicitNamespaces #-}
-{-# LANGUAGE RankNTypes         #-}
-{-# LANGUAGE TypeOperators      #-}
-
 -- |
 -- Module      : Control.Natural.IsoF
 -- Copyright   : (c) Justin Le 2019
@@ -20,11 +15,11 @@
   , isoF
   , viewF, reviewF, overF
   , fromF
-  , Exchange(..)
   ) where
 
-import           Data.Profunctor
 import           Control.Natural
+import           Data.Kind
+import           Data.Profunctor
 import           Data.Tagged
 
 -- | The type of an isomorphism between two functors.  @f '<~>' g@ means that
@@ -105,15 +100,7 @@
 -- 'reviewF' ('fromF' i) == 'viewF' i
 -- @
 fromF
-    :: f <~> g
+    :: forall (f :: Type -> Type) (g :: Type -> Type). ()
+    => f <~> g
     -> g <~> f
-fromF i = isoF g f
-  where
-    Exchange f g = i (Exchange id id)
-
--- | Profunctor that allows us to implement 'fromF'.
-data Exchange a b s t = Exchange (s -> a) (b -> t)
-  deriving Functor
-
-instance Profunctor (Exchange a b) where
-    dimap f g (Exchange x y) = Exchange (x . f) (g . y)
+fromF i = isoF (reviewF i) (viewF i)
diff --git a/src/Data/Functor/Apply/Free.hs b/src/Data/Functor/Apply/Free.hs
--- a/src/Data/Functor/Apply/Free.hs
+++ b/src/Data/Functor/Apply/Free.hs
@@ -1,16 +1,3 @@
-{-# LANGUAGE DeriveFunctor       #-}
-{-# LANGUAGE GADTs               #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE PatternSynonyms     #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving  #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE ViewPatterns        #-}
-
 -- |
 -- Module      : Data.Functor.Apply.Free
 -- Copyright   : (c) Justin Le 2019
@@ -123,9 +110,7 @@
 instance HBind Ap1 where
     hbind = runAp1
 
-instance Interpret Ap1 where
-    type C Ap1 = Apply
-
+instance Apply f => Interpret Ap1 f where
     retract = retractAp1
     interpret = runAp1
 
diff --git a/src/Data/Functor/Combinator.hs b/src/Data/Functor/Combinator.hs
--- a/src/Data/Functor/Combinator.hs
+++ b/src/Data/Functor/Combinator.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ExplicitNamespaces #-}
-
 -- |
 -- Module      : Data.Functor.Combinator
 -- Copyright   : (c) Justin Le 2019
@@ -16,7 +14,7 @@
 --
 -- *  'HFunctor' and 'HBifunctor', used to swap out the functors that the
 --    combinators modify
--- *  'Interpret', 'Associative', 'Monoidal', used to inject and interpret
+-- *  'Interpret', 'Associative', 'Tensor', used to inject and interpret
 -- functor values with respect to their combinators.
 --
 -- We have some helpful utility functions, as well, built on top of these
@@ -53,16 +51,15 @@
   , HBifunctor(..)
   -- *** Associative
   , Associative(..)
-  , Semigroupoidal(SF, appendSF, consSF, toSF, biretract, binterpret)
-  , CS
+  , SemigroupIn(..)
   , biget, bicollect
   , (!*!)
+  , (!+!)
   , (!$!)
   -- *** Tensor
   , Tensor(..)
-  , Monoidal(MF, appendMF, splitSF, toMF, fromSF, pureT, upgradeC)
-  , CM
-  , nilMF, consMF
+  , MonoidIn(..)
+  , nilLB, consLB
   , inL, inR
   , outL, outR
   -- * Combinators
diff --git a/src/Data/Functor/Combinator/Unsafe.hs b/src/Data/Functor/Combinator/Unsafe.hs
--- a/src/Data/Functor/Combinator/Unsafe.hs
+++ b/src/Data/Functor/Combinator/Unsafe.hs
@@ -1,7 +1,3 @@
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-
 -- |
 -- Module      : Data.Functor.Combinator.Unsafe
 -- Copyright   : (c) Justin Le 2019
diff --git a/src/Data/HBifunctor.hs b/src/Data/HBifunctor.hs
--- a/src/Data/HBifunctor.hs
+++ b/src/Data/HBifunctor.hs
@@ -1,19 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable   #-}
-{-# LANGUAGE DeriveFoldable       #-}
-{-# LANGUAGE DeriveFunctor        #-}
-{-# LANGUAGE DeriveGeneric        #-}
-{-# LANGUAGE DeriveTraversable    #-}
-{-# LANGUAGE DerivingVia          #-}
-{-# LANGUAGE KindSignatures       #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE StandaloneDeriving   #-}
-{-# LANGUAGE TemplateHaskell      #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ViewPatterns         #-}
+{-# LANGUAGE DerivingVia #-}
 
 -- |
 -- Module      : Data.HBifunctor
@@ -38,7 +23,6 @@
 import           Control.Natural.IsoF
 import           Data.Biapplicative
 import           Data.Bifunctor.TH
-import           Data.Constraint.Trivial
 import           Data.Data
 import           Data.Deriving
 import           Data.HFunctor
@@ -102,19 +86,18 @@
 instance HBifunctor RightF where
     hbimap _ g (RightF x) = RightF (g x)
 
-deriving via (WrappedHBifunctor RightF f)
-    instance HFunctor (RightF f)
+deriving via (WrappedHBifunctor RightF g)
+    instance HFunctor (RightF g)
 
-instance HFunctor (RightF f) where
+instance HFunctor (RightF g) where
     hmap f (RightF x) = RightF (f x)
 
-instance Inject (RightF f) where
+instance Inject (RightF g) where
     inject = RightF
 
-instance HBind (RightF f) where
+instance HBind (RightF g) where
     hbind f (RightF x) = f x
 
-instance Interpret (RightF f) where
-    type C (RightF f) = Unconstrained
+instance Interpret (RightF g) f where
     retract (RightF x) = x
     interpret f (RightF x) = f x
diff --git a/src/Data/HBifunctor/Associative.hs b/src/Data/HBifunctor/Associative.hs
--- a/src/Data/HBifunctor/Associative.hs
+++ b/src/Data/HBifunctor/Associative.hs
@@ -1,37 +1,4 @@
-{-# LANGUAGE AllowAmbiguousTypes        #-}
-{-# LANGUAGE ConstraintKinds            #-}
-{-# LANGUAGE DefaultSignatures          #-}
-{-# LANGUAGE DeriveDataTypeable         #-}
-{-# LANGUAGE DeriveFoldable             #-}
-{-# LANGUAGE DeriveFunctor              #-}
-{-# LANGUAGE DeriveGeneric              #-}
-{-# LANGUAGE DeriveTraversable          #-}
-{-# LANGUAGE DerivingStrategies         #-}
-{-# LANGUAGE DerivingVia                #-}
-{-# LANGUAGE EmptyCase                  #-}
-{-# LANGUAGE EmptyDataDeriving          #-}
-{-# LANGUAGE FlexibleContexts           #-}
-{-# LANGUAGE FlexibleInstances          #-}
-{-# LANGUAGE FunctionalDependencies     #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE InstanceSigs               #-}
-{-# LANGUAGE KindSignatures             #-}
-{-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE MultiParamTypeClasses      #-}
-{-# LANGUAGE PatternSynonyms            #-}
-{-# LANGUAGE QuantifiedConstraints      #-}
-{-# LANGUAGE RankNTypes                 #-}
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE StandaloneDeriving         #-}
-{-# LANGUAGE TemplateHaskell            #-}
-{-# LANGUAGE TupleSections              #-}
-{-# LANGUAGE TypeApplications           #-}
-{-# LANGUAGE TypeFamilies               #-}
-{-# LANGUAGE TypeInType                 #-}
-{-# LANGUAGE TypeOperators              #-}
-{-# LANGUAGE UndecidableInstances       #-}
-{-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE DerivingVia #-}
 
 -- |
 -- Module      : Data.HBifunctor.Associative
@@ -51,42 +18,38 @@
 -- The high-level usage of this is
 --
 -- @
--- 'biretract' :: t f f ~> f
+-- 'biretract' :: 'SemigroupIn' t f => t f f ~> f
 -- @
 --
 -- which lets you fully "mix" together the two input functors.
 --
--- This class also associates each 'HBifunctor' with its "semigroup functor
--- combinator", so we can "squish together" repeated applications of @t@.
---
--- That is, an @'SF' t f a@ is either:
---
--- *   @f a@
--- *   @t f f a@
--- *   @t f (t f f) a@
--- *   @t f (t f (t f f)) a@
--- *   .. etc.
---
--- which means we can have "list-like" schemas that represent multiple
--- copies of @f@.
+-- @
+-- 'biretract' :: (f ':+:' f) a -> f a
+-- biretract :: 'Plus' f => (f ':*:' f) a -> f a
+-- biretract :: 'Applicative' f => 'Day' f f a -> f a
+-- biretract :: 'Monad' f => 'Comp' f f a -> f a
+-- @
 --
--- See "Data.HBifunctor.Tensor" for a version that also provides an analogy
--- to 'inject', and a more flexible "squished" combinator
--- 'Data.HBifunctor.Tensor.MF' that has an "empty" element.
+-- See "Data.HBifunctor.Tensor" for the next stage of structure in tensors
+-- and moving in and out of them.
 module Data.HBifunctor.Associative (
   -- * 'Associative'
     Associative(..)
   , assoc
   , disassoc
-  -- * 'Semigroupoidal'
-  , Semigroupoidal(..)
-  , CS
-  , matchingSF
+  -- * 'SemigroupIn'
+  , SemigroupIn(..)
+  , matchingNE
+  , retractNE
+  , interpretNE
   -- ** Utility
   , biget
   , bicollect
   , (!*!)
   , (!$!)
+  , (!+!)
+  , WrapHBF(..)
+  , WrapNE(..)
   ) where
 
 import           Control.Applicative
@@ -94,6 +57,7 @@
 import           Control.Applicative.Step
 import           Control.Monad.Freer.Church
 import           Control.Monad.Trans.Compose
+import           Control.Monad.Trans.Identity
 import           Control.Natural
 import           Control.Natural.IsoF
 import           Data.Bifunctor.Joker
@@ -102,6 +66,7 @@
 import           Data.Foldable
 import           Data.Functor.Apply.Free
 import           Data.Functor.Bind
+import           Data.Functor.Classes
 import           Data.Functor.Day             (Day(..))
 import           Data.Functor.Identity
 import           Data.Functor.Plus
@@ -114,7 +79,7 @@
 import           Data.HFunctor.Interpret
 import           Data.Kind
 import           Data.List.NonEmpty           (NonEmpty(..))
-import           GHC.Generics hiding          (C)
+import           GHC.Generics
 import qualified Data.Functor.Day             as D
 import qualified Data.Map.NonEmpty            as NEM
 
@@ -129,14 +94,74 @@
 -- @
 --
 -- We know that @f :*: (g :*: h)@ is the same as @(f :*: g) :*: h@.
-class HBifunctor t => Associative t where
+--
+-- Formally, we can say that @t@ enriches a the category of
+-- endofunctors with semigroup strcture: it turns our endofunctor category
+-- into a "semigroupoidal category".
+--
+-- Different instances of @t@ each enrich the endofunctor category in
+-- different ways, giving a different semigroupoidal category.
+class (HBifunctor t, Inject (NonEmptyBy t)) => Associative t where
+    -- | The "semigroup functor combinator" generated by @t@.
+    --
+    -- A value of type @NonEmptyBy t f a@ is /equivalent/ to one of:
+    --
+    -- *  @f a@
+    -- *  @t f f a@
+    -- *  @t f (t f f) a@
+    -- *  @t f (t f (t f f)) a@
+    -- *  @t f (t f (t f (t f f))) a@
+    -- *  .. etc
+    --
+    -- For example, for ':*:', we have 'NonEmptyF'.  This is because:
+    --
+    -- @
+    -- x             ~ 'NonEmptyF' (x ':|' [])      ~ 'inject' x
+    -- x ':*:' y       ~ NonEmptyF (x :| [y])     ~ 'toNonEmptyBy' (x :*: y)
+    -- x :*: y :*: z ~ NonEmptyF (x :| [y,z])
+    -- -- etc.
+    -- @
+    --
+    -- You can create an "singleton" one with 'inject', or else one from
+    -- a single @t f f@ with 'toNonEmptyBy'.
+    --
+    -- See 'Data.HBifunctor.Tensor.ListBy' for a "possibly empty" version
+    -- of this type.
+    type NonEmptyBy t :: (Type -> Type) -> Type -> Type
+
     -- | The isomorphism between @t f (t g h) a@ and @t (t f g) h a@.  To
     -- use this isomorphism, see 'assoc' and 'disassoc'.
     associating
         :: (Functor f, Functor g, Functor h)
         => t f (t g h) <~> t (t f g) h
-    {-# MINIMAL associating #-}
 
+    -- | If a @'NonEmptyBy' t f@ represents multiple applications of @t f@ to
+    -- itself, then we can also "append" two @'NonEmptyBy' t f@s applied to
+    -- themselves into one giant @'NonEmptyBy' t f@ containing all of the @t f@s.
+    --
+    -- Note that this essentially gives an instance for @'SemigroupIn'
+    -- t (NonEmptyBy t f)@, for any functor @f@.
+    appendNE :: t (NonEmptyBy t f) (NonEmptyBy t f) ~> NonEmptyBy t f
+
+    -- | If a @'NonEmptyBy' t f@ represents multiple applications of @t f@
+    -- to itself, then we can split it based on whether or not it is just
+    -- a single @f@ or at least one top-level application of @t f@.
+    --
+    -- Note that you can recursively "unroll" a 'NonEmptyBy' completely
+    -- into a 'Data.HFunctor.Chain.Chain1' by using
+    -- 'Data.HFunctor.Chain.unrollNE'.
+    matchNE  :: Functor f => NonEmptyBy t f ~> f :+: t f (NonEmptyBy t f)
+
+    -- | Prepend an application of @t f@ to the front of a @'NonEmptyBy' t f@.
+    consNE :: t f (NonEmptyBy t f) ~> NonEmptyBy t f
+    consNE = appendNE . hleft inject
+
+    -- | Embed a direct application of @f@ to itself into a @'NonEmptyBy' t f@.
+    toNonEmptyBy :: t f f ~> NonEmptyBy t f
+    toNonEmptyBy = consNE . hright inject
+
+    {-# MINIMAL associating, appendNE, matchNE #-}
+
 -- | Reassociate an application of @t@.
 assoc
     :: (Associative t, Functor f, Functor g, Functor h)
@@ -151,139 +176,121 @@
     ~> t f (t g h)
 disassoc = reviewF associating
 
--- | For some @t@s, you can represent the act of applying a functor @f@ to
--- @t@ many times, as a single type.  That is, there is some type @'SF'
--- t f@ that is equivalent to one of:
---
--- *  @f a@                             -- 1 time
--- *  @t f f a@                         -- 2 times
--- *  @t f (t f f) a@                   -- 3 times
--- *  @t f (t f (t f f)) a@             -- 4 times
--- *  @t f (t f (t f (t f f))) a@       -- 5 times
--- *  .. etc
+-- | For different @'Associative' t@, we have functors @f@ that we can
+-- "squash", using 'biretract':
 --
--- This typeclass associates each @t@ with its "induced semigroupoidal
--- functor combinator" @'SF' t@.
+-- @
+-- t f f ~> f
+-- @
 --
--- This is useful because sometimes you might want to describe a type that
--- can be @t f f@, @t f (t f f)@, @t f (t f (t f f))@, etc.; "f applied to
--- itself", with at least one @f@.  This typeclass lets you use a type like
--- 'NonEmptyF' in terms of repeated applications of ':*:', or 'Ap1' in
--- terms of repeated applications of 'Day', or 'Free1' in terms of repeated
--- applications of 'Comp', etc.
+-- This gives us the ability to squash applications of @t@.
 --
--- For example, @f ':*:' f@ can be interpreted as "a free selection of two
--- @f@s", allowing you to specify "I have to @f@s that I can use".  If you
--- want to specify "I want 1, 2, or many different @f@s that I can use",
--- you can use @'NonEmptyF' f@.
+-- Formally, if we have @'Associative' t@, we are enriching the category of
+-- endofunctors with semigroup structure, turning it into a semigroupoidal
+-- category.  Different choices of @t@ give different semigroupoidal
+-- categories.
 --
--- At the high level, the main way to /use/ a 'Semigroupoidal' is with
--- 'biretract' and 'binterpret':
+-- A functor @f@ is known as a "semigroup in the (semigroupoidal) category
+-- of endofunctors on @t@" if we can 'biretract':
 --
 -- @
--- 'biretract' :: t f f '~>' f
--- 'binterpret' :: (f ~> h) -> (g ~> h) -> t f g ~> h
+-- t f f ~> f
 -- @
 --
--- which are like the 'HBifunctor' versions of 'retract' and 'interpret':
--- they fully "mix" together the two inputs of @t@.
+-- This gives us a few interesting results in category theory, which you
+-- can stil reading about if you don't care:
 --
--- Also useful is:
+-- *  /All/ functors are semigroups in the semigroupoidal category
+--    on ':+:'
+-- *  The class of functors that are semigroups in the semigroupoidal
+--    category on ':*:' is exactly the functors that are instances of
+--    'Alt'.
+-- *  The class of functors that are semigroups in the semigroupoidal
+--    category on 'Day' is exactly the functors that are instances of
+--    'Apply'.
+-- *  The class of functors that are semigroups in the semigroupoidal
+--    category on 'Comp' is exactly the functors that are instances of
+--    'Bind'.
 --
+-- Note that instances of this class are /intended/ to be written with @t@
+-- as a fixed type constructor, and @f@ to be allowed to vary freely:
+--
 -- @
--- 'toSF' :: t f f a -> SF t f a
+-- instance Bind f => SemigroupIn Comp f
 -- @
 --
--- Which converts a @t@ into its aggregate type 'SF'.
+-- Any other sort of instance and it's easy to run into problems with type
+-- inference.  If you want to write an instance that's "polymorphic" on
+-- tensor choice, use the 'WrapHBF' newtype wrapper over a type variable,
+-- where the second argument also uses a type constructor:
 --
--- In reality, most 'Semigroupoidal' instances are also
--- 'Data.HBifunctor.Tensor.Monoidal' instances, so you can think of the
--- separation as mostly to help organize functionality.  However, there are
--- two non-monoidal semigroupoidal instances of note: 'LeftF' and 'RightF',
--- which are higher order analogues of the 'Data.Semigroup.First' and
--- 'Data.Semigroup.Last' semigroups, roughly.
-class (Associative t, Interpret (SF t)) => Semigroupoidal t where
-    -- | The "semigroup functor combinator" generated by @t@.
-    --
-    -- A value of type @SF t f a@ is /equivalent/ to one of:
-    --
-    -- *  @f a@
-    -- *  @t f f a@
-    -- *  @t f (t f f) a@
-    -- *  @t f (t f (t f f)) a@
-    -- *  @t f (t f (t f (t f f))) a@
-    -- *  .. etc
-    --
-    -- For example, for ':*:', we have 'NonEmptyF'.  This is because:
-    --
-    -- @
-    -- x             ~ 'NonEmptyF' (x ':|' [])      ~ 'inject' x
-    -- x ':*:' y       ~ NonEmptyF (x :| [y])     ~ 'toSF' (x :*: y)
-    -- x :*: y :*: z ~ NonEmptyF (x :| [y,z])
-    -- -- etc.
-    -- @
-    --
-    -- You can create an "singleton" one with 'inject', or else one from
-    -- a single @t f f@ with 'toSF'.
-    type SF t :: (Type -> Type) -> Type -> Type
-
-    -- | If a @'SF' t f@ represents multiple applications of @t f@ to
-    -- itself, then we can also "append" two @'SF' t f@s applied to
-    -- themselves into one giant @'SF' t f@ containing all of the @t f@s.
-    appendSF :: t (SF t f) (SF t f) ~> SF t f
-    matchSF  :: Functor f => SF t f ~> f :+: t f (SF t f)
-
-    -- | Prepend an application of @t f@ to the front of a @'SF' t f@.
-    consSF :: t f (SF t f) ~> SF t f
-    consSF = appendSF . hleft inject
-
-    -- | Embed a direct application of @f@ to itself into a @'SF' t f@.
-    toSF :: t f f ~> SF t f
-    toSF = consSF . hright inject
-
+-- @
+-- instance SemigroupIn (WrapHBF t) (MyFunctor t i)
+-- @
+--
+-- This will prevent problems with overloaded instances.
+class Associative t => SemigroupIn t f where
     -- | The 'HBifunctor' analogy of 'retract'. It retracts /both/ @f@s
     -- into a single @f@, effectively fully mixing them together.
-    biretract :: CS t f => t f f ~> f
-    biretract = retract . toSF
+    --
+    -- This function makes @f@ a semigroup in the category of endofunctors
+    -- with respect to tensor @t@.
+    biretract :: t f f ~> f
 
+    default biretract :: Interpret (NonEmptyBy t) f => t f f ~> f
+    biretract = retract . consNE . hright inject
+
     -- | The 'HBifunctor' analogy of 'interpret'.  It takes two
     -- interpreting functions, and mixes them together into a target
     -- functor @h@.
+    --
+    -- Note that this is useful in the poly-kinded case, but it is not possible
+    -- to define generically for all 'SemigroupIn' because it only is defined
+    -- for @Type -> Type@ inputes.  See '!+!' for a version that is poly-kinded
+    -- for ':+:' in specific.
     binterpret
-        :: CS t h
-        => f ~> h
-        -> g ~> h
-        -> t f g ~> h
-    binterpret f g = retract . toSF . hbimap f g
+        :: g ~> f
+        -> h ~> f
+        -> t g h ~> f
 
-    {-# MINIMAL appendSF, matchSF #-}
+    default binterpret :: Interpret (NonEmptyBy t) f => (g ~> f) -> (h ~> f) -> t g h ~> f
+    binterpret f g = retract . toNonEmptyBy . hbimap f g
 
--- | Convenient alias for the constraint required for 'biretract',
--- 'binterpret', etc.
+-- | An implementation of 'retract' that works for any instance of
+-- @'SemigroupIn' t@ for @'NonEmptyBy' t@.
 --
--- It's usually a constraint on the target/result context of interpretation
--- that allows you to "exit" or "run" a @'Semigroupoidal' t@.
-type CS t = C (SF t)
+-- Can be useful as a default implementation if you already have
+-- 'SemigroupIn' implemented.
+retractNE :: forall t f. (SemigroupIn t f, Functor f) => NonEmptyBy t f ~> f
+retractNE = (id !*! biretract @t . hright (retractNE @t))
+          . matchNE @t
 
--- | An @'SF' t f@ represents the successive application of @t@ to @f@,
--- over and over again.   So, that means that an @'SF' t f@ must either be
--- a single @f@, or an @t f (SF t f)@.
+-- | An implementation of 'interpret' that works for any instance of
+-- @'SemigroupIn' t@ for @'NonEmptyBy' t@.
 --
--- 'matchingSF' states that these two are isomorphic.  Use 'matchSF' and
--- @'inject' '!*!' 'consSF'@ to convert between one and the other.
-matchingSF :: (Semigroupoidal t, Functor f) => SF t f <~> f :+: t f (SF t f)
-matchingSF = isoF matchSF (inject !*! consSF)
+-- Can be useful as a default implementation if you already have
+-- 'SemigroupIn' implemented.
+interpretNE :: forall t g f. (SemigroupIn t f, Functor f) => (g ~> f) -> NonEmptyBy t g ~> f
+interpretNE f = retractNE @t . hmap f
 
+-- | An @'NonEmptyBy' t f@ represents the successive application of @t@ to @f@,
+-- over and over again.   So, that means that an @'NonEmptyBy' t f@ must either be
+-- a single @f@, or an @t f (NonEmptyBy t f)@.
+--
+-- 'matchingNE' states that these two are isomorphic.  Use 'matchNE' and
+-- @'inject' '!*!' 'consNE'@ to convert between one and the other.
+matchingNE :: (Associative t, Functor f) => NonEmptyBy t f <~> f :+: t f (NonEmptyBy t f)
+matchingNE = isoF matchNE (inject !*! consNE)
+
 -- | Useful wrapper over 'binterpret' to allow you to directly extract
 -- a value @b@ out of the @t f a@, if you can convert @f x@ into @b@.
 --
--- Note that depending on the constraints on the interpretation of @t@, you
--- may have extra constraints on @b@.
+-- Note that depending on the constraints on @f@ in @'SemigroupIn' t f@,
+-- you may have extra constraints on @b@.
 --
--- *    If @'C' ('SF' t)@ is 'Data.Constraint.Trivial.Unconstrained', there
---      are no constraints on @b@
--- *    If @'C' ('SF' t)@ is 'Apply', @b@ needs to be an instance of 'Semigroup'
--- *    If @'C' ('SF' t)@ is 'Applicative', @b@ needs to be an instance of 'Monoid'
+-- *    If @f@ is unconstrained, there are no constraints on @b@
+-- *    If @f@ must be 'Apply', @b@ needs to be an instance of 'Semigroup'
+-- *    If @f@ must be 'Applicative', @b@ needs to be an instance of 'Monoid'
 --
 -- For some constraints (like 'Monad'), this will not be usable.
 --
@@ -300,7 +307,7 @@
 --     -> Sum Int
 -- @
 biget
-    :: (Semigroupoidal t, CS t (Const b))
+    :: SemigroupIn t (Const b)
     => (forall x. f x -> b)
     -> (forall x. g x -> b)
     -> t f g a
@@ -322,7 +329,7 @@
 --     -> Sum Int
 -- @
 (!$!)
-    :: (Semigroupoidal t, CS t (Const b))
+    :: SemigroupIn t (Const b)
     => (forall x. f x -> b)
     -> (forall x. g x -> b)
     -> t f g a
@@ -331,8 +338,13 @@
 infixr 5 !$!
 
 -- | Infix alias for 'binterpret'
+--
+-- Note that this is useful in the poly-kinded case, but it is not possible
+-- to define generically for all 'SemigroupIn' because it only is defined
+-- for @Type -> Type@ inputes.  See '!+!' for a version that is poly-kinded
+-- for ':+:' in specific.
 (!*!)
-    :: (Semigroupoidal t, CS t h)
+    :: SemigroupIn t h
     => (f ~> h)
     -> (g ~> h)
     -> t f g
@@ -340,13 +352,25 @@
 (!*!) = binterpret
 infixr 5 !*!
 
+-- | A version of '!*!' specifically for ':+:' that is poly-kinded
+(!+!)
+    :: (f ~> h)
+    -> (g ~> h)
+    -> (f :+: g)
+    ~> h
+(!+!) f g = \case
+    L1 x -> f x
+    R1 y -> g y
+infixr 5 !+!
+
+
 -- | Useful wrapper over 'biget' to allow you to collect a @b@ from all
 -- instances of @f@ and @g@ inside a @t f g a@.
 --
--- This will work if @'C' t@ is 'Data.Constraint.Trivial.Unconstrained',
--- 'Apply', or 'Applicative'.
+-- This will work if the constraint on @f@ for @'SemigroupIn' t f@ is
+-- 'Apply' or 'Applicative', or if it is unconstrained.
 bicollect
-    :: (Semigroupoidal t, CS t (Const [b]))
+    :: SemigroupIn t (Const [b])
     => (forall x. f x -> b)
     -> (forall x. g x -> b)
     -> t f g a
@@ -354,133 +378,98 @@
 bicollect f g = biget ((:[]) . f) ((:[]) . g)
 
 instance Associative (:*:) where
+    type NonEmptyBy (:*:) = NonEmptyF
+
     associating = isoF to_ from_
       where
         to_   (x :*: (y :*: z)) = (x :*: y) :*: z
         from_ ((x :*: y) :*: z) = x :*: (y :*: z)
 
-instance Associative Product where
-    associating = isoF to_ from_
-      where
-        to_   (Pair x (Pair y z)) = Pair (Pair x y) z
-        from_ (Pair (Pair x y) z) = Pair x (Pair y z)
-
-instance Associative Day where
-    associating = isoF D.assoc D.disassoc
-
-instance Associative (:+:) where
-    associating = isoF to_ from_
-      where
-        to_ = \case
-          L1 x      -> L1 (L1 x)
-          R1 (L1 y) -> L1 (R1 y)
-          R1 (R1 z) -> R1 z
-        from_ = \case
-          L1 (L1 x) -> L1 x
-          L1 (R1 y) -> R1 (L1 y)
-          R1 z      -> R1 (R1 z)
-
-instance Associative Sum where
-    associating = isoF to_ from_
-      where
-        to_ = \case
-          InL x       -> InL (InL x)
-          InR (InL y) -> InL (InR y)
-          InR (InR z) -> InR z
-        from_ = \case
-          InL (InL x) -> InL x
-          InL (InR y) -> InR (InL y)
-          InR z       -> InR (InR z)
-
-instance Associative These1 where
-    associating = isoF to_ from_
-      where
-        to_ = \case
-          This1  x              -> This1  (This1  x  )
-          That1    (This1  y  ) -> This1  (That1    y)
-          That1    (That1    z) -> That1               z
-          That1    (These1 y z) -> These1 (That1    y) z
-          These1 x (This1  y  ) -> This1  (These1 x y)
-          These1 x (That1    z) -> These1 (This1  x  ) z
-          These1 x (These1 y z) -> These1 (These1 x y) z
-        from_ = \case
-          This1  (This1  x  )   -> This1  x
-          This1  (That1    y)   -> That1    (This1  y  )
-          This1  (These1 x y)   -> These1 x (This1  y  )
-          That1               z -> That1    (That1    z)
-          These1 (This1  x  ) z -> These1 x (That1    z)
-          These1 (That1    y) z -> That1    (These1 y z)
-          These1 (These1 x y) z -> These1 x (These1 y z)
-
-instance Associative Void3 where
-    associating = isoF coerce coerce
-
-instance Associative Comp where
-    associating = isoF to_ from_
-      where
-        to_   (x :>>= y) = (x :>>= (unComp . y)) :>>= id
-        from_ ((x :>>= y) :>>= z) = x :>>= ((:>>= z) . y)
-
-instance Semigroupoidal (:*:) where
-    type SF (:*:) = NonEmptyF
-
-    appendSF (NonEmptyF xs :*: NonEmptyF ys) = NonEmptyF (xs <> ys)
-    matchSF x = case ys of
+    appendNE (NonEmptyF xs :*: NonEmptyF ys) = NonEmptyF (xs <> ys)
+    matchNE x = case ys of
         L1 ~Proxy -> L1 y
         R1 zs     -> R1 $ y :*: zs
       where
         y :*: ys = fromListF `hright` nonEmptyProd x
 
-    consSF (x :*: NonEmptyF xs) = NonEmptyF $ x :| toList xs
-    toSF   (x :*: y           ) = NonEmptyF $ x :| [y]
+    consNE (x :*: NonEmptyF xs) = NonEmptyF $ x :| toList xs
+    toNonEmptyBy   (x :*: y           ) = NonEmptyF $ x :| [y]
 
+-- | Instances of 'Alt' are semigroups in the semigroupoidal category on
+-- ':*:'.
+instance Alt f => SemigroupIn (:*:) f where
     biretract (x :*: y) = x <!> y
     binterpret f g (x :*: y) = f x <!> g y
 
-instance Semigroupoidal Product where
-    type SF Product = NonEmptyF
+instance Associative Product where
+    type NonEmptyBy Product = NonEmptyF
 
-    appendSF (NonEmptyF xs `Pair` NonEmptyF ys) = NonEmptyF (xs <> ys)
-    matchSF x = case ys of
+    associating = isoF to_ from_
+      where
+        to_   (Pair x (Pair y z)) = Pair (Pair x y) z
+        from_ (Pair (Pair x y) z) = Pair x (Pair y z)
+
+    appendNE (NonEmptyF xs `Pair` NonEmptyF ys) = NonEmptyF (xs <> ys)
+    matchNE x = case ys of
         L1 ~Proxy -> L1 y
         R1 zs     -> R1 $ Pair y zs
       where
         y :*: ys = fromListF `hright` nonEmptyProd x
 
-    consSF (x `Pair` NonEmptyF xs) = NonEmptyF $ x :| toList xs
-    toSF   (x `Pair` y           ) = NonEmptyF $ x :| [y]
+    consNE (x `Pair` NonEmptyF xs) = NonEmptyF $ x :| toList xs
+    toNonEmptyBy   (x `Pair` y           ) = NonEmptyF $ x :| [y]
 
+-- | Instances of 'Alt' are semigroups in the semigroupoidal category on
+-- 'Product'.
+instance Alt f => SemigroupIn Product f where
     biretract (Pair x y) = x <!> y
     binterpret f g (Pair x y) = f x <!> g y
 
-instance Semigroupoidal Day where
-    type SF Day = Ap1
+instance Associative Day where
+    type NonEmptyBy Day = Ap1
+    associating = isoF D.assoc D.disassoc
 
-    appendSF (Day x y z) = z <$> x <.> y
-    matchSF a = case fromAp `hright` ap1Day a of
+    appendNE (Day x y z) = z <$> x <.> y
+    matchNE a = case fromAp `hright` ap1Day a of
       Day x y z -> case y of
         L1 (Identity y') -> L1 $ (`z` y') <$> x
         R1 ys            -> R1 $ Day x ys z
 
-    consSF (Day x y z) = Ap1 x $ flip z <$> toAp y
-    toSF   (Day x y z) = z <$> inject x <.> inject y
+    consNE (Day x y z) = Ap1 x $ flip z <$> toAp y
+    toNonEmptyBy   (Day x y z) = z <$> inject x <.> inject y
 
+-- | Instances of 'Apply' are semigroups in the semigroupoidal category on
+-- 'Day'.
+instance Apply f => SemigroupIn Day f where
     biretract (Day x y z) = z <$> x <.> y
     binterpret f g (Day x y z) = z <$> f x <.> g y
 
-instance Semigroupoidal (:+:) where
-    type SF (:+:) = Step
+instance Associative (:+:) where
+    type NonEmptyBy (:+:) = Step
 
-    appendSF = \case
+    associating = isoF to_ from_
+      where
+        to_ = \case
+          L1 x      -> L1 (L1 x)
+          R1 (L1 y) -> L1 (R1 y)
+          R1 (R1 z) -> R1 z
+        from_ = \case
+          L1 (L1 x) -> L1 x
+          L1 (R1 y) -> R1 (L1 y)
+          R1 z      -> R1 (R1 z)
+
+    appendNE = \case
       L1 (Step i x) -> Step (i + 1) x
       R1 (Step i y) -> Step (i + 2) y
-    matchSF = hright stepDown . stepDown
+    matchNE = hright stepDown . stepDown
 
-    consSF = stepUp . R1 . stepUp
-    toSF = \case
+    consNE = stepUp . R1 . stepUp
+    toNonEmptyBy = \case
       L1 x -> Step 1 x
       R1 y -> Step 2 y
 
+-- | All functors are semigroups in the semigroupoidal category on ':+:'.
+instance SemigroupIn (:+:) f where
     biretract = \case
       L1 x -> x
       R1 y -> y
@@ -488,19 +477,31 @@
       L1 x -> f x
       R1 y -> g y
 
-instance Semigroupoidal Sum where
-    type SF Sum = Step
+instance Associative Sum where
+    type NonEmptyBy Sum = Step
+    associating = isoF to_ from_
+      where
+        to_ = \case
+          InL x       -> InL (InL x)
+          InR (InL y) -> InL (InR y)
+          InR (InR z) -> InR z
+        from_ = \case
+          InL (InL x) -> InL x
+          InL (InR y) -> InR (InL y)
+          InR z       -> InR (InR z)
 
-    appendSF = \case
+    appendNE = \case
       InL (Step i x) -> Step (i + 1) x
       InR (Step i y) -> Step (i + 2) y
-    matchSF = hright (viewF sumSum . stepDown) . stepDown
+    matchNE = hright (viewF sumSum . stepDown) . stepDown
 
-    consSF = stepUp . R1 . stepUp . reviewF sumSum
-    toSF = \case
+    consNE = stepUp . R1 . stepUp . reviewF sumSum
+    toNonEmptyBy = \case
       InL x -> Step 1 x
       InR y -> Step 2 y
 
+-- | All functors are semigroups in the semigroupoidal category on 'Sum'.
+instance SemigroupIn Sum f where
     biretract = \case
       InR x -> x
       InL y -> y
@@ -508,42 +509,55 @@
       InL x -> f x
       InR y -> g y
 
--- data TC f a = TCA (f a) Bool
---             | TCB (Maybe (f a)) (TC f a)
-                -- sparse, non-empty list
-                -- and the last item has a Bool
-                -- aka sparse non-empty list tagged with a bool
-
--- | Ideally here 'SF' would be equivalent to 'Data.HBifunctor.Tensor.MF',
+-- | Ideally here 'NonEmptyBy' would be equivalent to 'Data.HBifunctor.Tensor.ListBy',
 -- just like for ':+:'. This should be possible if we can write
 -- a bijection.  This bijection should be possible in theory --- but it has
 -- not yet been implemented.
-instance Semigroupoidal These1 where
-    type SF These1 = ComposeT Flagged Steps
+instance Associative These1 where
+    type NonEmptyBy These1 = ComposeT Flagged Steps
+    associating = isoF to_ from_
+      where
+        to_ = \case
+          This1  x              -> This1  (This1  x  )
+          That1    (This1  y  ) -> This1  (That1    y)
+          That1    (That1    z) -> That1               z
+          That1    (These1 y z) -> These1 (That1    y) z
+          These1 x (This1  y  ) -> This1  (These1 x y)
+          These1 x (That1    z) -> These1 (This1  x  ) z
+          These1 x (These1 y z) -> These1 (These1 x y) z
+        from_ = \case
+          This1  (This1  x  )   -> This1  x
+          This1  (That1    y)   -> That1    (This1  y  )
+          This1  (These1 x y)   -> These1 x (This1  y  )
+          That1               z -> That1    (That1    z)
+          These1 (This1  x  ) z -> These1 x (That1    z)
+          These1 (That1    y) z -> That1    (These1 y z)
+          These1 (These1 x y) z -> These1 x (These1 y z)
 
-    appendSF s = ComposeT $ case s of
+    appendNE s = ComposeT $ case s of
         This1  (ComposeT (Flagged _ q))                       ->
           Flagged True q
         That1                           (ComposeT (Flagged b q)) ->
           Flagged b        (stepsUp (That1 q))
         These1 (ComposeT (Flagged a q)) (ComposeT (Flagged b r)) ->
           Flagged (a || b) (q <> r)
-    matchSF (ComposeT (Flagged isImpure q)) = case stepsDown q of
+    matchNE (ComposeT (Flagged isImpure q)) = case stepsDown q of
       This1  x
         | isImpure  -> R1 $ This1 x
         | otherwise -> L1 x
       That1    y    -> R1 . That1 . ComposeT $ Flagged isImpure y
       These1 x y    -> R1 . These1 x .  ComposeT $ Flagged isImpure y
 
-    consSF s = ComposeT $ case s of
+    consNE s = ComposeT $ case s of
       This1  x                          -> Flagged True (inject x)
       That1    (ComposeT (Flagged b y)) -> Flagged b    (stepsUp (That1    y))
       These1 x (ComposeT (Flagged b y)) -> Flagged b    (stepsUp (These1 x y))
-    toSF  s = ComposeT $ case s of
+    toNonEmptyBy  s = ComposeT $ case s of
       This1  x   -> Flagged True  . Steps $ NEM.singleton 0 x
       That1    y -> Flagged False . Steps $ NEM.singleton 1 y
       These1 x y -> Flagged False . Steps $ NEM.fromDistinctAscList $ (0, x) :| [(1, y)]
 
+instance Alt f => SemigroupIn These1 f where
     biretract = \case
       This1  x   -> x
       That1    y -> y
@@ -553,58 +567,136 @@
       That1    y -> g y
       These1 x y -> f x <!> g y
 
-instance Semigroupoidal Comp where
-    type SF Comp = Free1
+instance Associative Void3 where
+    type NonEmptyBy Void3 = IdentityT
+    associating = isoF coerce coerce
 
-    appendSF (x :>>= y) = x >>- y
-    matchSF = matchFree1
+    appendNE = \case {}
+    matchNE  = L1 . runIdentityT
 
-    consSF (x :>>= y) = liftFree1 x >>- y
-    toSF   (x :>>= g) = liftFree1 x >>- inject . g
+    consNE = \case {}
+    toNonEmptyBy   = \case {}
 
+-- | All functors are semigroups in the semigroupoidal category on 'Void3'.
+instance SemigroupIn Void3 f where
+    biretract = \case {}
+    binterpret _ _ = \case {}
+
+instance Associative Comp where
+    type NonEmptyBy Comp = Free1
+    associating = isoF to_ from_
+      where
+        to_   (x :>>= y) = (x :>>= (unComp . y)) :>>= id
+        from_ ((x :>>= y) :>>= z) = x :>>= ((:>>= z) . y)
+
+    appendNE (x :>>= y) = x >>- y
+    matchNE = matchFree1
+
+    consNE (x :>>= y) = liftFree1 x >>- y
+    toNonEmptyBy   (x :>>= g) = liftFree1 x >>- inject . g
+
+-- | Instances of 'Bind' are semigroups in the semigroupoidal category on
+-- 'Comp'.
+instance Bind f => SemigroupIn Comp f where
     biretract      (x :>>= y) = x >>- y
     binterpret f g (x :>>= y) = f x >>- (g . y)
 
+---- data TC f a = TCA (f a) Bool
+----             | TCB (Maybe (f a)) (TC f a)
+--                -- sparse, non-empty list
+--                -- and the last item has a Bool
+--                -- aka sparse non-empty list tagged with a bool
+
 instance Associative Joker where
+    type NonEmptyBy Joker = Flagged
     associating = isoF (Joker . Joker    . runJoker)
                        (Joker . runJoker . runJoker)
+    appendNE (Joker (Flagged _ x)) = Flagged True x
+    matchNE (Flagged False x) = L1 x
+    matchNE (Flagged True  x) = R1 $ Joker x
 
+instance SemigroupIn Joker f where
+    biretract = runJoker
+    binterpret f _ = f . runJoker
+
 instance Associative LeftF where
+    type NonEmptyBy LeftF = Flagged
     associating = isoF (LeftF . LeftF    . runLeftF)
                        (LeftF . runLeftF . runLeftF)
 
+    appendNE = hbind (Flagged True) . runLeftF
+    matchNE (Flagged False x) = L1 x
+    matchNE (Flagged True  x) = R1 $ LeftF x
+
+    consNE = Flagged True . runLeftF
+    toNonEmptyBy   = Flagged True . runLeftF
+
+instance SemigroupIn LeftF f where
+    biretract      = runLeftF
+    binterpret f _ = f . runLeftF
+
 instance Associative RightF where
+    type NonEmptyBy RightF = Step
     associating = isoF (RightF . runRightF . runRightF)
                        (RightF . RightF    . runRightF)
 
-instance Semigroupoidal Joker where
-    type SF Joker = Flagged
+    appendNE = stepUp . R1 . runRightF
+    matchNE  = hright RightF . stepDown
 
-    appendSF (Joker (Flagged _ x)) = Flagged True x
-    matchSF (Flagged False x) = L1 x
-    matchSF (Flagged True  x) = R1 $ Joker x
+    consNE   = stepUp . R1 . runRightF
+    toNonEmptyBy     = Step 1 . runRightF
 
-instance Semigroupoidal LeftF where
-    type SF LeftF = Flagged
+instance SemigroupIn RightF f where
+    biretract      = runRightF
+    binterpret _ g = g . runRightF
 
-    appendSF = hbind (Flagged True) . runLeftF
-    matchSF (Flagged False x) = L1 x
-    matchSF (Flagged True  x) = R1 $ LeftF x
+-- | A newtype wrapper meant to be used to define polymorphic 'SemigroupIn'
+-- instances.  See documentation for 'SemigroupIn' for more information.
+--
+-- Please do not ever define an instance of 'SemigroupIn' "naked" on the
+-- second parameter:
+--
+-- @
+-- instance SemigroupIn (WrapHBF t) f
+-- @
+--
+-- As that would globally ruin everything using 'WrapHBF'.
+newtype WrapHBF t f g a = WrapHBF { unwrapHBF :: t f g a }
+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable, Typeable, Generic, Data)
 
-    consSF = Flagged True . runLeftF
-    toSF   = Flagged True . runLeftF
+instance Show1 (t f g) => Show1 (WrapHBF t f g) where
+    liftShowsPrec sp sl d (WrapHBF x) = showsUnaryWith (liftShowsPrec sp sl) "WrapHBF" d x
 
-    biretract      = runLeftF
-    binterpret f _ = f . runLeftF
+instance Eq1 (t f g) => Eq1 (WrapHBF t f g) where
+    liftEq eq (WrapHBF x) (WrapHBF y) = liftEq eq x y
 
-instance Semigroupoidal RightF where
-    type SF RightF = Step
+instance Ord1 (t f g) => Ord1 (WrapHBF t f g) where
+    liftCompare c (WrapHBF x) (WrapHBF y) = liftCompare c x y
 
-    appendSF = stepUp . R1 . runRightF
-    matchSF  = hright RightF . stepDown
+instance HBifunctor t => HBifunctor (WrapHBF t) where
+    hbimap f g (WrapHBF x) = WrapHBF (hbimap f g x)
+    hleft f (WrapHBF x) = WrapHBF (hleft f x)
+    hright g (WrapHBF x) = WrapHBF (hright g x)
 
-    consSF   = stepUp . R1 . runRightF
-    toSF     = Step 1 . runRightF
+deriving via (WrappedHBifunctor (WrapHBF t) f)
+    instance HBifunctor t => HFunctor (WrapHBF t f)
 
-    biretract      = runRightF
-    binterpret _ g = g . runRightF
+instance Associative t => Associative (WrapHBF t) where
+    type NonEmptyBy (WrapHBF t) = NonEmptyBy t
+    associating = isoF (hright unwrapHBF . unwrapHBF) (WrapHBF . hright WrapHBF)
+                . associating @t
+                . isoF (WrapHBF . hleft WrapHBF) (hleft unwrapHBF . unwrapHBF)
+
+    appendNE     = appendNE . unwrapHBF
+    matchNE      = hright WrapHBF . matchNE
+    consNE       = consNE . unwrapHBF
+    toNonEmptyBy = toNonEmptyBy . unwrapHBF
+
+-- | Any @'NonEmptyBy' t f@ is a @'SemigroupIn' t@ if we have
+-- @'Associative' t@. This newtype wrapper witnesses that fact.  We require
+-- a newtype wrapper to avoid overlapping instances.
+newtype WrapNE t f a = WrapNE { unwrapNE :: NonEmptyBy t f a }
+
+instance Associative t => SemigroupIn (WrapHBF t) (WrapNE t f) where
+    biretract = WrapNE . appendNE . hbimap unwrapNE unwrapNE . unwrapHBF
+    binterpret f g = biretract . hbimap f g
diff --git a/src/Data/HBifunctor/Tensor.hs b/src/Data/HBifunctor/Tensor.hs
--- a/src/Data/HBifunctor/Tensor.hs
+++ b/src/Data/HBifunctor/Tensor.hs
@@ -1,35 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes        #-}
-{-# LANGUAGE ConstraintKinds            #-}
-{-# LANGUAGE DefaultSignatures          #-}
-{-# LANGUAGE DeriveFoldable             #-}
-{-# LANGUAGE DeriveFunctor              #-}
-{-# LANGUAGE DeriveTraversable          #-}
-{-# LANGUAGE DerivingStrategies         #-}
-{-# LANGUAGE DerivingVia                #-}
-{-# LANGUAGE EmptyCase                  #-}
-{-# LANGUAGE EmptyDataDeriving          #-}
-{-# LANGUAGE FlexibleContexts           #-}
-{-# LANGUAGE FlexibleInstances          #-}
-{-# LANGUAGE FunctionalDependencies     #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE InstanceSigs               #-}
-{-# LANGUAGE KindSignatures             #-}
-{-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE MultiParamTypeClasses      #-}
-{-# LANGUAGE PatternSynonyms            #-}
-{-# LANGUAGE QuantifiedConstraints      #-}
-{-# LANGUAGE RankNTypes                 #-}
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE StandaloneDeriving         #-}
-{-# LANGUAGE TupleSections              #-}
-{-# LANGUAGE TypeApplications           #-}
-{-# LANGUAGE TypeFamilies               #-}
-{-# LANGUAGE TypeInType                 #-}
-{-# LANGUAGE TypeOperators              #-}
-{-# LANGUAGE UndecidableInstances       #-}
-{-# LANGUAGE ViewPatterns               #-}
-
 -- |
 -- Module      : Data.HBifunctor.Tensor
 -- Copyright   : (c) Justin Le 2019
@@ -48,15 +16,28 @@
 -- The binary analog of 'HFunctor' is 'HBifunctor': we can map
 -- a structure-transforming function over both of the transformed functors.
 --
--- The binary analog of 'Interpret' is 'Monoidal' (and 'Tensor').  If your
--- combinator is an instance of 'Monoidal', it means that you can "squish"
--- both arguments together into an 'Interpret'.  For example:
+-- 'Tensor' gives some extra properties of your binary functor combinator:
+-- associativity and identity (see docs for 'Tensor' for more details).
 --
+-- The binary analog of 'Interpret' is 'MonoidIn'.  If your combinator @t@
+-- and target functor @f@ is an instance of @'MonoidIn' t f@, it means you
+-- can "interpret" out of your tensored values, and also "generate" values
+-- of @f@.
+--
 -- @
--- 'toMF' :: (f ':*:' f) a -> 'ListF' f a
--- 'toMF' :: 'Comp' f f a -> 'Free' f a
--- 'toMF' :: 'Day' f f a -> 'Ap' f a
+-- 'biretract' :: (f ':+:' f) a -> f a
+-- 'pureT'     :: 'V1' a -> f a
+--
+-- biretract :: 'Plus' f => (f ':*:' f) a -> f a
+-- pureT     :: Plus f => 'Proxy' a -> f a
+--
+-- biretract :: 'Applicative' f => 'Day' f f a -> f a
+-- pureT     :: Applicative f => 'Identity' a -> f a
+--
+-- biretract :: 'Monad' f => 'Comp' f f a -> f a
+-- pureT     :: Monad f => 'Identity' a -> f a
 -- @
+--
 module Data.HBifunctor.Tensor (
   -- * 'Tensor'
     Tensor(..)
@@ -66,25 +47,26 @@
   , sumRightIdentity
   , prodLeftIdentity
   , prodRightIdentity
-  -- * 'Monoidal'
-  , Monoidal(..)
-  , CM
-  , nilMF
-  , consMF
-  , unconsMF
+  -- * 'MonoidIn'
+  , MonoidIn(..)
+  , nilLB
+  , consLB
+  , unconsLB
+  , retractLB
+  , interpretLB
   -- ** Utility
   , inL
   , inR
   , outL
   , outR
-  , biretractT
-  , binterpretT
   , prodOutL
   , prodOutR
+  , WrapF(..)
+  , WrapLB(..)
   -- * 'Matchable'
   , Matchable(..)
-  , splittingSF
-  , matchingMF
+  , splittingNE
+  , matchingLB
   ) where
 
 import           Control.Applicative.Free
@@ -94,10 +76,12 @@
 import           Control.Monad.Trans.Compose
 import           Control.Natural
 import           Control.Natural.IsoF
+import           Data.Data
 import           Data.Function
 import           Data.Functor.Apply.Free
-import           Data.Functor.Combinator.Unsafe
-import           Data.Functor.Day               (Day(..))
+import           Data.Functor.Bind
+import           Data.Functor.Classes
+import           Data.Functor.Day            (Day(..))
 import           Data.Functor.Identity
 import           Data.Functor.Plus
 import           Data.Functor.Product
@@ -109,14 +93,13 @@
 import           Data.HFunctor.Internal
 import           Data.HFunctor.Interpret
 import           Data.Kind
-import           Data.List.NonEmpty             (NonEmpty(..))
-import           Data.Proxy
-import           GHC.Generics hiding            (C)
-import qualified Data.Functor.Day               as D
-import qualified Data.Map.NonEmpty              as NEM
+import           Data.List.NonEmpty          (NonEmpty(..))
+import           GHC.Generics
+import qualified Data.Functor.Day            as D
+import qualified Data.Map.NonEmpty           as NEM
 
 -- | An 'Associative' 'HBifunctor' can be a 'Tensor' if there is some
--- identity @i@ where @t i f@ is equivalent to just @f@.
+-- identity @i@ where @t i f@ and @t f i@ are equivalent to just @f@.
 --
 -- That is, "enhancing" @f@ with @t i@ does nothing.
 --
@@ -125,82 +108,133 @@
 --
 -- The 'Tensor' is essentially the 'HBifunctor' equivalent of 'Inject',
 -- with 'intro1' and 'intro2' taking the place of 'inject'.
-class Associative t => Tensor t where
-    -- | The identity of @'Tensor' t@.  If you "combine" @f@ with the
-    -- identity, it leaves @f@ unchanged.
-    --
-    -- For example, the identity of ':*:' is 'Proxy'.  This is because
-    --
-    -- @
-    -- ('Proxy' :*: f) a
-    -- @
-    --
-    -- is equivalent to just
+--
+-- Formally, we can say that @t@ enriches a the category of
+-- endofunctors with monoid strcture: it turns our endofunctor category
+-- into a "monoidal category".
+--
+-- Different instances of @t@ each enrich the endofunctor category in
+-- different ways, giving a different monoidal category.
+class (Associative t, Inject (ListBy t)) => Tensor t i | t -> i where
+    -- | The "monoidal functor combinator" induced by @t@.
     --
-    -- @
-    -- f a
-    -- @
+    -- A value of type @ListBy t f a@ is /equivalent/ to one of:
     --
-    -- ':*:'-ing @f@ with 'Proxy' gives you no additional structure.
+    -- *  @I a@                         -- zero fs
+    -- *  @f a@                         -- one f
+    -- *  @t f f a@                     -- two fs
+    -- *  @t f (t f f) a@               -- three fs
+    -- *  @t f (t f (t f f)) a@
+    -- *  @t f (t f (t f (t f f))) a@
+    -- *  .. etc
     --
-    -- Another example:
+    -- For example, for ':*:', we have 'ListF'.  This is because:
     --
     -- @
-    -- ('V1' ':+:' f) a
+    -- 'Proxy'         ~ 'ListF' []         ~ 'nilLB' \@(':*:')
+    -- x             ~ ListF [x]        ~ 'inject' x
+    -- x :*: y       ~ ListF [x,y]      ~ 'toListBy' (x :*: y)
+    -- x :*: y :*: z ~ ListF [x,y,z]
+    -- -- etc.
     -- @
     --
-    -- is equivalent to just
-    --
-    -- @
-    -- f a
-    -- @
+    -- You can create an "empty" one with 'nilLB', a "singleton" one with
+    -- 'inject', or else one from a single @t f f@ with 'toListBy'.
     --
-    -- because the 'L1' case is unconstructable.
-    type I t :: Type -> Type
+    -- See 'Data.HBifunctor.Associative.NonEmptyBy' for a "non-empty"
+    -- version of this type.
+    type ListBy t :: (Type -> Type) -> Type -> Type
 
     -- | Because @t f (I t)@ is equivalent to @f@, we can always "insert"
     -- @f@ into @t f (I t)@.
     --
     -- This is analogous to 'inject' from 'Inject', but for 'HBifunctor's.
-    intro1 :: f ~> t f (I t)
+    intro1 :: f ~> t f i
 
     -- | Because @t (I t) g@ is equivalent to @f@, we can always "insert"
     -- @g@ into @t (I t) g@.
     --
     -- This is analogous to 'inject' from 'Inject', but for 'HBifunctor's.
-    intro2 :: g ~> t (I t) g
+    intro2 :: g ~> t i g
 
-    -- | Witnesses the property that @'I' t@ is the identity of @t@: @t
-    -- f (I t)@ always leaves @f@ unchanged, so we can always just drop the
-    -- @'I' t@.
-    elim1 :: Functor f => t f (I t) ~> f
+    -- | Witnesses the property that @i@ is the identity of @t@: @t
+    -- f i@ always leaves @f@ unchanged, so we can always just drop the
+    -- @i@.
+    elim1 :: Functor f => t f i ~> f
 
-    -- | Witnesses the property that @'I' t@ is the identity of @t@: @t
-    -- (I t) g@ always leaves @g@ unchanged, so we can always just drop the
-    -- @'I' t@.
-    elim2 :: Functor g => t (I t) g ~> g
+    -- | Witnesses the property that @i@ is the identity of @t@: @t i g@
+    -- always leaves @g@ unchanged, so we can always just drop the @i t@.
+    elim2 :: Functor g => t i g ~> g
 
-    {-# MINIMAL intro1, intro2, elim1, elim2 #-}
+    -- | If a @'ListBy' t f@ represents multiple applications of @t f@ to
+    -- itself, then we can also "append" two @'ListBy' t f@s applied to
+    -- themselves into one giant @'ListBy' t f@ containing all of the @t f@s.
+    --
+    -- Note that this essentially gives an instance for @'SemigroupIn'
+    -- t (ListBy t f)@, for any functor @f@; this is witnessed by
+    -- 'WrapLB'.
+    appendLB    :: t (ListBy t f) (ListBy t f) ~> ListBy t f
 
--- | @f@ is isomorphic to @t f ('I' t)@: that is, @'I' t@ is the identity
--- of @t@, and leaves @f@ unchanged.
-rightIdentity :: (Tensor t, Functor f) => f <~> t f    (I t)
+    -- | Lets you convert an @'NonEmptyBy' t f@ into a single application of @f@ to
+    -- @'ListBy' t f@.
+    --
+    -- Analogous to a function @'Data.List.NonEmpty.NonEmpty' a -> (a,
+    -- [a])@
+    --
+    -- Note that this is not reversible in general unless we have
+    -- @'Matchable' t@.
+    splitNE     :: NonEmptyBy t f ~> t f (ListBy t f)
+
+    -- | An @'ListBy' t f@ is either empty, or a single application of @t@ to @f@
+    -- and @ListBy t f@ (the "head" and "tail").  This witnesses that
+    -- isomorphism.
+    --
+    -- To /use/ this property, see 'nilLB', 'consLB', and 'unconsLB'.
+    splittingLB :: ListBy t f <~> i :+: t f (ListBy t f)
+
+    -- | Embed a direct application of @f@ to itself into a @'ListBy' t f@.
+    toListBy   :: t f f ~> ListBy t f
+    toListBy   = reviewF (splittingLB @t)
+           . R1
+           . hright (inject @(ListBy t))
+
+    -- | @'NonEmptyBy' t f@ is "one or more @f@s", and @'ListBy t f@ is "zero or more
+    -- @f@s".  This function lets us convert from one to the other.
+    --
+    -- This is analogous to a function @'Data.List.NonEmpty.NonEmpty' a ->
+    -- [a]@.
+    --
+    -- Note that because @t@ is not inferrable from the input or output
+    -- type, you should call this using /-XTypeApplications/:
+    --
+    -- @
+    -- 'fromNE' \@(':*:') :: 'NonEmptyF' f a -> 'ListF' f a
+    -- fromNE \@'Comp'  :: 'Free1' f a -> 'Free' f a
+    -- @
+    fromNE :: NonEmptyBy t f ~> ListBy t f
+    fromNE = reviewF (splittingLB @t) . R1 . splitNE @t
+
+    {-# MINIMAL intro1, intro2, elim1, elim2, appendLB, splitNE, splittingLB #-}
+
+-- | @f@ is isomorphic to @t f i@: that is, @i@ is the identity of @t@, and
+-- leaves @f@ unchanged.
+rightIdentity :: (Tensor t i, Functor f) => f <~> t f i
 rightIdentity = isoF intro1 elim1
 
--- | @g@ is isomorphic to @t ('I' t) g@: that is, @'I' t@ is the identity
--- of @t@, and leaves @g@ unchanged.
-leftIdentity  :: (Tensor t, Functor g) => g <~> t (I t) g
+-- | @g@ is isomorphic to @t i g@: that is, @i@ is the identity of @t@, and
+-- leaves @g@ unchanged.
+leftIdentity  :: (Tensor t i, Functor g) => g <~> t i g
 leftIdentity = isoF intro2 elim2
 
 -- | 'leftIdentity' ('intro1' and 'elim1') for ':+:' actually does not
 -- require 'Functor'.  This is the more general version.
 sumLeftIdentity :: f <~> V1 :+: f
-sumLeftIdentity = isoF R1 (absurd1 !*! id)
+sumLeftIdentity = isoF R1 (absurd1 !+! id)
 
 -- | 'rightIdentity' ('intro2' and 'elim2') for ':+:' actually does not
 -- require 'Functor'.  This is the more general version.
 sumRightIdentity :: f <~> f :+: V1
-sumRightIdentity = isoF L1 (id !*! absurd1)
+sumRightIdentity = isoF L1 (id !+! absurd1)
 
 -- | 'leftIdentity' ('intro1' and 'elim1') for ':*:' actually does not
 -- require 'Functor'.  This is the more general version.
@@ -222,122 +256,78 @@
 prodOutR :: f :*: g ~> g
 prodOutR (_ :*: y) = y
 
--- | A @'Monoidal' t@ is a 'Semigroupoidal', in that it provides some type
--- @'MF' t f@ that is equivalent to one of:
+-- | This class effectively gives us a way to generate a value of @f a@
+-- based on an @i a@, for @'Tensor' t i@.  Having this ability makes a lot
+-- of interesting functions possible when used with 'biretract' from
+-- 'SemigroupIn' that weren't possible without it: it gives us a "base
+-- case" for recursion in a lot of cases.
 --
--- *  @I a@                             -- 0 times
--- *  @f a@                             -- 1 time
--- *  @t f f a@                         -- 2 times
--- *  @t f (t f f) a@                   -- 3 times
--- *  @t f (t f (t f f)) a@             -- 4 times
--- *  @t f (t f (t f (t f f))) a@       -- 5 times
--- *  .. etc
+-- Essentially, we get an @i ~> f@, 'pureT', where we can introduce an @f
+-- a@ as long as we have an @i a@.
 --
--- The difference is that unlike @'SF' t@, @'MF' t@ has the "zero times"
--- value.
+-- Formally, if we have @'Tensor' t i@, we are enriching the category of
+-- endofunctors with monoid structure, turning it into a monoidal category.
+-- Different choices of @t@ give different monoidal categories.
 --
--- This typeclass lets you use a type like 'ListF' in terms of repeated
--- applications of ':*:', or 'Ap' in terms of repeated applications of
--- 'Day', or 'Free' in terms of repeated applications of 'Comp', etc.
+-- A functor @f@ is known as a "monoid in the (monoidal) category
+-- of endofunctors on @t@" if we can 'biretract':
 --
--- For example, @f ':*:' f@ can be interpreted as "a free selection of two
--- @f@s", allowing you to specify "I have to @f@s that I can use".  If you
--- want to specify "I want 0, 1, or many different @f@s that I can use",
--- you can use @'ListF' f@.
+-- @
+-- t f f ~> f
+-- @
 --
--- At the high level, the thing that 'Monoidal' adds to 'Semigroupoidal'
--- is 'inL', 'inR', and 'nilMF':
+-- and also 'pureT':
 --
 -- @
--- 'inL'    :: f a -> t f g a
--- 'inR'    :: g a -> t f g a
--- 'nilMF'  :: I a -> MF t f a
+-- i ~> f
 -- @
 --
--- which are like the 'HBifunctor' versions of 'inject': it lets you inject
--- an @f@ into @t f g@, so you can start doing useful mixing operations
--- with it.  'nilMF' lets you construct an "empty" @'MF' t@.
+-- This gives us a few interesting results in category theory, which you
+-- can stil reading about if you don't care:
 --
--- Also useful is:
+-- *  /All/ functors are monoids in the monoidal category
+--    on ':+:'
+-- *  The class of functors that are monoids in the monoidal
+--    category on ':*:' is exactly the functors that are instances of
+--    'Plus'.
+-- *  The class of functors that are monoids in the monoidal
+--    category on 'Day' is exactly the functors that are instances of
+--    'Applicative'.
+-- *  The class of functors that are monoids in the monoidal
+--    category on 'Comp' is exactly the functors that are instances of
+--    'Monad'.
 --
+--    This is the meaning behind the common adage, "monads are just monoids
+--    in the category of endofunctors".  It means that if you enrich the
+--    category of endofunctors to be monoidal with 'Comp', then the class
+--    of functors that are monoids in that monoidal category are exactly
+--    what monads are.  However, the adage is a little misleading: there
+--    are many other ways to enrich the category of endofunctors to be
+--    monoidal, and 'Comp' is just one of them.  Similarly, the class of
+--    functors that are monoids in the category of endofunctors enriched by
+--    'Day' are 'Applicative'.
+--
+-- Note that instances of this class are /intended/ to be written with @t@
+-- and @i@ to be fixed type constructors, and @f@ to be allowed to vary
+-- freely:
+--
 -- @
--- 'toMF' :: t f f a -> MF t f a
+-- instance Monad f => MonoidIn Comp Identity f
 -- @
 --
--- Which converts a @t@ into its aggregate type 'MF'
-class (Tensor t, Semigroupoidal t, Interpret (MF t)) => Monoidal t where
-    -- | The "monoidal functor combinator" induced by @t@.
-    --
-    -- A value of type @MF t f a@ is /equivalent/ to one of:
-    --
-    -- *  @I a@                         -- zero fs
-    -- *  @f a@                         -- one f
-    -- *  @t f f a@                     -- two fs
-    -- *  @t f (t f f) a@               -- three fs
-    -- *  @t f (t f (t f f)) a@
-    -- *  @t f (t f (t f (t f f))) a@
-    -- *  .. etc
-    --
-    -- For example, for ':*:', we have 'ListF'.  This is because:
-    --
-    -- @
-    -- 'Proxy'         ~ 'ListF' []         ~ 'nilMF' \@(':*:')
-    -- x             ~ ListF [x]        ~ 'inject' x
-    -- x :*: y       ~ ListF [x,y]      ~ 'toMF' (x :*: y)
-    -- x :*: y :*: z ~ ListF [x,y,z]
-    -- -- etc.
-    -- @
-    --
-    -- You can create an "empty" one with 'nilMF', a "singleton" one with
-    -- 'inject', or else one from a single @t f f@ with 'toMF'.
-    type MF t :: (Type -> Type) -> Type -> Type
-
-
-    -- | If a @'MF' t f@ represents multiple applications of @t f@ to
-    -- itself, then we can also "append" two @'MF' t f@s applied to
-    -- themselves into one giant @'MF' t f@ containing all of the @t f@s.
-    appendMF    :: t (MF t f) (MF t f) ~> MF t f
-
-    -- | Lets you convert an @'SF' t f@ into a single application of @f@ to
-    -- @'MF' t f@.
-    --
-    -- Analogous to a function @'Data.List.NonEmpty.NonEmpty' a -> (a,
-    -- [a])@
-    --
-    -- Note that this is not reversible in general unless we have
-    -- @'Matchable' t@.
-    splitSF     :: SF t f ~> t f (MF t f)
-
-    -- | An @'MF' t f@ is either empty, or a single application of @t@ to @f@
-    -- and @MF t f@ (the "head" and "tail").  This witnesses that
-    -- isomorphism.
-    --
-    -- To /use/ this property, see 'nilMF', 'consMF', and 'unconsMF'.
-    splittingMF :: MF t f <~> I t :+: t f (MF t f)
-
-    -- | Embed a direct application of @f@ to itself into a @'MF' t f@.
-    toMF   :: t f f ~> MF t f
-    toMF   = reviewF (splittingMF @t)
-           . R1
-           . hright (inject @(MF t))
-
-    -- | @'SF' t f@ is "one or more @f@s", and @'MF t f@ is "zero or more
-    -- @f@s".  This function lets us convert from one to the other.
-    --
-    -- This is analogous to a function @'Data.List.NonEmpty.NonEmpty' a ->
-    -- [a]@.
-    --
-    -- Note that because @t@ is not inferrable from the input or output
-    -- type, you should call this using /-XTypeApplications/:
-    --
-    -- @
-    -- 'fromSF' \@(':*:') :: 'NonEmptyF' f a -> 'ListF' f a
-    -- fromSF \@'Comp'  :: 'Free1' f a -> 'Free' f a
-    -- @
-    fromSF :: SF t f ~> MF t f
-    fromSF = reviewF (splittingMF @t) . R1 . splitSF @t
+-- Any other sort of instance and it's easy to run into problems with type
+-- inference.  If you want to write an instance that's "polymorphic" on
+-- tensor choice, use the 'WrapHBF' and 'WrapF' newtype wrappers over type
+-- variables, where the third argument also uses a type constructor:
+--
+-- @
+-- instance MonoidIn (WrapHBF t) (WrapF i) (MyFunctor t i)
+-- @
+--
+-- This will prevent problems with overloaded instances.
+class (Tensor t i, SemigroupIn t f) => MonoidIn t i f where
 
-    -- | If we have an @'I' t@, we can generate an @f@ based on how it
+    -- | If we have an @i@, we can generate an @f@ based on how it
     -- interacts with @t@.
     --
     -- Specialized (and simplified), this type is:
@@ -351,110 +341,70 @@
     -- Note that because @t@ appears nowhere in the input or output types,
     -- you must always use this with explicit type application syntax (like
     -- @pureT \@Day@)
-    pureT  :: CM t f => I t ~> f
-    pureT  = retract . reviewF (splittingMF @t) . L1
-
-    -- | If we have a constraint on the 'Monoidal' satisfied, it should
-    -- also imply the constraint on the 'Semigroupoidal'.
     --
-    -- This is basically saying that @'C' ('SF' t)@ should be a superclass
-    -- of @'C' ('MF' t)@.
-    --
-    -- For example, for ':*:', this type signature says that 'Alt' is
-    -- a superclass of 'Plus', so whenever you have 'Plus', you should
-    -- always also have 'Alt'.
-    --
-    -- For 'Day', this type signature says that 'Apply' is a superclass of
-    -- 'Applicative', so whenever you have 'Applicative', you should always
-    -- also have 'Apply'.
-    --
-    -- This is necessary because in the current class hierarchy, 'Apply'
-    -- isn't a true superclass of 'Applicative'.  'upgradeC' basically
-    -- "imbues" @f@ with an 'Apply' instance based on its 'Applicative'
-    -- instance, so things can be easier to use.
-    --
-    -- For example, let's say I have a type @Parser@ that is an
-    -- 'Applicative' instance, but the source library does not define an
-    -- 'Apply' instance.  I cannot use 'biretract' or 'binterpret' with it,
-    -- even though I should be able to, because they require 'Apply'.
-    --
-    -- That is:
-    --
-    -- @
-    -- 'biretract' :: 'Day' Parser Parser a -> Parser a
-    -- @
-    --
-    -- is a type error, because it requires @'Apply' Parser@.
-    --
-    -- But, if we know that @Parser@ has an 'Applicative' instance, we can
-    -- use:
-    --
-    -- @
-    -- 'upgradeC' @'Day' ('Proxy' \@Parser) 'biretract'
-    --   :: Day Parser Parser a -> a
-    -- @
-    --
-    -- and this will now typecheck properly.
-    --
-    -- Ideally, @Parser@ would also have an 'Apply' instance.  But we
-    -- cannot control this if an external library defines @Parser@.
-    --
-    -- (Alternatively you can just use 'biretractT'.)
-    --
-    -- Note that you should only use this if @f@ doesn't already have the
-    -- 'SF' constraint.  If it does, this could lead to conflicting
-    -- instances.  Only use this with /specific/, concrete @f@s.  Otherwise
-    -- this is unsafe and can possibly break coherence guarantees.
-    --
-    -- The @proxy@ argument can be provided using something like @'Proxy'
-    -- \@f@, to specify which @f@ you want to upgrade.
-    upgradeC :: CM t f => proxy f -> (CS t f => r) -> r
+    -- Along with 'biretract', this function makes @f@ a monoid in the
+    -- category of endofunctors with respect to tensor @t@.
+    pureT  :: i ~> f
 
-    {-# MINIMAL appendMF, splitSF, splittingMF, upgradeC #-}
+    default pureT :: Interpret (ListBy t) f => i ~> f
+    pureT  = retract . reviewF (splittingLB @t) . L1
 
--- | Convenient alias for the constraint required for 'inL', 'inR',
--- 'pureT', etc.
+-- | An implementation of 'retract' that works for any instance of
+-- @'MonoidIn' t i@ for @'ListBy' t@.
 --
--- It's usually a constraint on the target/result context of interpretation
--- that allows you to "exit" or "run" a @'Monoidal' t@.
-type CM t = C (MF t)
+-- Can be useful as a default implementation if you already have 'MonoidIn'
+-- implemented.
+retractLB :: forall t i f. MonoidIn t i f => ListBy t f ~> f
+retractLB = (pureT @t !*! biretract @t . hright (retractLB @t))
+              . unconsLB @t
 
--- | Create the "empty 'MF'@.
+-- | An implementation of 'interpret' that works for any instance of
+-- @'MonoidIn' t i@ for @'ListBy' t@.
 --
--- If @'MF' t f@ represents multiple applications of @t f@ with
--- itself, then @nilMF@ gives us "zero applications of @f@".
+-- Can be useful as a default implementation if you already have 'MonoidIn'
+-- implemented.
+interpretLB :: forall t i g f. MonoidIn t i f => (g ~> f) -> ListBy t g ~> f
+interpretLB f = retractLB @t . hmap f
+
+-- | Create the "empty 'ListBy'".
 --
+-- If @'ListBy' t f@ represents multiple applications of @t f@ with
+-- itself, then @nilLB@ gives us "zero applications of @f@".
+--
 -- Note that @t@ cannot be inferred from the input or output type of
--- 'nilMF', so this function must always be called with -XTypeApplications:
+-- 'nilLB', so this function must always be called with -XTypeApplications:
 --
 -- @
--- 'nilMF' \@'Day' :: 'Identity' '~>' 'Ap' f
--- nilMF \@'Comp' :: Identity ~> 'Free' f
--- nilMF \@(':*:') :: 'Proxy' ~> 'ListF' f
+-- 'nilLB' \@'Day' :: 'Identity' '~>' 'Ap' f
+-- nilLB \@'Comp' :: Identity ~> 'Free' f
+-- nilLB \@(':*:') :: 'Proxy' ~> 'ListF' f
 -- @
-nilMF    :: forall t f. Monoidal t => I t ~> MF t f
-nilMF    = reviewF (splittingMF @t) . L1
+--
+-- Note that this essentially gives an instance for @'MonoidIn' t i (ListBy
+-- t f)@, for any functor @f@; this is witnessed by 'WrapLB'.
+nilLB    :: forall t i f. Tensor t i => i ~> ListBy t f
+nilLB    = reviewF (splittingLB @t) . L1
 
--- | Lets us "cons" an application of @f@ to the front of an @'MF' t f@.
-consMF   :: Monoidal t => t f (MF t f) ~> MF t f
-consMF   = reviewF splittingMF . R1
+-- | Lets us "cons" an application of @f@ to the front of an @'ListBy' t f@.
+consLB   :: Tensor t i => t f (ListBy t f) ~> ListBy t f
+consLB   = reviewF splittingLB . R1
 
--- | "Pattern match" on an @'MF' t@
+-- | "Pattern match" on an @'ListBy' t@
 --
--- An @'MF' t f@ is either empty, or a single application of @t@ to @f@
--- and @MF t f@ (the "head" and "tail")
+-- An @'ListBy' t f@ is either empty, or a single application of @t@ to @f@
+-- and @ListBy t f@ (the "head" and "tail")
 --
 -- This is analogous to the function @'Data.List.uncons' :: [a] -> Maybe
 -- (a, [a])@.
-unconsMF :: Monoidal t => MF t f ~> I t :+: t f (MF t f)
-unconsMF = viewF splittingMF
+unconsLB :: Tensor t i => ListBy t f ~> i :+: t f (ListBy t f)
+unconsLB = viewF splittingLB
 
 -- | Convenient wrapper over 'intro1' that lets us introduce an arbitrary
 -- functor @g@ to the right of an @f@.
 --
 -- You can think of this as an 'HBifunctor' analogue of 'inject'.
 inL
-    :: forall t f g. (Monoidal t, CM t g)
+    :: forall t i f g. MonoidIn t i g
     => f ~> t f g
 inL = hright (pureT @t) . intro1
 
@@ -463,7 +413,7 @@
 --
 -- You can think of this as an 'HBifunctor' analogue of 'inject'.
 inR
-    :: forall t f g. (Monoidal t, CM t f)
+    :: forall t i f g. MonoidIn t i f
     => g ~> t f g
 inR = hleft (pureT @t) . intro2
 
@@ -474,7 +424,7 @@
 -- See 'prodOutL' for a version that does not require @'Functor' f@,
 -- specifically for ':*:'.
 outL
-    :: (Tensor t, I t ~ Proxy, Functor f)
+    :: (Tensor t Proxy, Functor f)
     => t f g ~> f
 outL = elim1 . hright absorb
 
@@ -485,63 +435,23 @@
 -- See 'prodOutR' for a version that does not require @'Functor' g@,
 -- specifically for ':*:'.
 outR
-    :: (Tensor t, I t ~ Proxy, Functor g)
+    :: (Tensor t Proxy, Functor g)
     => t f g ~> g
 outR = elim2 . hleft absorb
 
--- | This is 'biretract', but taking a @'C' ('MF' t)@ constraint instead of
--- a @'C' ('SF' t)@ constraint.  For example, for 'Day', it takes an
--- 'Applicative' constraint instead of an 'Apply' constraint.
---
--- In an ideal world, this would be not necessary, and we can use
--- 'biretract'.  However, sometimes @'C' ('MF' t)@ is not an actual
--- subclass of @'C' ('SF' t)@ (like 'Apply' and 'Applicative'), even though
--- it should technically always be so.
---
--- Note that you should only use this if @f@ doesn't already have the 'SF'
--- constraint (for example, for 'Day', if @f@ already has an 'Apply'
--- instance).  If it does, this could lead to conflicting instances.  If
--- @f@ already has the 'SF' instance, just use 'biretract' directly.  Only
--- use this with /specific/, concrete @f@s.
-biretractT :: forall t f. (Monoidal t, CM t f) => t f f ~> f
-biretractT = upgradeC @t (Proxy @f)
-               biretract
-
--- | This is 'binterpret', but taking a @'C' ('MF' t)@ constraint instead of
--- a @'C' ('SF' t)@ constraint.  For example, for 'Day', it takes an
--- 'Applicative' constraint instead of an 'Apply' constraint.
---
--- In an ideal world, this would be not necessary, and we can use
--- 'biretract'.  However, sometimes @'C' ('MF' t)@ is not an actual
--- subclass of @'C' ('SF' t)@ (like 'Apply' and 'Applicative'), even though
--- it should technically always be so.
---
--- Note that you should only use this if @f@ doesn't already have the 'SF'
--- constraint (for example, for 'Day', if @f@ already has an 'Apply'
--- instance).  If it does, this could lead to conflicting instances.  If
--- @f@ already has the 'SF' instance, just use 'biretract' directly.  Only
--- use this with /specific/, concrete @f@s.
-binterpretT
-    :: forall t f g h. (Monoidal t, CM t h)
-    => f ~> h
-    -> g ~> h
-    -> t f g ~> h
-binterpretT f g = upgradeC @t (Proxy @h) $
-                    binterpret f g
-
--- | For some @t@, we have the ability to "statically analyze" the @'MF' t@
+-- | For some @t@, we have the ability to "statically analyze" the @'ListBy' t@
 -- and pattern match and manipulate the structure without ever
 -- interpreting or retracting.  These are 'Matchable'.
-class Monoidal t => Matchable t where
-    -- | The inverse of 'splitSF'.  A consing of @f@ to @'MF' t f@ is
-    -- non-empty, so it can be represented as an @'SF' t f@.
+class Tensor t i => Matchable t i where
+    -- | The inverse of 'splitNE'.  A consing of @f@ to @'ListBy' t f@ is
+    -- non-empty, so it can be represented as an @'NonEmptyBy' t f@.
     --
     -- This is analogous to a function @'uncurry' ('Data.List.NonEmpty.:|')
     -- :: (a, [a]) -> 'Data.List.NonEmpty.NonEmpty' a@.
-    unsplitSF :: t f (MF t f) ~> SF t f
+    unsplitNE :: t f (ListBy t f) ~> NonEmptyBy t f
 
-    -- | "Pattern match" on an @'MF' t f@: it is either empty, or it is
-    -- non-empty (and so can be an @'SF' t f@).
+    -- | "Pattern match" on an @'ListBy' t f@: it is either empty, or it is
+    -- non-empty (and so can be an @'NonEmptyBy' t f@).
     --
     -- This is analgous to a function @'Data.List.NonEmpty.nonEmpty' :: [a]
     -- -> Maybe ('Data.List.NonEmpty.NonEmpty' a)@.
@@ -550,102 +460,39 @@
     -- type, you should use this with /-XTypeApplications/:
     --
     -- @
-    -- 'matchMF' \@'Day' :: 'Ap' f a -> ('Identity' :+: 'Ap1' f) a
+    -- 'matchLB' \@'Day' :: 'Ap' f a -> ('Identity' :+: 'Ap1' f) a
     -- @
-    matchMF   :: MF t f ~> I t :+: SF t f
+    --
+    -- Note that you can recursively "unroll" a 'ListBy' completely into
+    -- a 'Data.HFunctor.Chain.Chain' by using
+    -- 'Data.HFunctor.Chain.unrollLB'.
+    matchLB   :: ListBy t f ~> i :+: NonEmptyBy t f
 
--- | An @'SF' t f@ is isomorphic to an @f@ consed with an @'MF' t f@, like
+-- | An @'NonEmptyBy' t f@ is isomorphic to an @f@ consed with an @'ListBy' t f@, like
 -- how a @'Data.List.NonEmpty.NonEmpty' a@ is isomorphic to @(a, [a])@.
-splittingSF :: Matchable t => SF t f <~> t f (MF t f)
-splittingSF = isoF splitSF unsplitSF
+splittingNE
+    :: Matchable t i
+    => NonEmptyBy t f <~> t f (ListBy t f)
+splittingNE = isoF splitNE unsplitNE
 
--- | An @'MF' t f@ is isomorphic to either the empty case (@'I' t@) or the
--- non-empty case (@'SF' t f@), like how @[a]@ is isomorphic to @'Maybe'
+-- | An @'ListBy' t f@ is isomorphic to either the empty case (@i@) or the
+-- non-empty case (@'NonEmptyBy' t f@), like how @[a]@ is isomorphic to @'Maybe'
 -- ('Data.List.NonEmpty.NonEmpty' a)@.
-matchingMF :: forall t f. Matchable t => MF t f <~> I t :+: SF t f
-matchingMF = isoF (matchMF @t) (nilMF @t !*! fromSF @t)
-
-instance Tensor (:*:) where
-    type I (:*:) = Proxy
+matchingLB
+    :: forall t i f. Matchable t i
+    => ListBy t f <~> i :+: NonEmptyBy t f
+matchingLB = isoF (matchLB @t) (nilLB @t !*! fromNE @t)
 
+instance Tensor (:*:) Proxy where
+    type ListBy (:*:) = ListF
     intro1 = (:*: Proxy)
     intro2 = (Proxy :*:)
-
     elim1 (x      :*: ~Proxy) = x
     elim2 (~Proxy :*: y     ) = y
 
-instance Tensor Product where
-    type I Product = Proxy
-
-    intro1 = (`Pair` Proxy)
-    intro2 = (Proxy `Pair`)
-
-    elim1 (Pair x ~Proxy) = x
-    elim2 (Pair ~Proxy y) = y
-
-instance Tensor Day where
-    type I Day = Identity
-
-    intro1   = D.intro2
-    intro2   = D.intro1
-    elim1    = D.elim2
-    elim2    = D.elim1
-
-instance Tensor (:+:) where
-    type I (:+:) = V1
-
-    intro1 = L1
-    intro2 = R1
-
-    elim1 = \case
-      L1 x -> x
-      R1 y -> absurd1 y
-    elim2 = \case
-      L1 x -> absurd1 x
-      R1 y -> y
-
-instance Tensor Sum where
-    type I Sum = V1
-
-    intro1 = InL
-    intro2 = InR
-
-    elim1 = \case
-      InL x -> x
-      InR y -> absurd1 y
-    elim2 = \case
-      InL x -> absurd1 x
-      InR y -> y
-
-instance Tensor These1 where
-    type I These1 = V1
-
-    intro1 = This1
-    intro2 = That1
-    elim1  = \case
-      This1  x   -> x
-      That1    y -> absurd1 y
-      These1 _ y -> absurd1 y
-    elim2 = \case
-      This1  x   -> absurd1 x
-      That1    y -> y
-      These1 x _ -> absurd1 x
-
-instance Tensor Comp where
-    type I Comp = Identity
-
-    intro1 = (:>>= Identity)
-    intro2 = (Identity () :>>=) . const
-
-    elim1 (x :>>= y) = runIdentity . y <$> x
-    elim2 (x :>>= y) = y (runIdentity x)
-
-instance Monoidal (:*:) where
-    type MF (:*:) = ListF
-
-    appendMF (ListF xs :*: ListF ys) = ListF (xs ++ ys)
-    splitSF     = nonEmptyProd
-    splittingMF = isoF to_ from_
+    appendLB (ListF xs :*: ListF ys) = ListF (xs ++ ys)
+    splitNE     = nonEmptyProd
+    splittingLB = isoF to_ from_
       where
         to_ = \case
           ListF []     -> L1 Proxy
@@ -654,17 +501,23 @@
           L1 ~Proxy           -> ListF []
           R1 (x :*: ListF xs) -> ListF (x:xs)
 
-    toMF (x :*: y) = ListF [x, y]
-    pureT _        = zero
+    toListBy (x :*: y) = ListF [x, y]
 
-    upgradeC _ x = x
+-- | Instances of 'Plus' are monoids in the monoidal category on
+-- ':*:'.
+instance Plus f => MonoidIn (:*:) Proxy f where
+    pureT _        = zero
 
-instance Monoidal Product where
-    type MF Product = ListF
+instance Tensor Product Proxy where
+    type ListBy Product = ListF
+    intro1 = (`Pair` Proxy)
+    intro2 = (Proxy `Pair`)
+    elim1 (Pair x ~Proxy) = x
+    elim2 (Pair ~Proxy y) = y
 
-    appendMF (ListF xs `Pair` ListF ys) = ListF (xs ++ ys)
-    splitSF     = viewF prodProd . nonEmptyProd
-    splittingMF = isoF to_ from_
+    appendLB (ListF xs `Pair` ListF ys) = ListF (xs ++ ys)
+    splitNE     = viewF prodProd . nonEmptyProd
+    splittingLB = isoF to_ from_
       where
         to_ = \case
           ListF []     -> L1 Proxy
@@ -673,17 +526,23 @@
           L1 ~Proxy              -> ListF []
           R1 (x `Pair` ListF xs) -> ListF (x:xs)
 
-    toMF (Pair x y) = ListF [x, y]
-    pureT _         = zero
+    toListBy (Pair x y) = ListF [x, y]
 
-    upgradeC _ x = x
+-- | Instances of 'Plus' are monoids in the monoidal category on
+-- 'Product'.
+instance Plus f => MonoidIn Product Proxy f where
+    pureT _         = zero
 
-instance Monoidal Day where
-    type MF Day = Ap
+instance Tensor Day Identity where
+    type ListBy Day = Ap
+    intro1   = D.intro2
+    intro2   = D.intro1
+    elim1    = D.elim2
+    elim2    = D.elim1
 
-    appendMF (Day x y z) = z <$> x <*> y
-    splitSF     = ap1Day
-    splittingMF = isoF to_ from_
+    appendLB (Day x y z) = z <$> x <*> y
+    splitNE     = ap1Day
+    splittingLB = isoF to_ from_
       where
         to_ = \case
           Pure x  -> L1 (Identity x)
@@ -692,65 +551,109 @@
           L1 (Identity x) -> Pure x
           R1 (Day x xs f) -> Ap x (flip f <$> xs)
 
-    toMF (Day x y z) = z <$> liftAp x <*> liftAp y
+    toListBy (Day x y z) = z <$> liftAp x <*> liftAp y
+
+-- | Instances of 'Applicative' are monoids in the monoidal category on
+-- 'Day'.
+--
+-- Note that because of typeclass constraints, this requires 'Apply' as
+-- well as 'Applicative'.  But, you can get a "local" instance of 'Apply'
+-- for any 'Applicative' using
+-- 'Data.Functor.Combinators.Unsafe.unsafeApply'.
+instance (Apply f, Applicative f) => MonoidIn Day Identity f where
     pureT            = generalize
 
-    upgradeC = unsafeApply
+instance Tensor (:+:) V1 where
+    type ListBy (:+:) = Step
+    intro1 = L1
+    intro2 = R1
 
-instance Monoidal (:+:) where
-    type MF (:+:) = Step
+    elim1 = \case
+      L1 x -> x
+      R1 y -> absurd1 y
+    elim2 = \case
+      L1 x -> absurd1 x
+      R1 y -> y
 
-    appendMF    = id !*! stepUp . R1
-    splitSF     = stepDown
-    splittingMF = stepping . sumLeftIdentity
+    appendLB    = id !*! stepUp . R1
+    splitNE     = stepDown
+    splittingLB = stepping . sumLeftIdentity
 
-    toMF  = \case
+    toListBy  = \case
       L1 x -> Step 0 x
       R1 x -> Step 1 x
+
+-- | All functors are monoids in the monoidal category on ':+:'.
+instance MonoidIn (:+:) V1 f where
     pureT = absurd1
 
-    upgradeC _ x = x
+instance Tensor Sum V1 where
+    type ListBy Sum = Step
+    intro1 = InL
+    intro2 = InR
 
-instance Monoidal Sum where
-    type MF Sum = Step
+    elim1 = \case
+      InL x -> x
+      InR y -> absurd1 y
+    elim2 = \case
+      InL x -> absurd1 x
+      InR y -> y
 
-    appendMF    = id !*! stepUp . R1
-    splitSF     = viewF sumSum . stepDown
-    splittingMF = stepping
+    appendLB    = id !*! stepUp . R1
+    splitNE     = viewF sumSum . stepDown
+    splittingLB = stepping
                 . sumLeftIdentity
                 . overHBifunctor id sumSum
 
-    toMF  = \case
+    toListBy  = \case
       InL x -> Step 0 x
       InR x -> Step 1 x
+
+-- | All functors are monoids in the monoidal category on 'Sum'.
+instance MonoidIn Sum V1 f where
     pureT = absurd1
 
-    upgradeC _ x = x
 
-instance Monoidal These1 where
-    type MF These1 = Steps
+instance Tensor These1 V1 where
+    type ListBy These1 = Steps
+    intro1 = This1
+    intro2 = That1
+    elim1  = \case
+      This1  x   -> x
+      That1    y -> absurd1 y
+      These1 _ y -> absurd1 y
+    elim2 = \case
+      This1  x   -> absurd1 x
+      That1    y -> y
+      These1 x _ -> absurd1 x
 
-    appendMF    = \case
+    appendLB    = \case
       This1  x   -> x
       That1    y -> stepsUp . That1 $ y
       These1 x y -> x <> y
-    splitSF     = stepsDown . flaggedVal . getComposeT
-    splittingMF = steppings . sumLeftIdentity
+    splitNE     = stepsDown . flaggedVal . getComposeT
+    splittingLB = steppings . sumLeftIdentity
 
-    toMF  = \case
+    toListBy  = \case
       This1  x   -> Steps $ NEM.singleton 0 x
       That1    y -> Steps $ NEM.singleton 1 y
       These1 x y -> Steps $ NEM.fromDistinctAscList ((0, x) :| [(1, y)])
+
+instance Alt f => MonoidIn These1 V1 f where
     pureT = absurd1
 
-    upgradeC _ x = x
+instance Tensor Comp Identity where
+    type ListBy Comp = Free
 
-instance Monoidal Comp where
-    type MF Comp = Free
+    intro1 = (:>>= Identity)
+    intro2 = (Identity () :>>=) . const
 
-    appendMF (x :>>= y) = x >>= y
-    splitSF             = free1Comp
-    splittingMF = isoF to_ from_
+    elim1 (x :>>= y) = runIdentity . y <$> x
+    elim2 (x :>>= y) = y (runIdentity x)
+
+    appendLB (x :>>= y) = x >>= y
+    splitNE             = free1Comp
+    splittingLB = isoF to_ from_
       where
         to_ :: Free f ~> Identity :+: Comp f (Free f)
         to_ = foldFree' (L1 . Identity) $ \y n -> R1 $
@@ -759,32 +662,91 @@
         from_ = generalize
             !*! (\case x :>>= f -> liftFree x >>= f)
 
-    toMF (x :>>= y) = liftFree x >>= (inject . y)
-    pureT           = generalize
+    toListBy (x :>>= y) = liftFree x >>= (inject . y)
 
-    upgradeC = unsafeBind
+-- | Instances of 'Monad' are monoids in the monoidal category on
+-- 'Comp'.
+--
+-- This instance is the "proof" that "monads are the monoids in the
+-- category of endofunctors (enriched with 'Comp')"
+--
+-- Note that because of typeclass constraints, this requires 'Bind' as
+-- well as 'Monad'.  But, you can get a "local" instance of 'Apply'
+-- for any 'Monad' using
+-- 'Data.Functor.Combinators.Unsafe.unsafeBind'.
+instance (Bind f, Monad f) => MonoidIn Comp Identity f where
+    pureT           = generalize
 
-instance Matchable (:*:) where
-    unsplitSF = ProdNonEmpty
-    matchMF   = fromListF
+instance Matchable (:*:) Proxy where
+    unsplitNE = ProdNonEmpty
+    matchLB   = fromListF
 
-instance Matchable Product where
-    unsplitSF = ProdNonEmpty . reviewF prodProd
-    matchMF   = fromListF
+instance Matchable Product Proxy where
+    unsplitNE = ProdNonEmpty . reviewF prodProd
+    matchLB   = fromListF
 
-instance Matchable Day where
-    unsplitSF = DayAp1
-    matchMF   = fromAp
+instance Matchable Day Identity where
+    unsplitNE = DayAp1
+    matchLB   = fromAp
 
-instance Matchable (:+:) where
-    unsplitSF   = stepUp
-    matchMF     = R1
+instance Matchable (:+:) V1 where
+    unsplitNE   = stepUp
+    matchLB     = R1
 
-instance Matchable Sum where
-    unsplitSF   = stepUp . reviewF sumSum
-    matchMF     = R1
+instance Matchable Sum V1 where
+    unsplitNE   = stepUp . reviewF sumSum
+    matchLB     = R1
 
 -- We can't write this until we get an isomorphism between MF These1 and SF These1
 -- instance Matchable These1 where
---     unsplitSF = stepsUp
---     matchMF   = R1
+--     unsplitNE = stepsUp
+--     matchLB   = R1
+
+-- | A newtype wrapper meant to be used to define polymorphic 'MonoidIn'
+-- instances.  See documentation for 'MonoidIn' for more information.
+--
+-- Please do not ever define an instance of 'MonoidIn' "naked" on the
+-- third parameter:
+--
+-- @
+-- instance MonidIn (WrapHBF t) (WrapF i) f
+-- @
+--
+-- As that would globally ruin everything using 'WrapHBF'.
+newtype WrapF f a = WrapF { unwrapF :: f a }
+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable, Typeable, Generic, Data)
+
+instance Show1 f => Show1 (WrapF f) where
+    liftShowsPrec sp sl d (WrapF x) = showsUnaryWith (liftShowsPrec sp sl) "WrapF" d x
+
+instance Eq1 f => Eq1 (WrapF f) where
+    liftEq eq (WrapF x) (WrapF y) = liftEq eq x y
+
+instance Ord1 f => Ord1 (WrapF f) where
+    liftCompare c (WrapF x) (WrapF y) = liftCompare c x y
+
+instance Tensor t i => Tensor (WrapHBF t) (WrapF i) where
+    type ListBy (WrapHBF t) = ListBy t
+
+    intro1 = WrapHBF . hright WrapF .  intro1
+    intro2 = WrapHBF . hleft WrapF . intro2
+    elim1 = elim1 . hright unwrapF . unwrapHBF
+    elim2 = elim2 . hleft unwrapF . unwrapHBF
+    appendLB = appendLB . unwrapHBF
+    splitNE = WrapHBF . splitNE
+    splittingLB = splittingLB @t
+                . overHBifunctor (isoF WrapF unwrapF) (isoF WrapHBF unwrapHBF)
+    toListBy = toListBy . unwrapHBF
+    fromNE = fromNE @t
+
+-- | Any @'ListBy' t f@ is a @'SemigroupIn' t@ and a @'MonoidIn' t i@, if we
+-- have @'Tensor' t i@. This newtype wrapper witnesses that fact.  We
+-- require a newtype wrapper to avoid overlapping instances.
+newtype WrapLB t f a = WrapLB { unwrapLB :: ListBy t f a }
+
+instance Tensor t i => SemigroupIn (WrapHBF t) (WrapLB t f) where
+    biretract = WrapLB . appendLB . hbimap unwrapLB unwrapLB . unwrapHBF
+    binterpret f g = biretract . hbimap f g
+
+instance Tensor t i => MonoidIn (WrapHBF t) (WrapF i) (WrapLB t f) where
+    pureT = WrapLB . nilLB @t . unwrapF
diff --git a/src/Data/HFunctor.hs b/src/Data/HFunctor.hs
--- a/src/Data/HFunctor.hs
+++ b/src/Data/HFunctor.hs
@@ -1,25 +1,3 @@
-{-# LANGUAGE ConstraintKinds         #-}
-{-# LANGUAGE DeriveDataTypeable      #-}
-{-# LANGUAGE DeriveFoldable          #-}
-{-# LANGUAGE DeriveFunctor           #-}
-{-# LANGUAGE DeriveGeneric           #-}
-{-# LANGUAGE DeriveTraversable       #-}
-{-# LANGUAGE FlexibleInstances       #-}
-{-# LANGUAGE InstanceSigs            #-}
-{-# LANGUAGE LambdaCase              #-}
-{-# LANGUAGE MultiParamTypeClasses   #-}
-{-# LANGUAGE PolyKinds               #-}
-{-# LANGUAGE RankNTypes              #-}
-{-# LANGUAGE ScopedTypeVariables     #-}
-{-# LANGUAGE StandaloneDeriving      #-}
-{-# LANGUAGE TemplateHaskell         #-}
-{-# LANGUAGE TypeFamilies            #-}
-{-# LANGUAGE TypeInType              #-}
-{-# LANGUAGE TypeOperators           #-}
-{-# LANGUAGE UndecidableInstances    #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
-{-# LANGUAGE ViewPatterns            #-}
-
 -- |
 -- Module      : Data.HFunctor
 -- Copyright   : (c) Justin Le 2019
@@ -75,6 +53,7 @@
 import           Data.Functor.Sum
 import           Data.Functor.These
 import           Data.HFunctor.Internal
+import           Data.Kind
 import           Data.List.NonEmpty             (NonEmpty(..))
 import           Data.Pointed
 import           Data.Semigroup.Foldable
@@ -407,7 +386,7 @@
 instance Inject (These1 f) where
     inject = That1
 
-instance Applicative f => Inject (Comp f) where
+instance Applicative f => Inject (Comp f :: (Type -> Type) -> Type -> Type) where
     inject x = pure () :>>= const x
 
 instance Applicative f => Inject ((:.:) f) where
diff --git a/src/Data/HFunctor/Chain.hs b/src/Data/HFunctor/Chain.hs
--- a/src/Data/HFunctor/Chain.hs
+++ b/src/Data/HFunctor/Chain.hs
@@ -1,18 +1,3 @@
-{-# LANGUAGE DeriveFoldable       #-}
-{-# LANGUAGE DeriveFunctor        #-}
-{-# LANGUAGE DeriveGeneric        #-}
-{-# LANGUAGE DeriveTraversable    #-}
-{-# LANGUAGE InstanceSigs         #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE StandaloneDeriving   #-}
-{-# LANGUAGE TypeApplications     #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
-
 -- |
 -- Module      : Data.HFunctor.Chain
 -- Copyright   : (c) Justin Le 2019
@@ -25,15 +10,15 @@
 -- This module provides an 'Interpret'able data type of "linked list of
 -- tensor applications".
 --
--- The type @'Chain' t@, for any @'Monoidal' t@, is meant to be the same as
--- @'MF' t@ (the monoidal functor combinator for @t@), and represents "zero
--- or more" applications of @f@ to @t@.
+-- The type @'Chain' t@, for any @'Tensor' t@, is meant to be the same as
+-- @'ListBy' t@ (the monoidal functor combinator for @t@), and represents
+-- "zero or more" applications of @f@ to @t@.
 --
--- The type @'Chain1' t@, for any @'Semigroupoidal' t@, is meant to be the
--- same as @'SF' t@ (the semigroupoidal functor combinator for @t@) and
+-- The type @'Chain1' t@, for any @'Associative' t@, is meant to be the
+-- same as @'NonEmptyBy' t@ (the semigroupoidal functor combinator for @t@) and
 -- represents "one or more" applications of @f@ to @t@.
 --
--- The advantage of using 'Chain' and 'Chain1' over 'MF' or 'SF' is that
+-- The advantage of using 'Chain' and 'Chain1' over 'ListBy' or 'NonEmptyBy' is that
 -- they provide a universal interface for pattern matching and constructing
 -- such values, which may simplify working with new such functor
 -- combinators you might encounter.
@@ -42,17 +27,17 @@
     Chain(..)
   , foldChain
   , unfoldChain
-  , unrollMF
-  , rerollMF
-  , unrollingMF
+  , unroll
+  , reroll
+  , unrolling
   , appendChain
   -- * 'Chain1'
   , Chain1(..)
   , foldChain1
   , unfoldChain1
-  , unrollingSF
-  , unrollSF
-  , rerollSF
+  , unrollingNE
+  , unrollNE
+  , rerollNE
   , appendChain1
   , fromChain1
   -- ** Matchable
@@ -64,9 +49,15 @@
   , unmatchChain
   ) where
 
+import           Control.Monad.Freer.Church
 import           Control.Natural
 import           Control.Natural.IsoF
+import           Data.Functor.Bind
 import           Data.Functor.Classes
+import           Data.Functor.Day hiding     (intro1, intro2, elim1, elim2)
+import           Data.Functor.Identity
+import           Data.Functor.Plus
+import           Data.Functor.Product
 import           Data.HBifunctor
 import           Data.HBifunctor.Associative
 import           Data.HBifunctor.Tensor
@@ -74,12 +65,12 @@
 import           Data.HFunctor.Interpret
 import           Data.Kind
 import           Data.Typeable
-import           GHC.Generics hiding         (C)
+import           GHC.Generics
 
 -- | A useful construction that works like a "non-empty linked list" of @t
 -- f@ applied to itself multiple times.  That is, it contains @t f f@, @t
 -- f (t f f)@, @t f (t f (t f f))@, etc, with @f@ occuring /one or more/
--- times.  It is meant to be the same as @'SF' t@.
+-- times.  It is meant to be the same as @'NonEmptyBy' t@.
 --
 -- A @'Chain1' t f a@ is explicitly one of:
 --
@@ -89,25 +80,47 @@
 -- *  @t f (t f (t f f)) a@
 -- *  .. etc
 --
--- Note that this is exactly the description of @'SF' t@.  And that's "the
--- point": for all instances of 'Semigroupoidal', @'Chain1' t@ is
--- isomorphic to @'SF' t@ (witnessed by 'unrollingSF').  That's big picture
--- of 'SF': it's supposed to be a type that consists of all possible
+-- Note that this is exactly the description of @'NonEmptyBy' t@.  And that's "the
+-- point": for all instances of 'Associative', @'Chain1' t@ is
+-- isomorphic to @'NonEmptyBy' t@ (witnessed by 'unrollingNE').  That's big picture
+-- of 'NonEmptyBy': it's supposed to be a type that consists of all possible
 -- self-applications of @f@ to @t@.
 --
--- 'Chain1' gives you a way to work with all @'SF' t@ in a uniform way.
--- Unlike for @'SF' t f@ in general, you can always explicitly /pattern
+-- 'Chain1' gives you a way to work with all @'NonEmptyBy' t@ in a uniform way.
+-- Unlike for @'NonEmptyBy' t f@ in general, you can always explicitly /pattern
 -- match/ on a 'Chain1' (with its two constructors) and do what you please
 -- with it.  You can also /construct/ 'Chain1' using normal constructors
 -- and functions.
 --
--- You can convert in between @'SF' t f@ and @'Chain1' t f@ with 'unrollSF'
--- and 'rerollSF'.  You can fully "collapse" a @'Chain1' t f@ into an @f@
--- with 'retract', if @t@ is 'Semigroupoidal'; this could be considered
--- a fundamental property of semigroupoidal-ness.
+-- You can convert in between @'NonEmptyBy' t f@ and @'Chain1' t f@ with 'unrollNE'
+-- and 'rerollNE'.  You can fully "collapse" a @'Chain1' t f@ into an @f@
+-- with 'retract', if you have @'SemigroupIn' t f@; this could be considered
+-- a fundamental property of semigroup-ness.
 --
 -- See 'Chain' for a version that has an "empty" value.
 --
+-- Another way of thinking of this is that @'Chain1' t@ is the "free
+-- @'SemigroupIn' t@".  Given any functor @f@, @'Chain1' t f@ is
+-- a semigroup in the semigroupoidal category of endofunctors enriched by
+-- @t@.  So, @'Chain1' 'Control.Monad.Freer.Church.Comp'@ is the "free
+-- 'Data.Functor.Bind.Bind'", @'Chain1' 'Day'@ is the "free
+-- 'Data.Functor.Apply.Apply'", etc. You "lift" from @f a@ to @'Chain1'
+-- t f a@ using 'inject'.
+--
+-- Note: this instance doesn't exist directly because of restrictions in
+-- typeclasses, but is implemented as
+--
+-- @
+-- 'Associative' t => 'SemigroupIn' ('WrapHBF' t) ('Chain1' t f)
+-- @
+--
+-- where 'biretract' is 'appendChain1'.
+--
+-- You can fully "collapse" a @'Chain' t i f@ into an @f@ with
+-- 'retract', if you have @'MonoidIn' t i f@; this could be considered
+-- a fundamental property of monoid-ness.
+--
+--
 -- This construction is inspired by iteratees and machines.
 data Chain1 t f a = Done1 (f a)
                   | More1 (t f (Chain1 t f) a)
@@ -187,87 +200,136 @@
 instance HBifunctor t => Inject (Chain1 t) where
     inject  = Done1
 
-instance (HBifunctor t, Semigroupoidal t) => Interpret (Chain1 t) where
-    type C (Chain1 t) = CS t
+instance (HBifunctor t, SemigroupIn t f) => Interpret (Chain1 t) f where
     retract = \case
       Done1 x  -> x
       More1 xs -> binterpret id retract xs
-    interpret :: forall f g. CS t g => f ~> g -> Chain1 t f ~> g
+    interpret :: forall g. g ~> f -> Chain1 t g ~> f
     interpret f = go
       where
-        go :: Chain1 t f ~> g
+        go :: Chain1 t g ~> f
         go = \case
           Done1 x  -> f x
           More1 xs -> binterpret f go xs
 
--- | A type @'SF' t@ is supposed to represent the successive application of
+-- | A type @'NonEmptyBy' t@ is supposed to represent the successive application of
 -- @t@s to itself.  The type @'Chain1' t f@ is an actual concrete ADT that contains
 -- successive applications of @t@ to itself, and you can pattern match on
 -- each layer.
 --
--- 'unrollingSF' states that the two types are isormorphic.  Use 'unrollSF'
--- and 'rerollSF' to convert between the two.
-unrollingSF :: forall t f. (Semigroupoidal t, Functor f) => SF t f <~> Chain1 t f
-unrollingSF = isoF unrollSF rerollSF
+-- 'unrollingNE' states that the two types are isormorphic.  Use 'unrollNE'
+-- and 'rerollNE' to convert between the two.
+unrollingNE :: forall t f. (Associative t, Functor f) => NonEmptyBy t f <~> Chain1 t f
+unrollingNE = isoF unrollNE rerollNE
 
--- | A type @'SF' t@ is supposed to represent the successive application of
--- @t@s to itself.  'unrollSF' makes that successive application explicit,
+-- | A type @'NonEmptyBy' t@ is supposed to represent the successive application of
+-- @t@s to itself.  'unrollNE' makes that successive application explicit,
 -- buy converting it to a literal 'Chain1' of applications of @t@ to
 -- itself.
 --
 -- @
--- 'unrollSF' = 'unfoldChain1' 'matchSF'
+-- 'unrollNE' = 'unfoldChain1' 'matchNE'
 -- @
-unrollSF :: (Semigroupoidal t, Functor f) => SF t f ~> Chain1 t f
-unrollSF = unfoldChain1 matchSF
+unrollNE :: (Associative t, Functor f) => NonEmptyBy t f ~> Chain1 t f
+unrollNE = unfoldChain1 matchNE
 
--- | A type @'SF' t@ is supposed to represent the successive application of
--- @t@s to itself.  'rerollSF' takes an explicit 'Chain1' of applications
--- of @t@ to itself and rolls it back up into an @'SF' t@.
+-- | A type @'NonEmptyBy' t@ is supposed to represent the successive application of
+-- @t@s to itself.  'rerollNE' takes an explicit 'Chain1' of applications
+-- of @t@ to itself and rolls it back up into an @'NonEmptyBy' t@.
 --
 -- @
--- 'rerollSF' = 'foldChain1' 'inject' 'consSF'
+-- 'rerollNE' = 'foldChain1' 'inject' 'consNE'
 -- @
-rerollSF :: Semigroupoidal t => Chain1 t f ~> SF t f
-rerollSF = foldChain1 inject consSF
+rerollNE :: Associative t => Chain1 t f ~> NonEmptyBy t f
+rerollNE = foldChain1 inject consNE
 
 -- | 'Chain1' is a semigroup with respect to @t@: we can "combine" them in
 -- an associative way.
 --
+-- This is essentially 'biretract', but only requiring @'Associative' t@:
+-- it comes from the fact that @'Chain1' t@ is the "free @'SemigroupIn'
+-- t@".
+--
 -- @since 0.1.1.0
 appendChain1
-    :: forall t f. (Semigroupoidal t, Functor f)
+    :: forall t f. (Associative t, Functor f)
     => t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
-appendChain1 = unrollSF
-             . appendSF
-             . hbimap rerollSF rerollSF
+appendChain1 = unrollNE
+             . appendNE
+             . hbimap rerollNE rerollNE
 
+-- | @'Chain1' t@ is the "free @'SemigroupIn' t@".  However, we have to
+-- wrap @t@ in 'WrapHBF' to prevent overlapping instances.
+instance (Associative t, Functor f) => SemigroupIn (WrapHBF t) (Chain1 t f) where
+    biretract = appendChain1 . unwrapHBF
+    binterpret f g = biretract . hbimap f g
+
+-- | @'Chain1' 'Day'@ is the free "semigroup in the semigroupoidal category
+-- of endofunctors enriched by 'Day'" --- aka, the free 'Apply'.
+instance Functor f => Apply (Chain1 Day f) where
+    f <.> x = appendChain1 $ Day f x ($)
+
+instance Functor f => Apply (Chain1 Comp f) where
+    (<.>) = apDefault
+
+-- | @'Chain1' 'Comp'@ is the free "semigroup in the semigroupoidal
+-- category of endofunctors enriched by 'Comp'" --- aka, the free 'Bind'.
+instance Functor f => Bind (Chain1 Comp f) where
+    x >>- f = appendChain1 (x :>>= f)
+
+-- | @'Chain1' (':*:')@ is the free "semigroup in the semigroupoidal
+-- category of endofunctors enriched by ':*:'" --- aka, the free 'Alt'.
+instance Functor f => Alt (Chain1 (:*:) f) where
+    x <!> y = appendChain1 (x :*: y)
+
+-- | @'Chain1' 'Product'@ is the free "semigroup in the semigroupoidal
+-- category of endofunctors enriched by 'Product'" --- aka, the free 'Alt'.
+instance Functor f => Alt (Chain1 Product f) where
+    x <!> y = appendChain1 (Pair x y)
+
 -- | A useful construction that works like a "linked list" of @t f@ applied
 -- to itself multiple times.  That is, it contains @t f f@, @t f (t f f)@,
 -- @t f (t f (t f f))@, etc, with @f@ occuring /zero or more/ times.  It is
--- meant to be the same as @'MF' t@.
+-- meant to be the same as @'ListBy' t@.
 --
--- If @t@ is 'Monoidal', then it means we can "collapse" this linked list
--- into some final type @'MF' t@ ('rerollMF'), and also extract it back
--- into a linked list ('unrollMF').
+-- If @t@ is 'Tensor', then it means we can "collapse" this linked list
+-- into some final type @'ListBy' t@ ('reroll'), and also extract it back
+-- into a linked list ('unroll').
 --
--- So, a value of type @'Chain' t ('I' t) f a@ is one of either:
+-- So, a value of type @'Chain' t i f a@ is one of either:
 --
--- *  @'I' t a@
+-- *  @i a@
 -- *  @f a@
 -- *  @t f f a@
 -- *  @t f (t f f) a@
 -- *  @t f (t f (t f f)) a@
 -- *  .. etc.
 --
--- Note that this is /exactly/ what an @'MF' t@ is supposed to be.  Using
--- 'Chain' allows us to work with all @'MF' t@s in a uniform way, with
+-- Note that this is /exactly/ what an @'ListBy' t@ is supposed to be.  Using
+-- 'Chain' allows us to work with all @'ListBy' t@s in a uniform way, with
 -- normal pattern matching and normal constructors.
 --
--- You can fully "collapse" a @'Chain' t (I t) f@ into an @f@ with
--- 'retract', if @t@ is 'Monoidal'; this could be considered a fundamental
--- property of monoidal-ness.
+-- You can fully "collapse" a @'Chain' t i f@ into an @f@ with
+-- 'retract', if you have @'MonoidIn' t i f@; this could be considered
+-- a fundamental property of monoid-ness.
 --
+-- Another way of thinking of this is that @'Chain' t i@ is the "free
+-- @'MonoidIn' t i@".  Given any functor @f@, @'Chain' t i f@ is a monoid
+-- in the monoidal category of endofunctors enriched by @t@.  So, @'Chain'
+-- 'Control.Monad.Freer.Church.Comp' 'Data.Functor.Identity.Identity'@ is
+-- the "free 'Monad'", @'Chain' 'Data.Functor.Day.Day'
+-- 'Data.Functor.Identity.Identity'@ is the "free 'Applicative'", etc.  You
+-- "lift" from @f a@ to @'Chain' t i f a@ using 'inject'.
+--
+-- Note: this instance doesn't exist directly because of restrictions in
+-- typeclasses, but is implemented as
+--
+-- @
+-- 'Tensor' t i => 'MonoidIn' ('WrapHBF' t) ('WrapF' i) ('Chain' t i f)
+-- @
+--
+-- where 'pureT' is 'Done' and 'biretract' is 'appendChain'.
+--
 -- This construction is inspired by
 -- <http://oleg.fi/gists/posts/2018-02-21-single-free.html>
 data Chain t i f a = Done (i a)
@@ -310,7 +372,7 @@
          <> readsUnaryWith (liftReadsPrec rp rl) "More" More
 
 -- | Recursively fold down a 'Chain'.  Provide a function on how to handle
--- the "single @f@ case" ('nilMF'), and how to handle the "combined @t f g@
+-- the "single @f@ case" ('nilLB'), and how to handle the "combined @t f g@
 -- case", and this will fold the entire @'Chain' t i) f@ into a single @g@.
 --
 -- This is a catamorphism.
@@ -343,19 +405,18 @@
 instance HBifunctor t => HFunctor (Chain t i) where
     hmap f = foldChain Done (More . hleft f)
 
-instance (Tensor t, i ~ I t) => Inject (Chain t i) where
+instance Tensor t i => Inject (Chain t i) where
     inject = More . hright Done . intro1
 
 -- | We can collapse and interpret an @'Chain' t i@ if we have @'Tensor' t@.
-instance (Monoidal t, i ~ I t) => Interpret (Chain t i) where
-    type C (Chain t i) = CM t
+instance MonoidIn t i f => Interpret (Chain t i) f where
     interpret
-        :: forall f g. CM t g
-        => f ~> g
-        -> Chain t i f ~> g
-    interpret f = upgradeC @t (Proxy @g) go
+        :: forall g. ()
+        => g ~> f
+        -> Chain t i g ~> f
+    interpret f = go
       where
-        go :: CS t g => Chain t i f ~> g
+        go :: Chain t i g ~> f
         go = \case
           Done x  -> pureT @t x
           More xs -> binterpret f go xs
@@ -365,92 +426,157 @@
 -- always has at least one @f@.
 --
 -- The result of this function always is made with 'More' at the top level.
-fromChain1 :: Tensor t => Chain1 t f ~> Chain t (I t) f
+fromChain1
+    :: Tensor t i
+    => Chain1 t f ~> Chain t i f
 fromChain1 = foldChain1 (More . hright Done . intro1) More
 
--- | A type @'MF' t@ is supposed to represent the successive application of
--- @t@s to itself.  The type @'Chain' t ('I' t) f@ is an actual concrete
+-- | A type @'ListBy' t@ is supposed to represent the successive application of
+-- @t@s to itself.  The type @'Chain' t i f@ is an actual concrete
 -- ADT that contains successive applications of @t@ to itself, and you can
 -- pattern match on each layer.
 --
--- 'unrollingMF' states that the two types are isormorphic.  Use 'unrollMF'
--- and 'rerollMF' to convert between the two.
-unrollingMF :: Monoidal t => MF t f <~> Chain t (I t) f
-unrollingMF = isoF unrollMF rerollMF
+-- 'unrolling' states that the two types are isormorphic.  Use 'unroll'
+-- and 'reroll' to convert between the two.
+unrolling
+    :: Tensor t i
+    => ListBy t f <~> Chain t i f
+unrolling = isoF unroll reroll
 
--- | A type @'MF' t@ is supposed to represent the successive application of
--- @t@s to itself.  'unrollMF' makes that successive application explicit,
+-- | A type @'ListBy' t@ is supposed to represent the successive application of
+-- @t@s to itself.  'unroll' makes that successive application explicit,
 -- buy converting it to a literal 'Chain' of applications of @t@ to
 -- itself.
 --
 -- @
--- 'unrollMF' = 'unfoldChain' 'unconsMF'
+-- 'unroll' = 'unfoldChain' 'unconsLB'
 -- @
-unrollMF :: Monoidal t => MF t f ~> Chain t (I t) f
-unrollMF = unfoldChain unconsMF
+unroll
+    :: Tensor t i
+    => ListBy t f ~> Chain t i f
+unroll = unfoldChain unconsLB
 
--- | A type @'MF' t@ is supposed to represent the successive application of
--- @t@s to itself.  'rerollSF' takes an explicit 'Chain' of applications of
--- @t@ to itself and rolls it back up into an @'MF' t@.
+-- | A type @'ListBy' t@ is supposed to represent the successive application of
+-- @t@s to itself.  'rerollNE' takes an explicit 'Chain' of applications of
+-- @t@ to itself and rolls it back up into an @'ListBy' t@.
 --
 -- @
--- 'rerollMF' = 'foldChain' 'nilMF' 'consMF'
+-- 'reroll' = 'foldChain' 'nilLB' 'consLB'
 -- @
 --
 -- Because @t@ cannot be inferred from the input or output, you should call
 -- this with /-XTypeApplications/:
 --
 -- @
--- 'rerollMF' \@'Control.Monad.Freer.Church.Comp'
+-- 'reroll' \@'Control.Monad.Freer.Church.Comp'
 --     :: 'Chain' Comp 'Data.Functor.Identity.Identity' f a -> 'Control.Monad.Freer.Church.Free' f a
 -- @
-rerollMF :: forall t f. Monoidal t => Chain t (I t) f ~> MF t f
-rerollMF = foldChain (nilMF @t) consMF
+reroll
+    :: forall t i f. Tensor t i
+    => Chain t i f ~> ListBy t f
+reroll = foldChain (nilLB @t) consLB
 
 -- | 'Chain' is a monoid with respect to @t@: we can "combine" them in
 -- an associative way.  The identity here is anything made with the 'Done'
 -- constructor.
 --
+-- This is essentially 'biretract', but only requiring @'Tensor' t i@: it
+-- comes from the fact that @'Chain1' t i@ is the "free @'MonoidIn' t i@".
+-- 'pureT' is 'Done'.
+--
 -- @since 0.1.1.0
 appendChain
-    :: forall t f. Monoidal t
-    => t (Chain t (I t) f) (Chain t (I t) f) ~> Chain t (I t) f
-appendChain = unrollMF
-            . appendMF
-            . hbimap rerollMF rerollMF
+    :: forall t i f. Tensor t i
+    => t (Chain t i f) (Chain t i f) ~> Chain t i f
+appendChain = unroll
+            . appendLB
+            . hbimap reroll reroll
 
 -- | A @'Chain1' t f@ is like a non-empty linked list of @f@s, and
--- a @'Chain' t ('I' t) f@ is a possibly-empty linked list of @f@s.  This
+-- a @'Chain' t i f@ is a possibly-empty linked list of @f@s.  This
 -- witnesses the fact that the former is isomorphic to @f@ consed to the
 -- latter.
 splittingChain1
-    :: forall t f. (Matchable t, Functor f)
-    => Chain1 t f <~> t f (Chain t (I t) f)
-splittingChain1 = fromF unrollingSF
-                . splittingSF @t
-                . overHBifunctor id unrollingMF
+    :: forall t i f. (Matchable t i, Functor f)
+    => Chain1 t f <~> t f (Chain t i f)
+splittingChain1 = fromF unrollingNE
+                . splittingNE @t
+                . overHBifunctor id unrolling
 
 -- | The "forward" function representing 'splittingChain1'.  Provided here
 -- as a separate function because it does not require @'Functor' f@.
 splitChain1
-    :: forall t f. Matchable t
-    => Chain1 t f ~> t f (Chain t (I t) f)
-splitChain1 = hright (unrollMF @t) . splitSF @t . rerollSF
+    :: forall t i f. Tensor t i
+    => Chain1 t f ~> t f (Chain t i f)
+splitChain1 = hright (unroll @t) . splitNE @t . rerollNE
 
--- | A @'Chain' t ('I' t) f@ is a linked list of @f@s, and a @'Chain1' t f@ is
+-- | A @'Chain' t i f@ is a linked list of @f@s, and a @'Chain1' t f@ is
 -- a non-empty linked list of @f@s.  This witnesses the fact that
--- a @'Chain' t (I t) f@ is either empty (@'I' t@) or non-empty (@'Chain1'
--- t f@).
+-- a @'Chain' t i f@ is either empty (@i@) or non-empty (@'Chain1' t f@).
 matchingChain
-    :: forall t f. (Matchable t, Functor f)
-    => Chain t (I t) f <~> I t :+: Chain1 t f
-matchingChain = fromF unrollingMF
-              . matchingMF @t
-              . overHBifunctor id unrollingSF
+    :: forall t i f. (Tensor t i, Matchable t i, Functor f)
+    => Chain t i f <~> i :+: Chain1 t f
+matchingChain = fromF unrolling
+              . matchingLB @t
+              . overHBifunctor id unrollingNE
 
 -- | The "reverse" function representing 'matchingChain'.  Provided here
 -- as a separate function because it does not require @'Functor' f@.
 unmatchChain
-    :: forall t f. Matchable t
-    => I t :+: Chain1 t f ~> Chain t (I t) f
-unmatchChain = unrollMF . (nilMF @t !*! fromSF @t) . hright rerollSF
+    :: forall t i f. Tensor t i
+    => i :+: Chain1 t f ~> Chain t i f
+unmatchChain = unroll . (nilLB @t !*! fromNE @t) . hright rerollNE
+
+-- | We have to wrap @t@ in 'WrapHBF' to prevent overlapping instances.
+instance (Tensor t i, Functor f) => SemigroupIn (WrapHBF t) (Chain t i f) where
+    biretract = appendChain . unwrapHBF
+    binterpret f g = biretract . hbimap f g
+
+-- | @'Chain' t i@ is the "free @'MonoidIn' t i@".  However, we have to
+-- wrap @t@ in 'WrapHBF' and @i@ in 'WrapF' to prevent overlapping instances.
+instance (Tensor t i, Functor f) => MonoidIn (WrapHBF t) (WrapF i) (Chain t i f) where
+    pureT = Done . unwrapF
+
+instance Apply (Chain Day Identity f) where
+    f <.> x = appendChain $ Day f x ($)
+
+-- | @'Chain' 'Day' 'Identity'@ is the free "monoid in the monoidal
+-- category of endofunctors enriched by 'Day'" --- aka, the free
+-- 'Applicative'.
+instance Applicative (Chain Day Identity f) where
+    pure  = Done . Identity
+    (<*>) = (<.>)
+
+instance Apply (Chain Comp Identity f) where
+    (<.>) = apDefault
+
+instance Applicative (Chain Comp Identity f) where
+    pure  = Done . Identity
+    (<*>) = (<.>)
+
+instance Bind (Chain Comp Identity f) where
+    x >>- f = appendChain (x :>>= f)
+
+-- | @'Chain' 'Comp' 'Identity'@ is the free "monoid in the monoidal
+-- category of endofunctors enriched by 'Comp'" --- aka, the free
+-- 'Monad'.
+instance Monad (Chain Comp Identity f) where
+    (>>=) = (>>-)
+
+instance Functor f => Alt (Chain (:*:) Proxy f) where
+    x <!> y = appendChain (x :*: y)
+
+-- | @'Chain' (':*:') 'Proxy'@ is the free "monoid in the monoidal
+-- category of endofunctors enriched by ':*:'" --- aka, the free
+-- 'Plus'.
+instance Functor f => Plus (Chain (:*:) Proxy f) where
+    zero = Done Proxy
+
+instance Functor f => Alt (Chain Product Proxy f) where
+    x <!> y = appendChain (Pair x y)
+
+-- | @'Chain' (':*:') 'Proxy'@ is the free "monoid in the monoidal
+-- category of endofunctors enriched by ':*:'" --- aka, the free
+-- 'Plus'.
+instance Functor f => Plus (Chain Product Proxy f) where
+    zero = Done Proxy
diff --git a/src/Data/HFunctor/Final.hs b/src/Data/HFunctor/Final.hs
--- a/src/Data/HFunctor/Final.hs
+++ b/src/Data/HFunctor/Final.hs
@@ -1,13 +1,3 @@
-{-# LANGUAGE ConstraintKinds        #-}
-{-# LANGUAGE DefaultSignatures      #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses  #-}
-{-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE TypeOperators          #-}
-{-# LANGUAGE UndecidableInstances   #-}
-
 -- |
 -- Module      : Data.HFunctor.Final
 -- Copyright   : (c) Justin Le 2019
@@ -228,9 +218,7 @@
 instance Inject (Final c) where
     inject x = Final ($ x)
 
-instance Interpret (Final c) where
-    type C (Final c) = c
-
+instance c f => Interpret (Final c) f where
     retract x = runFinal x id
     interpret f x = runFinal x f
 
@@ -260,11 +248,11 @@
 -- In the case where 'toFinal' doesn't lose any information, this will form
 -- an isomorphism with 'fromFinal', and @t@ is known as the "Free @c@".
 -- For such a situation, @t@ will have a 'FreeOf' instance.
-toFinal :: (Interpret t, C t (Final c f)) => t f ~> Final c f
+toFinal :: Interpret t (Final c f) => t f ~> Final c f
 toFinal = interpret inject
 
 -- | "Concretize" a 'Final'.
-
+--
 -- @
 -- fromFinal :: 'Final' 'Functor' f '~>' 'Coyoneda' f
 -- fromFinal :: 'Final' 'Applicative' f '~>' 'Ap' f
@@ -279,7 +267,7 @@
 --
 -- In the case that this forms an isomorphism with 'toFinal', the @t@ will
 -- have an instance of 'FreeOf'.
-fromFinal :: (Interpret t, c (t f)) => Final c f ~> t f
+fromFinal :: (Inject t, c (t f)) => Final c f ~> t f
 fromFinal = interpret inject
 
 -- | A typeclass associating a free structure with the typeclass it is free
@@ -296,28 +284,28 @@
 -- This can be useful because 'Final' doesn't have a concrete structure
 -- that you can pattern match on and inspect, but @t@ might.  This lets you
 -- work on a concrete structure if you desire.
-class Interpret t => FreeOf c t | t -> c where
+class FreeOf c t | t -> c where
     fromFree :: t f ~> Final c f
     toFree   :: Functor f => Final c f ~> t f
 
-    default fromFree :: C t (Final c f) => t f ~> Final c f
+    default fromFree :: Interpret t (Final c f) => t f ~> Final c f
     fromFree = toFinal
-    default toFree :: c (t f) => Final c f ~> t f
+    default toFree :: (Inject t, c (t f)) => Final c f ~> t f
     toFree = fromFinal
 
 -- | The isomorphism between a free structure and its encoding as 'Final'.
 finalizing :: (FreeOf c t, Functor f) => t f <~> Final c f
 finalizing = isoF fromFree toFree
 
-instance FreeOf Functor Coyoneda
-instance FreeOf Applicative Ap
-instance FreeOf Apply Ap1
-instance FreeOf Applicative FAF.Ap
-instance FreeOf Alternative Alt.Alt
-instance FreeOf Monad Free
-instance FreeOf Bind Free1
-instance FreeOf Pointed Lift
-instance FreeOf Pointed MaybeApply
-instance FreeOf Alt NonEmptyF
-instance FreeOf Plus ListF
+instance FreeOf Functor       Coyoneda
+instance FreeOf Applicative   Ap
+instance FreeOf Apply         Ap1
+instance FreeOf Applicative   FAF.Ap
+instance FreeOf Alternative   Alt.Alt
+instance FreeOf Monad         Free
+instance FreeOf Bind          Free1
+instance FreeOf Pointed       Lift
+instance FreeOf Pointed       MaybeApply
+instance FreeOf Alt           NonEmptyF
+instance FreeOf Plus          ListF
 instance FreeOf Unconstrained IdentityT
diff --git a/src/Data/HFunctor/Internal.hs b/src/Data/HFunctor/Internal.hs
--- a/src/Data/HFunctor/Internal.hs
+++ b/src/Data/HFunctor/Internal.hs
@@ -1,14 +1,4 @@
-{-# LANGUAGE DeriveFunctor       #-}
-{-# LANGUAGE DerivingVia         #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving  #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeInType          #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE DerivingVia #-}
 
 module Data.HFunctor.Internal (
     HFunctor(..)
@@ -49,7 +39,7 @@
 import           Data.Vinyl.CoRec
 import           Data.Vinyl.Core                (Rec)
 import           Data.Vinyl.Recursive
-import           GHC.Generics hiding            (C)
+import           GHC.Generics
 import qualified Control.Alternative.Free       as Alt
 import qualified Control.Applicative.Free.Fast  as FAF
 import qualified Control.Applicative.Free.Final as FA
@@ -131,17 +121,17 @@
 --
 -- This ensures that 'hleft', 'hright', and 'hbimap' do not affect the
 -- structure that @t@ adds on top of the underlying functors.
-class HBifunctor t where
+class HBifunctor (t :: (k -> Type) -> (k -> Type) -> k -> Type) where
     -- | Swap out the first transformed functor.
     hleft  :: f ~> j -> t f g ~> t j g
     hleft = (`hbimap` id)
 
     -- | Swap out the second transformed functor.
-    hright :: g ~> k -> t f g ~> t f k
+    hright :: g ~> l -> t f g ~> t f l
     hright = hbimap id
 
     -- | Swap out both transformed functors at the same time.
-    hbimap :: f ~> j -> g ~> k -> t f g ~> t j k
+    hbimap :: f ~> j -> g ~> l -> t f g ~> t j l
     hbimap f g = hleft f . hright g
 
     {-# MINIMAL hleft, hright | hbimap #-}
@@ -157,7 +147,7 @@
 -- @
 --
 -- to give us an automatic 'HFunctor' instance and save us some work.
-newtype WrappedHBifunctor t (f :: k -> Type) (g :: k -> Type) a
+newtype WrappedHBifunctor t (f :: k -> Type) (g :: k -> Type) (a :: k)
     = WrapHBifunctor { unwrapHBifunctor :: t f g a }
   deriving Functor
 
diff --git a/src/Data/HFunctor/Interpret.hs b/src/Data/HFunctor/Interpret.hs
--- a/src/Data/HFunctor/Interpret.hs
+++ b/src/Data/HFunctor/Interpret.hs
@@ -1,16 +1,3 @@
-{-# LANGUAGE ConstraintKinds         #-}
-{-# LANGUAGE DefaultSignatures       #-}
-{-# LANGUAGE FlexibleInstances       #-}
-{-# LANGUAGE InstanceSigs            #-}
-{-# LANGUAGE LambdaCase              #-}
-{-# LANGUAGE MultiParamTypeClasses   #-}
-{-# LANGUAGE PolyKinds               #-}
-{-# LANGUAGE RankNTypes              #-}
-{-# LANGUAGE ScopedTypeVariables     #-}
-{-# LANGUAGE TypeFamilies            #-}
-{-# LANGUAGE TypeOperators           #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
-
 -- |
 -- Module      : Data.HFunctor.Interpret
 -- Copyright   : (c) Justin Le 2019
@@ -59,6 +46,7 @@
   , getI
   , collectI
   , AndC
+  , WrapHF(..)
   ) where
 
 import           Control.Applicative
@@ -73,8 +61,9 @@
 import           Control.Monad.Trans.Identity
 import           Control.Natural
 import           Data.Coerce
-import           Data.Constraint.Trivial
+import           Data.Data
 import           Data.Functor.Bind
+import           Data.Functor.Classes
 import           Data.Functor.Coyoneda
 import           Data.Functor.Plus
 import           Data.Functor.Product
@@ -82,19 +71,19 @@
 import           Data.Functor.Sum
 import           Data.Functor.These
 import           Data.HFunctor
-import           Data.Kind
 import           Data.Maybe
 import           Data.Pointed
-import           Data.Proxy
 import           Data.Semigroup.Foldable
-import           GHC.Generics hiding            (C)
+import           GHC.Generics
 import qualified Control.Alternative.Free       as Alt
 import qualified Control.Applicative.Free       as Ap
 import qualified Control.Applicative.Free.Fast  as FAF
 import qualified Control.Applicative.Free.Final as FA
 import qualified Data.Map.NonEmpty              as NEM
 
--- | An 'Interpret' lets us move in and out of the "enhanced" 'Functor'.
+-- | An 'Interpret' lets us move in and out of the "enhanced" 'Functor' (@t
+-- f@) and the functor it enhances (@f@).  An instance @'Interpret' t f@
+-- means we have @t f a -> f a@.
 --
 -- For example, @'Free' f@ is @f@ enhanced with monadic structure.  We get:
 --
@@ -108,10 +97,6 @@
 -- we can give an /interpreting function/ that interprets @f@ into some
 -- target 'Monad'.
 --
--- The type family 'C' tells us the typeclass constraint of the "target"
--- functor.  For 'Free', it is 'Monad', but for other 'Interpret'
--- instances, we might have other constraints.
---
 -- We enforce that:
 --
 -- @
@@ -122,42 +107,56 @@
 --
 -- That is, if we lift a value into our structure, then immediately
 -- interpret it out as itself, it should lave the value unchanged.
-class Inject t => Interpret t where
-    -- | The constraint on the target context of 'interpret'.  It's
-    -- basically the constraint that allows you to "exit" or "run" an
-    -- 'Interpret'.
-    type C t :: (Type -> Type) -> Constraint
+--
+-- Note that instances of this class are /intended/ to be written with @t@
+-- as a fixed type constructor, and @f@ to be allowed to vary freely:
+--
+-- @
+-- instance Monad f => Interpret Free f
+-- @
+--
+-- Any other sort of instance and it's easy to run into problems with type
+-- inference.  If you want to write an instance that's "polymorphic" on
+-- tensor choice, use the 'WrapHF' newtype wrapper over a type variable,
+-- where the second argument also uses a type constructor:
+--
+-- @
+-- instance Interpret (WrapHF t) (MyFunctor t)
+-- @
+--
+-- This will prevent problems with overloaded instances.
+class Inject t => Interpret t f where
 
     -- | Remove the @f@ out of the enhanced @t f@ structure, provided that
     -- @f@ satisfies the necessary constraints.  If it doesn't, it needs to
     -- be properly 'interpret'ed out.
-    retract :: C t f => t f ~> f
+    retract :: t f ~> f
     retract = interpret id
 
     -- | Given an "interpeting function" from @f@ to @g@, interpret the @f@
     -- out of the @t f@ into a final context @g@.
-    interpret :: C t g => (f ~> g) -> t f ~> g
+    interpret :: (g ~> f) -> t g ~> f
     interpret f = retract . hmap f
 
     {-# MINIMAL retract | interpret #-}
 
 -- | A convenient flipped version of 'interpret'.
 forI
-    :: (Interpret t, C t g)
-    => t f a
-    -> (f ~> g)
-    -> g a
+    :: Interpret t f
+    => t g a
+    -> (g ~> f)
+    -> f a
 forI x f = interpret f x
 
 -- | Useful wrapper over 'interpret' to allow you to directly extract
 -- a value @b@ out of the @t f a@, if you can convert @f x@ into @b@.
 --
--- Note that depending on the constraints on the interpretation of @t@, you
+-- Note that depending on the constraints on @f@ in @'Interpret' t f@, you
 -- may have extra constraints on @b@.
 --
--- *    If @'C' t@ is 'Unconstrained', there are no constraints on @b@
--- *    If @'C' t@ is 'Apply', @b@ needs to be an instance of 'Semigroup'
--- *    If @'C' t@ is 'Applicative', @b@ needs to be an instance of 'Monoid'
+-- *    If @f@ is unconstrained, there are no constraints on @b@
+-- *    If @f@ must be 'Apply', @b@ needs to be an instance of 'Semigroup'
+-- *    If @f@ is 'Applicative', @b@ needs to be an instance of 'Monoid'
 --
 -- For some constraints (like 'Monad'), this will not be usable.
 --
@@ -168,7 +167,7 @@
 --      -> Int
 -- @
 getI
-    :: (Interpret t, C t (Const b))
+    :: Interpret t (Const b)
     => (forall x. f x -> b)
     -> t f a
     -> b
@@ -177,7 +176,9 @@
 -- | Useful wrapper over 'getI' to allow you to collect a @b@ from all
 -- instances of @f@ inside a @t f a@.
 --
--- This will work if @'C' t@ is 'Unconstrained', 'Apply', or 'Applicative'.
+-- Will work if there is an instance of @'Interpret' t ('Const' [b])@,
+-- which will be the case if the constraint on the target functor is
+-- 'Functor', 'Apply', 'Applicative', or unconstrianed.
 --
 -- @
 -- -- get the lengths of all @Map String@s in the 'Ap.Ap'.
@@ -186,96 +187,75 @@
 --      -> [Int]
 -- @
 collectI
-    :: (Interpret t, C t (Const [b]))
+    :: Interpret t (Const [b])
     => (forall x. f x -> b)
     -> t f a
     -> [b]
 collectI f = getI ((:[]) . f)
 
 -- | A free 'Functor'
-instance Interpret Coyoneda where
-    type C Coyoneda = Functor
-
+instance Functor f => Interpret Coyoneda f where
     retract                    = lowerCoyoneda
     interpret f (Coyoneda g x) = g <$> f x
 
 -- | A free 'Applicative'
-instance Interpret Ap.Ap where
-    type C Ap.Ap = Applicative
-
+instance Applicative f => Interpret Ap.Ap f where
     retract   = \case
       Ap.Pure x  -> pure x
       Ap.Ap x xs -> x <**> retract xs
     interpret = Ap.runAp
 
 -- | A free 'Plus'
-instance Interpret ListF where
-    type C ListF = Plus
-
+instance Plus f => Interpret ListF f where
     retract     = foldr (<!>) zero . runListF
     interpret f = foldr ((<!>) . f) zero . runListF
 
 -- | A free 'Alt'
-instance Interpret NonEmptyF where
-    type C NonEmptyF = Alt
-
+instance Alt f => Interpret NonEmptyF f where
     retract     = asum1 . runNonEmptyF
     interpret f = asum1 . fmap f . runNonEmptyF
 
--- | Technically, 'C' is over-constrained: we only need @'zero' :: f a@,
+-- | Technically, @f@ is over-constrained: we only need @'zero' :: f a@,
 -- but we don't really have that typeclass in any standard hierarchies.  We
 -- use 'Plus' here instead, but we never use '<!>'.  This would only go
 -- wrong in situations where your type supports 'zero' but not '<!>', like
 -- instances of 'Control.Monad.Fail.MonadFail' without
 -- 'Control.Monad.MonadPlus'.
-instance Interpret MaybeF where
-    type C MaybeF = Plus
-
+instance Plus f => Interpret MaybeF f where
     retract     = fromMaybe zero . runMaybeF
     interpret f = maybe zero f . runMaybeF
 
-instance Monoid k => Interpret (MapF k) where
-    type C (MapF k) = Plus
-
+instance (Monoid k, Plus f) => Interpret (MapF k) f where
     retract = foldr (<!>) zero . runMapF
     interpret f = foldr ((<!>) . f) zero . runMapF
 
-instance Monoid k => Interpret (NEMapF k) where
-    type C (NEMapF k) = Alt
-
+instance (Monoid k, Alt f) => Interpret (NEMapF k) f where
     retract = asum1 . runNEMapF
     interpret f = asum1 . fmap f . runNEMapF
 
 -- | Equivalent to instance for @'EnvT' ('Data.Semigroup.Sum'
 -- 'Numeric.Natural.Natural')@.
-instance Interpret Step where
-    type C Step = Unconstrained
-
+instance Interpret Step f where
     retract = stepVal
     interpret f = f . stepVal
 
-instance Interpret Steps where
-    type C Steps = Alt
-
+instance Alt f => Interpret Steps f where
     retract     = asum1 . getSteps
     interpret f = asum1 . NEM.map f . getSteps
 
 -- | Equivalent to instance for @'EnvT' 'Data.Semigroup.Any'@ and @'HLift'
 -- 'IdentityT'@.
-instance Interpret Flagged where
-    type C Flagged = Unconstrained
-
+instance Interpret Flagged f where
     retract = flaggedVal
     interpret f = f . flaggedVal
 
--- | Technically, 'C' is over-constrained: we only need @'zero' :: f a@,
+-- | Technically, @f@ is over-constrained: we only need @'zero' :: f a@,
 -- but we don't really have that typeclass in any standard hierarchies.  We
 -- use 'Plus' here instead, but we never use '<!>'.  This would only go
 -- wrong in situations where your type supports 'zero' but not '<!>', like
 -- instances of 'Control.Monad.Fail.MonadFail' without
 -- 'Control.Monad.MonadPlus'.
-instance Interpret (These1 f) where
-    type C (These1 f) = Plus
+instance Plus f => Interpret (These1 g) f where
     retract = \case
       This1  _   -> zero
       That1    y -> y
@@ -286,160 +266,121 @@
       These1 _ y -> f y
 
 -- | A free 'Alternative'
-instance Interpret Alt.Alt where
-    type C Alt.Alt = Alternative
-
+instance Alternative f => Interpret Alt.Alt f where
     interpret = Alt.runAlt
 
-instance Plus f => Interpret ((:*:) f) where
-    type C ((:*:) f) = Unconstrained
+instance Plus g => Interpret ((:*:) g) f where
     retract (_ :*: y) = y
 
-instance Plus f => Interpret (Product f) where
-    type C (Product f) = Unconstrained
+instance Plus g => Interpret (Product g) f where
     retract (Pair _ y) = y
 
--- | Technically, 'C' is over-constrained: we only need @'zero' :: f a@,
+-- | Technically, @f@ is over-constrained: we only need @'zero' :: f a@,
 -- but we don't really have that typeclass in any standard hierarchies.  We
 -- use 'Plus' here instead, but we never use '<!>'.  This would only go
 -- wrong in situations where your type supports 'zero' but not '<!>', like
 -- instances of 'Control.Monad.Fail.MonadFail' without
 -- 'Control.Monad.MonadPlus'.
-instance Interpret ((:+:) f) where
-    type C ((:+:) f) = Plus
+instance Plus f => Interpret ((:+:) g) f where
     retract = \case
       L1 _ -> zero
       R1 y -> y
 
--- | Technically, 'C' is over-constrained: we only need @'zero' :: f a@,
+-- | Technically, @f@ is over-constrained: we only need @'zero' :: f a@,
 -- but we don't really have that typeclass in any standard hierarchies.  We
 -- use 'Plus' here instead, but we never use '<!>'.  This would only go
 -- wrong in situations where your type supports 'zero' but not '<!>', like
 -- instances of 'Control.Monad.Fail.MonadFail' without
 -- 'Control.Monad.MonadPlus'.
-instance Interpret (Sum f) where
-    type C (Sum f) = Plus
+instance Plus f => Interpret (Sum g) f where
     retract = \case
       InL _ -> zero
       InR y -> y
 
-instance Interpret (M1 i c) where
-    type C (M1 i c) = Unconstrained
+instance Interpret (M1 i c) f where
     retract (M1 x) = x
     interpret f (M1 x) = f x
 
 -- | A free 'Monad'
-instance Interpret Free where
-    type C Free = Monad
-
+instance Monad f => Interpret Free f where
     retract   = retractFree
     interpret = interpretFree
 
 -- | A free 'Bind'
-instance Interpret Free1 where
-    type C Free1 = Bind
-
+instance Bind f => Interpret Free1 f where
     retract   = retractFree1
     interpret = interpretFree1
 
 -- | A free 'Applicative'
-instance Interpret FA.Ap where
-    type C FA.Ap = Applicative
-
+instance Applicative f => Interpret FA.Ap f where
     retract   = FA.retractAp
     interpret = FA.runAp
 
 -- | A free 'Applicative'
-instance Interpret FAF.Ap where
-    type C FAF.Ap = Applicative
-
+instance Applicative f => Interpret FAF.Ap f where
     retract   = FAF.retractAp
     interpret = FAF.runAp
 
--- | A free 'Unconstrained'
-instance Interpret IdentityT where
-    type C IdentityT = Unconstrained
-
+instance Interpret IdentityT f where
     retract = coerce
     interpret f = f . runIdentityT
 
 -- | A free 'Pointed'
-instance Interpret Lift where
-    type C Lift = Pointed
-
+instance Pointed f => Interpret Lift f where
     retract   = elimLift point id
     interpret = elimLift point
 
 -- | A free 'Pointed'
-instance Interpret MaybeApply where
-    type C MaybeApply = Pointed
-
+instance Pointed f => Interpret MaybeApply f where
     retract     = either id point . runMaybeApply
     interpret f = either f point . runMaybeApply
 
-instance Interpret Backwards where
-    type C Backwards = Unconstrained
-
+instance Interpret Backwards f where
     retract     = forwards
     interpret f = f . forwards
 
-instance Interpret WrappedApplicative where
-    type C WrappedApplicative = Unconstrained
-
+instance Interpret WrappedApplicative f where
     retract     = unwrapApplicative
     interpret f = f . unwrapApplicative
 
 -- | A free 'MonadReader', but only when applied to a 'Monad'.
-instance Interpret (ReaderT r) where
-    type C (ReaderT r) = MonadReader r
-
+instance MonadReader r f => Interpret (ReaderT r) f where
     retract     x = runReaderT x =<< ask
     interpret f x = f . runReaderT x =<< ask
 
 -- | This ignores the environment, so @'interpret' /= 'hbind'@
-instance Monoid e => Interpret (EnvT e) where
-    type C (EnvT e) = Unconstrained
-
+instance Monoid e => Interpret (EnvT e) f where
     retract     (EnvT _ x) = x
     interpret f (EnvT _ x) = f x
 
-instance Interpret Reverse where
-    type C Reverse = Unconstrained
-
+instance Interpret Reverse f where
     retract     = getReverse
     interpret f = f . getReverse
 
--- | The only way for this to obey @'retract' . 'inject' == 'id'@ is to
--- have it impossible to retract out of.
-instance Interpret ProxyF where
-    type C ProxyF = Impossible
-
-    retract = nope . reProxy
-
-reProxy :: p f a -> Proxy f
-reProxy _ = Proxy
+-- -- | The only way for this to obey @'retract' . 'inject' == 'id'@ is to
+-- -- have it impossible to retract out of.
+-- instance Impossible f => Interpret ProxyF f where
+--     retract = nope . reProxy
 
--- | The only way for this to obey @'retract' . 'inject' == 'id'@ is to
--- have it impossible to retract out of.
-instance Monoid e => Interpret (ConstF e) where
-    type C (ConstF e) = Impossible
+-- reProxy :: p f a -> Proxy f
+-- reProxy _ = Proxy
 
-    retract = nope . reProxy
+-- -- | The only way for this to obey @'retract' . 'inject' == 'id'@ is to
+-- -- have it impossible to retract out of.
+-- instance (Monoid e, Impossible f) => Interpret (ConstF e) f where
+--     retract = nope . reProxy
 
 -- | A constraint on @a@ for both @c a@ and @d a@.  Requiring @'AndC'
 -- 'Show' 'Eq' a@ is the same as requiring @('Show' a, 'Eq' a)@.
 class (c a, d a) => AndC c d a
 instance (c a, d a) => AndC c d a
 
-instance (Interpret s, Interpret t) => Interpret (ComposeT s t) where
-    type C (ComposeT s t) = AndC (C s) (C t)
-
+instance (Interpret s f, Interpret t f) => Interpret (ComposeT s t) f where
     retract     = interpret retract . getComposeT
     interpret f = interpret (interpret f) . getComposeT
 
 -- | Never uses 'inject'
-instance Interpret t => Interpret (HLift t) where
-    type C (HLift t) = C t
+instance Interpret t f => Interpret (HLift t) f where
     retract = \case
       HPure  x -> x
       HOther x -> retract x
@@ -448,8 +389,41 @@
       HOther x -> interpret f x
 
 -- | Never uses 'inject'
-instance Interpret t => Interpret (HFree t) where
-    type C (HFree t) = C t
+instance Interpret t f => Interpret (HFree t) f where
     retract = \case
       HReturn x -> x
       HJoin   x -> interpret retract x
+
+-- | A newtype wrapper meant to be used to define polymorphic 'Interpret'
+-- instances.  See documentation for 'Interpret' for more information.
+--
+-- Please do not ever define an instance of 'Interpret' "naked" on the
+-- second parameter:
+--
+-- @
+-- instance Interpret (WrapHF t) f
+-- @
+--
+-- As that would globally ruin everything using 'WrapHF'.
+newtype WrapHF t f a = WrapHF { unwrapHF :: t f a }
+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable, Typeable, Generic, Data)
+
+instance Show1 (t f) => Show1 (WrapHF t f) where
+    liftShowsPrec sp sl d (WrapHF x) = showsUnaryWith (liftShowsPrec sp sl) "WrapHF" d x
+
+instance Eq1 (t f) => Eq1 (WrapHF t f) where
+    liftEq eq (WrapHF x) (WrapHF y) = liftEq eq x y
+
+instance Ord1 (t f) => Ord1 (WrapHF t f) where
+    liftCompare c (WrapHF x) (WrapHF y) = liftCompare c x y
+
+instance HFunctor t => HFunctor (WrapHF t) where
+    hmap f (WrapHF x) = WrapHF (hmap f x)
+
+instance Inject t => Inject (WrapHF t) where
+    inject = WrapHF . inject
+
+instance HBind t => HBind (WrapHF t) where
+    hbind f (WrapHF x) = WrapHF (hbind (unwrapHF . f) x)
+    hjoin (WrapHF x) = WrapHF (hbind unwrapHF x)
+
diff --git a/test/Tests/HBifunctor.hs b/test/Tests/HBifunctor.hs
--- a/test/Tests/HBifunctor.hs
+++ b/test/Tests/HBifunctor.hs
@@ -1,11 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE OverloadedStrings   #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeOperators       #-}
-
 module Tests.HBifunctor (
     hbifunctorTests
   ) where
@@ -60,65 +52,65 @@
     -> PropertyT m ()
 associatingProp = isoProp (associating @t)
 
-matchingSFProp
+matchingNEProp
     :: forall t f m a.
-     ( Semigroupoidal t
+     ( Associative t
      , Monad m
      , Functor f
      , Show (f a), Eq (f a)
-     , Show (SF t f a), Eq (SF t f a)
-     , Show (t f (SF t f) a), Eq (t f (SF t f) a)
+     , Show (NonEmptyBy t f a), Eq (NonEmptyBy t f a)
+     , Show (t f (NonEmptyBy t f) a), Eq (t f (NonEmptyBy t f) a)
      )
-    => Gen (SF t f a)
+    => Gen (NonEmptyBy t f a)
     -> Gen (f a)
-    -> Gen (t f (SF t f) a)
+    -> Gen (t f (NonEmptyBy t f) a)
     -> PropertyT m ()
-matchingSFProp gx gy gz = isoProp (matchingSF @t) gx (sumGen gy gz)
+matchingNEProp gx gy gz = isoProp (matchingNE @t) gx (sumGen gy gz)
 
-unrollingSFProp
+unrollingNEProp
     :: forall t f m a.
-     ( Semigroupoidal t
+     ( SemigroupIn t f
      , Monad m
      , Functor f
-     , Show (SF t f a), Eq (SF t f a)
+     , Show (NonEmptyBy t f a), Eq (NonEmptyBy t f a)
      , Show (f a), Eq (f a)
      , Show (t f (Chain1 t f) a), Eq (t f (Chain1 t f) a)
      )
-    => Gen (SF t f a)
+    => Gen (NonEmptyBy t f a)
     -> Gen (Chain1 t f a)
     -> PropertyT m ()
-unrollingSFProp = isoProp (unrollingSF @t)
+unrollingNEProp = isoProp (unrollingNE @t)
 
-consSFProp
+consNEProp
     :: forall t f m a.
-     ( Semigroupoidal t
+     ( Associative t
      , Monad m
-     , Show (t f (SF t f) a)
-     , Show (SF t f a), Eq (SF t f a)
+     , Show (t f (NonEmptyBy t f) a)
+     , Show (NonEmptyBy t f a), Eq (NonEmptyBy t f a)
      )
-    => Gen (t f (SF t f) a)
+    => Gen (t f (NonEmptyBy t f) a)
     -> PropertyT m ()
-consSFProp gx = do
+consNEProp gx = do
     x <- forAll gx
-    appendSF (hleft inject x) === consSF x
+    appendNE (hleft inject x) === consNE x
 
-toSFProp
+toNonEmptyByProp
     :: forall t f m a.
-     ( Semigroupoidal t
+     ( Associative t
      , Monad m
      , Show (t f f a)
-     , Show (SF t f a), Eq (SF t f a)
+     , Show (NonEmptyBy t f a), Eq (NonEmptyBy t f a)
      )
     => Gen (t f f a)
     -> PropertyT m ()
-toSFProp gx = do
+toNonEmptyByProp gx = do
     x <- forAll gx
-    appendSF (hbimap inject inject x) === toSF x
+    appendNE (hbimap inject inject x) === toNonEmptyBy x
 
 biretractProp
     :: forall t f m a.
-     ( Semigroupoidal t
-     , CS t f
+     ( SemigroupIn t f
+     , Interpret (NonEmptyBy t) f
      , Monad m
      , Show (t f f a)
      , Show (f a), Eq (f a)
@@ -127,12 +119,11 @@
     -> PropertyT m ()
 biretractProp gx = do
     x <- forAll gx
-    retract (appendSF (hbimap inject inject x)) === biretract x
+    retract (appendNE (hbimap inject inject x)) === biretract x
 
 binterpretProp
     :: forall t f m a.
-     ( Semigroupoidal t
-     , CS t f
+     ( SemigroupIn t f
      , Monad m
      , Show (t f f a)
      , Show (f a), Eq (f a)
@@ -144,142 +135,142 @@
     biretract x === binterpret id id x
 
 rightIdentityProp
-    :: forall t f m a.
-     ( Tensor t
+    :: forall t i f m a.
+     ( Tensor t i
      , Monad m
      , Functor f
      , Show (f a), Eq (f a)
-     , Show (t f (I t) a), Eq (t f (I t) a)
+     , Show (t f i a), Eq (t f i a)
      )
     => Gen (f a)
-    -> Gen (t f (I t) a)
+    -> Gen (t f i a)
     -> PropertyT m ()
 rightIdentityProp = isoProp (rightIdentity @t)
 
 leftIdentityProp
-    :: forall t g m a.
-     ( Tensor t
+    :: forall t i g m a.
+     ( Tensor t i
      , Monad m
      , Functor g
      , Show (g a), Eq (g a)
-     , Show (t (I t) g a), Eq (t (I t) g a)
+     , Show (t i g a), Eq (t i g a)
      )
     => Gen (g a)
-    -> Gen (t (I t) g a)
+    -> Gen (t i g a)
     -> PropertyT m ()
 leftIdentityProp = isoProp (leftIdentity @t)
 
-splittingMFProp
-    :: forall t f m a.
-     ( Monoidal t
+splittingLBProp
+    :: forall t i f m a.
+     ( Tensor t i
      , Monad m
-     , Show (I t a), Eq (I t a)
-     , Show (MF t f a), Eq (MF t f a)
-     , Show (t f (MF t f) a), Eq (t f (MF t f) a)
+     , Show (i a), Eq (i a)
+     , Show (ListBy t f a), Eq (ListBy t f a)
+     , Show (t f (ListBy t f) a), Eq (t f (ListBy t f) a)
      )
-    => Gen (MF t f a)
-    -> Gen ((I t :+: t f (MF t f)) a)
+    => Gen (ListBy t f a)
+    -> Gen ((i :+: t f (ListBy t f)) a)
     -> PropertyT m ()
-splittingMFProp = isoProp (splittingMF @t)
+splittingLBProp = isoProp (splittingLB @t)
 
-unrollingMFProp
-    :: forall t f m a.
-     ( Monoidal t
+unrollingProp
+    :: forall t i f m a.
+     ( MonoidIn t i f
      , Monad m
-     , Show (MF t f a), Eq (MF t f a)
-     , Show (I t a), Eq (I t a)
-     , Show (t f (Chain t (I t) f) a), Eq (t f (Chain t (I t) f) a)
+     , Show (ListBy t f a), Eq (ListBy t f a)
+     , Show (i a), Eq (i a)
+     , Show (t f (Chain t i f) a), Eq (t f (Chain t i f) a)
      )
-    => Gen (MF t f a)
-    -> Gen (Chain t (I t) f a)
+    => Gen (ListBy t f a)
+    -> Gen (Chain t i f a)
     -> PropertyT m ()
-unrollingMFProp = isoProp (unrollingMF @t)
+unrollingProp = isoProp (unrolling @t)
 
-toMFProp
-    :: forall t f m a.
-     ( Monoidal t
+toListByProp
+    :: forall t i f m a.
+     ( Tensor t i
      , Monad m
      , Show (t f f a)
-     , Show (MF t f a), Eq (MF t f a)
+     , Show (ListBy t f a), Eq (ListBy t f a)
      )
     => Gen (t f f a)
     -> PropertyT m ()
-toMFProp gx = do
+toListByProp gx = do
     x <- forAll gx
-    reviewF (splittingMF @t) (R1 (hright (inject @(MF t)) x)) === toMF @t x
+    reviewF (splittingLB @t) (R1 (hright (inject @(ListBy t)) x)) === toListBy @t x
 
-fromSFProp
-    :: forall t f m a.
-     ( Monoidal t
+fromNEProp
+    :: forall t i f m a.
+     ( Tensor t i
      , Monad m
-     , Show (SF t f a)
-     , Show (MF t f a), Eq (MF t f a)
+     , Show (NonEmptyBy t f a)
+     , Show (ListBy t f a), Eq (ListBy t f a)
      )
-    => Gen (SF t f a)
+    => Gen (NonEmptyBy t f a)
     -> PropertyT m ()
-fromSFProp gx = do
+fromNEProp gx = do
     x <- forAll gx
-    reviewF (splittingMF @t) (R1 (splitSF @t x)) === fromSF @t x
+    reviewF (splittingLB @t) (R1 (splitNE @t x)) === fromNE @t x
 
 pureTProp
-    :: forall t f m a.
-     ( Monoidal t
+    :: forall t i f m a.
+     ( MonoidIn t i f
+     , Interpret (ListBy t) f
      , Monad m
-     , C (MF t) f
-     , Show (I t a)
+     , Show (i a)
      , Show (f a), Eq (f a)
      )
-    => Gen (I t a)
+    => Gen (i a)
     -> PropertyT m ()
 pureTProp gx = do
     x <- forAll gx
-    retract (reviewF (splittingMF @t) (L1 x)) === pureT @t @f x
+    retract (reviewF (splittingLB @t) (L1 x)) === pureT @t @_ @f x
 
-splittingSFProp
-    :: forall t f m a.
-     ( Matchable t
+splittingNEProp
+    :: forall t i f m a.
+     ( Matchable t i
      , Monad m
-     , Show (SF t f a), Eq (SF t f a)
-     , Show (t f (MF t f) a), Eq (t f (MF t f) a)
+     , Show (NonEmptyBy t f a), Eq (NonEmptyBy t f a)
+     , Show (t f (ListBy t f) a), Eq (t f (ListBy t f) a)
      )
-    => Gen (SF t f a)
-    -> Gen (t f (MF t f) a)
+    => Gen (NonEmptyBy t f a)
+    -> Gen (t f (ListBy t f) a)
     -> PropertyT m ()
-splittingSFProp = isoProp (splittingSF @t)
+splittingNEProp = isoProp (splittingNE @t)
 
-matchingMFProp
-    :: forall t f m a.
-     ( Matchable t
+matchingLBProp
+    :: forall t i f m a.
+     ( Matchable t i
      , Monad m
-     , Show (I t a), Eq (I t a)
-     , Show (MF t f a), Eq (MF t f a)
-     , Show (SF t f a), Eq (SF t f a)
+     , Show (i a), Eq (i a)
+     , Show (ListBy t f a), Eq (ListBy t f a)
+     , Show (NonEmptyBy t f a), Eq (NonEmptyBy t f a)
      )
-    => Gen (MF t f a)
-    -> Gen ((I t :+: SF t f) a)
+    => Gen (ListBy t f a)
+    -> Gen ((i :+: NonEmptyBy t f) a)
     -> PropertyT m ()
-matchingMFProp = isoProp (matchingMF @t)
+matchingLBProp = isoProp (matchingLB @t)
 
 matchingChainProp
-    :: forall t f m a.
-     ( Matchable t
+    :: forall t i f m a.
+     ( Matchable t i
      , Monad m
      , Functor f
      , Show (f a), Eq (f a)
-     , Show (I t a), Eq (I t a)
+     , Show (i a), Eq (i a)
      , Show (t f (Chain1 t f) a), Eq (t f (Chain1 t f) a)
-     , Show (t f (Chain t (I t) f) a), Eq (t f (Chain t (I t) f) a)
+     , Show (t f (Chain t i f) a), Eq (t f (Chain t i f) a)
      )
-    => Gen (Chain t (I t ) f a)
-    -> Gen ((I t :+: Chain1 t f) a)
+    => Gen (Chain t i f a)
+    -> Gen ((i :+: Chain1 t f) a)
     -> PropertyT m ()
 matchingChainProp = isoProp (matchingChain @t)
 
 genChain
-    :: forall t f m a. (MonadGen m, TestHBifunctor t)
+    :: forall t i f m a. (MonadGen m, TestHBifunctor t)
     => m (f a)
-    -> Maybe (m (I t a))
-    -> m (Chain t (I t) f a)
+    -> Maybe (m (i a))
+    -> m (Chain t i f a)
 genChain gx gy = go
   where
     go = case gy of
@@ -306,166 +297,167 @@
     [ ("hbimap", hbimapProp @t (genHB gx gx))
     ]
 
-semigroupoidalProps
+associativeProps
     :: forall t f a.
-     ( Semigroupoidal t
+     ( SemigroupIn t f
+     , Interpret (NonEmptyBy t) f
      , TestHBifunctor t
-     , TestHFunctor (SF t)
-     , CS t f
+     , TestHFunctor (NonEmptyBy t)
      , Functor f
      , Show (t f (t f f) a)     , Eq (t f (t f f) a)
      , Show (t (t f f) f a)     , Eq (t (t f f) f a)
      , Show (t f f a)
-     , Show (t f (SF t f) a)    , Eq (t f (SF t f) a)
-     , Show (SF t f a)          , Eq (SF t f a)
+     , Show (t f (NonEmptyBy t f) a)    , Eq (t f (NonEmptyBy t f) a)
+     , Show (NonEmptyBy t f a)          , Eq (NonEmptyBy t f a)
      , Show (t f (Chain1 t f) a), Eq (t f (Chain1 t f) a)
      , Show (f a)               , Eq (f a)
      )
     => Gen (f a)
     -> TestTree
-semigroupoidalProps gx = testGroup "Semigroupoidal"
+associativeProps gx = testGroup "Associative"
                        . map (uncurry testProperty . second property) $
     [ ("associating", associatingProp @t (genHB gx (genHB gx gx)) (genHB (genHB gx gx) gx))
-    , ("matchingSF" , matchingSFProp  @t (genHF gx) gx (genHB gx (genHF gx)))
-    , ("unrollingSF", unrollingSFProp @t (genHF gx) (genHF gx))
-    , ("consSF"     , consSFProp      @t (genHB gx (genHF gx)))
-    , ("toSF"       , toSFProp        @t (genHB gx gx))
+    , ("matchingNE" , matchingNEProp  @t (genHF gx) gx (genHB gx (genHF gx)))
+    , ("unrollingNE", unrollingNEProp @t (genHF gx) (genHF gx))
+    , ("consNE"     , consNEProp      @t (genHB gx (genHF gx)))
+    , ("toNonEmptyBy"       , toNonEmptyByProp        @t (genHB gx gx))
     , ("biretract"  , biretractProp   @t (genHB gx gx))
     , ("binterpret" , binterpretProp  @t (genHB gx gx))
     ]
 
-monoidalProps
-    :: forall t f a.
-     ( Monoidal t
+tensorProps
+    :: forall t i f a.
+     ( MonoidIn t i f
+     , Interpret (ListBy t) f
      , TestHBifunctor t
-     , TestHFunctor (MF t)
-     , TestHFunctor (SF t)
-     , CM t f
+     , TestHFunctor (ListBy t)
+     , TestHFunctor (NonEmptyBy t)
      , Functor f
-     , Show (t f (I t) a)            , Eq (t f (I t) a)
-     , Show (t (I t) f a)            , Eq (t (I t) f a)
-     , Show (t f (MF t f) a)         , Eq (t f (MF t f) a)
-     , Show (t f (Chain t (I t) f) a), Eq (t f (Chain t (I t) f) a)
+     , Show (t f i a)            , Eq (t f i a)
+     , Show (t i f a)            , Eq (t i f a)
+     , Show (t f (ListBy t f) a)         , Eq (t f (ListBy t f) a)
+     , Show (t f (Chain t i f) a), Eq (t f (Chain t i f) a)
      , Show (t f f a)
-     , Show (MF t f a)               , Eq (MF t f a)
-     , Show (SF t f a)
-     , Show (I t a)                  , Eq (I t a)
+     , Show (ListBy t f a)               , Eq (ListBy t f a)
+     , Show (NonEmptyBy t f a)
+     , Show (i a)                  , Eq (i a)
      , Show (f a)                    , Eq (f a)
      )
     => Gen (f a)
-    -> Maybe (Gen (I t a))
+    -> Maybe (Gen (i a))
     -> TestTree
-monoidalProps gx gy = testGroup "Monoidal"
+tensorProps gx gy = testGroup "Tensor"
                     . map (uncurry testProperty . second property)
                     . catMaybes $
     [ gy <&> \y -> ("rightIdentity", rightIdentityProp @t gx (genHB gx y))
     , gy <&> \y -> ("leftIdentity" , leftIdentityProp  @t gx (genHB y gx))
-    , Just ("splittingMF", splittingMFProp @t (genHF gx) (maybeSumGen gy (genHB gx (genHF gx))))
-    , Just ("unrollingMF", unrollingMFProp @t (genHF gx) (genChain gx gy))
-    , Just ("toMF"       , toMFProp        @t (genHB gx gx))
-    , Just ("fromSF"     , fromSFProp      @t (genHF gx))
-    , gy <&> \y -> ("pureT"        , pureTProp          @t @f y)
+    , Just ("splittingLB", splittingLBProp @t (genHF gx) (maybeSumGen gy (genHB gx (genHF gx))))
+    , Just ("unrolling", unrollingProp @t (genHF gx) (genChain gx gy))
+    , Just ("toListBy"       , toListByProp        @t (genHB gx gx))
+    , Just ("fromNE"     , fromNEProp      @t (genHF gx))
+    , gy <&> \y -> ("pureT"        , pureTProp          @t @_ @f y)
     ]
 
 matchableProps
-    :: forall t f a.
-     ( Matchable t
+    :: forall t i f a.
+     ( Matchable t i
      , TestHBifunctor t
-     , TestHFunctor (MF t)
-     , TestHFunctor (SF t)
+     , TestHFunctor (ListBy t)
+     , TestHFunctor (NonEmptyBy t)
      , Functor f
-     , Show (t f (MF t f) a)         , Eq (t f (MF t f) a)
-     , Show (t f (Chain t (I t) f) a), Eq (t f (Chain t (I t) f) a)
+     , Show (t f (ListBy t f) a)         , Eq (t f (ListBy t f) a)
+     , Show (t f (Chain t i f) a), Eq (t f (Chain t i f) a)
      , Show (t f (Chain1 t f) a)     , Eq (t f (Chain1 t f) a)
-     , Show (MF t f a)               , Eq (MF t f a)
-     , Show (SF t f a)               , Eq (SF t f a)
-     , Show (I t a)                  , Eq (I t a)
+     , Show (ListBy t f a)               , Eq (ListBy t f a)
+     , Show (NonEmptyBy t f a)               , Eq (NonEmptyBy t f a)
+     , Show (i a)                  , Eq (i a)
      , Show (f a)                    , Eq (f a)
      )
     => Gen (f a)
-    -> Maybe (Gen (I t a))
+    -> Maybe (Gen (i a))
     -> TestTree
 matchableProps gx gy = testGroup "Matchable"
                      . map (uncurry testProperty . second property) $
-    [ ("splittingSF"  , splittingSFProp   @t (genHF gx) (genHB gx (genHF gx)))
-    , ("matchingMF"   , matchingMFProp    @t (genHF gx) (maybeSumGen gy (genHF gx)))
+    [ ("splittingNE"  , splittingNEProp   @t (genHF gx) (genHB gx (genHF gx)))
+    , ("matchingLB"   , matchingLBProp    @t (genHF gx) (maybeSumGen gy (genHF gx)))
     , ("matchingChain", matchingChainProp @t (genChain gx gy) (maybeSumGen gy (genHF gx)))
     ]
 
-semigroupoidalProps_
+associativeProps_
     :: forall t f a.
-     ( Semigroupoidal t
+     ( SemigroupIn t f
+     , Interpret (NonEmptyBy t) f
      , TestHBifunctor t
-     , TestHFunctor (SF t)
-     , CS t f
+     , TestHFunctor (NonEmptyBy t)
      , Functor f
      , Show (t f (t f f) a)     , Eq (t f (t f f) a)
      , Show (t (t f f) f a)     , Eq (t (t f f) f a)
      , Show (t f f a)           , Eq (t f f a)
-     , Show (t f (SF t f) a)    , Eq (t f (SF t f) a)
-     , Show (SF t f a)          , Eq (SF t f a)
+     , Show (t f (NonEmptyBy t f) a)    , Eq (t f (NonEmptyBy t f) a)
+     , Show (NonEmptyBy t f a)          , Eq (NonEmptyBy t f a)
      , Show (t f (Chain1 t f) a), Eq (t f (Chain1 t f) a)
      , Show (f a)               , Eq (f a)
      )
     => Gen (f a)
     -> [TestTree]
-semigroupoidalProps_ gx = [ hbifunctorProps @t gx, semigroupoidalProps @t gx ]
+associativeProps_ gx = [ hbifunctorProps @t gx, associativeProps @t gx ]
 
-monoidalProps_
-    :: forall t f a.
-     ( Monoidal t
+tensorProps_
+    :: forall t i f a.
+     ( MonoidIn t i f
+     , Interpret (NonEmptyBy t) f
+     , Interpret (ListBy t) f
      , TestHBifunctor t
-     , TestHFunctor (MF t)
-     , TestHFunctor (SF t)
-     , CM t f
-     , CS t f
+     , TestHFunctor (ListBy t)
+     , TestHFunctor (NonEmptyBy t)
      , Functor f
      , Show (t f (t f f) a)          , Eq (t f (t f f) a)
      , Show (t (t f f) f a)          , Eq (t (t f f) f a)
-     , Show (t f (I t) a)            , Eq (t f (I t) a)
-     , Show (t (I t) f a)            , Eq (t (I t) f a)
-     , Show (t f (MF t f) a)         , Eq (t f (MF t f) a)
-     , Show (t f (SF t f) a)         , Eq (t f (SF t f) a)
-     , Show (t f (Chain t (I t) f) a), Eq (t f (Chain t (I t) f) a)
+     , Show (t f i a)            , Eq (t f i a)
+     , Show (t i f a)            , Eq (t i f a)
+     , Show (t f (ListBy t f) a)         , Eq (t f (ListBy t f) a)
+     , Show (t f (NonEmptyBy t f) a)         , Eq (t f (NonEmptyBy t f) a)
+     , Show (t f (Chain t i f) a), Eq (t f (Chain t i f) a)
      , Show (t f (Chain1 t f) a)     , Eq (t f (Chain1 t f) a)
      , Show (t f f a)                , Eq (t f f a)
-     , Show (MF t f a)               , Eq (MF t f a)
-     , Show (SF t f a)               , Eq (SF t f a)
-     , Show (I t a)                  , Eq (I t a)
+     , Show (ListBy t f a)               , Eq (ListBy t f a)
+     , Show (NonEmptyBy t f a)               , Eq (NonEmptyBy t f a)
+     , Show (i a)                  , Eq (i a)
      , Show (f a)                    , Eq (f a)
      )
     => Gen (f a)
-    -> Maybe (Gen (I t a))
+    -> Maybe (Gen (i a))
     -> [TestTree]
-monoidalProps_ gx gy = semigroupoidalProps_ @t gx ++ [ monoidalProps @t gx gy ]
+tensorProps_ gx gy = associativeProps_ @t gx ++ [ tensorProps @t gx gy ]
 
 matchableProps_
-    :: forall t f a.
-     ( Matchable t
+    :: forall t i f a.
+     ( Matchable t i
+     , Interpret (NonEmptyBy t) f
+     , Interpret (ListBy t) f
+     , MonoidIn t i f
      , TestHBifunctor t
-     , TestHFunctor (MF t)
-     , TestHFunctor (SF t)
-     , CM t f
-     , CS t f
+     , TestHFunctor (ListBy t)
+     , TestHFunctor (NonEmptyBy t)
      , Functor f
      , Show (t f (t f f) a)          , Eq (t f (t f f) a)
      , Show (t (t f f) f a)          , Eq (t (t f f) f a)
-     , Show (t f (I t) a)            , Eq (t f (I t) a)
-     , Show (t (I t) f a)            , Eq (t (I t) f a)
-     , Show (t f (MF t f) a)         , Eq (t f (MF t f) a)
-     , Show (t f (SF t f) a)         , Eq (t f (SF t f) a)
-     , Show (t f (Chain t (I t) f) a), Eq (t f (Chain t (I t) f) a)
+     , Show (t f i a)            , Eq (t f i a)
+     , Show (t i f a)            , Eq (t i f a)
+     , Show (t f (ListBy t f) a)         , Eq (t f (ListBy t f) a)
+     , Show (t f (NonEmptyBy t f) a)         , Eq (t f (NonEmptyBy t f) a)
+     , Show (t f (Chain t i f) a), Eq (t f (Chain t i f) a)
      , Show (t f (Chain1 t f) a)     , Eq (t f (Chain1 t f) a)
      , Show (t f f a)                , Eq (t f f a)
-     , Show (MF t f a)               , Eq (MF t f a)
-     , Show (SF t f a)               , Eq (SF t f a)
-     , Show (I t a)                  , Eq (I t a)
+     , Show (ListBy t f a)               , Eq (ListBy t f a)
+     , Show (NonEmptyBy t f a)               , Eq (NonEmptyBy t f a)
+     , Show (i a)                  , Eq (i a)
      , Show (f a)                    , Eq (f a)
      )
     => Gen (f a)
-    -> Maybe (Gen (I t a))
+    -> Maybe (Gen (i a))
     -> [TestTree]
-matchableProps_ gx gy = monoidalProps_ @t gx gy ++ [ matchableProps @t gx gy ]
+matchableProps_ gx gy = tensorProps_ @t gx gy ++ [ matchableProps @t gx gy ]
 
 hbifunctorTests :: TestTree
 hbifunctorTests = testGroup "HBifunctors"
@@ -473,12 +465,12 @@
     , testGroup "Sum'"     $ matchableProps_      @Sum     listGen Nothing
     , testGroup "Product"  $ matchableProps_      @(:*:)   listGen (Just (pure Proxy))
     , testGroup "Product'" $ matchableProps_      @Product listGen (Just (pure Proxy))
-    , testGroup "These1"   $ monoidalProps_       @These1  listGen Nothing
-    , testGroup "LeftF"    $ semigroupoidalProps_ @LeftF   listGen
-    , testGroup "Joker"    $ semigroupoidalProps_ @Joker   listGen
-    , testGroup "RightF"   $ semigroupoidalProps_ @RightF  listGen
+    , testGroup "These1"   $ tensorProps_       @These1  listGen Nothing
+    , testGroup "LeftF"    $ associativeProps_ @LeftF   listGen
+    , testGroup "Joker"    $ associativeProps_ @Joker   listGen
+    , testGroup "RightF"   $ associativeProps_ @RightF  listGen
     , testGroup "Day"      $ matchableProps_      @Day     (Const . S.Sum <$> intGen)
                                                            (Just (Identity <$> intGen))
-    , testGroup "Comp"     $ monoidalProps_       @Comp    (Gen.list (Range.linear 0 3) intGen)
+    , testGroup "Comp"     $ tensorProps_       @Comp    (Gen.list (Range.linear 0 3) intGen)
                                                            (Just (Identity <$> intGen))
     ]
diff --git a/test/Tests/HFunctor.hs b/test/Tests/HFunctor.hs
--- a/test/Tests/HFunctor.hs
+++ b/test/Tests/HFunctor.hs
@@ -1,10 +1,3 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE LambdaCase          #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications    #-}
-
 module Tests.HFunctor (
     hfunctorTests
   ) where
@@ -43,9 +36,8 @@
 
 retractingProp
     :: forall t f m a.
-     ( Interpret t
+     ( Interpret t f
      , Monad m
-     , C t f
      , Show (f a)
      , Show (t f a)
      , Eq (f a)
@@ -58,9 +50,8 @@
 
 interpretProp
     :: forall t f m a.
-     ( Interpret t
+     ( Interpret t f
      , Monad m
-     , C t f
      , Show (f a)
      , Show (t f a)
      , Eq (f a)
@@ -140,9 +131,8 @@
 
 interpretProps
     :: forall t f a.
-     ( Interpret t
+     ( Interpret t f
      , TestHFunctor t
-     , C t f
      , Show (f a)          , Eq (f a)
      , Show (t f a)
      )
@@ -170,9 +160,8 @@
 
 interpretProps_
     :: forall t f a.
-     ( Interpret t
+     ( Interpret t f
      , TestHFunctor t
-     , C t f
      , Show (f a)          , Eq (f a)
      , Show (t f a)        , Eq (t f a)
      )
@@ -186,9 +175,8 @@
 bindInterpProps_
     :: forall t f a.
      ( HBind t
-     , Interpret t
+     , Interpret t f
      , TestHFunctor t
-     , C t f
      , Show (f a)          , Eq (f a)
      , Show (t f a)        , Eq (t f a)
      , Show (t (t f) a)
diff --git a/test/Tests/Util.hs b/test/Tests/Util.hs
--- a/test/Tests/Util.hs
+++ b/test/Tests/Util.hs
@@ -1,13 +1,3 @@
-{-# LANGUAGE DefaultSignatures    #-}
-{-# LANGUAGE EmptyCase            #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE StandaloneDeriving   #-}
-{-# LANGUAGE TypeApplications     #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans      #-}
 
 module Tests.Util (
@@ -38,6 +28,7 @@
 import           Data.GADT.Show
 import           Data.HBifunctor.Tensor
 import           Data.HFunctor.Chain
+import           Data.Kind
 import           Data.Semigroup                 (Any(..))
 import           Data.Semigroup.Traversable
 import           GHC.Generics                   (M1(..))
@@ -101,7 +92,7 @@
     showsPrec = gshowsPrec
 
 instance GShow f => GShow (Ap1 f) where
-    gshowsPrec d (Ap1 x y) = case matchMF @Day y of
+    gshowsPrec d (Ap1 x y) = case matchLB @Day y of
       L1 _  -> showsUnaryWith gshowsPrec "inject" d x
       R1 ys -> showsBinaryWith gshowsPrec gshowsPrec "Ap1" d x ys
 
@@ -345,7 +336,7 @@
 instance TestHFunctor WrappedApplicative
 instance TestHFunctor Reverse
 instance TestHFunctor Backwards
-instance Applicative f => TestHFunctor (Comp f)
+instance Applicative f => TestHFunctor (Comp f :: (Type -> Type) -> Type -> Type)
 instance TestHFunctor (M1 i c)
 instance Plus f => TestHFunctor ((:*:) f)
 instance Plus f => TestHFunctor (Product f)
