diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -5,25 +5,31 @@
 
 Refer to [ManySpec.hs](https://github.com/louispan/data-diverse-lens/blob/master/test/Data/Diverse/Lens/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/Lens/WhichSpec.hs) for example usages.
 
-
 # Changelog
 
+* 3.0.0.0
+  - Renamed `SelectWith` to `MakeFrom`, split `ChooseBtween` to `ChooseBoth` and `ChooseFrom`.
+  - Removed hard to remember operators ``>&&>` `*&&*` `+||+` `>||>`
+  - Removed `faceted'`
+  - Added `instance AsFacet Void (Which '[])` and `instance AsFacet (Which '[]) Void`
+  - Polymorphic `HasItemX` now only requires two to three type args.
+
 * 2.1.0.0
-  - Removed profunctor variable @w@ from the constraint synonyms for Projected/Injected.
+  - Removed profunctor variable `w` from the constraint synonyms for `Projected`/`Injected`.
 
 * 2.0.0.1
-  - Forgot to expose constraint synonyms for Projected/Injected.
+  - Forgot to expose constraint synonyms for `Projected`/`Injected`.
 
 * 2.0.0.0
-  - Breaking change: Removed HasProject and AsInject typeclasses and changed them back to functions.
-  - Added 'MatchingFacet' typeclasses for polymorphic 'matching' of prisms.
-  - Added constraint synonyms for Project/Inject/Projected/Injected.
+  - Breaking change: Removed `HasProject` and `AsInject` typeclasses and changed them back to functions.
+  - Added `MatchingFacet` typeclasses for polymorphic `matching` of prisms.
+  - Added constraint synonyms for `Project`/`Inject`/`Projected`/`Injected`.
 
 * 1.0.0.1
   - Fixed missing exports of the new lens classes.
 
 * 1.0.0.0
-  - Removed overlapping instances of Data.Generics lens
+  - Removed overlapping instances of `Data.Generics` lens
   - Using typeclass instead of plain functions so that lens can be used for other data types
     - Added default implementations for some of these typeclasses using Data.Generic typeclasses.
   - Breaking change: the xxx' version of functions are now consistently the simpler or non-polymorphic version    - This is more consistent with 'Control.Lens' as well.
@@ -37,13 +43,12 @@
       - `projectN`, `projectN'`
 
 * 0.5.2.0
-  - Added itemTag and facetTag that also tag/untags the field.
-  - Added overlapping instances of Data.Generics lens
+  - Added `itemTag` and `facetTag` that also tag/untags the field.
+  - Added overlapping instances of `Data.Generics` lens
 
 * 0.5.1.0
-  - Added faceted, injected, itemized, projected, which is analogous to Profunctor Choice and Strong
-    but using 'Which' and 'Many'
-  - Added +||+ (analogous to +++ and |||), >||>; and *&&* (analogous to *** and &&&), and >&&>.
+  - Added `faceted`, `injected`, `itemized`, `projected`, which is analogous to `Profunctor` `Choice` and `Strong` but using `Which` and `Many`
+  - Added `+||+` (analogous to `+++` and `|||`), `>||>`; and `*&&*` (analogous to `***` and `&&&`), and `>&&>`.
 
 * 0.5.0.0
   - min bounds: data-diverse >=1.2.1
@@ -56,10 +61,10 @@
   - included data-diverse 1.0 in the upper bounds
 
 * 0.4.0.0
-  - Changed type variable ordering of 'itemL' and 'itemL', so it's consistently 'x', 'y', then 'xs'
+  - Changed type variable ordering of `itemL` and `itemL`, so it's consistently `x`, `y`, then `xs`
 
 * 0.3.0.0
-  - Changed type variable ordering of 'facetL' and 'facetN', so it's consistently 'x' then 'xs'
+  - Changed type variable ordering of `facetL` and `facetN`, so it's consistently `x` then `xs`
 
 * pre 0.3.0.0
-  - Initial version represented as (Int, Data.Map Int Any)
+  - Initial version.
diff --git a/data-diverse-lens.cabal b/data-diverse-lens.cabal
--- a/data-diverse-lens.cabal
+++ b/data-diverse-lens.cabal
@@ -1,5 +1,5 @@
 name:                data-diverse-lens
-version:             2.1.0.0
+version:             3.0.0.0
 synopsis:            Isos & Lens for Data.Diverse.Many and Prisms for Data.Diverse.Which
 description:         Isos & Lens for Data.Diverse.Many and Prisms for Data.Diverse.Which
                      Refer to [ManySpec.hs](https://github.com/louispan/data-diverse-lens/blob/master/test/Data/Diverse/Lens/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse-lens/blob/master/test/Data/Diverse/Lens/WhichSpec.hs) for example usages.
@@ -24,7 +24,7 @@
                        Data.Diverse.Profunctor.Many
                        Data.Diverse.Profunctor.Which
   build-depends:       base >= 4.7 && < 5
-                     , data-diverse >= 2.0.1.0
+                     , data-diverse >= 3.0.0.0
                      , tagged >= 0.8.5
                      , profunctors >= 5.2
                      , generic-lens >= 0.5.0.0
@@ -39,7 +39,7 @@
   other-modules:       Data.Diverse.Lens.ManySpec
                        Data.Diverse.Lens.WhichSpec
   build-depends:       base
-                     , data-diverse >= 2.0.1.0
+                     , data-diverse >= 3.0.0.0
                      , data-diverse-lens
                      , hspec >= 2
                      , lens >= 4
diff --git a/src/Data/Diverse/Lens/Many.hs b/src/Data/Diverse/Lens/Many.hs
--- a/src/Data/Diverse/Lens/Many.hs
+++ b/src/Data/Diverse/Lens/Many.hs
@@ -48,11 +48,11 @@
     ) where
 
 import Control.Lens
-import Data.Tagged
 import Data.Diverse.Many
 import Data.Diverse.TypeLevel
 import Data.Generics.Product
 import Data.Kind
+import Data.Tagged
 import GHC.TypeLits
 
 -- | @_Many = iso fromMany toMany@
@@ -65,7 +65,7 @@
 
 -----------------------------------------------------------------------
 
--- | 'fetch' ('view' 'item') and 'replace'' ('set' 'item'') in 'Lens'' form.
+-- | 'grab' ('view' 'item') and 'replace'' ('set' 'item'') in 'Lens'' form.
 --
 -- @
 -- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nil'
