diff --git a/src/Data/Type/Boolean.hs b/src/Data/Type/Boolean.hs
--- a/src/Data/Type/Boolean.hs
+++ b/src/Data/Type/Boolean.hs
@@ -30,6 +30,7 @@
 
 import Data.Type.Quantifier (Some(..))
 import Type.Family.Bool
+import Type.Family.Constraint
 import Type.Class.Known
 import Type.Class.Higher
 
@@ -83,11 +84,13 @@
 (<==>) = (.==)
 infixr 1 <==>
 
-class BoolEq (f :: k -> *) where
-  (.==) :: f a -> f b -> Boolean (a == b)
+class BoolEquality (f :: k -> *) where
+  type BoolEqC f (a :: k) (b :: k) :: Constraint
+  type BoolEqC f a b = ØC
+  (.==) :: BoolEqC f a b => f a -> f b -> Boolean (a == b)
 infix 4 .==
 
-instance BoolEq Boolean where
+instance BoolEquality Boolean where
   (.==) = \case
     False_ -> \case
       False_ -> True_
diff --git a/src/Data/Type/Conjunction.hs b/src/Data/Type/Conjunction.hs
--- a/src/Data/Type/Conjunction.hs
+++ b/src/Data/Type/Conjunction.hs
@@ -36,6 +36,7 @@
 import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Tuple
