diff --git a/Data/Exists/Constrained.hs b/Data/Exists/Constrained.hs
--- a/Data/Exists/Constrained.hs
+++ b/Data/Exists/Constrained.hs
@@ -1,7 +1,10 @@
-{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
 module Data.Exists.Constrained where
 
 import Data.Typeable
 
 -- | Dependent sum
-data E c a = forall k . (Typeable k, c k) => E { unE :: a k }
+data E c a = ∀ k . (Typeable k, c k) => E { unE :: a k }
+
+liftE :: (∀ k . c k => a k -> b k) -> E c a -> E c b
+liftE f (E a) = E (f a)
diff --git a/exist.cabal b/exist.cabal
--- a/exist.cabal
+++ b/exist.cabal
@@ -1,5 +1,5 @@
 name:                exist
-version:             0.1.0.0
+version:             0.1.1.0
 synopsis:            Dependent sum type
 -- description:
 license:             BSD3