diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,16 @@
 Changelog
 =========
 
+Version 0.2.0.0
+---------------
+
+*August 12, 2019*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.2.0.0>
+
+*   Full restructuring of the Universe system, pulling it all out into a new
+    package, *functor-products*.
+
 Version 0.1.5.0
 ---------------
 
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.0.
+-- This file has been generated from package.yaml by hpack version 0.31.2.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 39c525768bc5e732a9d0d8a6b1931c269a0e4339a68d83434f6b3a4cf3f80c9f
+-- hash: 91c5808428e945b6349291657cb7510e476dba940bd88509714b4178da856af3
 
 name:           decidable
-version:        0.1.5.0
+version:        0.2.0.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,7 +22,7 @@
 copyright:      (c) Justin Le 2018
 license:        BSD3
 license-file:   LICENSE
-tested-with:    GHC >= 8.4 && < 8.8
+tested-with:    GHC >= 8.6
 build-type:     Simple
 extra-source-files:
     README.md
@@ -48,5 +48,8 @@
   ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns
   build-depends:
       base >=4.11 && <5
-    , singletons >=2.4
+    , functor-products
+    , microlens
+    , singletons >=2.5
+    , vinyl
   default-language: Haskell2010
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
@@ -1,8 +1,10 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds     #-}
 {-# LANGUAGE DefaultSignatures   #-}
+{-# LANGUAGE EmptyCase           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE InstanceSigs        #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -27,7 +29,7 @@
     -- * Predicates
     Predicate, Wit(..)
     -- ** Construct Predicates
-  , TyPred, Evident, EqualTo, BoolPred, Impossible
+  , TyPred, Evident, EqualTo, BoolPred, Impossible, In
     -- ** Manipulate predicates
   , PMap, type Not, decideNot
     -- * Provable Predicates
@@ -50,12 +52,17 @@
   , mapRefuted
   ) where
 
+import           Data.Functor.Identity
 import           Data.Kind
+import           Data.List.NonEmpty                    (NonEmpty(..))
 import           Data.Maybe
 import           Data.Singletons
 import           Data.Singletons.Decide
-import           Data.Singletons.Prelude hiding (Not)
+import           Data.Singletons.Prelude hiding        (Not, ElemSym1)
+import           Data.Singletons.Prelude.Identity
+import           Data.Type.Functor.Product
 import           Data.Void
+import qualified Data.Singletons.Prelude.List.NonEmpty as NE
 
 -- | A type-level predicate in Haskell.  We say that the predicate @P ::
 -- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists
@@ -354,6 +361,37 @@
 instance Provable Evident where
     prove = id
 
+-- | @since 2.0.0
+instance Provable (TyPred (Rec Sing)) where
+    prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (Rec Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PMaybe Sing)) where
+    prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PMaybe Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (NERec Sing)) where
+    prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (NERec Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PIdentity Sing)) where
+    prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PIdentity Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PEither Sing)) where
+    prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PEither Sing))
+-- | @since 2.0.0
+instance Provable (TyPred (PTup Sing)) where
+    prove = singProd
+-- | @since 2.0.0
+instance Decidable (TyPred (PTup Sing))
+
 instance (Decidable p, SingI f) => Decidable (PMap f p) where
     decide = decide @p . applySing (sing :: Sing f)
 
@@ -463,3 +501,58 @@
     -> Refuted b
     -> Refuted a
 mapRefuted = flip (.)
+
+-- | @'In' f as@ is a predicate that a given input @a@ is a member of
+-- collection @as@.
+type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
+
+instance (SDecide k, SingI (as :: [k])) => Decidable (In [] as) where
+    decide :: forall a. Sing a -> Decision (Index as a)
+    decide x = go (sing @as)
+      where
+        go :: Sing bs -> Decision (Index bs a)
+        go = \case
+          SNil         -> Disproved $ \case {}
+          y `SCons` ys -> case x %~ y of
+            Proved Refl -> Proved IZ
+            Disproved v -> case go ys of
+              Proved i    -> Proved (IS i)
+              Disproved u -> Disproved $ \case
+                IZ   -> v Refl
+                IS i -> u i
+
+instance (SDecide k, SingI (as :: Maybe k)) => Decidable (In Maybe as) where
+    decide x = case sing @as of
+      SNothing -> Disproved $ \case {}
+      SJust y  -> case x %~ y of
+        Proved Refl -> Proved IJust
+        Disproved v -> Disproved $ \case IJust -> v Refl
+
+instance (SDecide k, SingI (as :: Either j k)) => Decidable (In (Either j) as) where
+    decide x = case sing @as of
+      SLeft _  -> Disproved $ \case {}
+      SRight y -> case x %~ y of
+        Proved Refl -> Proved IRight
+        Disproved v -> Disproved $ \case IRight -> v Refl
+
+instance (SDecide k, SingI (as :: NonEmpty k)) => Decidable (In NonEmpty as) where
+    decide x = case sing @as of
+      y NE.:%| (Sing :: Sing bs) -> case x %~ y of
+        Proved Refl -> Proved NEHead
+        Disproved v -> case decide @(In [] bs) x of
+          Proved i    -> Proved $ NETail i
+          Disproved u -> Disproved $ \case
+            NEHead   -> v Refl
+            NETail i -> u i
+
+instance (SDecide k, SingI (as :: (j, k))) => Decidable (In ((,) j) as) where
+    decide x = case sing @as of
+      STuple2 _ y -> case x %~ y of
+        Proved Refl -> Proved ISnd
+        Disproved v -> Disproved $ \case ISnd -> v Refl
+
+instance (SDecide k, SingI (as :: Identity k)) => Decidable (In Identity as) where
+    decide x = case sing @as of
+      SIdentity y -> case x %~ y of
+        Proved Refl -> Proved IId
+        Disproved v -> Disproved $ \case IId -> v Refl
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
@@ -43,6 +43,7 @@
 import           Data.Singletons
 import           Data.Singletons.Sigma
 import           Data.Type.Equality