@@ -80,27 +80,38 @@
     item' = typed
 
 instance UniqueMember x xs => HasItem' x (Many xs) where
-    item' = lens fetch replace'
+    item' = lens grab replace'
 
 -- | Polymorphic version of 'item''
-class HasItem a b s t | s a b -> t, t a b -> s where
-    item :: Lens s t a b
+class (HasItem' a s, Replaced a a s ~ s) => HasItem a s where
+    type Replaced a b s
+    item :: Lens s (Replaced a b s) a b
 
-instance (UniqueMember x xs, ys ~ Replace x y xs) => HasItem x y (Many xs) (Many ys) where
-    item = lens fetch (replace @x @y)
+instance (UniqueMember x xs) => HasItem x (Many xs) where
+    type Replaced a b (Many xs) = Many (Replace a b xs)
+    item = lens grab (replace @x)
 
--- | 'fetchL' ('view' 'itemL') and 'replaceL' ('set' 'itemL') in 'Lens'' form.
+-- | 'grabL' ('view' 'itemL') and 'replaceL' ('set' 'itemL') in 'Lens'' form.
 --
 -- @
 -- let x = (5 :: Int) './' Tagged \@Foo False './' Tagged \@Bar \'X' './' 'nil'
 -- x '^.' 'itemL'' \@Foo \`shouldBe` Tagged \@Foo False
 -- (x '&' 'itemL'' \@Foo '.~' Tagged \@Foo True) \`shouldBe` (5 :: Int) './' Tagged \@Foo True './' Tagged \@Bar \'X' './' 'nil'
 -- @
+--
+-- A default implementation using generics is not provided as it make GHC think that @l@ must be type @Symbol@
+-- when @l@ can actually be any kind.
+-- Create instances of 'HasItemL'' using "Data.Generics.Product.Fields" as follows:
+-- @
+-- instance HasField' l Foo a => itemL' l a Foo where
+--     itemL' = field @l
+-- default itemL' :: forall (l :: Symbol) a s. (HasField' l s a) => Lens' s a
+-- itemL' = field @l
 class HasItemL' (l :: k) a s | s l -> a where
     itemL' :: Lens' s a
 
 instance (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => HasItemL' l x (Many xs) where
-    itemL' = lens (fetchL @l) (replaceL' @l)
+    itemL' = lens (grabL @l) (replaceL' @l)
 
 -- | Polymorphic version of 'itemL''
 --
@@ -108,41 +119,31 @@
 -- let x = (5 :: Int) './' Tagged @Foo False './' Tagged \@Bar \'X' './' 'nil'
 -- (x '&' 'itemL' \@Foo '.~' \"foo") \`shouldBe` (5 :: Int) './' \"foo" './' Tagged \@Bar \'X' './' 'nil'
 -- @
