diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.2
+version:             0.2.1
 synopsis:            Poly-kinded, extensible ADTs
 homepage:            https://github.com/fumieval/extensible
 description:         Extensible Products/Unions
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
--- a/src/Data/Extensible/Inclusion.hs
+++ b/src/Data/Extensible/Inclusion.hs
@@ -21,7 +21,7 @@
 type xs ⊆ ys = Include ys xs
 
 -- | @ys@ contains @xs@
-type Include ys xs = Forall (Member ys) xs
+type Include ys = Forall (Member ys)
 
 -- | Reify the inclusion of type level sets.
 inclusion :: forall xs ys. Include ys xs => Position ys :* xs
@@ -31,6 +31,6 @@
 shrink :: (xs ⊆ ys) => h :* ys -> h :* xs
 shrink h = hmap (\pos -> hlookup pos h) inclusion
 
--- | /O(m log n)/ Embed to a larger union.
+-- | /O(log n)/ Embed to a larger union.
 spread :: (xs ⊆ ys) => h :| xs -> h :| ys
 spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
diff --git a/src/Data/Extensible/Plain.hs b/src/Data/Extensible/Plain.hs
--- a/src/Data/Extensible/Plain.hs
+++ b/src/Data/Extensible/Plain.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DataKinds, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Plain
@@ -12,6 +12,8 @@
 ------------------------------------------------------------------------
 module Data.Extensible.Plain (
   K0(..)
+  , AllOf
+  , OneOf
   , (<%)
   , pluck
   , bury
@@ -25,32 +27,46 @@
 import Data.Extensible.Match
 import Data.Typeable
 import Unsafe.Coerce
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable)
+import Control.Applicative
 -- | Just a value.
-newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable)
+newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable, Functor, Foldable, Traversable)
 
+instance Applicative K0 where
+  pure = K0
+  K0 f <*> K0 a = K0 (f a)
+
+instance Monad K0 where
+  return = K0
+  K0 a >>= k = k a
+
 instance Show a => Show (K0 a) where
   showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a
 
+type AllOf xs = K0 :* xs
+type OneOf xs = K0 :| xs
+
 -- | /O(log n)/ Add a plain value to a product.