+import           Data.Type.Functor.Product
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
 import           Data.Type.Predicate.Param
@@ -167,18 +168,9 @@
 instance AutoElem ((,) j) '(w, a) a where
     autoElem = ISnd
 
--- 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
 
@@ -219,25 +211,12 @@
         NEHead   -> auto @_ @p @a
         NETail i -> runWitAll (autoAll @[] @p @as) i
 
-instance AutoAll f (All g p) ass => AutoAll (f :.: g) p ('Comp ass) where
-    autoAll = WitAll $ \(i :? j) ->
-      runWitAll (runWitAll (autoAll @f @(All g p) @ass) i) j
-
 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
@@ -265,12 +244,6 @@
 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.
 --
@@ -339,3 +312,22 @@
 instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p))) as where
     auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))
          $ auto @_ @(Not (Any f (Found p))) @as
+
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (Rec Sing)) as where
+    auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PMaybe Sing)) as where
+    auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (NERec Sing)) as where
+    auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PEither Sing)) as where
+    auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PTup Sing)) as where
+    auto = singProd sing
+-- | @since 2.0.0
+instance SingI as => Auto (TyPred (PIdentity Sing)) as where
+    auto = singProd sing
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
@@ -208,7 +208,7 @@
 
 -- | We cannot have both @p@ and @'Not' p@.
 --
--- (Renamed in v0.1.4.0; used to be 'excludedMiddle')
+-- (Renamed in v0.1.4.0; used to be @excludedMiddle@)
 --
 -- @since 0.1.4.0
 complementation :: forall p. (p &&& Not p) --> Impossible
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
@@ -44,6 +44,7 @@
 import           Data.Singletons.Decide
 import           Data.Singletons.Prelude.Tuple
 import           Data.Singletons.Sigma
+import           Data.Type.Functor.Product
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
 import           Data.Type.Universe
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
--- a/src/Data/Type/Predicate/Quantification.hs
+++ b/src/Data/Type/Predicate/Quantification.hs
@@ -25,8 +25,6 @@
   , decideAny, idecideAny, decideNone, idecideNone
   -- ** Entailment
   , entailAny, ientailAny, entailAnyF, ientailAnyF
-  -- ** Composition
-  , allComp, compAll
   -- * All
   , All, WitAll(..), NotAll
   -- ** Decision
@@ -34,8 +32,6 @@
   -- ** Entailment
   , entailAll, ientailAll, entailAllF, ientailAllF
   , decideEntailAll, idecideEntailAll
-  -- ** Composition
-  , anyComp, compAny
   -- * Logical interplay
   , allToAny
   , allNotNone, noneAllNot
@@ -45,6 +41,7 @@
 import           Data.Kind
 import           Data.Singletons
 import           Data.Singletons.Decide
+import           Data.Type.Functor.Product
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
 import           Data.Type.Universe
@@ -74,7 +71,7 @@
     => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)        -- ^ implication
     -> Any f p @@ as
     -> Any f q @@ as
-ientailAny f (WitAny i x) = WitAny i (f i (index i sing) x)
+ientailAny f (WitAny i x) = WitAny i (f i (indexSing i sing) x)
 
 -- | If there exists an @a@ s.t. @p a@, and if @p@ implies @q@, then there
 -- must exist an @a@ s.t. @q a@.
@@ -90,7 +87,7 @@
     => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a)      -- ^ implication
     -> All f p @@ as
     -> All f q @@ as
-ientailAll f a = WitAll $ \i -> f i (index i sing) (runWitAll a i)
+ientailAll f a = WitAll $ \i -> f i (indexSing i sing) (runWitAll a i)
 
 -- | If for all @a@ we have @p a@, and if @p@ implies @q@, then for all @a@
 -- we must also have @p a@.
