diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,12 @@
+Changelog
+=========
+
+Version 0.1.0.0
+---------------
+
+*October 10, 2018*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.0.0>
+
+*   Initial release.
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Justin Le (c) 2018
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Justin Le nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,11 @@
+# [decidable][]
+
+[![decidable on Hackage](https://img.shields.io/hackage/v/decidable.svg?maxAge=86400)](https://hackage.haskell.org/package/decidable)
+[![Build Status](https://travis-ci.org/mstksg/decidable.svg?branch=master)](https://travis-ci.org/mstksg/decidable)
+[decidable]: https://mstksg.github.io/decidable/
+
+This library provides combinators and typeclasses for working and manipulating
+type-level predicates in Haskell, which are represented as matchable type-level
+functions `k ~> Type` from the *singletons* library.  See *Data.Type.Predicate*
+for a good starting point.
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/decidable.cabal b/decidable.cabal
new file mode 100644
--- /dev/null
+++ b/decidable.cabal
@@ -0,0 +1,46 @@
+-- This file has been generated from package.yaml by hpack version 0.28.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: fa635fe6f55a295cab015d273dc723b843bac34ddd35415b9495c1c9306ba671
+
+name:           decidable
+version:        0.1.0.0
+synopsis:       Combinators for manipulating dependently-typed predicates.
+description:    Please see the README on GitHub at <https://github.com/mstksg/decidable#readme>
+category:       Dependent Types
+homepage:       https://github.com/mstksg/decidable#readme
+bug-reports:    https://github.com/mstksg/decidable/issues
+author:         Justin Le
+maintainer:     justin@jle.im
+copyright:      (c) Justin Le 2018
+license:        BSD3
+license-file:   LICENSE
+tested-with:    GHC >= 8.4 && < 8.8
+build-type:     Simple
+cabal-version:  >= 1.10
+extra-source-files:
+    CHANGELOG.md
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/mstksg/decidable
+
+library
+  exposed-modules:
+      Data.Type.Predicate
+      Data.Type.Predicate.Logic
+      Data.Type.Predicate.Param
+      Data.Type.Predicate.Quantification
+      Data.Type.Universe
+      Data.Type.Universe.Subset
+  other-modules:
+      Paths_decidable
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wredundant-constraints
+  build-depends:
+      base >=4.11 && <5
+    , singletons >=2.4
+  default-language: Haskell2010
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Predicate.hs
@@ -0,0 +1,314 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE EmptyCase              #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE LambdaCase             #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TemplateHaskell        #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+
+-- |
+-- Module      : Data.Type.Predicate
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Combinators for working with type-level predicates, along with
+-- typeclasses for canonical proofs and deciding functions.
+--
+module Data.Type.Predicate (
+    -- * Predicates
+    Predicate, Wit(..)
+    -- ** Construct Predicates
+  , TyPred, Evident, EqualTo, BoolPred, Impossible
+    -- ** Manipulate predicates
+  , PMap, type Not, decideNot
+    -- * Provable Predicates
+  , Prove, type (-->), type (-->#)
+  , Provable(..)
+  , Disprovable, disprove
+  , TFunctor(..)
+  , compImpl
+    -- * Decidable Predicates
+  , Decide, type (-?>), type (-?>#)
+  , Decidable(..)
+  , DFunctor(..)
+  , mapDecision
+  ) where
+
+import           Data.Kind
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Singletons.Prelude hiding (Not)
+import           Data.Void
+
+-- | A type-level predicate in Haskell.  We say that the predicate @P ::
+-- 'Predicate' k@ is true/satisfied by input @x :: k@ if there exists
+-- a value of type @P \@\@ x@, and that it false/disproved if such a value
+-- cannot exist. (Where '@@' is 'Apply', the singleton library's type-level
+-- function application for mathcable functions)
+--
+-- See 'Provable' and 'Decidable' for more information on how to use, prove
+-- and decide these predicates.
+--
+-- The kind @k ~> 'Type'@ is the kind of "matchable" type-level functions
+-- in Haskell.  They are type-level functions that are encoded as dummy
+-- type constructors ("defunctionalization symbols") that can be decidedly
+-- "matched" on for things like typeclass instances.
+--
+-- There are two ways to define your own predicates:
+--
+--     1. Using the predicate combinators and predicate transformers in
+--     this library and the /singletons/ library, which let you construct
+--     pre-made predicates and sometimes create predicates from other
+--     predicates.
+--
+--     2. Manually creating a data type that acts as a matchable predicate.
+--
+-- For an example of the latter, we can create the "not p" predicate, which
+-- takes a predicate @p@ as input and returns the negation of the
+-- predicate:
+--
+-- @
+-- -- First, create the data type with the kind signature you want
+-- data Not :: Predicate k -> Predicate k
+--
+-- -- Then, write the 'Apply' instance, to specify the type of the
+-- -- witnesses of that predicate
+-- instance 'Apply' (Not p) a = (p '@@' a) -> Void
+-- @
+--
+-- See the source of "Data.Type.Predicate" and "Data.Type.Predicate.Logic"
+-- for simple examples of hand-made predicates.  For example, we have the
+-- always-true predicate 'Evident':
+--
+-- @
+-- data Evident :: Predicate k
+-- instance Apply Evident a = Sing a
+-- @
+--
+-- And the "and" predicate combinator:
+--
+-- @
+-- data (&&&) :: Predicate k -> Predicate k -> Predicate k
+-- instance Apply (p &&& q) a = (p '@@' a, q '@@' a)
+-- @
+--
+-- Typically it is recommended to create predicates from the supplied
+-- predicate combinators ('TyPred' can be used for any type constructor to
+-- turn it into a predicate, for instance) whenever possible.
+type Predicate k = k ~> Type
+
+-- | Convert a normal '->' type constructor into a 'Predicate'.
+--
+-- @
+-- 'TyPred' :: (k -> 'Type') -> 'Predicate' k
+-- @
+type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
+
+-- | The always-true predicate.
+--
+-- @
+-- 'Evident' :: 'Predicate' k
+-- @
+type Evident = (TyPred Sing :: Predicate k)
+
+-- | The always-false predicate
+--
+-- Could also be defined as @'ConstSym1' Void@, but this defintion gives
+-- us a free 'Decidable' instance.
+type Impossible = (Not Evident :: Predicate k)
+
+-- | @'EqualTo' a@ is a predicate that the input is equal to @a@.
+type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
+
+-- | Convert a tradtional @k ~> 'Bool'@ predicate into a 'Predicate'.
+--
+-- @
+-- 'BoolPred' :: (k ~> Bool) -> Predicate k
+-- @
+type BoolPred (p :: k ~> Bool) = (EqualTo 'True .@#@$$$ p :: Predicate k)
+
+-- | Pre-compose a function to a predicate
+--
+-- @
+-- 'PMap' :: (k ~> j) -> 'Predicate' j -> Predicate k
+-- @
+type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)
+
+-- | A @'Wit' p a@ is a value of type @p \@\@ a@ --- that is, it is a proof
+-- or witness that @p@ is satisfied for @a@.
+newtype Wit p a = Wit { getWit :: p @@ a }
+
+-- | A decision function for predicate @p@.  See 'Decidable' for more
+-- information.
+type Decide p = forall a. Sing a -> Decision (p @@ a)
+
+-- | Like implication '-->', but knowing @p \@\@ a@ can only let us decidably
+-- prove @q @@ a@ is true or false.
+type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
+
+-- | Like '-?>', but only in a specific context @h@.
+type (p -?># q) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
+
+-- | A proving function for predicate @p@.  See 'Provable' for more
+-- information.
+type Prove p = forall a. Sing a -> p @@ a
+
+-- | We say that @p@ implies @q@ (@p '-->' q@) if, given @p @@ a@, we can
+-- always prove @q \@\@ a@.
+type p --> q = forall a. Sing a -> p @@ a -> q @@ a
+
+-- | This is implication '-->#', but only in a specific context @h@.
+type (p --># q) h = forall a. Sing a -> p @@ a -> h (q @@ a)
+
+infixr 1 -?>
+infixr 1 -?>#
+infixr 1 -->
+infixr 1 -->#
+
+-- | A typeclass for decidable predicates.
+--
+-- A predicate is decidable if, given any input @a@, you can either prove
+-- or disprove @p \@\@ a@.  A @'Decision' (p \@\@ a)@ is a data type
+-- that has a branch @p \@\@ a@ and @'Refuted' (p \@\@ a)@.
+--
+-- This typeclass associates a canonical decision function for every
+-- decidable predicate.
+--
+-- It confers two main advatnages:
+--
+--     1. The decision function for every predicate is available via the
+--     same name
+--
+--     2. We can write 'Decidable' instances for polymorphic predicate
+--     transformers (predicates parameterized on other predicates) easily,
+--     by refering to 'Decidable' instances of the transformed predicates.
+class Decidable p where
+    -- | The canonical decision function for predicate @p@.
+    --
+    -- Note that 'decide' is ambiguously typed, so you /always/ need to call by
+    -- specifying the predicate you want to prove using TypeApplications
+    -- syntax:
+    --
+    -- @
+    -- 'decide' \@MyPredicate
+    -- @
+    decide :: Decide p
+
+    default decide :: Provable p => Decide p
+    decide = Proved . prove @p
+
+-- | A typeclass for provable predicates (constructivist tautologies).
+--
+-- A predicate is provable if, given any input @a@, you can generate
+-- a proof of @p \@\@ a@.  Essentially, it means that a predicate is "always
+-- true".
+--
+-- This typeclass associates a canonical proof function for every provable
+-- predicate.
+--
+-- It confers two main advatnages:
+--
+--     1. The proof function for every predicate is available via the same
+--     name
+--
+--     2. We can write 'Provable' instances for polymorphic predicate
+--     transformers (predicates parameterized on other predicates) easily,
+--     by refering to 'Provable' instances of the transformed predicates.
+class Provable p where
+    -- | The canonical proving function for predicate @p@.
+    --
+    -- Note that 'prove' is ambiguously typed, so you /always/ need to call
+    -- by specifying the predicate you want to prove using TypeApplications
+    -- syntax:
+    --
+    -- @
+    -- 'prove' \@MyPredicate
+    -- @
+    prove :: Prove p
+
+-- | @'Disprovable' p@ is a constraint that @p@ can be disproven.
+type Disprovable p = Provable (Not p)
+
+-- | The deciding/disproving function for @'Disprovable' p@.
+--
+-- Must be called by applying the 'Predicate' to disprove:
+--
+-- @
+-- 'disprove' \@p
+-- @
+disprove :: forall p. Disprovable p => Prove (Not p)
+disprove = prove @(Not p)
+
+-- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an
+-- @f p '-?>' f q@.
+class DFunctor f where
+    dmap :: forall p q. (p -?> q) -> (f p -?> f q)
+
+-- | Implicatons @p '-->' q@ can be lifted "through" a 'TFunctor' into an
+-- @f p '-->' f q@.
+class TFunctor f where
+    tmap :: forall p q. (p --> q) -> (f p --> f q)
+
+instance (SDecide k, SingI (a :: k)) => Decidable (EqualTo a) where
+    decide = (sing %~)
+
+instance Decidable Evident
+instance Provable Evident where
+    prove = id
+
+instance (Decidable f, SingI g) => Decidable (f .@#@$$$ g) where
+    decide = decide @f . ((sing :: Sing g) @@)
+
+instance (Provable f, SingI g) => Provable (f .@#@$$$ g) where
+    prove = prove @f . ((sing :: Sing g) @@)
+
+-- | Compose two implications.
+compImpl
+    :: forall p q r. ()
+    => p --> q
+    -> q --> r
+    -> p --> r
+compImpl f g s = g s . f s
+
+-- | @'Not' p@ is the predicate that @p@ is not true.
+data Not :: Predicate k -> Predicate k
+type instance Apply (Not p) a = Refuted (p @@ a)
+
+instance Decidable p => Decidable (Not p) where
+    decide (x :: Sing a) = decideNot @p @a (decide @p x)
+
+instance Provable (Not Impossible) where
+    prove x v = absurd $ v x
+
+-- | Decide @Not p@ based on decisions of @p@.
+decideNot
+    :: forall p a. ()
+    => Decision (p @@ a)
+    -> Decision (Not p @@ a)
+decideNot = \case
+    Proved p    -> Disproved ($ p)
+    Disproved v -> Proved v
+
+-- | Map over the value inside a 'Decision'.
+mapDecision
+    :: (a -> b)
+    -> (b -> a)
+    -> Decision a
+    -> Decision b
+mapDecision f g = \case
+    Proved    p -> Proved $ f p
+    Disproved v -> Disproved $ v . g
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -0,0 +1,224 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE EmptyCase           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeInType          #-}
+{-# LANGUAGE TypeOperators       #-}
+
+-- |
+-- Module      : Data.Type.Predicate.Logic
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Logical and algebraic connectives for predicates, as well as common
+-- logical combinators.
+module Data.Type.Predicate.Logic (
+  -- * Top and bottom
+    Evident, Impossible
+  -- * Logical connectives
+  , type Not, decideNot
+  , type (&&&), decideAnd
+  , type (|||), decideOr, type (^||), type (||^)
+  , type (^^^), decideXor
+  , type (==>), proveImplies, Implies
+  , type (<==>), Equiv
+  -- * Logical deductions
+  , compImpl, explosion, atom, excludedMiddle, doubleNegation
+  , contrapositive, contrapositive'
+  -- ** Lattice
+  , projAndFst, projAndSnd, injOrLeft, injOrRight
+  ) where
+
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Singletons.Prelude.Bool (Sing(..))
+import           Data.Type.Predicate
+import           Data.Void
+
+-- | @p '&&&' q@ is a predicate that both @p@ and @q@ are true.
+data (&&&) :: Predicate k -> Predicate k -> Predicate k
+type instance Apply (p &&& q) a = (p @@ a, q @@ a)
+infixr 3 &&&
+
+instance (Decidable p, Decidable q) => Decidable (p &&& q) where
+    decide (x :: Sing a) = decideAnd @p @q @a (decide @p x) (decide @q x)
+
+instance (Provable p, Provable q) => Provable (p &&& q) where
+    prove x = (prove @p x, prove @q x)
+
+-- | Decide @p '&&&' q@ based on decisions of @p@ and @q@.
+decideAnd
+    :: forall p q a. ()
+    => Decision (p @@ a)
+    -> Decision (q @@ a)
+    -> Decision ((p &&& q) @@ a)
+decideAnd = \case
+    Proved p    -> \case
+      Proved q    -> Proved (p, q)
+      Disproved v -> Disproved $ \(_, q) -> v q
+    Disproved v -> \_ -> Disproved $ \(p, _) -> v p
+
+-- | @p '|||' q@ is a predicate that either @p@ and @q@ are true.
+data (|||) :: Predicate k -> Predicate k -> Predicate k
+type instance Apply (p ||| q) a = Either (p @@ a) (q @@ a)
+infixr 2 |||
+
+instance (Decidable p, Decidable q) => Decidable (p ||| q) where
+    decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)
+
+-- | Picks the proof of @p@.  Note that this is instance has stronger
+-- constraints than is strictly necessary; we should really only have to
+-- require that either @p@ or @q@ is true.
+instance Provable p => Provable (p ||| q) where
+    prove x = Left (prove @p x)
+
+-- | Decide @p '|||' q@ based on decisions of @p@ and @q@.
+decideOr
+    :: forall p q a. ()
+    => Decision (p @@ a)
+    -> Decision (q @@ a)
+    -> Decision ((p ||| q) @@ a)
+decideOr = \case
+    Proved p    -> \_ -> Proved $ Left p
+    Disproved v -> \case
+      Proved q    -> Proved $ Right q
+      Disproved w -> Disproved $ \case
+        Left p  -> v p
+        Right q -> w q
+
+-- | Left-biased "or".  In proofs, prioritize a proof of the left side over
+-- a proof of the right side.
+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.
+type p ||^ q = p &&& Not q ||| q
+
+-- | @p '^^^' q@ is a predicate that either @p@ and @q@ are true, but not
+-- both.
+type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)
+
+-- | Decide @p '^^^' q@ based on decisions of @p@ and @q@.
+decideXor
+    :: forall p q a. ()
+    => Decision (p @@ a)
+    -> Decision (q @@ a)
+    -> Decision ((p ^^^ q) @@ a)
+decideXor p q = decideOr @(p &&& Not q) @(Not p &&& q) @a
+                  (decideAnd @p @(Not q) @a p (decideNot @q @a q))
+                  (decideAnd @(Not p) @q @a (decideNot @p @a p) q)
+
+-- | @p ==> q@ is true if @q@ is provably true under the condition that @p@
+-- is true.
+data (==>) :: Predicate k -> Predicate k -> Predicate k
+type instance Apply (p ==> q) a = p @@ a -> q @@ a
+
+infixr 1 ==>
+
+instance Decidable (Impossible ==> p) where
+instance Provable (Impossible ==> p) where
+    prove = explosion @p
+
+instance (Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p) where
+    decide x = case decide @(p ==> q) x of
+      Proved pq     -> Proved $ \vq p -> vq (pq p)
+      Disproved vpq -> case decide @q x of
+        Proved    q  -> Disproved $ \_     -> vpq (const q)
+        Disproved vq -> Disproved $ \vnpnq -> vpq (absurd . vnpnq vq)
+instance Provable (p ==> q) => Provable (Not q ==> Not p) where
+    prove = contrapositive @p @q (prove @(p ==> q))
+
+-- | @'Implies' p q@ is a constraint that @p '==>' q@ is 'Provable'; that
+-- is, you can prove that @p@ implies @q@.
+type Implies  p q = Provable  (p ==> q)
+
+-- | @'Equiv' p q@ is a constraint that @p '<==>' q@ is 'Provable'; that
+-- is, you can prove that @p@ is logically equivalent to @q@.
+type Equiv  p q = Provable  (p <==> q)
+
+-- | If @q@ is provable, then so is @p '==>' q@.
+--
+-- This can be used as an easy plug-in 'Provable' instance for @p '==>' q@
+-- if @q@ is 'Provable':
+--
+-- @
+-- instance Provable (p ==> MyPred) where
+--     prove = proveImplies @MyPred
+-- @
+--
+-- This instance isn't provided polymorphically because of overlapping
+-- instance issues.
+proveImplies :: Prove q -> Prove (p ==> q)
+proveImplies q x _ = q x
+
+-- | Two-way implication, or logical equivalence
+type (p <==> q) = p ==> q &&& q ==> p
+infixr 1 <==>
+
+-- | From @'Impossible' @@ a@, you can prove anything.  Essentially
+-- a lifted version of 'absurd'.
+explosion :: Impossible --> p
+explosion x v = absurd $ v x
+
+-- | 'Evident' can be proven from all predicates.
+atom :: p --> Evident
+atom = const
+
+-- | We cannot have both @p@ and @'Not' p@.
+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
+
+-- | If p implies q, then not q implies not p.
+contrapositive
+    :: (p --> q)
+    -> (Not q --> Not p)
+contrapositive f x v p = v (f x p)
+
+-- | Reverse direction of 'contrapositive'.  Only possible if @q@ is
+-- 'Decidable' on its own, without the help of @p@, which makes this much
+-- less useful.
+contrapositive'
+    :: forall p q. Decidable q
+    => (Not q --> Not p)
+    -> (p --> q)
+contrapositive' f x p = case decide @q x of
+    Proved     q -> q
+    Disproved vq -> absurd $ f x vq p
+
+-- | Logical double negation.  Only possible if @p@ is 'Decidable'.
+doubleNegation :: forall p. Decidable p => Not (Not p) --> p
+doubleNegation x vvp = case decide @p x of
+    Proved    p  -> p
+    Disproved vp -> absurd $ vvp vp
+
+-- | If @p '&&&' q@ is true, then so is @p@.
+projAndFst :: (p &&& q) --> p
+projAndFst _ = fst
+
+-- | If @p '&&&' q@ is true, then so is @q@.
+projAndSnd :: (p &&& q) --> q
+projAndSnd _ = snd
+
+-- | If @p@ is true, then so is @p '|||' q@.
+injOrLeft :: forall p q. p --> (p ||| q)
+injOrLeft _ = Left
+
+-- | If @q@ is true, then so is @p '|||' q@.
+injOrRight :: forall p q. q --> (p ||| q)
+injOrRight _ = Right
diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Predicate/Param.hs
@@ -0,0 +1,166 @@
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE DefaultSignatures    #-}
+{-# LANGUAGE EmptyCase            #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeInType           #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- |
+-- Module      : Data.Type.Universe.Param
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Manipulate "parameterized predicates".  See 'ParamPred' and 'Found' for
+-- more information.
+--
+module Data.Type.Predicate.Param (
+  -- * Parameterized Predicates
+    ParamPred
+  , FlipPP, ConstPP, PPMap, InP, AnyMatch
+  -- * Deciding and Proving
+  , Found
+  , Selectable, select
+  , Searchable, search
+  ) where
+
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Singletons.Sigma
+import           Data.Type.Predicate
+import           Data.Type.Predicate.Logic
+import           Data.Type.Universe
+
+-- | A parameterized predicate.  See 'Found' for more information.
+type ParamPred k v = k -> Predicate v
+
+-- | Convert a parameterized predicate into a predicate on the parameter.
+--
+-- A @'Found' p@ is a predicate on @p :: 'ParamPred' k v@ that tests a @k@
+-- for the fact that there exists a @v@ where @'ParamPred' k v@ is satisfied.
+--
+-- Intended as the basic interface for 'ParamPred', since it turns
+-- a 'ParamPred' into a normal 'Predicate', which can have 'Decidable' and
+-- 'Provable' instances.
+--
+-- For some context, an instance of @'Provable' ('Found' P)@, where @P ::
+-- 'ParamPred' k v@, means that for any input @x :: k@, we can always find
+-- a @y :: v@ such that we have @P x @@ y@.
+--
+-- In the language of quantifiers, it means that forall @x :: k@, there
+-- exists a @y :: v@ such that @P x @@ y@.
+--
+-- For an instance of @'Decidable' ('Found' P)@, it means that for all @x
+-- :: k@, we can prove or disprove the fact that there exists a @y :: v@
+-- such that @P x @@ y@.
+data Found :: ParamPred k v -> Predicate k
+type instance Apply (Found (p :: ParamPred k v)) a = Σ v (p a)
+
+-- | Flip the arguments of a 'ParamPred'.
+data FlipPP :: ParamPred v k -> ParamPred k v
+type instance Apply (FlipPP p x) y = p y @@ x
+
+-- | Promote a @'Predicate' v@ to a @'ParamPred' k v@, ignoring the @k@
+-- input.
+data ConstPP :: Predicate v -> ParamPred k v
+type instance Apply (ConstPP p k) v = p @@ v
+
+-- | Pre-compose a function to a 'ParamPred'.  Is essentially @'flip'
+-- ('.')@, but unfortunately defunctionalization doesn't work too well with
+-- that definition.
+data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v
+type instance Apply (PPMap f p x) y = p (f @@ x) @@ y
+
+instance (Decidable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Decidable (Found (PPMap f p)) where
+    decide (x :: Sing a) = case decide @(Found p) ((sing :: Sing f) @@ x) of
+        Proved (i :&: p) -> Proved $ i :&: p
+        Disproved v      -> Disproved $ \case i :&: p -> v (i :&: p)
+
+instance (Provable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Provable (Found (PPMap f p)) where
+    prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of
+        i :&: p -> i :&: p
+
+-- | A constraint that a @'ParamPred' k v@ is "searchable".  It means that
+-- for any input @x :: k@, we can prove or disprove that there exists a @y
+-- :: v@ that satisfies @P x \@\@ y@.  We can "search" for that @y@, and
+-- prove that it can or cannot be found.
+type Searchable p = Decidable (Found p)
+
+-- | A constraint that a @'ParamPred' k v@ s "selectable".  It means that
+-- for any input @x :: k@, we can always find a @y :: v@ that satisfies @P
+-- x \@\@ y@.  We can "select" that @y@, no matter what.
+type Selectable p = Provable  (Found p)
+
+-- | The deciding/searching function for @'Searchable' p@.
+--
+-- Must be called by applying the 'ParamPred':
+--
+-- @
+-- 'search' \@p
+-- @
+search
+    :: forall p. Searchable p
+    => Decide (Found p)
+search = decide @(Found p)
+
+-- | The proving/selecting function for @'Selectable' p@.
+--
+-- Must be called by applying the 'ParamPred':
+--
+-- @
+-- 'select' \@p
+-- @
+select
+    :: forall p. Selectable p
+    => Prove (Found p)
+select = prove @(Found p)
+
+-- | A @'ParamPred' (f k) k@.  Parameterized on an @as :: f k@, returns
+-- a predicate that is true if there exists any @a :: k@ in @as@.
+--
+-- Essentially 'NotNull'.
+type InP f = (ElemSym1 f :: ParamPred (f k) k)
+
+instance Universe f => Decidable (Found (InP f)) where
+    decide xs = case decide @(NotNull f) xs of
+      Proved (WitAny i s) -> Proved $ s :&: i
+      Disproved v         -> Disproved $ \case
+        s :&: i -> v $ WitAny i s
+
+instance Decidable (NotNull f ==> Found (InP f))
+instance Provable (NotNull f ==> Found (InP f)) where
+    prove _ (WitAny i s) = s :&: i
+
+instance Decidable (Found (InP f) ==> NotNull f)
+instance Provable (Found (InP f) ==> NotNull f) where
+    prove _ (s :&: i) = WitAny i s
+
+-- | @'AnyMatch' f@ takes a parmaeterized predicate on @k@ (testing for
+-- a @v@) and turns it into a parameterized predicate on @f k@ (testing for
+-- a @v@).  It "lifts" the domain into @f@.
+--
+-- An @'AnyMatch' f p as@ is a predicate taking an argument @a@ and
+-- testing if @p a :: 'Predicate' k@ is satisfied for any item in @as ::
+-- f k@.
+--
+-- A @'ParamPred' k v@ tests if a @k@ can create some @v@.  The resulting
+-- @'ParamPred' (f k) v@ tests if any @k@ in @f k@ can create some @v@.
+data AnyMatch f :: ParamPred k v -> ParamPred (f k) v
+type instance Apply (AnyMatch f p as) a = Any f (FlipPP p a) @@ as
+
+instance (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p)) where
+    decide xs = case decide @(Any f (Found p)) xs of
+      Proved (WitAny i (x :&: p)) -> Proved $ x :&: WitAny i p
+      Disproved v                 -> Disproved $ \case
+        x :&: WitAny i p -> v $ WitAny i (x :&: p)
+
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Predicate/Quantification.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-- |
+-- Module      : Data.Type.Predicate.Quantification
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Higher-level predicates for quantifying predicates over universes and
+-- sets.
+--
+module Data.Type.Predicate.Quantification (
+  -- * Any
+    Any, WitAny(..), None
+  -- ** Decision
+  , decideAny, idecideAny, decideNone, idecideNone
+  -- ** Entailment
+  , entailAny, ientailAny, entailAnyF, ientailAnyF
+  -- * All
+  , All, WitAll(..)
+  -- ** Decision
+  , decideAll, idecideAll
+  -- ** Entailment
+  , entailAll, ientailAll, entailAllF, ientailAllF
+  , decideEntailAll, idecideEntailAll
+  ) where
+
+import           Data.Kind
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Type.Predicate
+import           Data.Type.Universe
+
+-- | 'decideNone', but providing an 'Elem'.
+idecideNone
+    :: forall f k (p :: k ~> Type) (as :: f k). Universe f
+    => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))    -- ^ predicate on value
+    -> (Sing as -> Decision (None f p @@ as))                    -- ^ predicate on collection
+idecideNone f xs = decideNot @(Any f p) $ idecideAny f xs
+
+-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
+-- a collection @as@ that is true if and only if /no/ item in @as@
+-- satisfies the original predicate.
+--
+-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
+-- of kind @f k ~> Type@.
+decideNone
+    :: forall f k (p :: k ~> Type). Universe f
+    => Decide p                         -- ^ predicate on value
+    -> Decide (None f p)                -- ^ predicate on collection
+decideNone f = idecideNone (const f)
+
+-- | 'entailAny', but providing an 'Elem'.
+ientailAny
+    :: forall f p q as. (Universe f, SingI as)
+    => (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)
+
+-- | If there exists an @a@ s.t. @p a@, and if @p@ implies @q@, then there
+-- must exist an @a@ s.t. @q a@.
+entailAny
+    :: forall f p q. Universe f
+    => (p --> q)
+    -> (Any f p --> Any f q)
+entailAny = tmap @(Any f)
+
+-- | 'entailAll', but providing an 'Elem'.
+ientailAll
+    :: forall f p q as. (Universe f, SingI as)
+    => (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)
+
+-- | If for all @a@ we have @p a@, and if @p@ implies @q@, then for all @a@
+-- we must also have @p a@.
+entailAll
+    :: forall f p q. Universe f
+    => (p --> q)
+    -> (All f p --> All f q)
+entailAll = tmap @(All f)
+
+-- | 'entailAnyF', but providing an 'Elem'.
+ientailAnyF
+    :: forall f p q as h. Functor h
+    => (forall a. Elem f as a -> p @@ a -> h (q @@ a))      -- ^ implication in context
+    -> Any f p @@ as
+    -> h (Any f q @@ as)
+ientailAnyF f = \case WitAny i x -> WitAny i <$> f i x
+
+-- | If @p@ implies @q@ under some context @h@, and if there exists some
+-- @a@ such that @p a@, then there must exist some @a@ such that @p q@
+-- under that context @h@.
+--
+-- @h@ might be something like, say, 'Maybe', to give predicate that is
+-- either provably true or unprovably false.
+--
+-- Note that it is not possible to do this with @p a -> 'Decision' (q a)@.
+-- This is if the @p a -> 'Decision' (q a)@ implication is false, there
+-- it doesn't mean that there is /no/ @a@ such that @q a@, necessarily.
+-- There could have been an @a@ where @p@ does not hold, but @q@ does.
+entailAnyF
+    :: forall f p q h. (Universe f, Functor h)
+    => (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
+
+-- | 'entailAllF', but providing an 'Elem'.
+ientailAllF
+    :: forall f p q as h. (Universe f, Applicative h, SingI as)
+    => (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
+
+-- | 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@.
+entailAllF
+    :: forall f p q h. (Universe f, Applicative h)
+    => (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
+
+-- | 'entailAllF', but providing an 'Elem'.
+idecideEntailAll
+    :: forall f p q as. (Universe f, SingI as)
+    => (forall a. Elem f as a -> p @@ a -> Decision (q @@ a))     -- ^ decidable implication
+    -> All f p @@ as
+    -> Decision (All f q @@ as)
+idecideEntailAll f a = idecideAll (\i _ -> f i (runWitAll a i)) sing
+
+-- | If we have @p a@ for all @a@, and @p a@ can be used to test for @q a@,
+-- then we can test all @a@s for @q a@.
+decideEntailAll
+    :: forall f p q. Universe f
+    => p -?> q
+    -> All f p -?> All f q
+decideEntailAll = dmap @(All f)
diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Universe.hs
@@ -0,0 +1,439 @@
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE InstanceSigs          #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-- |
+-- Module      : Data.Type.Universe
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Combinators for working with type-level predicates, along with
+-- typeclasses for canonical proofs and deciding functions.
+--
+module Data.Type.Universe (
+  -- * Universe
+    Elem, In, Universe(..)
+  -- ** Instances
+  , Index(..), IsJust(..), IsRight(..), NEIndex(..), Snd(..)
+  -- ** Predicates
+  , All, WitAll(..)
+  , Any, WitAny(..), None
+  , Null, NotNull
+  -- * Decisions and manipulations
+  , decideAny, decideAll, genAllA, genAll, igenAll
+  , foldMapUni, ifoldMapUni, index, pickElem
+  -- * Defunctionalization symbols
+  , ElemSym0, ElemSym1, ElemSym2
+  ) where
+
+import           Data.Type.Predicate.Logic
+import           Control.Applicative
+import           Data.Functor.Identity
+import           Data.Kind
+import           Data.List.NonEmpty                    (NonEmpty(..))
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Snd, Null, Not)
+import           Data.Type.Predicate
+import           Prelude hiding                        (any, all)
+import qualified Data.Singletons.Prelude.List.NonEmpty as NE
+
+-- | 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) = TyCon1 (Elem 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
+    WitAny :: Elem f as a -> p @@ a -> WitAny f p as
+
+-- | An @'Any' f p@ is a predicate testing a collection @as :: f a@ for the
+-- fact that at least one item in @as@ satisfies @p@.  Represents the
+-- "exists" quantifier over a given universe.
+--
+-- 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)
+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
+-- items @a@ in the type-level collection @as@.
+newtype WitAll f p (as :: f k) = WitAll { runWitAll :: forall a. Elem f as a -> p @@ a }
+
+-- | An @'All' f p@ is a predicate testing a collection @as :: f a@ for the
+-- fact that /all/ items in @as@ satisfy @p@.  Represents the "forall"
+-- quantifier over a given universe.
+--
+-- 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)
+type instance Apply (All f p) as = WitAll f p as
+
+instance (Universe f, Decidable p) => Decidable (Any f p) where
+    decide = decideAny @f @_ @p $ decide @p
+
+instance (Universe f, Decidable p) => Decidable (All f p) where
+    decide = decideAll @f @_ @p $ decide @p
+
+instance (Universe f, Provable p) => Decidable (NotNull f ==> Any f p) where
+
+instance Provable p => Provable (NotNull f ==> Any f p) where
+    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)
+
+instance Universe f => TFunctor (Any f) where
+    tmap f xs (WitAny i x) = WitAny i (f (index i xs) x)
+
+instance Universe f => TFunctor (All f) where
+    tmap f xs a = WitAll $ \i -> f (index 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
+    -- | 'decideAny', but providing an 'Elem'.
+    idecideAny
+        :: forall k (p :: k ~> Type) (as :: f k). ()
+        => (forall a. Elem f as a -> Sing a -> Decision (p @@ a))   -- ^ predicate on value
+        -> (Sing as -> Decision (Any f p @@ as))                         -- ^ predicate on collection
+
+    -- | 'decideAll', but providing an 'Elem'.
+    idecideAll
+        :: forall k (p :: k ~> Type) (as :: f k). ()
+        => (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
+
+-- | Predicate that a given @as :: f k@ is empty and has no items in it.
+type Null    f = (None f Evident :: Predicate (f k))
+
+-- | Predicate that a given @as :: f k@ is not empty, and has at least one
+-- item in it.
+type NotNull f = (Any f Evident :: Predicate (f k))
+
+-- | A @'None' f p@ is a predicate on a collection @as@ that no @a@ in @as@
+-- satisfies predicate @p@.
+type None f p = (Not (Any f p) :: Predicate (f k))
+
+-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
+-- a collection @as@ that is true if and only if /any/ item in @as@
+-- satisfies the original predicate.
+--
+-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
+-- of kind @f k ~> Type@.
+--
+-- Essentially tests existential quantification.
+decideAny
+    :: forall f k (p :: k ~> Type). Universe f
+    => Decide p                                 -- ^ predicate on value
+    -> Decide (Any f p)                -- ^ predicate on collection
+decideAny f = idecideAny (const f)
+
+-- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
+-- a collection @as@ that is true if and only if /all/ items in @as@
+-- satisfies the original predicate.
+--
+-- That is, it turns a predicate of kind @k ~> Type@ into a predicate
+-- of kind @f k ~> Type@.
+--
+-- Essentially tests universal quantification.
+decideAll
+    :: forall f k (p :: k ~> Type). Universe f
+    => Decide p                                 -- ^ predicate on value
+    -> 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 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)
+
+-- | '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)
+
+-- | If @p a@ is true for all values @a@ in @as@, then we have @'All'
+-- p as@.  Basically witnesses the definition of 'All'.
+genAll
+    :: 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
+
+-- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
+splitSing
+    :: forall f (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 = case decide @(Any f (TyPred ((:~:) a))) sing of
+    Proved (WitAny i Refl) -> Proved i
+    Disproved v            -> Disproved $ \i -> v $ WitAny i Refl
+
+-- | '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)
+
+-- | 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
+
+deriving instance Show (Index as a)
+instance (SingI (as :: [k]), SDecide k) => Decidable (TyPred (Index as)) where
+    decide x = withSingI x $ pickElem
+
+type instance Elem [] = Index
+
+instance Universe [] where
+    idecideAny
+        :: forall k (p :: k ~> Type) (as :: [k]). ()
+        => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
+        -> Sing as
+        -> Decision (Any [] p @@ as)
+    idecideAny f = \case
+      SNil -> Disproved $ \case
+        WitAny i _ -> case i of {}
+      x `SCons` xs -> case f IZ x of
+        Proved p    -> Proved $ WitAny IZ p
+        Disproved v -> case idecideAny @[] @_ @p (f . IS) xs of
+          Proved (WitAny i p) -> Proved $ WitAny (IS i) p
+          Disproved vs -> Disproved $ \case
+            WitAny IZ     p -> v p
+            WitAny (IS i) p -> vs (WitAny i p)
+
+    idecideAll
+        :: forall k (p :: k ~> Type) (as :: [k]). ()
+        => (forall a. Elem [] as a -> Sing a -> Decision (p @@ a))
+        -> Sing as
+        -> Decision (All [] p @@ as)
+    idecideAll f = \case
+      SNil -> Proved $ WitAll $ \case {}
+      x `SCons` xs -> case f IZ x of
+        Proved p -> case idecideAll @[] @_ @p (f . IS) xs of
+          Proved a -> Proved $ WitAll $ \case
+            IZ   -> p
+            IS i -> runWitAll a i
+          Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . IS)
+        Disproved v -> Disproved $ \a -> v $ runWitAll a IZ
+
+    igenAllA
+        :: forall (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
+      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 IsJust :: Maybe k -> k -> Type where
+    IsJust :: IsJust ('Just a) a
+
+deriving instance Show (IsJust as a)
+instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IsJust as)) where
+    decide x = withSingI x $ pickElem
+
+type instance Elem Maybe = IsJust
+
+instance Universe Maybe where
+    idecideAny f = \case
+      SNothing -> Disproved $ \case WitAny i _ -> case i of {}
+      SJust x  -> case f IsJust x of
+        Proved p    -> Proved $ WitAny IsJust p
+        Disproved v -> Disproved $ \case
+          WitAny IsJust p -> v p
+
+    idecideAll f = \case
+      SNothing -> Proved $ WitAll $ \case {}
+      SJust x  -> case f IsJust x of
+        Proved p    -> Proved $ WitAll $ \case IsJust -> p
+        Disproved v -> Disproved $ \a -> v $ runWitAll a IsJust
+
+    igenAllA f = \case
+      SNothing -> pure $ WitAll $ \case {}
+      SJust x  -> (\p -> WitAll $ \case IsJust -> p) <$> f IsJust x
+
+-- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
+-- is 'Right'.
+data IsRight :: Either j k -> k -> Type where
+    IsRight :: IsRight ('Right a) a
+
+deriving instance Show (IsRight as a)
+instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IsRight as)) where
+    decide x = withSingI x $ pickElem
+
+type instance Elem (Either j) = IsRight
+
+instance Universe (Either j) where
+    idecideAny f = \case
+      SLeft  _ -> Disproved $ \case WitAny i _ -> case i of {}
+      SRight x -> case f IsRight x of
+        Proved p    -> Proved $ WitAny IsRight p
+        Disproved v -> Disproved $ \case
+          WitAny IsRight p -> v p
+
+    idecideAll f = \case
+      SLeft  _ -> Proved $ WitAll $ \case {}
+      SRight x -> case f IsRight x of
+        Proved p    -> Proved $ WitAll $ \case IsRight -> p
+        Disproved v -> Disproved $ \a -> v $ runWitAll a IsRight
+
+    igenAllA f = \case
+      SLeft  _ -> pure $ WitAll $ \case {}
+      SRight x -> (\p -> WitAll $ \case IsRight -> p) <$> f IsRight 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
+
+type instance Elem NonEmpty = NEIndex
+
+instance Universe NonEmpty where
+    idecideAny
+        :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
+        => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
+        -> Sing as
+        -> Decision (Any NonEmpty p @@ as)
+    idecideAny f (x NE.:%| xs) = case f NEHead x of
+      Proved p    -> Proved $ WitAny NEHead p
+      Disproved v -> case idecideAny @[] @_ @p (f . NETail) xs of
+        Proved (WitAny i p) -> Proved $ WitAny (NETail i) p
+        Disproved vs     -> Disproved $ \case
+          WitAny i p -> case i of
+            NEHead    -> v p
+            NETail i' -> vs (WitAny i' p)
+
+    idecideAll
+        :: forall k (p :: k ~> Type) (as :: NonEmpty k). ()
+        => (forall a. Elem NonEmpty as a -> Sing a -> Decision (p @@ a))
+        -> Sing as
+        -> Decision (All NonEmpty p @@ as)
+    idecideAll f (x NE.:%| xs) = case f NEHead x of
+      Proved p -> case idecideAll @[] @_ @p (f . NETail) xs of
+        Proved ps -> Proved $ WitAll $ \case
+          NEHead   -> p
+          NETail i -> runWitAll ps i
+        Disproved v -> Disproved $ \a -> v $ WitAll (runWitAll a . NETail)
+      Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead
+
+    igenAllA
+        :: forall (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 Snd :: (j, k) -> k -> Type where
+    Snd :: Snd '(a, b) b
+
+deriving instance Show (Snd as a)
+instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (Snd as)) where
+    decide x = withSingI x $ pickElem
+
+type instance Elem ((,) j) = Snd
+
+instance Universe ((,) j) where
+    idecideAny f (STuple2 _ x) = case f Snd x of
+      Proved p    -> Proved $ WitAny Snd p
+      Disproved v -> Disproved $ \case WitAny Snd p -> v p
+
+    idecideAll f (STuple2 _ x) = case f Snd x of
+      Proved p    -> Proved $ WitAll $ \case Snd -> p
+      Disproved v -> Disproved $ \a -> v $ runWitAll a Snd
+
+    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case Snd -> p) <$> f Snd x
diff --git a/src/Data/Type/Universe/Subset.hs b/src/Data/Type/Universe/Subset.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Universe/Subset.hs
@@ -0,0 +1,168 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE EmptyCase             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE LambdaCase            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+-- |
+-- Module      : Data.Type.Universe.Subset
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Represent a decidable subset of a type-level collection.
+--
+module Data.Type.Universe.Subset (
+  -- * Subset
+    Subset, WitSubset(..)
+  , makeSubset
+  -- ** Subset manipulation
+  , intersection, union, symDiff, mergeSubset, imergeSubset
+  , mapSubset, imapSubset
+  -- ** Subset extraction
+  , subsetToList
+  -- ** Subset tests
+  , subsetToAny, subsetToAll, subsetToNone
+  -- ** Subset construction
+  , emptySubset, fullSubset
+  ) where
+
+import           Control.Applicative
+import           Data.Kind
+import           Data.Monoid                        (Alt(..))
+import           Data.Singletons
+import           Data.Singletons.Decide
+import           Data.Type.Predicate
+import           Data.Type.Predicate.Logic
+import           Data.Type.Predicate.Quantification
+import           Data.Type.Universe
+
+-- | A @'WitSubset' f p @@ as@ describes a /decidable/ subset of type-level
+-- collection @as@.
+newtype WitSubset f p (as :: f k) = WitSubset
+    { runWitSubset :: forall a. Elem f as a -> Decision (p @@ a)
+    }
+
+-- | A @'Subset' f p@ is a predicate that some decidable subset of an input
+-- @as@ is true.
+data Subset f :: (k ~> Type) -> (f k ~> Type)
+type instance Apply (Subset f p) as = WitSubset f p as
+
+instance (Universe f, Decidable p) => Decidable (Subset f p)
+instance (Universe f, Decidable p) => Provable (Subset f p) where
+    prove = makeSubset @f @_ @p (\_ -> decide @p)
+
+-- | Create a 'Subset' from a predicate.
+makeSubset
+    :: forall f k p (as :: f k). Universe f
+    => (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)
+
+-- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
+-- predicates.
+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
+    Proved p    -> pure $ WitAny i p
+    Disproved _ -> empty
+
+-- | Restrict a 'Subset' to a single (arbitrary) member, or fail if none
+-- exists.
+subsetToAny
+    :: forall f p. Universe f
+    => Subset f p -?> Any f p
+subsetToAny xs s = idecideAny (\i _ -> runWitSubset s i) xs
+
+-- | Construct an empty subset.
+emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as
+emptySubset = prove @(Subset f Impossible) sing
+
+-- | Construct a full subset
+fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
+fullSubset = prove @(Subset f Evident) sing
+
+-- | Test if a subset is empty.
+subsetToNone :: forall f p. Universe f => Subset f p -?> None f p
+subsetToNone xs s = idecideNone (\i _ -> runWitSubset s i) xs
+
+-- | Combine two subsets based on a decision function
+imergeSubset
+    :: forall f k p q r (as :: f k). ()
+    => (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
+    -> Subset f p @@ as
+    -> Subset f q @@ as
+    -> Subset f r @@ as
+imergeSubset f ps qs = WitSubset $ \i ->
+    f i (runWitSubset ps i) (runWitSubset qs i)
+
+-- | Combine two subsets based on a decision function
+mergeSubset
+    :: forall f k p q r (as :: f k). ()
+    => (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a))
+    -> Subset f p @@ as
+    -> Subset f q @@ as
+    -> Subset f r @@ as
+mergeSubset f = imergeSubset (\(_ :: Elem f as a) p -> f @a p)
+
+-- | Subset intersection
+intersection
+    :: forall f p q. ()
+    => ((Subset f p &&& Subset f q) --> Subset f (p &&& q))
+intersection _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideAnd @p @q @a
+
+-- | Subset union
+union
+    :: forall f p q. ()
+    => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))
+union _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideOr @p @q @a
+
+-- | Symmetric subset difference
+symDiff
+    :: forall f p q. ()
+    => ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))
+symDiff _ = uncurry $ imergeSubset $ \(_ :: Elem f as a) -> decideXor @p @q @a
+
+-- | Test if a subset is equal to the entire original collection
+subsetToAll
+    :: forall f p. Universe f
+    => Subset f p -?> All f p
+subsetToAll xs s = idecideAll (\i _ -> runWitSubset s i) xs
+
+-- | 'mapSubset', but providing an 'Elem'.
+imapSubset
+    :: (forall a. Elem f as a -> p @@ a -> q @@ a)
+    -> (forall a. Elem f as a -> q @@ a -> p @@ a)
+    -> Subset f p @@ as
+    -> Subset f q @@ as
+imapSubset f g s = WitSubset $ \i ->
+    mapDecision (f i) (g i) (runWitSubset s i)
+
+-- | Map a bidirectional implication over a subset described by that
+-- implication.
+--
+-- Implication needs to be bidirection, or otherwise we can't produce
+-- a /decidable/ subset as a result.
+mapSubset
+    :: Universe f
+    => (p --> q)
+    -> (q --> p)
+    -> (Subset f p --> Subset f q)
+mapSubset f g xs@Sing = withSingI xs $
+    imapSubset (\i -> f (index i xs))
+               (\i -> g (index i xs))