+import Data.Type.Boolean
 
 -- (:&:) {{{
 
@@ -79,9 +80,6 @@
 curryFan :: ((f :&: g) a -> r) -> f a -> g a -> r
 curryFan f a b = f (a :&: b)
 
-instance DecEquality f => DecEquality (f :&: g) where
-  decideEquality (a :&: _) (c :&: _) = decideEquality a c
-
 instance (Known f a, Known g a) => Known (f :&: g) a where
   known = known :&: known
 
@@ -158,6 +156,11 @@
 
 _snd :: (a#b) :~: (c#d) -> b :~: d
 _snd Refl = Refl
+
+{-
+instance (BoolEquality f, BoolEquality g) => BoolEquality (f :*: g) where
+  (a :*: b) .== (c :*: d) = a .== c .&& b .== d
+-}
 
 instance (DecEquality f, DecEquality g) => DecEquality (f :*: g) where
   decideEquality (a :*: b) (c :*: d) = case decideEquality a c of
diff --git a/src/Data/Type/Disjunction.hs b/src/Data/Type/Disjunction.hs
--- a/src/Data/Type/Disjunction.hs
+++ b/src/Data/Type/Disjunction.hs
@@ -167,6 +167,18 @@
     , (a,s2)    <- readsPrec1 11 s1
     ]
 
+{-
+instance (DecEquality f, DecEquality g) => DecEquality (f :+: g) where
+  decideEquality = \case
+    L' a -> \case
+      L' b -> decCase (decideEquality a b) (\Refl -> Proven Refl) (\contra -> Refuted $ contra . toEquality fromLeftCong)
+      R' _ -> Refuted $
+    R' a -> \case
+      L' b -> Refuted undefined
+      R' b -> undefined
+-}
+
+
 (>+<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :+: g) e -> r
 f >+< g = \case
   L' a -> f a
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -28,6 +28,7 @@
 
 module Data.Type.Nat where
 
+import Data.Type.Boolean
 import Data.Type.Equality
 import Data.Type.Quantifier
 import Type.Class.Higher
@@ -84,6 +85,15 @@
     S_ x -> \case
       Z_   -> Nothing
       S_ y -> testEquality x y //? qed
+
+instance BoolEquality Nat where
+  (.==) = \case
+    Z_ -> \case
+      Z_   -> True_
+      S_ _ -> False_
+    S_ x -> \case
+      Z_   -> False_
+      S_ y -> x .== y
 
 pred' :: Nat (S x) -> Nat x
 pred' (S_ x) = x
diff --git a/src/Data/Type/Nat/Inequality.hs b/src/Data/Type/Nat/Inequality.hs
--- a/src/Data/Type/Nat/Inequality.hs
+++ b/src/Data/Type/Nat/Inequality.hs
@@ -21,20 +21,6 @@
 import Type.Family.Constraint
 import Type.Family.Nat
 
-type family (x :: N) < (y :: N) :: Bool where
-  Z   < Z   = False
-  Z   < S y = True
-  S x < Z   = False
-  S x < S y = x < y
-infix 4 <
-
-type family (x :: N) > (y :: N) :: Bool where
-  Z   > Z   = False
-  Z   > S y = False
-  S x > Z   = True
-  S x > S y = x > y
-infix 4 >
-
 data NatLT :: N -> N -> * where
   LTZ :: NatLT Z (S y)
   LTS :: !(NatLT x y)
diff --git a/src/Data/Type/Quantifier.hs b/src/Data/Type/Quantifier.hs
--- a/src/Data/Type/Quantifier.hs
+++ b/src/Data/Type/Quantifier.hs
@@ -69,6 +69,15 @@
 onSome :: (forall a. f a -> g x) -> Some f -> Some g
 onSome f (Some a) = Some (f a)
 
+msome :: Monad m => f a -> m (Some f)
+msome = return . Some
+
+(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r
+m >>=- f = do
+  s <- m
+  s >>- f
+infixl 1 >>=-
+
 -- }}}
 
 -- Some2 {{{
@@ -93,6 +102,15 @@
 onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
 onSome2 f (Some2 a) = Some2 (f a)
 
+msome2 :: Monad m => f a b -> m (Some2 f)
+msome2 = return . Some2
+
+(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r
+m >>=-- f = do
+  s <- m
+  s >>-- f
+infixl 1 >>=--
+
 -- }}}
 
 -- Some3 {{{
@@ -117,6 +135,15 @@
 onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
 onSome3 f (Some3 a) = Some3 (f a)
 
+msome3 :: Monad m => f a b c -> m (Some3 f)
+msome3 = return . Some3
+
+(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r
+m >>=--- f = do
+  s <- m
+  s >>--- f
+infixl 1 >>=---
+
 -- }}}
 
 -- SomeC {{{
@@ -131,6 +158,15 @@
 (>>~) = someC
 infixl 1 >>~
 
+msomeC :: (Monad m, c a) => f a -> m (SomeC c f)
+msomeC = return . SomeC
+
+(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r
+m >>=~ f = do
+  s <- m
+  s >>~ f
+infixl 1 >>=~
+
 -- }}}
 
 -- EveryN {{{
@@ -143,6 +179,10 @@
 
 data Every3 (f :: k -> l -> m -> *) :: * where
   Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f
+
+data EveryC (c :: k -> Constraint) (f :: k -> *) :: * where
+  EveryC :: { instEveryC :: forall a. c a => f a }
+         -> EveryC c f
 
 -- }}}
 
diff --git a/src/Data/Type/Sym.hs b/src/Data/Type/Sym.hs
--- a/src/Data/Type/Sym.hs
+++ b/src/Data/Type/Sym.hs
@@ -29,6 +29,7 @@
 
 module Data.Type.Sym where
 
+import Data.Type.Boolean
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
@@ -53,6 +54,10 @@
 
 instance TestEquality Sym where
   testEquality Sym Sym = sameSymbol Proxy Proxy
+
+instance BoolEquality Sym where
+  type BoolEqC Sym a b = Known Boolean (a == b)
+  Sym .== Sym = known
 
 instance KnownSymbol x => Known Sym x where
   type KnownC Sym x = KnownSymbol x
diff --git a/src/Type/Class/Witness.hs b/src/Type/Class/Witness.hs
--- a/src/Type/Class/Witness.hs
+++ b/src/Type/Class/Witness.hs
@@ -88,6 +88,9 @@
   id              = Sub Wit
   Sub bc . Sub ab = Sub $ bc \\ ab
 
+transC :: (b :- c) -> (a :- b) -> a :- c
+transC = (.)
+
 -- }}}
 
 -- Witness {{{
@@ -176,6 +179,9 @@
 
 -- Initial/Terminal {{{
 
+toEquality :: (a ~ b) :- (c ~ d) -> a :~: b -> c :~: d
+toEquality p = \Refl -> Refl \\ p
+
 commute :: (a ~ b) :- (b ~ a)
 commute = Sub Wit
 
@@ -192,6 +198,8 @@
 bottom :: Fail :- c
 bottom = falso
 
+
+
 instance Witness ØC c (Wit c) where
   r \\ Wit = r
 
@@ -239,6 +247,14 @@
 
 impossible :: a -> Void
 impossible = unsafeCoerce
+
+exFalso :: Wit Fail -> a
+exFalso p = castWith q ()
+  where
+  q :: () :~: a
+  q = toEquality (contraC r) Refl
+  r :: (b ~ b) :- Fail
+  r = Sub p
 
 (=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b)
 (=?=) = testEquality
diff --git a/src/Type/Family/Bool.hs b/src/Type/Family/Bool.hs
--- a/src/Type/Family/Bool.hs
+++ b/src/Type/Family/Bool.hs
@@ -27,29 +27,16 @@
 
 module Type.Family.Bool
   ( module Type.Family.Bool
-  , type (==)
+  , module Exports
   ) where
 
 import Type.Family.Constraint
-import Type.Class.Witness (type (==))
+import Type.Class.Witness as Exports (type (==))
+import Data.Type.Bool as Exports (type Not, type (||), type (&&))
 
 type family BoolC (b :: Bool) :: Constraint where
   BoolC True  = ØC
   BoolC False = Fail
-
-type family (a :: Bool) || (b :: Bool) :: Bool where
-  True  || b = True
-  False || b = b
-infixr 2 ||
-
-type family (a :: Bool) && (b :: Bool) :: Bool where
-  True  && b = b
-  False && b = False
-infixr 3 &&
-
-type family Not (a :: Bool) :: Bool where
-  Not True  = False
-  Not False = True
 
 type a ==> b = Not a || b
 infixr 1 ==>
diff --git a/src/Type/Family/Nat.hs b/src/Type/Family/Nat.hs
--- a/src/Type/Family/Nat.hs
+++ b/src/Type/Family/Nat.hs
@@ -30,6 +30,7 @@
 module Type.Family.Nat where
 
 import Data.Type.Equality
+import Type.Family.Bool
 import Type.Family.Constraint
 import Type.Family.List
 import Type.Class.Witness
@@ -112,6 +113,26 @@
 
 ixCong :: (x ~ y,as ~ bs) :- (Ix x as ~ Ix y bs)
 ixCong = Sub Wit
+
+type family (x :: N) < (y :: N) :: Bool where
+  Z   < Z   = False
+  Z   < S y = True
+  S x < Z   = False
+  S x < S y = x < y
+infix 4 <
+
+type x <= y = (x == y) || (x < y)
+infix 4 <=
+
+type family (x :: N) > (y :: N) :: Bool where
+  Z   > Z   = False
+  Z   > S y = False
+  S x > Z   = True
+  S x > S y = x > y
+infix 4 >
+
+type x >= y = (x == y) || (x > y)
+infix 4 >=
 
 -- | Convenient aliases for low-value Peano numbers.
 type N0  = Z
diff --git a/type-combinators.cabal b/type-combinators.cabal
--- a/type-combinators.cabal
+++ b/type-combinators.cabal
@@ -1,5 +1,5 @@
 name: type-combinators
-version: 0.2.1.0
+version: 0.2.2.0
 category: Data
 synopsis: A collection of data types for type-level programming
 cabal-version: >=1.10