@@ -124,7 +121,7 @@
     => (p --># q) h                                     -- ^ implication in context
     -> (Any f p --># Any f q) h
 entailAnyF f x a = withSingI x $
-    ientailAnyF @f @p @q (\i -> f (index i x)) a
+    ientailAnyF @f @p @q (\i -> f (indexSing i x)) a
 
 -- | 'entailAllF', but providing an 'Elem'.
 ientailAllF
@@ -132,7 +129,9 @@
     => (forall a. Elem f as a -> p @@ a -> h (q @@ a))    -- ^ implication in context
     -> All f p @@ as
     -> h (All f q @@ as)
-ientailAllF f a = igenAllA (\i _ -> f i (runWitAll a i)) sing
+ientailAllF f a = fmap (prodAll getWit)
+                . itraverseProd (\i _ -> Wit @q <$> f i (runWitAll a i))
+                $ singProd (sing @as)
 
 -- | If @p@ implies @q@ under some context @h@, and if we have @p a@ for
 -- all @a@, then we must have @q a@ for all @a@ under context @h@.
@@ -141,7 +140,7 @@
     => (p --># q) h                                     -- ^ implication in context
     -> (All f p --># All f q) h
 entailAllF f x a = withSingI x $
-    ientailAllF @f @p @q (\i -> f (index i x)) a
+    ientailAllF @f @p @q (\i -> f (indexSing i x)) a
 
 -- | 'entailAllF', but providing an 'Elem'.
 idecideEntailAll
@@ -163,7 +162,7 @@
 --
 -- @since 0.1.2.0
 anyImpossible :: Universe f => Any f Impossible --> Impossible
-anyImpossible _ (WitAny i p) = p . index i
+anyImpossible _ (WitAny i p) = p . indexSing i
 
 -- | If any @a@ in @as@ does not satisfy @p@, then not all @a@ in @as@
 -- satisfy @p@.
@@ -182,7 +181,7 @@
     => NotAll f p --> Any f (Not p)
 notAllAnyNot xs vAll = elimDisproof (decide @(Any f (Not p)) xs) $ \vAny ->
     vAll $ WitAll $ \i ->
-      elimDisproof (decide @p (index i xs)) $ \vP ->
+      elimDisproof (decide @p (indexSing i xs)) $ \vP ->
         vAny $ WitAny i vP
 
 -- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies
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,21 +1,21 @@
-{-# 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       #-}
+{-# 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 TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
 
 -- |
 -- Module      : Data.Type.Universe
@@ -32,9 +32,9 @@
 module Data.Type.Universe (
   -- * Universe
     Elem, In, Universe(..)
+  , singAll
   -- ** Instances
-  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IProxy, IIdentity(..)
-  , CompElem(..), SumElem(..)
+  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..), IIdentity(..)
   -- ** Predicates
   , All, WitAll(..), NotAll
   , Any, WitAny(..), None
@@ -42,59 +42,26 @@
   -- *** Specialized
   , IsJust, IsNothing, IsRight, IsLeft
   -- * Decisions and manipulations
-  , decideAny, decideAll, genAllA, genAll, igenAll
-  , foldMapUni, ifoldMapUni, index, pickElem
-  -- * Universe Combination
-  -- ** 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
-  -- * Singletons
-  , SIndex(..), SIJust(..), SIRight(..), SNEIndex(..), SISnd(..), SIProxy, SIIdentity(..)
-  , Sing (SComp, SInL, SIndex', SIJust', SIRight', SNEIndex', SISnd', SIProxy', SIIdentity')
+  , decideAny, decideAll
+  , genAll, igenAll
+  , splitSing
+  , pickElem
   ) where
 
-import           Control.Applicative
 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)
+import           Data.Singletons.Prelude.Identity
+import           Data.Type.Functor.Product
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
-import           Data.Typeable                         (Typeable)
-import           GHC.Generics                          (Generic)
+import           GHC.Generics                          ((:*:)(..))
 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
-
-data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
-data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
-type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
-
-type instance Apply (ElemSym0 f) as = ElemSym1 f as
-type instance Apply (ElemSym1 f as) a = Elem f as a
-
--- | @'In' f as@ is a predicate that a given input @a@ is a member of
--- collection @as@.
-type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
-
 -- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the
 -- type-level collection @as@, the predicate @p a@ is true.
 data WitAny f :: (k ~> Type) -> f k -> Type where
@@ -135,20 +102,21 @@
     prove _ (WitAny i s) = WitAny i (prove @p s)
 
 instance (Universe f, Provable p) => Provable (All f p) where
-    prove xs = WitAll $ \i -> prove @p (index i xs)
+    prove xs = WitAll $ \i -> prove @p (indexSing i xs)
 
 instance Universe f => TFunctor (Any f) where
-    tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)
+    tmap f xs (WitAny i x) = WitAny i (f (indexSing i xs) x)
 
 instance Universe f => TFunctor (All f) where
-    tmap f xs a = WitAll $ \i -> f (index i xs) (runWitAll a i)
+    tmap f xs a = WitAll $ \i -> f (indexSing i xs) (runWitAll a i)
 
 instance Universe f => DFunctor (All f) where
     dmap f xs a = idecideAll (\i x -> f x (runWitAll a i)) xs
 
 -- | Typeclass for a type-level container that you can quantify or lift
 -- type-level predicates over.
-class Universe (f :: Type -> Type) where
+class FProd f => Universe (f :: Type -> Type) where
+
     -- | 'decideAny', but providing an 'Elem'.
     idecideAny
         :: forall k (p :: k ~> Type) (as :: f k). ()
@@ -161,12 +129,17 @@
         => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value
         -> (Sing as -> Decision (All f p @@ as))                         -- ^ predicate on collection
 
-    -- | 'genAllA', but providing an 'Elem'.
-    igenAllA
-        :: forall k (p :: k ~> Type) (as :: f k) h. Applicative h
-        => (forall a. Elem f as a -> Sing a -> h (p @@ a))        -- ^ predicate on value in context
-        -> (Sing as -> h (All f p @@ as))                              -- ^ predicate on collection in context
+    allProd
+        :: forall p g. ()
+        => (forall a. Sing a -> p @@ a -> g a)
+        -> All f p --> TyPred (Prod f g)
 
+    prodAll
+        :: forall p g as. ()
+        => (forall a. g a -> p @@ a)
+        -> Prod f g as
+        -> All f p @@ as
+
 -- | Predicate that a given @as :: f k@ is empty and has no items in it.
 type Null    f = (None f Evident :: Predicate (f k))
 
@@ -210,28 +183,28 @@
     -> Decide (All f p)                -- ^ predicate on collection
 decideAll f = idecideAll (const f)
 
--- | If @p a@ is true for all values @a@ in @as@ under some
--- (Applicative) context @h@, then you can create an @'All' p as@ under
--- that Applicative context @h@.
---
--- Can be useful with 'Identity' (which is basically unwrapping and
--- wrapping 'All'), or with 'Maybe' (which can express predicates that
--- are either provably true or not provably false).
---
--- In practice, this can be used to iterate and traverse and sequence
--- actions over all "items" in @as@.
-genAllA
-    :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
-    => (forall a. Sing a -> h (p @@ a))        -- ^ predicate on value in context
-    -> (Sing as -> h (All f p @@ as))               -- ^ predicate on collection in context
-genAllA f = igenAllA (const f)
+-- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
+splitSing
+    :: forall f k (as :: f k). Universe f
+    => Sing as
+    -> All f (TyPred Sing) @@ as
+splitSing = prodAll id . singProd
 
+-- | Automatically generate a witness for a member, if possible
+pickElem
+    :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)
+    => Decision (Elem f as a)
+pickElem = mapDecision (\case WitAny i Refl -> i)
+                       (\case i -> WitAny i Refl)
+         . decide @(Any f (TyPred ((:~:) a)))
+         $ sing
+
 -- | 'genAll', but providing an 'Elem'.
 igenAll
     :: forall f k (p :: k ~> Type) (as :: f k). Universe f
     => (forall a. Elem f as a -> Sing a -> p @@ a)            -- ^ always-true predicate on value
     -> (Sing as -> All f p @@ as)                                  -- ^ always-true predicate on collection
-igenAll f = runIdentity . igenAllA (\i -> Identity . f i)
+igenAll f = prodAll (\(i :*: x) -> f i x) . imapProd (:*:) . singProd
 
 -- | If @p a@ is true for all values @a@ in @as@, then we have @'All'
 -- p as@.  Basically witnesses the definition of 'All'.
@@ -239,110 +212,36 @@
     :: forall f k (p :: k ~> Type). Universe f
     => Prove p                 -- ^ always-true predicate on value
     -> Prove (All f p)         -- ^ always-true predicate on collection
-genAll f = igenAll (const f)
-
--- | Extract the item from the container witnessed by the 'Elem'
-index
-    :: forall f as a. Universe f
-    => Elem f as a        -- ^ Witness
-    -> Sing as            -- ^ Collection
-    -> Sing a
-index i = (`runWitAll` i) . splitSing
+genAll f = prodAll f . singProd
 
 -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
-splitSing
+singAll
     :: forall f k (as :: f k). Universe f
     => Sing as
-    -> All f (TyPred Sing) @@ as
-splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)
-
--- | Automatically generate a witness for a member, if possible
-pickElem
-    :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)
-    => Decision (Elem f as a)
-pickElem = mapDecision (\case WitAny i Refl -> i)
-                       (\case i -> WitAny i Refl)
-         . decide @(Any f (TyPred ((:~:) a)))
-         $ sing
-
--- | 'foldMapUni' but with access to the index.
-ifoldMapUni
-    :: forall f k (as :: f k) m. (Universe f, Monoid m)
-    => (forall a. Elem f as a -> Sing a -> m)
-    -> Sing as
-    -> m
-ifoldMapUni f = getConst . igenAllA (\i -> Const . f i)
-
--- | A 'foldMap' over all items in a collection.
-foldMapUni
-    :: forall f k (as :: f k) m. (Universe f, Monoid m)
-    => (forall (a :: k). Sing a -> m)
-    -> Sing as
-    -> m
-foldMapUni f = ifoldMapUni (const f)
+    -> All f Evident @@ as
+singAll = prodAll id . singProd
 
--- | Witness an item in a type-level list by providing its index.
-data Index :: [k] -> k -> Type where
-    IZ :: Index (a ': as) a
-    IS :: Index bs a -> Index (b ': bs) a
+-- | Test that a 'Maybe' is 'Just'.
+--
+-- @since 0.1.2.0
+type IsJust    = (NotNull Maybe :: Predicate (Maybe k))
 
-deriving instance Show (Index as a)
-instance (SingI (as :: [k]), SDecide k) => Decidable (TyPred (Index as)) where
-    decide x = withSingI x $ pickElem
+-- | Test that a 'Maybe' is 'Nothing'.
+--
+-- @since 0.1.2.0
+type IsNothing = (Null    Maybe :: Predicate (Maybe k))
 
-type instance Elem [] = Index
+-- | Test that an 'Either' is 'Right'
+--
+-- @since 0.1.2.0
+type IsRight = (NotNull (Either j) :: Predicate (Either j k))
 
--- | Kind-indexed singleton for 'Index'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper 'SIndex'',
--- which has an actual proper 'Sing' instance.
+-- | Test that an 'Either' is 'Left'
 --
--- @since 0.1.5.0
-data SIndex as a :: Index as a -> Type where
-    SIZ :: SIndex (a ': as) a 'IZ
-    SIS :: SIndex bs a i -> SIndex (b ': bs) a ('IS i)
+-- @since 0.1.2.0
+type IsLeft  = (Null    (Either j) :: Predicate (Either j k))
 
-deriving instance Show (SIndex as a i)
 
-newtype instance Sing (i :: Index as a) where
-    SIndex' :: SIndex as a i -> Sing i
-
-instance SingI 'IZ where
-    sing = SIndex' SIZ
-
-instance SingI i => SingI ('IS i) where
-    sing = case sing of
-      SIndex' i -> SIndex' (SIS i)
-
-instance SingKind (Index as a) where
-    type Demote (Index as a) = Index as a
-    fromSing (SIndex' i) = go i
-      where
-        go :: SIndex bs b i -> Index bs b
-        go = \case
-          SIZ   -> IZ
-          SIS j -> IS (go j)
-    toSing i = go i (SomeSing . SIndex')
-      where
-        go :: Index bs b -> (forall i. SIndex bs b i -> r) -> r
-        go = \case
-          IZ   -> ($ SIZ)
-          IS j -> \f -> go j (f . SIS)
-
-instance SDecide (Index as a) where
-    SIndex' i %~ SIndex' j = go i j
-      where
-        go :: SIndex bs b i -> SIndex bs b j -> Decision (i :~: j)
-        go = \case
-          SIZ -> \case
-            SIZ   -> Proved Refl
-            SIS _ -> Disproved $ \case {}
-          SIS i' -> \case
-            SIZ   -> Disproved $ \case {}
-            SIS j' -> case go i' j' of
-              Proved Refl -> Proved Refl
-              Disproved v -> Disproved $ \case Refl -> v Refl
-
 instance Universe [] where
     idecideAny
         :: forall k (p :: k ~> Type) (as :: [k]). ()
@@ -375,65 +274,31 @@
           Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)
         Disproved v -> Disproved $ \a -> v $ runWitAll a IZ
 
-    igenAllA
-        :: forall k (p :: k ~> Type) (as :: [k]) h. Applicative h
-        => (forall a. Elem [] as a -> Sing a -> h (p @@ a))
-        -> Sing as
-        -> h (All [] p @@ as)
-    igenAllA f = \case
-        SNil         -> pure $ WitAll $ \case {}
-        x `SCons` xs -> go <$> f IZ x <*> igenAllA (f . IS) xs
+    allProd
+        :: forall p g. ()
+        => (forall a. Sing a -> p @@ a -> g a)
+        -> All [] p --> TyPred (Prod [] g)
+    allProd f = go
       where
-        go :: p @@ b -> All [] p @@ bs -> All [] p @@ (b ': bs)
-        go p a = WitAll $ \case
-          IZ   -> p
-          IS i -> runWitAll a i
-
--- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
--- 'Just'.
-data IJust :: Maybe k -> k -> Type where
-    IJust :: IJust ('Just a) a
-
-deriving instance Show (IJust as a)
-instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where
-    decide x = withSingI x $ pickElem
-
--- | Kind-indexed singleton for 'IJust'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper 'SIJust'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIJust as a :: IJust as a -> Type where
-    SIJust :: SIJust ('Just a) a 'IJust
-
-deriving instance Show (SIJust as a i)
-
-newtype instance Sing (i :: IJust as a) where
-    SIJust' :: SIJust as a i -> Sing i
-
-instance SingI 'IJust where
-    sing = SIJust' SIJust
-
-instance SingKind (IJust as a) where
-    type Demote (IJust as a) = IJust as a
-    fromSing (SIJust' SIJust) = IJust
-    toSing IJust = SomeSing (SIJust' SIJust)
-
-instance SDecide (IJust as a) where
-    SIJust' SIJust %~ SIJust' SIJust = Proved Refl
-
-type instance Elem Maybe = IJust
-
--- | Test that a 'Maybe' is 'Just'.
---
--- @since 0.1.2.0
-type IsJust    = (NotNull Maybe :: Predicate (Maybe k))
+        go :: Sing as -> WitAll [] p as -> Prod [] g as
+        go = \case
+          SNil         -> \_ -> RNil
+          x `SCons` xs -> \a -> f x (runWitAll a IZ)
+                             :& go xs (WitAll (runWitAll a . IS))
 
--- | Test that a 'Maybe' is 'Nothing'.
---
--- @since 0.1.2.0
-type IsNothing = (Null    Maybe :: Predicate (Maybe k))
+    prodAll
+        :: forall p g as. ()
+        => (forall a. g a -> p @@ a)
+        -> Prod [] g as
+        -> All [] p @@ as
+    prodAll f = go
+      where
+        go :: Prod [] g bs -> All [] p @@ bs
+        go = \case
+          RNil    -> WitAll $ \case {}
+          x :& xs -> WitAll $ \case
+            IZ   -> f x
+            IS i -> runWitAll (go xs) i
 
 instance Universe Maybe where
     idecideAny f = \case
@@ -442,62 +307,17 @@
         Proved p    -> Proved $ WitAny IJust p
         Disproved v -> Disproved $ \case
           WitAny IJust p -> v p
-
     idecideAll f = \case
       SNothing -> Proved $ WitAll $ \case {}
       SJust x  -> case f IJust x of
         Proved p    -> Proved $ WitAll $ \case IJust -> p
         Disproved v -> Disproved $ \a -> v $ runWitAll a IJust
-
-    igenAllA f = \case
-      SNothing -> pure $ WitAll $ \case {}
-      SJust x  -> (\p -> WitAll $ \case IJust -> p) <$> f IJust x
-
--- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
--- is 'Right'.
-data IRight :: Either j k -> k -> Type where
-    IRight :: IRight ('Right a) a
-
-deriving instance Show (IRight as a)
-instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where
-    decide x = withSingI x $ pickElem
-
--- | Kind-indexed singleton for 'IRight'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper 'SIRight'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIRight as a :: IRight as a -> Type where
-    SIRight :: SIRight ('Right a) a 'IRight
-
-deriving instance Show (SIRight as a i)
-
-newtype instance Sing (i :: IRight as a) where
-    SIRight' :: SIRight as a i -> Sing i
-
-instance SingI 'IRight where
-    sing = SIRight' SIRight
-
-instance SingKind (IRight as a) where
-    type Demote (IRight as a) = IRight as a
-    fromSing (SIRight' SIRight) = IRight
-    toSing IRight = SomeSing (SIRight' SIRight)
-
-instance SDecide (IRight as a) where
-    SIRight' SIRight %~ SIRight' SIRight = Proved Refl
-
-type instance Elem (Either j) = IRight
-
--- | Test that an 'Either' is 'Right'
---
--- @since 0.1.2.0
-type IsRight = (NotNull (Either j) :: Predicate (Either j k))
-
--- | Test that an 'Either' is 'Left'
---
--- @since 0.1.2.0
-type IsLeft  = (Null    (Either j) :: Predicate (Either j k))
+    allProd f = \case
+      SNothing -> \_ -> PNothing
+      SJust x  -> \a -> PJust (f x (runWitAll a IJust))
+    prodAll f = \case
+      PNothing -> WitAll $ \case {}
+      PJust x  -> WitAll $ \case IJust -> f x
 
 instance Universe (Either j) where
     idecideAny f = \case
@@ -506,71 +326,17 @@
         Proved p    -> Proved $ WitAny IRight p
         Disproved v -> Disproved $ \case
           WitAny IRight p -> v p
-
     idecideAll f = \case
       SLeft  _ -> Proved $ WitAll $ \case {}
       SRight x -> case f IRight x of
         Proved p    -> Proved $ WitAll $ \case IRight -> p
         Disproved v -> Disproved $ \a -> v $ runWitAll a IRight
-
-    igenAllA f = \case
-      SLeft  _ -> pure $ WitAll $ \case {}
-      SRight x -> (\p -> WitAll $ \case IRight -> p) <$> f IRight x
-
--- | Witness an item in a type-level 'NonEmpty' by either indicating that
--- it is the "head", or by providing an index in the "tail".
-data NEIndex :: NonEmpty k -> k -> Type where
-    NEHead :: NEIndex (a ':| as) a
-    NETail :: Index as a -> NEIndex (b ':| as) a
-
-deriving instance Show (NEIndex as a)
-instance (SingI (as :: NonEmpty k), SDecide k) => Decidable (TyPred (NEIndex as)) where
-    decide x = withSingI x $ pickElem
-
--- | Kind-indexed singleton for 'NEIndex'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper
--- 'SNEIndex'', which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SNEIndex as a :: NEIndex as a -> Type where
-    SNEHead :: SNEIndex (a ':| as) a 'NEHead
-    SNETail :: SIndex as a i -> SNEIndex (b ':| as) a ('NETail i)
-
-deriving instance Show (SNEIndex as a i)
-
-newtype instance Sing (i :: NEIndex as a) where
-    SNEIndex' :: SNEIndex as a i -> Sing i
-
-instance SingI 'NEHead where
-    sing = SNEIndex' SNEHead
-
-instance SingI i => SingI ('NETail i) where
-    sing = case sing of
-      SIndex' i -> SNEIndex' (SNETail i)
-
-instance SingKind (NEIndex as a) where
-    type Demote (NEIndex as a) = NEIndex as a
-    fromSing = \case
-      SNEIndex' SNEHead     -> NEHead
-      SNEIndex' (SNETail i) -> NETail $ fromSing (SIndex' i)
-    toSing = \case
-      NEHead   -> SomeSing (SNEIndex' SNEHead)
-      NETail i -> withSomeSing i $ \case
-        SIndex' j -> SomeSing (SNEIndex' (SNETail j))
-
-instance SDecide (NEIndex as a) where
-    (%~) = \case
-      SNEIndex' SNEHead -> \case
-        SNEIndex' SNEHead     -> Proved Refl
-        SNEIndex' (SNETail _) -> Disproved $ \case {}
-      SNEIndex' (SNETail i) -> \case
-        SNEIndex' SNEHead -> Disproved $ \case {}
-        SNEIndex' (SNETail j) -> case SIndex' i %~ SIndex' j of
-          Proved Refl -> Proved Refl
-          Disproved v -> Disproved $ \case Refl -> v Refl
-
-type instance Elem NonEmpty = NEIndex
+    allProd f = \case
+      SLeft  w -> \_ -> PLeft w
+      SRight x -> \a -> PRight (f x (runWitAll a IRight))
+    prodAll f = \case
+      PLeft _  -> WitAll $ \case {}
+      PRight x -> WitAll $ \case IRight -> f x
 
 instance Universe NonEmpty where
     idecideAny
@@ -600,369 +366,41 @@
         Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)
       Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead
 
-    igenAllA
-        :: forall k (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h
-        => (forall a. Elem NonEmpty as a -> Sing a -> h (p @@ a))
-        -> Sing as
-        -> h (All NonEmpty p @@ as)
-    igenAllA f (x NE.:%| xs) = go <$> f NEHead x <*> igenAllA @[] @_ @p (f . NETail) xs
-      where
-        go :: p @@ b -> All [] p @@ bs -> All NonEmpty p @@ (b ':| bs)
-        go p ps = WitAll $ \case
-          NEHead   -> p
-          NETail i -> runWitAll ps i
-
--- | Trivially witness an item in the second field of a type-level tuple.
-data ISnd :: (j, k) -> k -> Type where
-    ISnd :: ISnd '(a, b) b
-
-deriving instance Show (ISnd as a)
--- TODO: does this interfere with NonNull stuff?
-instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where
-    decide x = withSingI x $ pickElem
-
--- | Kind-indexed singleton for 'ISnd'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper 'SISnd'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SISnd as a :: ISnd as a -> Type where
-    SISnd :: SISnd '(a, b) b 'ISnd
-
-deriving instance Show (SISnd as a i)
-
-newtype instance Sing (i :: ISnd as a) where
-    SISnd' :: SISnd as a i -> Sing i
-
-instance SingI 'ISnd where
-    sing = SISnd' SISnd
-
-instance SingKind (ISnd as a) where
-    type Demote (ISnd as a) = ISnd as a
-    fromSing (SISnd' SISnd) = ISnd
-    toSing ISnd = SomeSing (SISnd' SISnd)
-
-instance SDecide (ISnd as a) where
-    SISnd' SISnd %~ SISnd' SISnd = Proved Refl
-
-type instance Elem ((,) j) = ISnd
+    allProd
+        :: forall p g. ()
+        => (forall a. Sing a -> p @@ a -> g a)
+        -> All NonEmpty p --> TyPred (Prod NonEmpty g)
+    allProd f (x NE.:%| xs) a =
+          f x (runWitAll a NEHead)
+      :&| allProd @[] @p f xs (WitAll (runWitAll a . NETail))
+    prodAll
+        :: forall p g as. ()
+        => (forall a. g a -> p @@ a)
+        -> Prod NonEmpty g as
+        -> All NonEmpty p @@ as
+    prodAll f (x :&| xs) = WitAll $ \case
+        NEHead   -> f x
+        NETail i -> runWitAll (prodAll @[] @p f xs) i
 
 instance Universe ((,) j) where
     idecideAny f (STuple2 _ x) = case f ISnd x of
       Proved p    -> Proved $ WitAny ISnd p
       Disproved v -> Disproved $ \case WitAny ISnd p -> v p
-
     idecideAll f (STuple2 _ x) = case f ISnd x of
       Proved p    -> Proved $ WitAll $ \case ISnd -> p
       Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd
-
-    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 {}
-
--- | Kind-indexed singleton for 'IProxy'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper 'SIProxy'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIProxy as a :: IProxy as a -> Type
-
-deriving instance Show (SIProxy as a i)
-
-newtype instance Sing (i :: IProxy as a) where
-    SIProxy' :: SIProxy as a i -> Sing i
-
-instance SingKind (IProxy as a) where
-    type Demote (IProxy as a) = IProxy as a
-    fromSing (SIProxy' i) = case i of {}
-    toSing = \case {}
-
-instance SDecide (IProxy as a) where
-    SIProxy' i %~ SIProxy' _ = Proved $ case i of {}
-
-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
-
--- | Kind-indexed singleton for 'IIdentity'.  Provided as a separate data
--- declaration to allow you to use these at the type level.  However, the
--- main interface is still provided through the newtype wrapper 'SIIdentity'',
--- which has an actual proper 'Sing' instance.
---
--- @since 0.1.5.0
-data SIIdentity as a :: IIdentity as a -> Type where
-    SIId :: SIIdentity ('Identity a) a 'IId
-
-deriving instance Show (SIIdentity as a i)
-
-newtype instance Sing (i :: IIdentity as a) where
-    SIIdentity' :: SIIdentity as a i -> Sing i
-
-instance SingI 'IId where
-    sing = SIIdentity' SIId
-
-instance SingKind (IIdentity as a) where
-    type Demote (IIdentity as a) = IIdentity as a
-    fromSing (SIIdentity' SIId) = IId
-    toSing IId = SomeSing (SIIdentity' SIId)
-
-instance SDecide (IIdentity as a) where
-    SIIdentity' SIId %~ SIIdentity' SIId = Proved Refl
-
-type instance Elem Identity = IIdentity
+    allProd f (STuple2 w x) a = PTup w $ f x (runWitAll a ISnd)
+    prodAll f (PTup _ x) = WitAll $ \case ISnd -> f x
 
--- | The single-pointed universe.  Note that this instance is really only
--- usable in /singletons-2.5/ and higher (so GHC 8.6).
+-- | The single-pointed universe.
 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
--- 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', 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)
-deriving instance (Traversable f, Traversable g) => Traversable (f :.: g)
-
-data instance Sing (k :: (f :.: g) a) where
-    SComp :: Sing x -> Sing ('Comp x)
-
--- | 'getComp' lifted to the type level
---
--- @since 0.1.2.0
-type family GetComp c where
-    GetComp ('Comp a) = a
-
--- | Singletonized witness for 'GetComp'
---
--- @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
-
-data GetCompSym0 :: (f :.: g) k ~> f (g k)
-type instance Apply GetCompSym0 ('Comp ass) = ass
-type GetCompSym1 a = GetComp a
-
--- instance forall f g a f' g' a'. (SingKind (f (g a)), Demote (f (g a)) ~ f' (g' a')) => SingKind ((f :.: g) a) where
---     type Demote ((f :.: g) a) = (:.:) f' g' a'
-
--- | A pair of indices allows you to index into a nested structure.
---
--- @since 0.1.2.0
-data CompElem :: (f :.: g) k -> k -> Type where
-    (:?) :: Elem f ass as
-         -> Elem g as  a
-         -> CompElem ('Comp ass) a
-
--- deriving instance ((forall as. Show (Elem f ass as)), (forall as. Show (Elem g as a)))
---     => Show (CompElem ('Comp ass :: (f :.: g) k) a)
-
-type instance Elem (f :.: g) = CompElem
-
-instance (Universe f, Universe g) => Universe (f :.: g) where
-    idecideAny
-        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
-        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
-        -> Sing ass
-        -> Decision (Any (f :.: g) p @@ ass)
-    idecideAny f (SComp xss)
-        = mapDecision anyComp compAny
-        . idecideAny @f @_ @(Any g p) go
-        $ xss
-      where
-        go  :: Elem f (GetComp ass) as
-            -> Sing as
-            -> Decision (Any g p @@ as)
-        go i = idecideAny $ \j -> f (i :? j)
-
-    idecideAll
-        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
-        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
-        -> Sing ass
-        -> Decision (All (f :.: g) p @@ ass)
-    idecideAll f (SComp xss)
-        = mapDecision allComp compAll
-        . idecideAll @f @_ @(All g p) go
-        $ xss
-      where
-        go  :: Elem f (GetComp ass) as
-            -> Sing as
-            -> Decision (All g p @@ as)
-        go i = idecideAll $ \j -> f (i :? j)
-
-    igenAllA
-        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k) h. Applicative h
-        => (forall a. Elem (f :.: g) ass a -> Sing a -> h (p @@ a))
-        -> Sing ass
-        -> h (All (f :.: g) p @@ ass)
-    igenAllA f (SComp ass) = allComp <$> igenAllA @f @_ @(All g p) go ass
-      where
-        go  :: Elem f (GetComp ass) (as :: g k)
-            -> Sing as
-            -> h (All g p @@ as)
-        go i = igenAllA $ \j -> f (i :? j)
-
--- | Turn a composition of 'Any' into an 'Any' of a composition.
---
--- @since 0.1.2.0
-anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
-anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p
-
--- | Turn an 'Any' of a composition into a composition of 'Any'.
---
--- @since 0.1.2.0
-compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
-compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)
-
--- | Turn a composition of 'All' into an 'All' of a composition.
---
--- @since 0.1.2.0
-allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
-allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j
-
--- | Turn an 'All' of a composition into a composition of 'All'.
---
--- @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
+    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
+    allProd f (SIdentity x) a = PIdentity $ f x (runWitAll a IId)
+    prodAll f (PIdentity x) = WitAll $ \case IId -> f x
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
@@ -37,6 +37,7 @@
 import           Data.Monoid                        (Alt(..))
 import           Data.Singletons
 import           Data.Singletons.Decide
+import           Data.Type.Functor.Product
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
 import           Data.Type.Predicate.Quantification
@@ -63,7 +64,7 @@
     => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))
     -> Sing as
     -> Subset f p @@ as
-makeSubset f xs = WitSubset $ \i -> f i (index i xs)
+makeSubset f xs = WitSubset $ \i -> f i (indexSing i xs)
 
 -- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
 -- predicates.
@@ -72,7 +73,7 @@
 subsetToList
     :: forall f p t. (Universe f, Alternative t)
     => (Subset f p --># Any f p) t
-subsetToList xs s = getAlt $ (`ifoldMapUni` xs) $ \i _ -> Alt $ case runWitSubset s i of
+subsetToList xs s = getAlt $ (`ifoldMapSing` xs) $ \i _ -> Alt $ case runWitSubset s i of
     Proved p    -> pure $ WitAny i p
     Disproved _ -> empty
 
@@ -158,5 +159,5 @@
     -> (q --> p)
     -> (Subset f p --> Subset f q)
 mapSubset f g xs = withSingI xs $
-    imapSubset (\i -> f (index i xs))
-               (\i -> g (index i xs))
+    imapSubset (\i -> f (indexSing i xs))
+               (\i -> g (indexSing i xs))