diff --git a/Data/Functor/Adjunction.hs b/Data/Functor/Adjunction.hs
--- a/Data/Functor/Adjunction.hs
+++ b/Data/Functor/Adjunction.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
+{-# LANGUAGE ImplicitParams #-}
 
 -------------------------------------------------------------------------------------------
 -- |
@@ -15,8 +16,13 @@
   ( Adjunction(..)
   , tabulateAdjunction
   , indexAdjunction
+  , zipR, unzipF
+  , inhabitedL
+  , cozipL, uncozipF
   ) where
 
+import Control.Applicative
+import Control.Arrow ((&&&), (|||))
 import Control.Monad.Instances ()
 import Control.Monad.Trans.Identity
 
@@ -29,27 +35,72 @@
 import Data.Functor.Identity
 import Data.Functor.Compose
 
+import Data.Void
+
 -- | An adjunction between Hask and Hask.
 --
+-- Minimal definition: both 'unit' and 'counit' or both 'leftAdjunct' and 'rightAdjunct', 
+-- subject to the constraints imposed by the default definitions that the following laws
+-- should hold.
+--
+-- > unit = leftAdjunct id
+-- > counit = rightAdjunct id
+-- > leftAdjunct f = fmap f . unit
+-- > rightAdjunct f = counit . fmap f
+--
+-- Any implementation is required to ensure that 'leftAdjunct' and 'rightAdjunct' witness
+-- an isomorphism from @Nat (f a, b)@ to @Nat (a, g b)@
+--
 -- > rightAdjunct unit = id
 -- > leftAdjunct counit = id 
-class (Functor f, Representable g) => Adjunction f g | f -> g, g -> f where
-  unit :: a -> g (f a)
-  counit :: f (g a) -> a
-  leftAdjunct :: (f a -> b) -> a -> g b
-  rightAdjunct :: (a -> g b) -> f a -> b
+class (Functor f, Representable u) => Adjunction f u | f -> u, u -> f where
+  unit :: a -> u (f a)
+  counit :: f (u a) -> a
+  leftAdjunct :: (f a -> b) -> a -> u b
+  rightAdjunct :: (a -> u b) -> f a -> b
   
   unit = leftAdjunct id
   counit = rightAdjunct id
   leftAdjunct f = fmap f . unit
   rightAdjunct f = counit . fmap f
 
-tabulateAdjunction :: Adjunction f g => (f () -> b) -> g b
+-- | Every right adjoint is representable by its left adjoint applied to a unit element
+-- 
+-- Use this definition and the primitives in Data.Functor.Representable to meet the requirements
+-- of the superclasses of Representable.
+tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
 tabulateAdjunction f = leftAdjunct f ()
 
-indexAdjunction :: Adjunction f g => g b -> f a -> b
+-- | This definition admits a default definition for the 'index' method of 'Index", one of the
+-- superclasses of Representable.
+indexAdjunction :: Adjunction f u => u b -> f a -> b
 indexAdjunction = rightAdjunct . const
 
+-- | A right adjoint functor admits an intrinsic notion of zipping
+zipR :: Adjunction f u => (u a, u b) -> u (a, b)
+zipR = leftAdjunct (rightAdjunct fst &&& rightAdjunct snd)
+
+-- | Every functor in Haskell permits unzipping
+unzipF :: Functor u => u (a, b) -> (u a, u b)
+unzipF = fmap fst &&& fmap snd
+
+-- | A left adjoint must be inhabited, or we can derive bottom
+inhabitedL :: Adjunction f u => f Void -> Void
+inhabitedL = rightAdjunct absurd
+
+-- | And a left adjoint must be inhabited by exactly one element
+cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
+cozipL = rightAdjunct (leftAdjunct Left ||| leftAdjunct Right)
+
+-- | Every functor in Haskell permits 'uncozipping'
+uncozipF :: Functor f => Either (f a) (f b) -> f (Either a b)
+uncozipF = fmap Left ||| fmap Right
+
+-- Requires deprecated Impredicative types
+
+-- limitR :: Adjunction f u => (forall a. u a) -> u (forall a. a)
+-- limitR = leftAdjunct (rightAdjunct (\(x :: forall a. a) -> x))
+
 instance Adjunction ((,)e) ((->)e) where
   leftAdjunct f a e = f (e, a)
   rightAdjunct f ~(e, a) = f a e
@@ -64,11 +115,11 @@
 
 instance Adjunction w m => Adjunction (EnvT e w) (ReaderT e m) where
   unit = ReaderT . flip fmap EnvT . flip leftAdjunct
-  counit (EnvT e w) = counit $ fmap (flip runReaderT e) w
+  counit (EnvT e w) = rightAdjunct (flip runReaderT e) w
 
 instance Adjunction m w => Adjunction (WriterT s m) (TracedT s w) where
   unit = TracedT . leftAdjunct (\ma s -> WriterT (fmap (\a -> (a, s)) ma)) 
-  -- counit (WriterT mwas) = 
+  counit  = rightAdjunct (\(t, s) -> ($s) <$> runTracedT t) . runWriterT
 
 instance (Adjunction f g, Adjunction f' g') => Adjunction (Compose f' f) (Compose g g') where
   unit = Compose . leftAdjunct (leftAdjunct Compose) 
diff --git a/adjunctions.cabal b/adjunctions.cabal
--- a/adjunctions.cabal
+++ b/adjunctions.cabal
@@ -1,6 +1,6 @@
 name:          adjunctions
 category:      Data Structures, Adjunctions
-version:       0.8.0
+version:       0.8.1
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -31,7 +31,8 @@
     representable-functors >= 0.2 && < 0.3,
     semigroups >= 0.3.4 && < 0.4,
     semigroupoids >= 1.1.1 && < 1.2.0,
-    transformers >= 0.2.0 && < 0.3
+    transformers >= 0.2.0 && < 0.3,
+    void >= 0.4 && < 0.5
 
   exposed-modules:
     Data.Functor.Adjunction