-class HasItemL (l :: k) a b s t | s l -> a, t l -> b, s l b -> t, t l a -> s where
-    itemL :: Lens s t a b
+class (HasItemL' (l :: k) a s, ReplacedL l a a s ~ s) => HasItemL (l :: k) a s | s l -> a where
+    type ReplacedL l a b s
+    itemL :: Lens s (ReplacedL l a b s) a b
 
-instance (UniqueLabelMember l xs, x ~ KindAtLabel l xs, ys ~ Replace x y xs)
-  => HasItemL l x y (Many xs) (Many ys) where
-    itemL = lens (fetchL @l) (replaceL @l)
+instance (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => HasItemL l x (Many xs) where
+    type ReplacedL l _ b (Many xs) = Many (Replace (KindAtLabel l xs) b xs)
+    itemL = lens (grabL @l) (replaceL @l)
 
--- | Variation of 'itemL'' that automatically tags and untags the field.
--- A default implementation using generics is not provided as it make GHC think that @l@ must be type @Symbol@
--- when @l@ can actually be any kind.
--- Create instances of 'HasItemTag'' using "Data.Generics.Product.Fields" as follows:
--- @
--- instance HasField' l Foo a => HasItemTag' l a Foo where
---     itemTag' = field @l
+-- | Variation of 'itemL'' that automatically tags and untags a Tagged field.
 -- @
-class HasItemTag' (l :: k) a s where
+class HasItemL' l (Tagged l a) s => HasItemTag' (l :: k) a s where
     itemTag' :: Lens' s a
 
-instance (UniqueLabelMember l xs, Tagged l x ~ KindAtLabel l xs) => HasItemTag' l x (Many xs) where
-    itemTag' = lens (fetchTag @l) (replaceTag' @l)
-
--- | Variation of 'itemL' that automatically tags and untags the field.
-class HasItemTag (l :: k) a b s t | s l -> a, t l -> b, s l b -> t, t l a -> s where
-    itemTag :: Lens s t a b
+instance HasItemL' l (Tagged l a) s => HasItemTag' (l :: k) a s where
+    itemTag' = itemL' @l . iso unTagged Tagged
 
--- -- | Make it easy to create an instance of 'itemTag' using 'Data.Generics.Product.Fields'
--- -- NB. This is not a default signature for HasItemTag, as this makes GHC think that l must be type 'Symbol'
--- genericItemTag :: forall l a b s t. (HasField l s t a b) => Lens s t a b
--- genericItemTag = field @l
+-- | Polymorphic version of 'itemTag''
+-- @
+class HasItemL l (Tagged l a) s => HasItemTag (l :: k) a s where
+    itemTag :: Lens s (ReplacedL l (Tagged l a) (Tagged l b) s) a b
 
-instance (UniqueLabelMember l xs, Tagged l x ~ KindAtLabel l xs, ys ~ Replace (Tagged l x) (Tagged l y) xs)
-  => HasItemTag l x y (Many xs) (Many ys) where
-    itemTag = lens (fetchTag @l) (replaceTag @l)
+instance HasItemL l (Tagged l a) s => HasItemTag (l :: k) a s where
+    itemTag = itemL @l . iso unTagged (Tagged @l)
 
--- | 'fetchN' ('view' 'item') and 'replaceN'' ('set' 'item'') in 'Lens'' form.
+-- | 'grabN' ('view' 'item') and 'replaceN'' ('set' 'item'') in 'Lens'' form.
 --
 -- @
 -- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' ./ nil
@@ -153,19 +154,21 @@
     itemN' :: Lens' s a
 
 instance (MemberAt n x xs) => HasItemN' n x (Many xs) where
-    itemN' = lens (fetchN @n) (replaceN' @n)
+    itemN' = lens (grabN @n) (replaceN' @n)
 
 -- | Polymorphic version of 'itemN''
-class HasItemN (n :: Nat) a b s t | s n -> a, t n -> b, s n b -> t, t n a -> s where
-    itemN :: Lens s t a b
+class (HasItemN' (n :: Nat) a s, ReplacedN n a a s ~ s) => HasItemN (n :: Nat) a s | s n -> a where
+    type ReplacedN n a b s
+    itemN :: Lens s (ReplacedN n a b s) a b
 
     -- | Make it easy to create an instance of 'itemN' using 'Data.Generics.Product.Positions'
-    default itemN :: (HasPosition n s t a b) => Lens s t a b
+    default itemN :: (HasPosition n s (ReplacedN n a b s) a b) => Lens s (ReplacedN n a b s) a b
     itemN = position @n
 
-instance (MemberAt n x xs, ys ~ ReplaceIndex n y xs)
-  => HasItemN n x y (Many xs) (Many ys) where
-    itemN = lens (fetchN @n) (replaceN @n)
+instance (MemberAt n x xs)
+  => HasItemN n x (Many xs) where
+    type ReplacedN n a b (Many xs) = Many (ReplaceIndex n a b xs)
+    itemN = lens (grabN @n) (replaceN @n)
 
 -----------------------------------------------------------------------
 
diff --git a/src/Data/Diverse/Lens/Which.hs b/src/Data/Diverse/Lens/Which.hs
--- a/src/Data/Diverse/Lens/Which.hs
+++ b/src/Data/Diverse/Lens/Which.hs
@@ -6,9 +6,9 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -39,11 +39,12 @@
     ) where
 
 import Control.Lens
