diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,7 @@
+1.1.1
+-----
+* Added `Data.Functor.Contravariant.Applicative`
+
 1.0
 ---
 * Removed `Day` convolution. The right adjoint of Day convolution is in `kan-extensions` as the right Kan lift. Moving these there to avoid forcing orphan instances. It also rather dramatically reduces the number of extensions required.
diff --git a/Data/Functor/Contravariant/Compose.hs b/Data/Functor/Contravariant/Compose.hs
--- a/Data/Functor/Contravariant/Compose.hs
+++ b/Data/Functor/Contravariant/Compose.hs
@@ -15,13 +15,16 @@
   , ComposeCF(..)
   ) where
 
+import Control.Arrow
+import Control.Applicative
 import Data.Functor.Contravariant
+import Data.Functor.Contravariant.Divisible
 
 -- | Composition of two contravariant functors
 newtype Compose f g a = Compose { getCompose :: f (g a) }
 
 instance (Contravariant f, Contravariant g) => Functor (Compose f g) where
-    fmap f (Compose x) = Compose (contramap (contramap f) x)
+   fmap f (Compose x) = Compose (contramap (contramap f) x)
 
 -- | Composition of covariant and contravariant functors
 newtype ComposeFC f g a = ComposeFC { getComposeFC :: f (g a) }
@@ -32,6 +35,10 @@
 instance (Functor f, Functor g) => Functor (ComposeFC f g) where
     fmap f (ComposeFC x) = ComposeFC (fmap (fmap f) x)
 
+instance (Applicative f, Divisible g) => Divisible (ComposeFC f g) where
+  conquer = ComposeFC $ pure conquer
+  divide abc (ComposeFC fb) (ComposeFC fc) = ComposeFC $ divide abc <$> fb <*> fc
+
 -- | Composition of contravariant and covariant functors
 newtype ComposeCF f g a = ComposeCF { getComposeCF :: f (g a) }
 
@@ -40,3 +47,12 @@
 
 instance (Functor f, Functor g) => Functor (ComposeCF f g) where
     fmap f (ComposeCF x) = ComposeCF (fmap (fmap f) x)