-(<%) :: x -> K0 :* xs -> K0 :* (x ': xs)
+(<%) :: x -> AllOf xs -> AllOf (x ': xs)
 (<%) = unsafeCoerce (<:*)
 {-# INLINE (<%) #-}
 infixr 5 <%
 
 -- | Extract a plain value.
-pluck :: (x ∈ xs) => K0 :* xs -> x
+pluck :: (x ∈ xs) => AllOf xs -> x
 pluck = getK0 . hlookup membership
 
 -- | Embed a plain value.
-bury :: (x ∈ xs) => x -> K0 :| xs
+bury :: (x ∈ xs) => x -> OneOf xs
 bury = embed . K0
 
 -- | Naive pattern matching for a plain value.
-(<%|) :: (x -> r) -> (K0 :| xs -> r) -> K0 :| (x ': xs) -> r
+(<%|) :: (x -> r) -> (OneOf xs -> r) -> OneOf (x ': xs) -> r
 (<%|) = unsafeCoerce (<:|)
 
 -- | /O(log n)/ A lens for a plain value in a product.
-record :: (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))
+record :: (x ∈ xs, Functor f) => (x -> f x) -> (AllOf xs -> f (AllOf xs))
 record f = sector $ unsafeCoerce f `asTypeOf` (fmap K0 . f . getK0)
 {-# INLINE record #-}
 
@@ -58,3 +74,4 @@
 (<?%) :: (x -> a) -> Match K0 a :* xs -> Match K0 a :* (x ': xs)
 (<?%) = unsafeCoerce (<:*)
 infixr 1 <?%
+
diff --git a/src/Data/Extensible/Product.hs b/src/Data/Extensible/Product.hs
--- a/src/Data/Extensible/Product.hs
+++ b/src/Data/Extensible/Product.hs
@@ -18,6 +18,8 @@
   -- * Product
   (:*)(..)
   , (<:*)
+  , hhead
+  , htail
   , huncons
   , hmap
   , hzipWith
@@ -28,7 +30,8 @@
   , sector
   , sectorAt
   , Generate(..)
-  , Forall(..)) where
+  , Forall(..)
+  , ClassComp) where
 
 import Data.Extensible.Internal
 import Unsafe.Coerce
@@ -55,7 +58,11 @@
     . showString " <:* "
     . showsPrec 6 xs
 
--- | Extract the tail of the product.
+-- | /O(1)/ Extract the head element.
+hhead :: h :* (x ': xs) -> h x
+hhead (Tree a _ _) = a
+
+-- | /O(n)/ Extract the tail of the product.
 htail :: h :* (x ': xs) -> h :* xs
 htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
 htail (Tree _ Nil _) = unsafeCoerce Nil
@@ -98,12 +105,12 @@
 htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
 htraverse _ Nil = pure Nil
 
--- | Pick up an elemtnt.
+-- | /O(log n)/ Pick up an elemtnt.
 hlookup :: Position xs x -> h :* xs -> h x
 hlookup = view . sectorAt
 {-# INLINE hlookup #-}
 
--- | Composition for a class and a wrapper,
+-- | Composition for a class and a wrapper
 class c (h x) => ClassComp c h x
 instance c (h x) => ClassComp c h x
 
@@ -128,8 +135,8 @@
 newtype WrapOrd h x = WrapOrd { unwrapOrd :: h x -> h x -> Ordering }
 
 -- | /O(log n)/ A lens for a specific element.
-sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sector = sectorAt (membership :: Position xs x)
+sector :: (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+sector = sectorAt membership
 {-# INLINE sector #-}
 
 view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a
diff --git a/src/Data/Extensible/Union.hs b/src/Data/Extensible/Union.hs
--- a/src/Data/Extensible/Union.hs
+++ b/src/Data/Extensible/Union.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs, Rank2Types #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.Union
@@ -10,10 +10,12 @@
 -- Portability :  non-portable
 --
 ------------------------------------------------------------------------
-module Data.Extensible.Union (K1(..)
-  , (<?!)
+module Data.Extensible.Union (
+  (<$?~)
   , Union(..)
   , liftU
+  , Flux(..)
+  , mapFlux
   ) where
 
 import Data.Typeable
@@ -21,41 +23,30 @@
 import Data.Extensible.Sum
 import Data.Extensible.Product
 import Data.Extensible.Match
-import Unsafe.Coerce
 
--- | Wrap a type that has a kind @* -> *@.
-newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)
-
-instance Show (f a) => Show (K1 a f) where
-  showsPrec d (K1 a) = showParen (d > 10) $ showString "K1 " . showsPrec 11 a
-
--- | Prepend a clause for a parameterized value.
-(<?!) :: (f x -> a) -> Match (K1 x) a :* xs -> Match (K1 x) a :* (f ': fs)
-(<?!) = unsafeCoerce (<:*)
-infixr 1 <?!
+-- | A much more efficient representation for 'Union' of 'Functor's.
+newtype Union fs a = Union { getLeague :: Flux a :| fs } deriving Typeable
 
--- | A wrapper for @'K1' a ':|'' fs@ for having a kind @* -> *@.
-newtype Union fs a = Union { getUnion :: K1 a :| fs } deriving Typeable
+-- | fast fmap
+instance Functor (Union fs) where
+  fmap f (Union (UnionAt pos s)) = Union (UnionAt pos (mapFlux f s))
+  {-# INLINE fmap #-}
 
--- | /O(log n)/ Lift a value.
+-- | /O(log n)/ Embed a value.
 liftU :: (f ∈ fs) => f a -> Union fs a
-liftU = Union . embed . K1
+liftU = Union . embed . Flux id
 {-# INLINE liftU #-}
 
-instance Show (Union '[] a) where
-  show (Union u) = exhaust u
-
-instance (Show (f a), Show (Union fs a)) => Show (Union (f ': fs) a) where
-  showsPrec d (Union u) = (\(K1 f) -> showParen (d > 10) $ showString "liftU " . showsPrec 11 f)
-    <:| showsPrec d . Union
-    $ u
+-- | Flipped <http://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Coyoneda.html Coyoneda>
+data Flux a f where
+  Flux :: (a -> b) -> f a -> Flux b f
 
-instance Functor (Union '[]) where
-  fmap _ = exhaust . getUnion
+-- | 'fmap' for the content.
+mapFlux :: (a -> b) -> Flux a f -> Flux b f
+mapFlux f (Flux g m) = Flux (f . g) m
+{-# INLINE mapFlux #-}
 
--- | slow fmap
-instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where
-  fmap f (Union (UnionAt pos (K1 h))) = case runPosition pos of
-    Left Refl -> Union $ UnionAt pos $ K1 (fmap f h)
-    Right pos' -> case fmap f (Union (UnionAt pos' (K1 h))) of
-      Union (UnionAt _ h') -> Union (UnionAt (unsafeCoerce pos) h')
+-- | Prepend a clause for @'Match' ('Flux' x)@ as well as ('<?!').
+(<$?~) :: (forall b. f b -> (b -> x) -> a) -> Match (Flux x) a :* fs -> Match (Flux x) a :* (f ': fs)
+(<$?~) f = (<:*) $ Match $ \(Flux g m) -> f m g
+infixr 1 <$?~