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))

 divided = divide id

Redundant, but provided for symmetry.

 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

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!

 chosen = choose id

 lost = lose id