+
+instance (Divisible f, Applicative g) => Divisible (ComposeCF f g) where
+  conquer = ComposeCF conquer
+  divide abc (ComposeCF fb) (ComposeCF fc) = ComposeCF $ divide (funzip . fmap abc) fb fc
+
+funzip :: Functor f => f (a, b) -> (f a, f b)
+funzip = fmap fst &&& fmap snd
+
+-- | Composition of contravariant and covariant functors
diff --git a/Data/Functor/Contravariant/Divisible.hs b/Data/Functor/Contravariant/Divisible.hs
new file mode 100644
--- /dev/null
+++ b/Data/Functor/Contravariant/Divisible.hs
@@ -0,0 +1,179 @@
+module Data.Functor.Contravariant.Divisible
+  (
+  -- * Contravariant Applicative
+    Divisible(..), divided, conquered, liftD
+  -- * Contravariant Alternative
+  , Decidable(..), chosen, lost
+  ) where
+
+import Data.Functor.Contravariant
+import Data.Monoid
+import Data.Void
+
+--------------------------------------------------------------------------------
+-- * Contravariant Applicative
+--------------------------------------------------------------------------------
+
+-- |
+--
+-- A 'Divisible' contravariant functor is the contravariant analogue of 'Applicative'.
+--
+-- In denser jargon, a 'Divisible' contravariant functor is a monoid object in the category
+-- of presheaves from Hask to Hask, equipped with Day convolution mapping the Cartesian
+-- product of the source to the Cartesian product of the target.
+--
+-- By way of contrast, an 'Applicative' functor can be viewed as a monoid object in the
+-- category of copresheaves from Hask to Hask, equipped with Day convolution mapping the
+-- Cartesian product of the source to the Cartesian product of the target.
+--
+-- Given the canonical diagonal morphism:
+--
+-- @
+-- delta a = (a,a)
+-- @
+-- 
+-- @'divide' 'delta'@ should be associative with 'conquer' as a unit
+--
+-- @
+-- 'divide' 'delta' m 'conquer' = m
+-- 'divide' 'delta' 'conquer' m = m
+-- 'divide' 'delta' ('divide' 'delta' m n) o = 'divide' 'delta' m ('divide' 'delta' n o)
+-- @
+--
+-- With more general arguments you'll need to reassociate and project using the monoidal
+-- structure of the source category. (Here fst and snd are used in lieu of the more restricted
+-- lambda and rho, but this construction works with just a monoidal category.)
+--
+-- @
+-- 'divide' f m 'conquer' = 'contramap' ('fst' . f) m
+-- 'divide' f 'conquer' m = 'contramap' ('snd' . f) m
+-- 'divide' f ('divide' g m n) o = 'divide' f' m ('divide' 'id' n o) where
+--   f' a = case f a of (bc,d) -> case g bc of (b,c) -> (a,(b,c))
+-- @
+class Contravariant f => Divisible f where
+  divide  :: (a -> (b, c)) -> f b -> f c -> f a
+  -- | The underlying theory would suggest that this should be:
+  --
+  -- @
+  -- conquer :: (a -> ()) -> f a
+  -- @
+  --
+  -- However, as we are working over a Cartesian category (Hask) and the Cartesian product, such an input
+  -- morphism is uniquely determined to be @'const' 'mempty'@, so we elide it.
+  conquer :: f a
+
+-- |
+-- @
+-- 'divided' = 'divide' 'id'
+-- @
+divided :: Divisible f => f a -> f b -> f (a, b)
+divided = divide id
+
+-- | Redundant, but provided for symmetry.
+--
+-- @
+-- 'conquered' = 'conquer
+-- @
+conquered :: Divisible f => f ()
+conquered = conquer
+
+
+-- |
+-- This is the divisible analogue of 'liftA'. It gives a viable default definition for 'contramap' in terms
+-- of the members of 'Divisible'.
+--
+-- @
+-- 'liftD' f = 'divide' ((,) () . f) 'conquer'
+-- @
+liftD :: Divisible f => (a -> b) -> f b -> f a
+liftD f = divide ((,) () . f) conquer
+  
+instance Monoid r => Divisible (Op r) where
+  divide f (Op g) (Op h) = Op $ \a -> case f a of
+    (b, c) -> g b `mappend` h c
+  conquer = Op $ const mempty
+
+instance Divisible Comparison where
+  divide f (Comparison g) (Comparison h) = Comparison $ \a b -> case f a of
+    (a',a'') -> case f b of
+      (b',b'') -> g a' b' `mappend` h a'' b''
+  conquer = Comparison $ \_ _ -> EQ
+
+instance Divisible Equivalence where
+  divide f (Equivalence g) (Equivalence h) = Equivalence $ \a b -> case f a of
+    (a',a'') -> case f b of
+      (b',b'') -> g a' b' && h a'' b''
+  conquer = Equivalence $ \_ _ -> True
+
+instance Divisible Predicate where
+  divide f (Predicate g) (Predicate h) = Predicate $ \a -> case f a of
+    (b, c) -> g b && h c
+  conquer = Predicate $ const True
+
+--------------------------------------------------------------------------------
+-- * Contravariant Alternative
+--------------------------------------------------------------------------------
+
+-- |
+--
+-- A 'Divisible' contravariant functor is a monoid object in the category of presheaves 
+-- from Hask to Hask, equipped with Day convolution mapping the cartesian product of the
+-- source to the Cartesian product of the target.
+--
+-- @
+-- 'choose' Left m ('lose' f)  = m
+-- 'choose' Right ('lose' f) m = m
+-- 'choose' f ('choose' g m n) o = 'divide' f' m ('divide' 'id' n o) where
+--   f' bcd = 'either' ('either' 'id' ('Right' . 'Left') . g) ('Right' . 'Right') . f
+-- @
+--
+-- In addition, we expect the same kind of distributive law as is satisfied by the usual
+-- covariant 'Alternative', w.r.t 'Applicative', which should be fully formulated and
+-- added here at some point!
+
+class Divisible f => Decidable f where
+  -- | The only way to win is not to play.
+  lose :: (a -> Void) -> f a
+  choose :: (a -> Either b c) -> f b -> f c -> f a
+
+-- |
+-- @
+-- 'lost' = 'lose' 'id'
+-- @
+lost :: Decidable f => f Void
+lost = lose id
+
+-- |
+-- @
+-- 'chosen' = 'choose' 'id'
+-- @
+chosen :: Decidable f => f b -> f c -> f (Either b c)
+chosen = choose id
+
+instance Decidable Comparison where
+  lose f = Comparison $ \a _ -> absurd (f a)
+  choose f (Comparison g) (Comparison h) = Comparison $ \a b -> case f a of
+    Left c -> case f b of
+      Left d -> g c d
+      Right{} -> LT
+    Right c -> case f b of
+      Left{} -> GT
+      Right d -> h c d
+
+instance Decidable Equivalence where
+  lose f = Equivalence $ \a -> absurd (f a)
+  choose f (Equivalence g) (Equivalence h) = Equivalence $ \a b -> case f a of
+    Left c -> case f b of
+      Left d -> g c d
+      Right{} -> False
+    Right c -> case f b of
+      Left{} -> False
+      Right d -> h c d
+
+instance Decidable Predicate where
+  lose f = Predicate $ \a -> absurd (f a)
+  choose f (Predicate g) (Predicate h) = Predicate $ either g h . f
+
+instance Monoid r => Decidable (Op r) where
+  lose f = Op $ absurd . f
+  choose f (Op g) (Op h) = Op $ either g h . f
diff --git a/contravariant.cabal b/contravariant.cabal
--- a/contravariant.cabal
+++ b/contravariant.cabal
@@ -1,6 +1,6 @@
 name:          contravariant
 category:      Control, Data
-version:       1.1
+version:       1.2
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -34,7 +34,8 @@
     base < 5,
     semigroups >= 0.15.2 && < 1,
     transformers >= 0.2 && < 0.5,
-    transformers-compat >= 0.3 && < 1
+    transformers-compat >= 0.3 && < 1,
+    void >= 0.6 && < 1
 
   if flag(tagged) && !impl(ghc >= 7.7)
     build-depends: tagged >= 0.4.4 && < 1
@@ -44,6 +45,7 @@
 
   exposed-modules:
     Data.Functor.Contravariant
+    Data.Functor.Contravariant.Divisible
     Data.Functor.Contravariant.Compose
 
   ghc-options: -Wall