diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,19 @@
 Changelog
 =========
 
+Version 0.1.3.0
+---------------
+
+*October 24, 2018*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.3.0>
+
+*   Added a type and `Universe` for universe disjunction or summing, `:+:`,
+    with appropriate `Elem` and `Auto` instances.
+*   Added `Universe` instances (and appropriate `Elem` and `Auto` instances)
+    for `Proxy` (the null universe) and `Identity`.
+*   `Auto` instances for `IsNothing` and `IsLeft`.
+
 Version 0.1.2.0
 ---------------
 
@@ -25,7 +38,7 @@
     module documentation for a detailed list of new rules and classes in this
     version.
 *   Convenient combinators for dealing with `Refuted` and `Decision` added to
-    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted.
+    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted`.
 
 
 Version 0.1.1.0
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -1,11 +1,13 @@
--- This file has been generated from package.yaml by hpack version 0.28.2.
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 81cda78c02736265f023817475cdcf593f3a1cd1d8601f09bf92e4719d064fc1
+-- hash: 5deeebc3dd1fcd483724e8469079eba0875cd3698198d81352d5b3bd6c2696ef
 
 name:           decidable
-version:        0.1.2.0
+version:        0.1.3.0
 synopsis:       Combinators for manipulating dependently-typed predicates.
 description:    This library provides combinators and typeclasses for working and manipulating
                 type-level predicates in Haskell, which are represented as matchable type-level
@@ -22,10 +24,9 @@
 license-file:   LICENSE
 tested-with:    GHC >= 8.4 && < 8.8
 build-type:     Simple
-cabal-version:  >= 1.10
 extra-source-files:
-    CHANGELOG.md
     README.md
+    CHANGELOG.md
 
 source-repository head
   type: git
@@ -44,7 +45,7 @@
       Paths_decidable
   hs-source-dirs:
       src
-  ghc-options: -Wall -Wredundant-constraints -Wcompat
+  ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns
   build-depends:
       base >=4.11 && <5
     , singletons >=2.4
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
--- a/src/Data/Type/Predicate.hs
+++ b/src/Data/Type/Predicate.hs
@@ -132,9 +132,17 @@
 --
 -- Could also be defined as @'ConstSym1' Void@, but this defintion gives
 -- us a free 'Decidable' instance.
+--
+-- @
+-- 'Impossible' :: 'Predicate' k
+-- @
 type Impossible = (Not Evident :: Predicate k)
 
 -- | @'EqualTo' a@ is a predicate that the input is equal to @a@.
+--
+-- @
+-- 'EqualTo' :: k -> 'Predicate' k
+-- @
 type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
 
 -- | Convert a tradtional @k ~> 'Bool'@ predicate into a 'Predicate'.
@@ -142,7 +150,7 @@
 -- @
 -- 'BoolPred' :: (k ~> Bool) -> Predicate k
 -- @
-type BoolPred (p :: k ~> Bool) = (EqualTo 'True .@#@$$$ p :: Predicate k)
+type BoolPred (p :: k ~> Bool) = (PMap p (EqualTo 'True) :: Predicate k)
 
 -- | Pre-compose a function to a predicate
 --
@@ -271,6 +279,9 @@
 -- 'Type'@ instead of matchable type-level functions (that are @k ~>
 -- 'Type'@).
 --
+-- Mostly is in this library for compatiblity with "traditional" predicates
+-- that are GADT type constructors.
+--
 -- @since 0.1.1.0
 type DecidableTC p = Decidable (TyPred p)
 
@@ -291,6 +302,9 @@
 -- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@
 -- instead of matchable type-level functions (that are @k ~> 'Type'@).
 --
+-- Mostly is in this library for compatiblity with "traditional" predicates
+-- that are GADT type constructors.
+--
 -- @since 0.1.1.0
 type ProvableTC  p = Provable  (TyPred p)
 
@@ -318,10 +332,10 @@
     prove = id
 
 instance (Decidable p, SingI f) => Decidable (PMap f p) where
-    decide = decide @p . ((sing :: Sing f) @@)
+    decide = decide @p . applySing (sing :: Sing f)
 
 instance (Provable p, SingI f) => Provable (PMap f p) where
-    prove = prove @p . ((sing :: Sing f) @@)
+    prove = prove @p . applySing (sing :: Sing f)
 
 -- | Compose two implications.
 compImpl
diff --git a/src/Data/Type/Predicate/Auto.hs b/src/Data/Type/Predicate/Auto.hs
--- a/src/Data/Type/Predicate/Auto.hs
+++ b/src/Data/Type/Predicate/Auto.hs
@@ -38,6 +38,7 @@
   , autoAny, autoNotAll
   ) where
 
+import           Data.Functor.Identity
 import           Data.List.NonEmpty                 (NonEmpty(..))
 import           Data.Singletons
 import           Data.Singletons.Sigma
@@ -169,6 +170,15 @@
 -- TODO: ???
 -- instance AutoElem (f :.: g) p ('Comp ass) where
 
+instance AutoElem Identity ('Identity a) a where
+    autoElem = IId
+
+instance AutoElem f as a => AutoElem (f :+: g) ('InL as) a where
+    autoElem = IInL autoElem
+
+instance AutoElem g bs b => AutoElem (f :+: g) ('InR bs) b where
+    autoElem = IInR autoElem
+
 instance AutoElem f as a => Auto (In f as) a where
     auto = autoElem @f @as @a
 
@@ -216,6 +226,18 @@
 instance Auto p a => AutoAll ((,) j) p '(w, a) where
     autoAll = WitAll $ \case ISnd -> auto @_ @p @a
 
+instance AutoAll Proxy p 'Proxy where
+    autoAll = WitAll $ \case {}
+
+instance Auto p a => AutoAll Identity p ('Identity a) where
+    autoAll = WitAll $ \case IId -> auto @_ @p @a
+
+instance AutoAll f p as => AutoAll (f :+: g) p ('InL as) where
+    autoAll = allSumL $ autoAll @f @p @as
+
+instance AutoAll g p bs => AutoAll (f :+: g) p ('InR bs) where
+    autoAll = allSumR $ autoAll @g @p @bs
+
 -- | @since 0.1.2.0
 instance AutoAll f p as => Auto (All f p) as where
     auto = autoAll @f @p @as
@@ -228,10 +250,18 @@
 instance SingI a => Auto IsJust ('Just a) where
     auto = WitAny IJust sing
 
+-- | @since 0.1.3.0
+instance Auto IsNothing 'Nothing where
+    auto = \case WitAny i _ -> case i of {}
+
 -- | @since 0.1.2.0
 instance SingI a => Auto IsRight ('Right a) where
     auto = WitAny IRight sing
 
+-- | @since 0.1.3.0
+instance Auto IsLeft ('Left a) where
+    auto = \case WitAny i _ -> case i of {}
+
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where
     auto = WitAny NEHead sing
@@ -239,6 +269,18 @@
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
     auto = WitAny ISnd sing
+
+instance Auto (Null Proxy) 'Proxy where
+    auto = \case WitAny i _ -> case i of {}
+
+instance SingI a => Auto (NotNull Identity) ('Identity a) where
+    auto = WitAny IId sing
+
+instance Auto (NotNull f) as => Auto (NotNull (f :+: g)) ('InL as) where
+    auto = anySumL $ auto @_ @(NotNull f) @as
+
+instance Auto (NotNull g) bs => Auto (NotNull (f :+: g)) ('InR bs) where
+    auto = anySumR $ auto @_ @(NotNull g) @bs
 
 -- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to not be
 -- true at compiletime.
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
--- a/src/Data/Type/Predicate/Logic.hs
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -71,10 +71,13 @@
 type instance Apply (p ||| q) a = Either (p @@ a) (q @@ a)
 infixr 2 |||
 
+-- | Prefers @p@ over @q@.
 instance (Decidable p, Decidable q) => Decidable (p ||| q) where
     decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)
 
 -- | Decide @p '|||' q@ based on decisions of @p@ and @q@.
+--
+-- Prefers @p@ over @q@.
 decideOr
     :: forall p q a. ()
     => Decision (p @@ a)
@@ -86,10 +89,14 @@
 
 -- | Left-biased "or".  In proofs, prioritize a proof of the left side over
 -- a proof of the right side.
+--
+-- @since 0.1.2.0
 type p ^|| q = p ||| Not p &&& q
 
 -- | Right-biased "or".  In proofs, prioritize a proof of the right side over
 -- a proof of the left side.
+--
+-- @since 0.1.2.0
 type p ||^ q = p &&& Not q ||| q
 
 -- | @p '^^^' q@ is a predicate that either @p@ and @q@ are true, but not
@@ -202,11 +209,9 @@
 excludedMiddle :: (p &&& Not p) --> Impossible
 excludedMiddle _ (p, notP) _ = notP p
 
--- | If only this worked, but darn overlapping instances.  Same for p ==>
--- p ||| q and p &&& q ==> p :(
--- q) ==>
--- instance Provable (p &&& Not p ==> Impossible) where
---     prove = excludedMiddle @p
+-- | @since 0.1.3.0
+instance {-# OVERLAPPING #-} Provable (p &&& Not p ==> Impossible) where
+    prove = excludedMiddle @p
 
 -- | If p implies q, then not q implies not p.
 contrapositive
diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs
--- a/src/Data/Type/Predicate/Param.hs
+++ b/src/Data/Type/Predicate/Param.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE ConstraintKinds      #-}
 {-# LANGUAGE FlexibleContexts     #-}
 {-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
 {-# LANGUAGE LambdaCase           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE TypeApplications     #-}
@@ -30,9 +31,12 @@
   , Selectable, select
   , Searchable, search
   , inPNotNull, notNullInP
+  -- * Combining
+  , OrP, AndP
   ) where
 
 import           Data.Singletons
+import           Data.Singletons.Prelude.Tuple
 import           Data.Singletons.Sigma
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
@@ -192,3 +196,40 @@
     decide = mapDecision (\case WitAny i (x :&: p) -> x :&: WitAny i p  )
                          (\case x :&: WitAny i p   -> WitAny i (x :&: p))
            . decide @(Any f (Found p))
+
+-- | Disjunction on two 'ParamPred's, with appropriate 'Searchable'
+-- instance.  Priority is given to the left predicate.
+--
+-- @since 0.1.3.0
+data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v
+type instance Apply (OrP p q x) y = (p x ||| q x) @@ y
+
+-- | Conjunction on two 'ParamPred's, with appropriate 'Searchable' and
+-- 'Selectable' instances.
+--
+-- @since 0.1.3.0
+data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u)
+type instance Apply (AndP p q x) '(y, z) = (p x @@ y, q x @@ z)
+
+instance (Searchable p, Searchable q) => Decidable (Found (OrP p q)) where
+    decide x = case search @p x of
+      Proved (s :&: p) -> Proved $ s :&: Left p
+      Disproved vp     -> case search @q x of
+        Proved (s :&: q) -> Proved $ s :&: Right q
+        Disproved vq     -> Disproved $ \case
+          s :&: Left  p -> vp (s :&: p)
+          s :&: Right q -> vq (s :&: q)
+
+instance (Searchable p, Searchable q) => Decidable (Found (AndP p q)) where
+    decide x = case search @p x of
+      Proved (s :&: p) -> case search @q x of
+        Proved (t :&: q) -> Proved $ STuple2 s t :&: (p, q)
+        Disproved vq     -> Disproved $ \case
+          STuple2 _ t :&: (_, q) -> vq $ t :&: q
+      Disproved vp     -> Disproved $ \case
+        STuple2 s _ :&: (p, _) -> vp $ s :&: p
+
+instance (Selectable p, Selectable q) => Provable (Found (AndP p q)) where
+    prove x = case select @p x of
+        s :&: p -> case select @q x of
+          t :&: q -> STuple2 s t :&: (p, q)
diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs
--- a/src/Data/Type/Universe.hs
+++ b/src/Data/Type/Universe.hs
@@ -1,20 +1,21 @@
-{-# LANGUAGE DeriveDataTypeable   #-}
-{-# LANGUAGE DeriveFunctor        #-}
-{-# LANGUAGE DeriveGeneric        #-}
-{-# LANGUAGE DeriveTraversable    #-}
-{-# LANGUAGE EmptyCase            #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE GADTs                #-}
-{-# LANGUAGE InstanceSigs         #-}
-{-# LANGUAGE LambdaCase           #-}
-{-# LANGUAGE RankNTypes           #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE StandaloneDeriving   #-}
-{-# LANGUAGE TemplateHaskell      #-}
-{-# LANGUAGE TypeApplications     #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE DeriveFunctor       #-}
+{-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE DeriveTraversable   #-}
+{-# LANGUAGE EmptyCase           #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE InstanceSigs        #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeInType          #-}
+{-# LANGUAGE TypeOperators       #-}
 
 -- |
 -- Module      : Data.Type.Universe
@@ -25,15 +26,15 @@
 -- Stability   : experimental
 -- Portability : non-portable
 --
--- Combinators for working with type-level predicates, along with
--- typeclasses for canonical proofs and deciding functions.
+-- A type family for "containers", intended for allowing lifting of
+-- predicates on @k@ to be predicates on containers @f k@.
 --
 module Data.Type.Universe (
   -- * Universe
     Elem, In, Universe(..)
   -- ** Instances
-  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..)
-  , CompElem(..)
+  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)
+  , CompElem(..), SumElem(..)
   -- ** Predicates
   , All, WitAll(..), NotAll
   , Any, WitAny(..), None
@@ -43,9 +44,15 @@
   -- * Decisions and manipulations
   , decideAny, decideAll, genAllA, genAll, igenAll
   , foldMapUni, ifoldMapUni, index, pickElem
-  -- * Universe Composition
-  , (:.:)(..), Sing(SComp), sGetComp, GetComp
+  -- * Universe Combination
+  , Sing (SComp, SInL, SInR)
+  -- ** Universe Composition
+  , (:.:)(..), sGetComp, GetComp
   , allComp, compAll, anyComp, compAny
+  -- ** Universe Disjunction
+  , (:+:)(..)
+  , anySumL, anySumR, sumLAny, sumRAny
+  , allSumL, allSumR, sumLAll, sumRAll
   -- * Defunctionalization symbols
   , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1
   ) where
@@ -54,6 +61,7 @@
 import           Data.Functor.Identity
 import           Data.Kind
 import           Data.List.NonEmpty                    (NonEmpty(..))
+import           Data.Proxy
 import           Data.Singletons
 import           Data.Singletons.Decide
 import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not)
@@ -64,6 +72,13 @@
 import           Prelude hiding                        (any, all)
 import qualified Data.Singletons.Prelude.List.NonEmpty as NE
 
+#if MIN_VERSION_singletons(2,5,0)
+import           Data.Singletons.Prelude.Identity
+#else
+import           Data.Singletons.TH
+genSingletons [''Identity]
+#endif
+
 -- | A witness for membership of a given item in a type-level collection
 type family Elem (f :: Type -> Type) :: f k -> k -> Type
 
@@ -89,7 +104,7 @@
 --
 -- This is mostly useful for its 'Decidable' and 'TFunctor' instances,
 -- which lets you lift predicates on @p@ to predicates on @'Any' f p@.
-data Any f :: (k ~> Type) -> (f k ~> Type)
+data Any f :: Predicate k -> Predicate (f k)
 type instance Apply (Any f p) as = WitAny f p as
 
 -- | A @'WitAll' p as@ is a witness that the predicate @p a@ is true for all
@@ -103,7 +118,7 @@
 -- This is mostly useful for its 'Decidable', 'Provable', and 'TFunctor'
 -- instances, which lets you lift predicates on @p@ to predicates on @'All'
 -- f p@.
-data All f :: (k ~> Type) -> (f k ~> Type)
+data All f :: Predicate k -> Predicate (f k)
 type instance Apply (All f p) as = WitAll f p as
 
 instance (Universe f, Decidable p) => Decidable (Any f p) where
@@ -473,6 +488,49 @@
 
     igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x
 
+-- | There are no items of type @a@ in a @'Proxy' a@.
+--
+-- @since 0.1.3.0
+data IProxy :: Proxy k -> k -> Type
+
+deriving instance Show (IProxy 'Proxy a)
+
+instance Provable (Not (TyPred (IProxy 'Proxy))) where
+    prove _ = \case {}
+
+type instance Elem Proxy = IProxy
+
+-- | The null universe
+instance Universe Proxy where
+    idecideAny _ _ = Disproved $ \case
+        WitAny i _ -> case i of {}
+    idecideAll _ _ = Proved $ WitAll $ \case {}
+    igenAllA   _ _ = pure $ WitAll $ \case {}
+
+-- | Trivially witness the item held in an 'Identity'.
+--
+-- @since 0.1.3.0
+data IIdentity :: Identity k -> k -> Type where
+    IId :: IIdentity ('Identity x) x
+
+deriving instance Show (IIdentity as a)
+
+instance (SingI (as :: Identity k), SDecide k) => Decidable (TyPred (IIdentity as)) where
+    decide x = withSingI x $ pickElem
+
+type instance Elem Identity = IIdentity
+
+-- | The single-pointed universe.  Note that this instance is really only
+-- usable in /singletons-2.5/ and higher (so GHC 8.6).
+instance Universe Identity where
+    idecideAny f (SIdentity x) = mapDecision (WitAny IId)
+                                             (\case WitAny IId p -> p)
+                               $ f IId x
+    idecideAll f (SIdentity x) = mapDecision (\p -> WitAll $ \case IId -> p)
+                                             (`runWitAll` IId)
+                               $ f IId x
+    igenAllA f (SIdentity x) = (\p -> WitAll $ \case IId -> p) <$> f IId x
+
 -- | Compose two Functors.  Is the same as 'Data.Functor.Compose.Compose'
 -- and 'GHC.Generics.:.:', except with a singleton and meant to be used at
 -- the type level.  Will be redundant if either of the above gets brought
@@ -482,6 +540,8 @@
 -- 'SingKind'  instance; if you need 'fromSing' and 'toSing', try going
 -- through 'Comp' and 'getComp' and 'SComp' and 'sGetComp'.
 --
+-- Note that 'Identity' acts as an identity.
+--
 -- @since 0.1.2.0
 data (f :.: g) a = Comp { getComp :: f (g a) }
     deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
@@ -501,7 +561,7 @@
 -- @since 0.1.2.0
 sGetComp :: Sing a -> Sing (GetComp a)
 sGetComp (SComp x) = x
- 
+
 instance SingI ass => SingI ('Comp ass) where
     sing = SComp sing
 
@@ -591,3 +651,101 @@
 -- @since 0.1.2.0
 compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
 compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)
+
+-- | Disjoint union of two Functors.  Is the same as 'Data.Functor.Sum.Sum'
+-- and 'GHC.Generics.:+:', except with a singleton and meant to be used at
+-- the type level.  Will be redundant if either of the above gets brought
+-- into the singletons library.
+--
+-- Note that because this is a higher-kinded data constructor, there is no
+-- 'SingKind'  instance; if you need 'fromSing' and 'toSing', consider
+-- manually pattern matching.
+--
+-- Note that 'Proxy' acts as an identity.
+--
+-- @since 0.1.3.0
+data (f :+: g) a = InL (f a)
+                 | InR (g a)
+    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
+deriving instance (Traversable f, Traversable g) => Traversable (f :+: g)
+
+data instance Sing (k :: (f :+: g) a) where
+    SInL :: Sing x -> Sing ('InL x)
+    SInR :: Sing y -> Sing ('InR y)
+
+type family FromL s where
+    FromL ('InL a) = a
+
+-- | Index into a disjoint union by providing an index into one of the two
+-- possible options.
+--
+-- @since 0.1.3.0
+data SumElem :: (f :+: g) k -> k -> Type where
+    IInL :: Elem f as a -> SumElem ('InL as) a
+    IInR :: Elem f bs b -> SumElem ('InR bs) b
+
+type instance Elem (f :+: g) = SumElem
+
+instance (Universe f, Universe g) => Universe (f :+: g) where
+    idecideAny
+        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()
+        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))
+        -> Sing abs
+        -> Decision (Any (f :+: g) p @@ abs)
+    idecideAny f = \case
+      SInL xs -> mapDecision anySumL sumLAny
+               $ idecideAny @f @_ @p (f . IInL) xs
+      SInR ys -> mapDecision anySumR sumRAny
+               $ idecideAny @g @_ @p (f . IInR) ys
+
+    idecideAll
+        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k). ()
+        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> Decision (p @@ ab))
+        -> Sing abs
+        -> Decision (All (f :+: g) p @@ abs)
+    idecideAll f = \case
+      SInL xs -> mapDecision allSumL sumLAll
+               $ idecideAll @f @_ @p (f . IInL) xs
+      SInR xs -> mapDecision allSumR sumRAll
+               $ idecideAll @g @_ @p (f . IInR) xs
+
+    igenAllA
+        :: forall k (p :: k ~> Type) (abs :: (f :+: g) k) h. Applicative h
+        => (forall ab. Elem (f :+: g) abs ab -> Sing ab -> h (p @@ ab))
+        -> Sing abs
+        -> h (All (f :+: g) p @@ abs)
+    igenAllA f = \case
+      SInL xs -> allSumL <$> igenAllA @f @_ @p (f . IInL) xs
+      SInR xs -> allSumR <$> igenAllA @g @_ @p (f . IInR) xs
+
+-- | Turn an 'Any' of @f@ into an 'Any' of @f ':+:' g@.
+anySumL :: Any f p @@ as -> Any (f :+: g) p @@ 'InL as
+anySumL (WitAny i x) = WitAny (IInL i) x
+
+-- | Turn an 'Any' of @g@ into an 'Any' of @f ':+:' g@.
+anySumR :: Any g p @@ bs -> Any (f :+: g) p @@ 'InR bs
+anySumR (WitAny j y) = WitAny (IInR j) y
+
+-- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @f@.
+sumLAny :: Any (f :+: g) p @@ 'InL as -> Any f p @@ as
+sumLAny (WitAny (IInL i) x) = WitAny i x
+
+-- | Turn an 'Any' of @f ':+:' g@ into an 'Any' of @g@.
+sumRAny :: Any (f :+: g) p @@ 'InR bs -> Any g p @@ bs
+sumRAny (WitAny (IInR j) y) = WitAny j y
+
+-- | Turn an 'All' of @f@ into an 'All' of @f ':+:' g@.
+allSumL :: All f p @@ as -> All (f :+: g) p @@ 'InL as
+allSumL a = WitAll $ \case IInL i -> runWitAll a i
+
+-- | Turn an 'All' of @g@ into an 'All' of @f ':+:' g@.
+allSumR :: All g p @@ bs -> All (f :+: g) p @@ 'InR bs
+allSumR a = WitAll $ \case IInR j -> runWitAll a j
+
+-- | Turn an 'All' of @f ':+:' g@ into an 'All' of @f@.
+sumLAll :: All (f :+: g) p @@ 'InL as -> All f p @@ as
+sumLAll a = WitAll $ runWitAll a . IInL
+
+-- | Turn an 'All' of @f ':+:' g@ into an 'All' of @g@.
+sumRAll :: All (f :+: g) p @@ 'InR bs -> All g p @@ bs
+sumRAll a = WitAll $ runWitAll a . IInR
diff --git a/src/Data/Type/Universe/Subset.hs b/src/Data/Type/Universe/Subset.hs
--- a/src/Data/Type/Universe/Subset.hs
+++ b/src/Data/Type/Universe/Subset.hs
@@ -120,7 +120,7 @@
     => ((Subset f p &&& Subset f q) --> Subset f (p &&& q))
 intersection _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideAnd @p @q @a
 
--- | Subset union
+-- | Subset union (left-biased)
 union
     :: forall f p q. ()
     => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))