diff --git a/kind-apply.cabal b/kind-apply.cabal
--- a/kind-apply.cabal
+++ b/kind-apply.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                kind-apply
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            Utilities to work with lists of types
 description:         This packages reifies the concept of list of types, and application of those to list constructors.
 -- bug-reports:
diff --git a/src/Data/PolyKinded.hs b/src/Data/PolyKinded.hs
--- a/src/Data/PolyKinded.hs
+++ b/src/Data/PolyKinded.hs
@@ -15,7 +15,7 @@
   -- * Lists of types and application
   LoT(..), (:@@:)
   -- * Splitting types
-, SplitF, Nat(..), TyEnv(..), SplitN, Split
+, SplitF, Nat(..), TyEnv(..), SplitN
 ) where
 
 infixr 5 :&&:
@@ -64,11 +64,3 @@
 type family SplitN' (n :: Nat) (t :: d) (p :: LoT d) :: TyEnv where
   SplitN' 'Z     t            acc = 'TyEnv t acc
   SplitN' ('S n) (t (a :: l)) acc = SplitN' n t (a ':&&: acc)
-
--- | @Split t f x@ declares that the default way to split
--- the type @t@ is into a type constructor @f@ and a list
--- of types @x@.
---
--- > instance Split (Either a b) Either (a :&&: b :&&: LoT0)
-class (x ~ SplitF t f, t ~ (f :@@: x))
-      => Split t (f :: k) (x :: LoT k) | t -> k f x
diff --git a/src/Data/PolyKinded/Atom.hs b/src/Data/PolyKinded/Atom.hs
--- a/src/Data/PolyKinded/Atom.hs
+++ b/src/Data/PolyKinded/Atom.hs
@@ -24,10 +24,12 @@
 type V8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))
 type V9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))
 
+infixr 5 :&:
 data Atom d k where
-  Var    :: TyVar d k -> Atom d k
-  Kon    :: k         -> Atom d k
-  (:@:)  :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
+  Var   :: TyVar d k -> Atom d k
+  Kon   :: k         -> Atom d k
+  (:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
+  (:&:) :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint
 
 type f :$: x = 'Kon f ':@: x
 type a :~: b = 'Kon (~) ':@: a ':@: b
@@ -37,6 +39,7 @@
   Ty ('Var ('VS v)) (t ':&&: ts) = Ty ('Var v) ts
   Ty ('Kon t)       tys          = t
   Ty (f ':@: x)     tys          = (Ty f tys) (Ty x tys)
+  Ty (c ':&: d)     tys          = (Ty c tys, Ty d tys)
 
 type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where
   Satisfies '[]       tys = ()
diff --git a/src/Data/PolyKinded/Functor.hs b/src/Data/PolyKinded/Functor.hs
--- a/src/Data/PolyKinded/Functor.hs
+++ b/src/Data/PolyKinded/Functor.hs
@@ -23,8 +23,8 @@
 
 -- | The generalized version of 'fmap', 'bimap', 'dimap', and so on.
 -- This version uses 'Split' to obtain better type inference.
-kmapo :: forall t f v as bs. (Split t f as, KFunctor f v as bs)
-      => Mappings v as bs -> t -> f :@@: bs
+kmapo :: forall f v as bs. (KFunctor f v as bs)
+      => Mappings v as bs -> f :@@: as -> f :@@: bs
 kmapo = kfmap @_ @f
 
 -- ** Mappings of different variance