-import Data.Diverse.Which
 import Data.Diverse.TypeLevel
+import Data.Diverse.Which
 import Data.Generics.Sum
 import Data.Kind
 import Data.Tagged
+import Data.Void
 import GHC.TypeLits
 
 -----------------------------------------------------------------
@@ -66,6 +67,15 @@
     default facet :: (AsType a s) => Prism' s a
     facet = _Typed
 
+instance AsFacet Void (Which '[]) where
+    facet = prism' absurd impossible
+
+instance AsFacet (Which '[]) Void where
+    facet = prism' impossible absurd
+
+instance AsFacet x x where
+    facet = id
+
 instance UniqueMember x xs => AsFacet x (Which xs) where
     facet = prism' pick trial'
 
@@ -78,11 +88,11 @@
     -- This above causes problems when used monomorphically with @s ~ t@ and @x ~ y@ since
     -- @xs@ cannot equal @ys ~ Remove x x@.
     --
-    -- What is desirec is:
+    -- What is desired is:
     -- (UniqueMember x xs, ys ~ Remove x xs)
     -- => prism_ (pick :: x -> Which xs) (trial :: Which xs -> Either (Which ys) x)
     --
-    -- So we expose the polymorhpic 'matching' explicitly.
+    -- So we expose the polymorphic 'Control.Lens.Prism.matching' explicitly.
     matchingFacet :: s -> Either t a
 
 instance (UniqueMember x xs, ys ~ Remove x xs) => MatchingFacet x (Which xs) (Which ys) where
@@ -109,7 +119,7 @@
   => MatchingFacetL l x (Which xs) (Which ys) where
     matchingFacetL = trialL @l
 
--- | Variation of 'fetchL' specialized to 'Tagged' which automatically tags and untags the field.
+-- | Variation of 'grabL' specialized to 'Tagged' which automatically tags and untags the field.
 -- A default implementation using generics is not provided as it make GHC think that @l@ must be type @Symbol@
 -- when @l@ can actually be any kind.
 -- Create instances of 'AsFacetTag'' using "Data.Generics.Sum.Constructors" as follows:
diff --git a/src/Data/Diverse/Profunctor/Many.hs b/src/Data/Diverse/Profunctor/Many.hs
--- a/src/Data/Diverse/Profunctor/Many.hs
+++ b/src/Data/Diverse/Profunctor/Many.hs
@@ -12,28 +12,30 @@
       -- * Combinators similar to Profunctor Strong
       Itemized
     , itemized
-    , itemized'
+    , itemizedK
     , Projected
     , projected
-    , SelectWith
-    , (*&&*)
-    , ThenSelect
-    , (>&&>)
-    , (<&&<)
+    , projectedK
+    , MakeFrom
+    , MakeBoth
+    , makeBesides
+    , makeBesidesK
+    , thenMake
+    , thenMakeK
     ) where
 
-import qualified Control.Category as C
 import Control.Arrow
+import qualified Control.Category as C
 import Control.Lens
-import Data.Diverse.Many
 import Data.Diverse.Lens.Many
+import Data.Diverse.Many
 import Data.Diverse.TypeLevel
 import Data.Profunctor
 
 -- | A friendlier constraint synonym for 'itemized'.
 type Itemized a b s t =
-    ( HasItem a b s t
-    , HasItem' a s
+    ( HasItem a s
+    , t ~ Replaced a b s
     )
 
 -- | Like 'Strong' or 'Arrow' but lifting into 'Many'
@@ -46,9 +48,14 @@
     => w a b -> w s t
 itemized w = dimap (\c -> (view item' c, c)) (\(b, c) -> set (item @a) b c) (first' w)
 
--- | Like 'Strong' or 'Arrow' but lifting into 'Many' of one type
-itemized' :: Profunctor w => w a b -> w (Many '[a]) (Many '[b])
-itemized' w = dimap fetch single w
+-- | 'itemized' under 'Kleisli'
+itemizedK ::
+    forall m a b s t.
+    ( Monad m
+    , Itemized a b s t
+    )
+    => (a -> m b) -> (s -> m t)
+itemizedK f = runKleisli . itemized $ Kleisli f
 
 -- | A friendlier constraint synonym for 'projected'.
 type Projected a1 a2 b1 b2 =
@@ -58,20 +65,30 @@
     )
 
 -- | Like 'Strong' or 'Arrow' but lifting from a 'Many' to a 'Many' of another type
-projected :: forall proxy w a1 a2 b1 b2.
-    ( Profunctor w
-    , Strong w
+projected :: forall w a1 a2 b1 b2.
+    ( Strong w
     , Projected a1 a2 b1 b2
     )
-    => proxy a2 -> w (Many a1) (Many b1) -> w (Many a2) (Many b2)
-projected _ w = dimap (\c -> (select c, c)) (\(b, c) -> amend @a1 c b) (first' w)
+    => w (Many a1) (Many b1) -> w (Many a2) (Many b2)
+projected w = dimap (\c -> (select c, c)) (\(b, c) -> amend @a1 @b1 @a2 c b) (first' w)
 
+-- | 'projected' under 'Kleisli'
+projectedK :: forall m a1 a2 b1 b2.
+    ( Monad m
+    , Projected a1 a2 b1 b2
+    )
+    => (Many a1 -> m (Many b1)) -> (Many a2 -> m (Many b2))
+projectedK f = runKleisli . projected $ Kleisli f
+
 -- | A friendlier constraint synonym for '*&&*'.
-type SelectWith a1 a2 a3 b1 b2 b3 =
-    ( Select a1 (AppendUnique a1 a2)
-    , Select a2 (AppendUnique a1 a2)
+type MakeBoth b1 b2 b3 =
+    ( b3 ~ Append b1 b2
+    )
+
+type MakeFrom a1 a2 a3 =
+    ( Select a1 a3
+    , Select a2 a3
     , a3 ~ AppendUnique a1 a2
-    , b3 ~ Append b1 b2
     )
 
 -- | Split the input between the two argument arrows and combine their output.
@@ -79,52 +96,66 @@
 -- The type of the resultant output is a concatenated 'Many' of the arguments arrows' outputs.
 -- Analogous to a 'Many' combination of both of 'Control.Arrow.***' and 'Control.Arrow.&&&'.
 -- It is a compile error if the types are not distinct in each of the argument arrow inputs.
-(*&&*)
+makeBesides
     :: forall w a1 a2 a3 b1 b2 b3.
     ( C.Category w
-    , Profunctor w
     , Strong w
-    , SelectWith a1 a2 a3 b1 b2 b3
+    , MakeFrom a1 a2 a3
+    , MakeBoth b1 b2 b3
     )
     => w (Many a1) (Many b1)
     -> w (Many a2) (Many b2)
     -> w (Many a3) (Many b3)
-x *&&* y = rmap (uncurry (/./)) (lmap (select @a1 &&& select @a2) (first' x) C.>>> second' y)
-infixr 3 *&&* -- like ***
+x `makeBesides` y = rmap (uncurry (/./)) (lmap (select @a1 &&& select @a2) (first' x) C.>>> second' y)
+infixr 3 `makeBesides` -- like ***
 
--- | A friendlier constraint synonym for '>&&>'.
-type ThenSelect a2 b1 b2 b3 =
-    ( Select (Complement b1 a2) b1
-    , Select a2 b1
-    , b3 ~ Append (Complement b1 a2) b2
+makeBesidesK
+    :: forall m a1 a2 a3 b1 b2 b3.
+    ( Monad m
+    , MakeFrom a1 a2 a3
+    , MakeBoth b1 b2 b3
     )
+    => (Many a1 -> m (Many b1))
+    -> (Many a2 -> m (Many b2))
+    -> (Many a3 -> m (Many b3))
+makeBesidesK f g = runKleisli $ makeBesides (Kleisli f) (Kleisli g)
+infixr 3 `makeBesidesK` -- like ***
 
 -- | Left-to-right chaining of arrows one after another, where left over input not consumed
 -- by the right arrow is forwarded to the output.
 -- It is a compile error if the types are not distinct in each of the argument arrow inputs,
--- or if the input of the second arrow is not a subset of the output of the first arrow.
-(>&&>)
-    :: forall w a a2 b1 b2 b3.
+-- or if the input of the second arrow is not a complete subset of the output of the first arrow.
+thenMake :: forall w a a2 b1 b2 b3.
     ( C.Category w
-    , Profunctor w
     , Strong w
-    , ThenSelect a2 b1 b2 b3
+    , Projected a2 b1 b2 b3
     )
     => w a (Many b1)
     -> w (Many a2) (Many b2)
     -> w a (Many b3)
-x >&&> y = rmap (uncurry (/./)) (rmap (select @(Complement b1 a2) &&& select @a2) x C.>>> (second' y))
-infixr 3 >&&> -- like ***
+x `thenMake` y = x C.>>> projected y
+infixr 3 `thenMake` -- like ***
 
--- | right-to-left version of '(>&&>)'
-(<&&<) ::
-    ( C.Category w
-    , Profunctor w
-    , Strong w
-    , ThenSelect a2 b1 b2 b3
+thenMakeK :: forall m a a2 b1 b2 b3.
+    ( Monad m
+    , Projected a2 b1 b2 b3
     )
-    => w (Many a2) (Many b2)
-    -> w a (Many b1)
-    -> w a (Many b3)
-(<&&<) = flip (>&&>)
-infixl 2 <&&< -- like >&&>
+    => (a -> m (Many b1))
+    -> (Many a2 -> m (Many b2))
+    -> (a -> m (Many b3))
+thenMakeK f g = runKleisli $ thenMake (Kleisli f) (Kleisli g)
+infixr 3 `thenMakeK` -- like ***
+
+-----
+
+-- type Besides a1 a2 a3 = (a3 ~ Append a1 a2)
+
+-- besides :: (Applicative f, Besides a1 a2 a3)
+--     => f (Many a1) -> f (Many a2) -> f (Many a3)
+-- besides x y = liftA2 (/./) x y
+-- infixr 5 `besides` -- like (/./) and (++)
+
+-- besides2 :: (Biapplicative f, Besides a1 a2 a3, Besides b1 b2 b3)
+--     => f (Many a1) (Many b1) -> f (Many a2) (Many b2) -> f (Many a3) (Many b3)
+-- besides2 x y = biliftA2 (/./) (/./) x y
+-- infixr 5 `besides2` -- like (/./) and (++)
diff --git a/src/Data/Diverse/Profunctor/Which.hs b/src/Data/Diverse/Profunctor/Which.hs
--- a/src/Data/Diverse/Profunctor/Which.hs
+++ b/src/Data/Diverse/Profunctor/Which.hs
@@ -12,20 +12,30 @@
       -- * Combinators similar to Profunctor Choice
       Faceted
     , faceted
-    , faceted'
+    , facetedK
     , Injected
     , injected
-    , ChooseBetween
-    , (+||+)
-    , (>||>)
-    , (<||<)
+    , injectedK
+    , ChooseFrom
+    , ChooseBoth
+    -- , ChooseBetween
+    , chooseBetween
+    , chooseBetweenK
+    , thenChoose
+    , thenChooseK
+    , also
+    , alternatively
+    -- , (+||+)
+    -- , (>||>)
+    -- , (<||<)
     ) where
 
+import Control.Applicative
+import Control.Arrow
 import qualified Control.Category as C
 import Control.Lens
-import Data.Diverse.Which
-import Data.Diverse.TypeLevel
 import Data.Diverse.Lens
+import Data.Semigroup
 
 -- | A friendlier constraint synonym for 'faceted'.
 type Faceted a as x b bs y =
@@ -35,8 +45,7 @@
 
 -- | Like 'Choice' or 'ArrowChoice' but lifting into a polymorphic variant.
 faceted :: forall w a as x b bs y.
-    (Profunctor w
-    , Choice w
+    ( Choice w
     , Faceted a as x b bs y
     )
     => w a b -> w x y
@@ -44,43 +53,75 @@
                    (either id (review facet))
                    (right' w)
 
--- | Like 'Choice' or 'ArrowChoice' but lifting into 'Which' of one type
-faceted' :: (Profunctor w, Choice w) => w a b -> w (Which '[a]) (Which '[b])
-faceted' w = dimap obvious pickOnly w
+-- | 'faceted' under 'Kleisli'
+facetedK :: forall m a as x b bs y.
+    ( Monad m
+    , Faceted a as x b bs y
+    )
+    => (a -> m b) -> (x -> m y)
+facetedK f = runKleisli . faceted $ Kleisli f
 
 -- | A friendlier constraint synonym for 'injected'.
-type Injected a a' b b' =
-    ( Reinterpret a a'
-    , Diversify b (AppendUnique (Complement a' a) b)
-    , Diversify (Complement a' a) (AppendUnique (Complement a' a) b)
-    , b' ~ AppendUnique (Complement a' a) b
+type Injected a2 a3 b2 b3 =
+    ( Reinterpret a2 a3
+    , ChooseBoth (Complement a3 a2) b2 b3
     -- extra contraint to prevent surprises (see comment for 'injected')
-    , Complement a a' ~ '[]
+    , Complement a2 a3 ~ '[]
     )
 
 -- | Like 'Choice' or 'ArrowChoice' but lifting from 'Which' into another type of 'Which'
 -- NB. It is a compile error if all of the input types in the second arrow @a@
 -- is not the output types of the first arrow.
--- This prevents surprising behaviour where the second arrow is ignored.
-injected ::
-    ( Profunctor w
-    , Choice w
-    , Injected a a' b b'
+-- This prevents surprising behaviour where the second arrow is completely ignored.
+injected :: forall w a2 a3 b2 b3.
+    ( Choice w
+    , Injected a2 a3 b2 b3
     )
-    => w (Which a) (Which b)
-    -> w (Which a') (Which b')
-injected w = dimap reinterpret (either diversify diversify) (right' w)
+    => w (Which a2) (Which b2)
+    -> w (Which a3) (Which b3)
+injected w = dimap (reinterpret @a2 @a3) (either diversify diversify) (right' w)
 
--- | A friendlier constraint synonym for '+||+'.
-type ChooseBetween a1 a2 a3 b1 b2 b3 =
-    ( Reinterpret a2 (Append a1 a2)
-    , a1 ~ Complement (Append a1 a2) a2
-    , a3 ~ Append a1 a2
-    , Diversify b1 (AppendUnique b1 b2)
-    , Diversify b2 (AppendUnique b1 b2)
-    , b3 ~ AppendUnique b1 b2
+-- | 'injected' under 'Kleisli'
+injectedK :: forall m a2 a3 b2 b3.
+    ( Monad m
+    , Injected a2 a3 b2 b3
     )
+    => (Which a2 -> m (Which b2))
+    -> (Which a3 -> m (Which b3))
+injectedK f = runKleisli . injected $ Kleisli f
 
+-- | A friendlier constraint synonym for 'chooseBoth'.
+type ChooseBoth b1 b2 b3 =
+    ( Diversify b1 b3
+    , Diversify b2 b3
+    , b3 ~ AppendUnique b1 b2 -- ^ Redundant constraint: but narrows down @b3@
+    )
+
+-- chooseBoth ::
+--     ( C.Category w
+--     , Strong w
+--     , ChooseBoth b1 b2 b3
+--     )
+--     => w a (Which b1)
+--     -> w a (Which b2)
+--     -> w a (Which b3, Which b3)
+-- chooseBoth x y = lmap (\a -> (a, a)) (first' (rmap diversify x)) C.>>> (second' (rmap diversify y))
+-- infixr 2 `chooseBoth` -- like +++
+
+-- | A friendlier constraint synonym for 'chooseFrom'.
+type ChooseFrom a1 a2 a3 =
+    -- ( Reinterpreted a2 a3 a1 -- a1 ~ Complement a3 a2
+    ( Reinterpret a2 a3-- a1 ~ Complement a3 a2
+    , a1 ~ Complement a3 a2
+    , a3 ~ Append a1 a2 -- ^ Redundant constraint: but narrows down @a3@
+    )
+
+-- -- | A friendlier constraint synonym for 'chooseBetween'.
+-- type ChooseBetween a1 a2 a3 b1 b2 b3 =
+--     ( ChooseFrom a1 a2 a3
+--     , ChooseBoth b1 b2 b3
+--     )
+
 -- | Split the input between the two argument arrows, retagging and merging their outputs.
 -- The output is merged into a 'Which' of unique types.
 -- Analogous to a 'Which' combination of both 'Control.Arrow.+++' and 'Control.Arrow.|||'.
@@ -88,31 +129,49 @@
 -- This is to prevent accidently processing an input type twice.
 -- The compile error will be due to @(Append a1 a2)@ which will not satisfy
 -- @UniqueMember@ constraints in 'Reinterpret'.
-(+||+)
-    :: forall w a1 a2 a3 b1 b2 b3.
-       ( C.Category w
-       , Profunctor w
-       , Choice w
-       , ChooseBetween a1 a2 a3 b1 b2 b3
-       )
+chooseBetween :: forall w a1 a2 a3 b1 b2 b3.
+    ( C.Category w
+    , Choice w
+    , ChooseFrom a1 a2 a3
+    , ChooseBoth b1 b2 b3
+    )
     => w (Which a1) (Which b1)
     -> w (Which a2) (Which b2)
     -> w (Which a3) (Which b3)
-x +||+ y =
+x `chooseBetween` y =
     rmap
         (either diversify diversify)
-        (lmap (reinterpret @a2 @(Append a1 a2)) (left' x) C.>>> right' y)
-infixr 2 +||+ -- like +++
+        (lmap (reinterpret @a2 @a3) (left' x) C.>>> right' y)
+infixr 2 `chooseBetween` -- like +++
 
--- | Left-to-right chaining of arrows one after another,  where left over possibilities not handled
+-- | 'chooseBetween' under 'Kleisli'
+chooseBetweenK :: forall m a1 a2 a3 b1 b2 b3.
+    (Monad m, ChooseFrom a1 a2 a3, ChooseBoth b1 b2 b3)
+    => (Which a1 -> m (Which b1))
+    -> (Which a2 -> m (Which b2))
+    -> (Which a3 -> m (Which b3))
+chooseBetweenK f g = runKleisli $ chooseBetween (Kleisli f) (Kleisli g)
+infixr 2 `chooseBetweenK` -- like +++
+
+-- (+||+) ::
+--     ( C.Category w
+--     , Choice w
+--     , ChooseBetween a1 a2 a3 b1 b2 b3
+--     )
+--     => w (Which a1) (Which b1)
+--     -> w (Which a2) (Which b2)
+--     -> w (Which a3) (Which b3)
+-- (+||+) = chooseBetween
+-- infixr 2 +||+ -- like +++
+
+-- | Left-to-right chaining of arrows one after another, where left over possibilities not handled
 -- by the right arrow is forwarded to the output.
 -- It is a compile error if the types are not distinct in each of the argument arrow inputs,
--- or if the types are not distinct of each of the argument arrow output,
--- or if the input of the second arrow is not a subset of the output of the first arrow.
--- This is to prevent surprises behaviour of the second arrow being ignored.
--- The compile error will be due to the @Complement c b ~ '[]@ constraint.
-(>||>)
-    :: forall w a a2 b1 b2 b3.
+-- or if the types are not distinct in each of the argument arrow output.
+-- NB. It is currently not a compile error if the input of the second arrow is distinct from the
+-- output of the first arrrow, in which case this function does not change anything
+-- except to add the types of the second arrow to the output.
+thenChoose :: forall w a a2 b1 b2 b3.
        ( C.Category w
        , Choice w
        , Injected a2 b1 b2 b3
@@ -120,18 +179,38 @@
     => w a (Which b1)
     -> w (Which a2) (Which b2)
     -> w a (Which b3)
-(>||>) hdl1 hdl2 = hdl1 C.>>> injected @_ @_ @b1 hdl2
-infixr 2 >||> -- like +||+
+hdl1 `thenChoose` hdl2 = hdl1 C.>>> injected hdl2
+infixr 2 `thenChoose` -- like +++
 
--- | right-to-left version of '(>||>)'
-(<||<)
-    :: forall w a a2 b1 b2 b3.
-       ( C.Category w
-       , Choice w
-       , Injected a2 b1 b2 b3
-       )
-    => w (Which a2) (Which b2)
-    -> w a (Which b1)
-    -> w a (Which b3)
-(<||<) = flip (>||>)
-infixl 2 <||< -- like >||>
+-- | 'thenChoose' under 'Kleisli'
+thenChooseK :: forall m a a2 b1 b2 b3.
+       (Monad m, Injected a2 b1 b2 b3)
+    => (a -> m (Which b1))
+    -> (Which a2 -> m (Which b2))
+    -> (a -> m (Which b3))
+thenChooseK f g = runKleisli $ thenChoose (Kleisli f) (Kleisli g)
+infixr 2 `thenChooseK` -- like +++
+
+-- -- | right-to-left version of '(>||>)'
+-- (<||<)
+--     :: forall w a a2 b1 b2 b3.
+--        ( C.Category w
+--        , Choice w
+--        , Injected a2 b1 b2 b3
+--        )
+--     => w (Which a2) (Which b2)
+--     -> w a (Which b1)
+--     -> w a (Which b3)
+-- (<||<) = flip (>||>)
+-- infixr 2 <||< -- like >||>
+
+------------------------------------------
+
+also :: (Semigroup (f (Which a3)), Functor f, ChooseBoth a1 a2 a3) => f (Which a1) -> f (Which a2) -> f (Which a3)
+also x y = (diversify <$> x) <> (diversify <$> y)
+infixr 6 `also` -- like mappend
+
+alternatively :: (Alternative f, ChooseBoth a1 a2 a3) => f (Which a1) -> f (Which a2) -> f (Which a3)
+alternatively x y = (diversify <$> x) <|> (diversify <$> y)
+infixl 3 `alternatively` -- like <|>
+