diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 dist/
+dist-newstyle/
 .hsenv/
 docs
 wiki
@@ -12,3 +13,22 @@
 *.hi
 *~
 *#
+:w
+.stack-work/
+cabal-dev
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*
diff --git a/.hlint.yaml b/.hlint.yaml
new file mode 100644
--- /dev/null
+++ b/.hlint.yaml
@@ -0,0 +1,71 @@
+- arguments: [-XCPP]
+
+- extensions:
+  - default: false # all extension are banned by default
+  - name:
+    - CPP
+    - DeriveFunctor
+    - FlexibleContexts
+    - FlexibleInstances
+    - FunctionalDependencies
+    - GADTs
+    - InstanceSigs
+    - MultiParamTypeClasses
+    - PolyKinds
+    - RankNTypes
+    - Safe
+    - ScopedTypeVariables
+    - Trustworthy
+    - TypeFamilies
+    - TypeOperators
+    - UndecidableInstances
+
+- functions:
+  - {name: unsafeCoerce, within: []} # banned
+
+- ignore:
+    name: Use const
+    within:
+    - Data.Profunctor.Types
+
+- ignore:
+    name: Avoid lambda
+    within:
+    - Data.Profunctor.Choice
+    - Data.Profunctor.Traversing
+
+- ignore:
+    name: Use fmap
+    within:
+    - Data.Profunctor.Composition
+    - Data.Profunctor.Strong
+    - Data.Profunctor.Unsafe
+
+- ignore:
+    name: Avoid lambda
+    within: Data.Profunctor.Strong
+
+- ignore:
+    name: Redundant lambda
+    within: Data.Profunctor.Unsafe
+
+- ignore:
+    name: Collapse lambdas
+    within: Data.Profunctor.Unsafe
+
+- ignore:
+    name: Eta reduce
+    within:
+    - Data.Profunctor.Mapping
+    - Data.Profunctor.Choice
+    - Data.Profunctor.Strong
+
+- ignore:
+    name: "Use tuple-section"
+
+- ignore:
+    name: "Avoid lambda using `infix`"
+
+- fixity: "infixr 9 #."
+- fixity: "infixl 8 .#"
+- fixity: "infixr 0 :->"
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
--- a/.travis.yml
+++ /dev/null
@@ -1,66 +0,0 @@
-# NB: don't set `language: haskell` here
-
-# See also https://github.com/hvr/multi-ghc-travis for more information
-env:
- - GHCVER=7.0.1 CABALVER=1.16
- - GHCVER=7.0.4 CABALVER=1.16
- - GHCVER=7.2.2 CABALVER=1.16
- - GHCVER=7.4.2 CABALVER=1.16
- - GHCVER=7.6.3 CABALVER=1.16
- - GHCVER=7.8.4 CABALVER=1.18
- - GHCVER=7.10.1 CABALVER=1.22
- - GHCVER=head CABALVER=1.22
-
-matrix:
-  allow_failures:
-   - env: GHCVER=7.0.1 CABALVER=1.16
-   - env: GHCVER=7.0.4 CABALVER=1.16
-   - env: GHCVER=7.2.2 CABALVER=1.16
-   - env: GHCVER=head CABALVER=1.22
-
-# Note: the distinction between `before_install` and `install` is not
-#       important.
-before_install:
- - travis_retry sudo add-apt-repository -y ppa:hvr/ghc
- - travis_retry sudo apt-get update
- - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER
- - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
- - cabal --version
-
-install:
- - travis_retry cabal update
- - cabal install --only-dependencies
- - travis_retry sudo apt-get -q -y install hlint || cabal install hlint
-
-# Here starts the actual work to be performed for the package under
-# test; any command which exits with a non-zero exit code causes the
-# build to fail.
-script:
- # -v2 provides useful information for debugging
- - cabal configure -v2
-
- # this builds all libraries and executables
- # (including tests/benchmarks)
- - cabal build
-
- # tests that a source-distribution can be generated
- - cabal sdist
- - hlint src --cpp-define HLINT
-
- # check that the generated source-distribution can be built & installed
- - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ;
-   cd dist/;
-   if [ -f "$SRC_TGZ" ]; then
-      cabal install --force-reinstalls "$SRC_TGZ";
-   else
-      echo "expected '$SRC_TGZ' not found";
-      exit 1;
-   fi
-
-notifications:
-  irc:
-    channels:
-      - "irc.freenode.org#haskell-lens"
-    skip_join: true
-    template:
-      - "\x0313profunctors\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,89 @@
+5.6.3 [2025.06.17]
+------------------
+* Drop support for pre-8.0 versions of GHC.
+
+5.6.2 [2021.02.17]
+------------------
+* Add `Semigroup` and `Monoid` instances for `Forget`
+
+5.6.1 [2020.12.31]
+------------------
+* Add `Functor` instances for `PastroSum`, `CopastroSum`, `Environment`,
+  `FreeMapping`, `Pastro`, `Copastro`, `FreeTraversing`, and `Coyoneda`.
+* Explicitly mark modules as `Safe`.
+
+5.6 [2020.10.01]
+----------------
+* Enable the `PolyKinds` extension. The following datatypes now have
+  polymorphic kinds: `(:->)`, `Cayley`, `Procompose`, `Rift`,
+  `ProfunctorFunctor`, `Ran`, `Codensity`, `Prep`, `Coprep`, `Star`, `Costar`,
+  `WrappedArrow`, `Forget`.
+* Allow building with GHC 9.0.
+
+5.5.2 [2020.02.13]
+------------------
+* Add `Cochoice`, `Costrong`, `Closed`, `Traversing`, and `Mapping` instances
+  for `Cayley`.
+* Add `Mapping` and `Traversing` instances for `Tannen`.
+
+5.5.1 [2019.11.26]
+------------------
+* Add `Choice`, `Cochoice`, `Closed`, `Strong`, and `Costrong` instances for
+  `Data.Bifunctor.Sum`.
+
+5.5 [2019.09.06]
+----------------
+* Change the type of `roam` to make it actually useful.
+* Add a `Cochoice` instance for `Forget`.
+
+5.4 [2019.05.10]
+----------------
+* Add `wander`-like combinator `roam` to `Mapping`.
+* Remove illegal `instance Choice (Costar w)`.
+* Add `strong` combinator #62.
+* Only depend on `semigroups` before GHC 8.0.
+* Add `Contravariant` instances for `Star` and `Forget`.
+
+5.3 [2018.07.02]
+----------------
+* Generalize the types of `(#.)` and `(.#)`. Before, they were:
+
+  ```haskell
+  (#.) :: (Profunctor p, Coercible c b) => (b -> c) -> p a b    -> p a c
+  (.#) :: (Profunctor p, Coercible b a) => p b c    -> (a -> b) -> p a c
+  ```
+
+  Now, they are:
+
+  ```haskell
+  (#.) :: (Profunctor p, Coercible c b) => q b c    -> p a b    -> p a c
+  (.#) :: (Profunctor p, Coercible b a) => p b c    -> q a b    -> p a c
+  ```
+* Drop support for GHC < 7.8.
+* Add a `Profunctor` instance for `Data.Bifunctor.Sum`.
+
+5.2.2 [2018.01.18]
+------------------
+* Add `Semigroup` instances for `Closure` and `Tambara`
+
+5.2.1
+-----
+* Allow `base-orphans-0.6`.
+* Add `Traversing` instance for `Forget`
+* Add `Traversing` and `Mapping` instances for `Procompose`
+* Add `Category` instance for `Star`
+* Add `mapCayley` to `Data.Profunctor.Cayley`
+* Add `pastro` and `unpastro` to `Data.Profunctor.Strong`.
+* Add `dimapWandering`, `lmapWandering`, and `rmapWandering` to `Data.Profunctor.Traversing`
+* Add documentation stating the laws for various profunctors.
+* Introduce the `Data.Profunctor.Yoneda` module.
+
+5.2
+---
+* Renamed `Cotambara` to `TambaraChoice` and `Pastro` to `PastroChoice`.
+* Added a true `Cotambara` and `Copastro` construction for (co)freely generating costrength, along with `CotambaraSum` and `CopastroSum` variants.
+* Engaged in a fair bit of bikeshedding about the module structure for lesser used modules in this package.
+
 5.1.2
 -----
 * Added `Prep` and `Coprep` along with witnesses to the adjunctions `Prep -| Star : [Hask,Hask] -> Prof` and `Coprep -| Costar : [Hask,Hask]^op -> Prof`.
@@ -25,7 +111,7 @@
 -
 * `UpStar` and `DownStar` have become `Star` and `Costar`. `Star` is analogous to `Kleisli`, `Costar` is analogous to `Cokleisli`.
 * Split representability into sieves and representability.
-* Moved `Data.Profunctor.Collage` to `semigroupoids` 5, and removed the `semigroupoids` dependency. 
+* Moved `Data.Profunctor.Collage` to `semigroupoids` 5, and removed the `semigroupoids` dependency.
 * Rather greatly widened the range of GHC versions we can support.
 
 4.4.1
diff --git a/HLint.hs b/HLint.hs
deleted file mode 100644
--- a/HLint.hs
+++ /dev/null
@@ -1,1 +0,0 @@
-ignore "use const"
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2011-2013 Edward Kmett
+Copyright 2011-2015 Edward Kmett
 
 All rights reserved.
 
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,7 +1,7 @@
 Profunctors
 ===========
 
-[![Hackage](https://img.shields.io/hackage/v/profunctors.svg)](https://hackage.haskell.org/package/profunctors) [![Build Status](https://secure.travis-ci.org/ekmett/profunctors.png?branch=master)](http://travis-ci.org/ekmett/profunctors)
+[![Hackage](https://img.shields.io/hackage/v/profunctors.svg)](https://hackage.haskell.org/package/profunctors) [![Build Status](https://github.com/ekmett/profunctors/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/profunctors/actions?query=workflow%3AHaskell-CI)
 
 Profunctors for Haskell.
 
diff --git a/profunctors.cabal b/profunctors.cabal
--- a/profunctors.cabal
+++ b/profunctors.cabal
@@ -1,6 +1,6 @@
 name:          profunctors
 category:      Control, Categories
-version:       5.1.2
+version:       5.6.3
 license:       BSD3
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -11,49 +11,71 @@
 bug-reports:   http://github.com/ekmett/profunctors/issues
 copyright:     Copyright (C) 2011-2015 Edward A. Kmett
 synopsis:      Profunctors
-description:   Profunctors
-tested-with:   GHC==7.0.1, GHC == 7.0.4, GHC == 7.2.2, GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.1
+description:   Profunctors.
+tested-with:   GHC == 8.0.2
+             , GHC == 8.2.2
+             , GHC == 8.4.4
+             , GHC == 8.6.5
+             , GHC == 8.8.4
+             , GHC == 8.10.7
+             , GHC == 9.0.2
+             , GHC == 9.2.8
+             , GHC == 9.4.8
+             , GHC == 9.6.6
+             , GHC == 9.8.4
+             , GHC == 9.10.1
+             , GHC == 9.12.2
 build-type:    Simple
 extra-source-files:
   .ghci
   .gitignore
-  .travis.yml
+  .hlint.yaml
   .vim.custom
   README.markdown
   CHANGELOG.markdown
-  HLint.hs
 
 source-repository head
   type: git
-  location: git://github.com/ekmett/profunctors.git
+  location: https://github.com/ekmett/profunctors.git
 
 library
   build-depends:
-    base                >= 4     && < 5,
-    bifunctors          >= 5     && < 6,
-    comonad             >= 4     && < 5,
-    contravariant       >= 1     && < 2,
-    distributive        >= 0.4.4 && < 1,
-    tagged              >= 0.4.4 && < 1,
-    transformers        >= 0.2   && < 0.5
-
+    base                >= 4.9     && < 5,
+    base-orphans        >= 0.8.4   && < 0.10,
+    bifunctors          >= 5.5.9   && < 6,
+    comonad             >= 5.0.8   && < 6,
+    contravariant       >= 1.5.3   && < 2,
+    distributive        >= 0.5.2   && < 1,
+    tagged              >= 0.8.6.1 && < 1,
+    transformers        >= 0.3     && < 0.7
   exposed-modules:
     Data.Profunctor
     Data.Profunctor.Adjunction
     Data.Profunctor.Cayley
+    Data.Profunctor.Choice
     Data.Profunctor.Closed
-    Data.Profunctor.Codensity
     Data.Profunctor.Composition
+    Data.Profunctor.Mapping
     Data.Profunctor.Monad
-    Data.Profunctor.Monoid
     Data.Profunctor.Ran
     Data.Profunctor.Rep
     Data.Profunctor.Sieve
-    Data.Profunctor.Tambara
-    Data.Profunctor.Trace
+    Data.Profunctor.Strong
+    Data.Profunctor.Traversing
+    Data.Profunctor.Types
     Data.Profunctor.Unsafe
+    Data.Profunctor.Yoneda
 
-  ghc-options:     -Wall -O2
+  ghc-options:     -Wall -O2 -Wno-trustworthy-safe
+
+  if impl(ghc >= 8.6)
+    ghc-options: -Wno-star-is-type
+
+  if impl(ghc >= 9.0)
+    -- these flags may abort compilation with GHC-8.10
+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
+
   hs-source-dirs:  src
 
   default-language: Haskell2010
@@ -62,5 +84,6 @@
     GADTs
     FlexibleContexts
     FlexibleInstances
+    InstanceSigs
     UndecidableInstances
     TypeFamilies
diff --git a/src/Data/Profunctor.hs b/src/Data/Profunctor.hs
--- a/src/Data/Profunctor.hs
+++ b/src/Data/Profunctor.hs
@@ -1,13 +1,7 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE Safe #-}
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2011-2013 Edward Kmett,
+-- Copyright   :  (C) 2011-2015 Edward Kmett,
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -28,7 +22,12 @@
     Profunctor(dimap,lmap,rmap)
   -- ** Profunctorial Strength
   , Strong(..)
+  , uncurry'
   , Choice(..)
+  -- ** Closed
+  , Closed(..)
+  , curry'
+  , Mapping(..)
   -- ** Profunctorial Costrength
   , Costrong(..)
   , Cochoice(..)
@@ -37,401 +36,11 @@
   , Costar(..)
   , WrappedArrow(..)
   , Forget(..)
-#ifndef HLINT
   , (:->)
-#endif
   ) where
 
-import Control.Applicative hiding (WrappedArrow(..))
-import Control.Arrow
-import Control.Category
-import Control.Comonad
-import Control.Monad (liftM, MonadPlus(..))
-import Control.Monad.Fix
-import Data.Distributive
-import Data.Foldable
-import Data.Monoid
-import Data.Tagged
-import Data.Traversable
-import Data.Tuple
-import Data.Profunctor.Unsafe
-import Prelude hiding (id,(.),sequence)
-
-#if __GLASGOW_HASKELL__ >= 708
-import Data.Coerce
-#else
-import Unsafe.Coerce
-#endif
-
-infixr 0 :->
-type p :-> q = forall a b. p a b -> q a b
-
-------------------------------------------------------------------------------
--- Star
-------------------------------------------------------------------------------
-
--- | Lift a 'Functor' into a 'Profunctor' (forwards).
-newtype Star f d c = Star { runStar :: d -> f c }
-
-instance Functor f => Profunctor (Star f) where
-  dimap ab cd (Star bfc) = Star (fmap cd . bfc . ab)
-  {-# INLINE dimap #-}
-  lmap k (Star f) = Star (f . k)
-  {-# INLINE lmap #-}
-  rmap k (Star f) = Star (fmap k . f)
-  {-# INLINE rmap #-}
-  -- We cannot safely overload ( #. ) because we didn't write the 'Functor'.
-#if __GLASGOW_HASKELL__ >= 708
-  p .# _ = coerce p
-#else
-  p .# _ = unsafeCoerce p
-#endif
-  {-# INLINE ( .# ) #-}
-
-instance Functor f => Functor (Star f a) where
-  fmap = rmap
-  {-# INLINE fmap #-}
-
-instance Applicative f => Applicative (Star f a) where
-  pure a = Star $ \_ -> pure a
-  Star ff <*> Star fx = Star $ \a -> ff a <*> fx a
-  Star ff  *> Star fx = Star $ \a -> ff a  *> fx a
-  Star ff <*  Star fx = Star $ \a -> ff a <*  fx a
-
-instance Alternative f => Alternative (Star f a) where
-  empty = Star $ \_ -> empty
-  Star f <|> Star g = Star $ \a -> f a <|> g a
-
-instance Monad f => Monad (Star f a) where
-#if __GLASGOW_HASKELL__ < 710
-  return a = Star $ \_ -> return a
-#endif
-  Star m >>= f = Star $ \ e -> do
-    a <- m e
-    runStar (f a) e
-
-instance MonadPlus f => MonadPlus (Star f a) where
-  mzero = Star $ \_ -> mzero
-  Star f `mplus` Star g = Star $ \a -> f a `mplus` g a
-
-instance Distributive f => Distributive (Star f a) where
-  distribute fs = Star $ \a -> collect (($ a) .# runStar) fs
-
-------------------------------------------------------------------------------
--- Costar
-------------------------------------------------------------------------------
-
--- | Lift a 'Functor' into a 'Profunctor' (backwards).
-newtype Costar f d c = Costar { runCostar :: f d -> c }
-
-instance Functor f => Profunctor (Costar f) where
-  dimap ab cd (Costar fbc) = Costar (cd . fbc . fmap ab)
-  {-# INLINE dimap #-}
-  lmap k (Costar f) = Costar (f . fmap k)
-  {-# INLINE lmap #-}
-  rmap k (Costar f) = Costar (k . f)
-  {-# INLINE rmap #-}
-#if __GLASGOW_HASKELL__ >= 708
-  ( #. ) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
-#else
-  ( #. ) _ = unsafeCoerce
-#endif
-  {-# INLINE ( #. ) #-}
-  -- We cannot overload ( .# ) because we didn't write the 'Functor'.
-
-instance Distributive (Costar f d) where
-  distribute fs = Costar $ \gd -> fmap (($ gd) .# runCostar) fs
-
-instance Functor (Costar f a) where
-  fmap k (Costar f) = Costar (k . f)
-  {-# INLINE fmap #-}
-  a <$ _ = Costar $ \_ -> a
-  {-# INLINE (<$) #-}
-
-instance Applicative (Costar f a) where
-  pure a = Costar $ \_ -> a
-  Costar ff <*> Costar fx = Costar $ \a -> ff a (fx a)
-  _ *> m = m
-  m <* _ = m
-
-instance Monad (Costar f a) where
-  return = pure
-  Costar m >>= f = Costar $ \ x -> runCostar (f (m x)) x
-
-------------------------------------------------------------------------------
--- Wrapped Profunctors
-------------------------------------------------------------------------------
-
--- | Wrap an arrow for use as a 'Profunctor'.
-newtype WrappedArrow p a b = WrapArrow { unwrapArrow :: p a b }
-
-instance Category p => Category (WrappedArrow p) where
-  WrapArrow f . WrapArrow g = WrapArrow (f . g)
-  {-# INLINE (.) #-}
-  id = WrapArrow id
-  {-# INLINE id #-}
-
-instance Arrow p => Arrow (WrappedArrow p) where
-  arr = WrapArrow . arr
-  {-# INLINE arr #-}
-  first = WrapArrow . first . unwrapArrow
-  {-# INLINE first #-}
-  second = WrapArrow . second . unwrapArrow
-  {-# INLINE second #-}
-  WrapArrow a *** WrapArrow b = WrapArrow (a *** b)
-  {-# INLINE (***) #-}
-  WrapArrow a &&& WrapArrow b = WrapArrow (a &&& b)
-  {-# INLINE (&&&) #-}
-
-instance ArrowZero p => ArrowZero (WrappedArrow p) where
-  zeroArrow = WrapArrow zeroArrow
-  {-# INLINE zeroArrow #-}
-
-instance ArrowChoice p => ArrowChoice (WrappedArrow p) where
-  left = WrapArrow . left . unwrapArrow
-  {-# INLINE left #-}
-  right = WrapArrow . right . unwrapArrow
-  {-# INLINE right #-}
-  WrapArrow a +++ WrapArrow b = WrapArrow (a +++ b)
-  {-# INLINE (+++) #-}
-  WrapArrow a ||| WrapArrow b = WrapArrow (a ||| b)
-  {-# INLINE (|||) #-}
-
-instance ArrowApply p => ArrowApply (WrappedArrow p) where
-  app = WrapArrow $ app . arr (first unwrapArrow)
-  {-# INLINE app #-}
-
-instance ArrowLoop p => ArrowLoop (WrappedArrow p) where
-  loop = WrapArrow . loop . unwrapArrow
-  {-# INLINE loop #-}
-
-instance Arrow p => Profunctor (WrappedArrow p) where
-  lmap = (^>>)
-  {-# INLINE lmap #-}
-  rmap = (^<<)
-  {-# INLINE rmap #-}
-  -- We cannot safely overload ( #. ) or ( .# ) because we didn't write the 'Arrow'.
-
-------------------------------------------------------------------------------
--- Forget
-------------------------------------------------------------------------------
-
-newtype Forget r a b = Forget { runForget :: a -> r }
-
-instance Profunctor (Forget r) where
-  dimap f _ (Forget k) = Forget (k . f)
-  {-# INLINE dimap #-}
-  lmap f (Forget k) = Forget (k . f)
-  {-# INLINE lmap #-}
-  rmap _ (Forget k) = Forget k
-  {-# INLINE rmap #-}
-
-instance Functor (Forget r a) where
-  fmap _ (Forget k) = Forget k
-  {-# INLINE fmap #-}
-
-instance Foldable (Forget r a) where
-  foldMap _ _ = mempty
-  {-# INLINE foldMap #-}
-
-instance Traversable (Forget r a) where
-  traverse _ (Forget k) = pure (Forget k)
-  {-# INLINE traverse #-}
-
-------------------------------------------------------------------------------
--- Strong
-------------------------------------------------------------------------------
-
--- | Generalizing 'Star' of a strong 'Functor'
---
--- /Note:/ Every 'Functor' in Haskell is strong with respect to @(,)@.
---
--- This describes profunctor strength with respect to the product structure
--- of Hask.
---
--- <http://www-kb.is.s.u-tokyo.ac.jp/~asada/papers/arrStrMnd.pdf>
-class Profunctor p => Strong p where
-  first' :: p a b  -> p (a, c) (b, c)
-  first' = dimap swap swap . second'
-
-  second' :: p a b -> p (c, a) (c, b)
-  second' = dimap swap swap . first'
-
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-  {-# MINIMAL first' | second' #-}
-#endif
-
-instance Strong (->) where
-  first' ab ~(a, c) = (ab a, c)
-  {-# INLINE first' #-}
-  second' ab ~(c, a) = (c, ab a)
-
-instance Monad m => Strong (Kleisli m) where
-  first' (Kleisli f) = Kleisli $ \ ~(a, c) -> do
-     b <- f a
-     return (b, c)
-  {-# INLINE first' #-}
-  second' (Kleisli f) = Kleisli $ \ ~(c, a) -> do
-     b <- f a
-     return (c, b)
-  {-# INLINE second' #-}
-
-instance Functor m => Strong (Star m) where
-  first' (Star f) = Star $ \ ~(a, c) -> (\b' -> (b', c)) <$> f a
-  {-# INLINE first' #-}
-  second' (Star f) = Star $ \ ~(c, a) -> (,) c <$> f a
-  {-# INLINE second' #-}
-
--- | 'Arrow' is 'Strong' 'Category'
-instance Arrow p => Strong (WrappedArrow p) where
-  first' (WrapArrow k) = WrapArrow (first k)
-  {-# INLINE first' #-}
-  second' (WrapArrow k) = WrapArrow (second k)
-  {-# INLINE second' #-}
-
-instance Strong (Forget r) where
-  first' (Forget k) = Forget (k . fst)
-  {-# INLINE first' #-}
-  second' (Forget k) = Forget (k . snd)
-  {-# INLINE second' #-}
-
-------------------------------------------------------------------------------
--- Choice
-------------------------------------------------------------------------------
-
--- | The generalization of 'Costar' of 'Functor' that is strong with respect
--- to 'Either'.
---
--- Note: This is also a notion of strength, except with regards to another monoidal
--- structure that we can choose to equip Hask with: the cocartesian coproduct.
-class Profunctor p => Choice p where
-  left'  :: p a b -> p (Either a c) (Either b c)
-  left' =  dimap (either Right Left) (either Right Left) . right'
-
-  right' :: p a b -> p (Either c a) (Either c b)
-  right' =  dimap (either Right Left) (either Right Left) . left'
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-  {-# MINIMAL left' | right' #-}
-#endif
-
-instance Choice (->) where
-  left' ab (Left a) = Left (ab a)
-  left' _ (Right c) = Right c
-  {-# INLINE left' #-}
-  right' = fmap
-  {-# INLINE right' #-}
-
-instance Monad m => Choice (Kleisli m) where
-  left' = left
-  {-# INLINE left' #-}
-  right' = right
-  {-# INLINE right' #-}
-
-instance Applicative f => Choice (Star f) where
-  left' (Star f) = Star $ either (fmap Left . f) (pure . Right)
-  {-# INLINE left' #-}
-  right' (Star f) = Star $ either (pure . Left) (fmap Right . f)
-  {-# INLINE right' #-}
-
--- | 'extract' approximates 'costrength'
-instance Comonad w => Choice (Cokleisli w) where
-  left' = left
-  {-# INLINE left' #-}
-  right' = right
-  {-# INLINE right' #-}
-
--- NB: This instance is highly questionable
-instance Traversable w => Choice (Costar w) where
-  left' (Costar wab) = Costar (either Right Left . fmap wab . traverse (either Right Left))
-  {-# INLINE left' #-}
-  right' (Costar wab) = Costar (fmap wab . sequence)
-  {-# INLINE right' #-}
-
-instance Choice Tagged where
-  left' (Tagged b) = Tagged (Left b)
-  {-# INLINE left' #-}
-  right' (Tagged b) = Tagged (Right b)
-  {-# INLINE right' #-}
-
-instance ArrowChoice p => Choice (WrappedArrow p) where
-  left' (WrapArrow k) = WrapArrow (left k)
-  {-# INLINE left' #-}
-  right' (WrapArrow k) = WrapArrow (right k)
-  {-# INLINE right' #-}
-
-instance Monoid r => Choice (Forget r) where
-  left' (Forget k) = Forget (either k (const mempty))
-  {-# INLINE left' #-}
-  right' (Forget k) = Forget (either (const mempty) k)
-  {-# INLINE right' #-}
-
---------------------------------------------------------------------------------
--- * Costrength for (,)
---------------------------------------------------------------------------------
-
--- | Analogous to 'ArrowLoop', 'loop' = 'unfirst'
-class Profunctor p => Costrong p where
-  unfirst  :: p (a, d) (b, d) -> p a b
-  unfirst = unsecond . dimap swap swap
-
-  unsecond :: p (d, a) (d, b) -> p a b
-  unsecond = unfirst . dimap swap swap
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-  {-# MINIMAL unfirst | unsecond #-}
-#endif
-
-instance Costrong (->) where
-  unfirst f a = b where (b, d) = f (a, d)
-  unsecond f a = b where (d, b) = f (d, a)
-
-instance Functor f => Costrong (Costar f) where
-  unfirst (Costar f) = Costar f'
-    where f' fa = b where (b, d) = f ((\a -> (a, d)) <$> fa)
-  unsecond (Costar f) = Costar f'
-    where f' fa = b where (d, b) = f ((,) d <$> fa)
-
-instance Costrong Tagged where
-  unfirst (Tagged bd) = Tagged (fst bd)
-  unsecond (Tagged db) = Tagged (snd db)
-
-instance ArrowLoop p => Costrong (WrappedArrow p) where
-  unfirst (WrapArrow k) = WrapArrow (loop k)
-
-instance MonadFix m => Costrong (Kleisli m) where
-  unfirst (Kleisli f) = Kleisli (liftM fst . mfix . f')
-    where f' x y = f (x, snd y)
-
-instance Functor f => Costrong (Cokleisli f) where
-  unfirst (Cokleisli f) = Cokleisli f'
-    where f' fa = b where (b, d) = f ((\a -> (a, d)) <$> fa)
-
---------------------------------------------------------------------------------
--- * Costrength for Either
---------------------------------------------------------------------------------
-
-class Profunctor p => Cochoice p where
-  unleft  :: p (Either a d) (Either b d) -> p a b
-  unleft = unright . dimap (either Right Left) (either Right Left)
-
-  unright :: p (Either d a) (Either d b) -> p a b
-  unright = unleft . dimap (either Right Left) (either Right Left)
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-  {-# MINIMAL unleft | unright #-}
-#endif
-
-instance Cochoice (->) where
-  unleft f = go . Left where go = either id (go . Right) . f
-  unright f = go . Right where go = either (go . Left) id . f
-
-instance Applicative f => Cochoice (Costar f) where
-  unleft (Costar f) = Costar (go . fmap Left)
-    where go = either id (go . pure . Right) . f
-
--- NB: Another instance that's highly questionable
-instance Traversable f => Cochoice (Star f) where
-  unright (Star f) = Star (go . Right)
-    where go = either (go . Left) id . sequence . f
+import Data.Profunctor.Choice
+import Data.Profunctor.Closed
+import Data.Profunctor.Mapping
+import Data.Profunctor.Strong
+import Data.Profunctor.Types
diff --git a/src/Data/Profunctor/Adjunction.hs b/src/Data/Profunctor/Adjunction.hs
--- a/src/Data/Profunctor/Adjunction.hs
+++ b/src/Data/Profunctor/Adjunction.hs
@@ -1,12 +1,30 @@
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2015 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable, MPTCs, fundeps
+--
+----------------------------------------------------------------------------
 module Data.Profunctor.Adjunction where
 
-import Data.Profunctor
+import Data.Profunctor.Types
 import Data.Profunctor.Monad
 
+-- | Laws:
+--
+-- @
+-- 'unit' '.' 'counit' ≡ 'id'
+-- 'counit' '.' 'unit' ≡ 'id'
+-- @
+
+-- ProfunctorAdjunction :: ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> Constraint
 class (ProfunctorFunctor f, ProfunctorFunctor u) => ProfunctorAdjunction f u | f -> u, u -> f where
   unit   :: Profunctor p => p :-> u (f p)
   counit :: Profunctor p => f (u p) :-> p
diff --git a/src/Data/Profunctor/Cayley.hs b/src/Data/Profunctor/Cayley.hs
--- a/src/Data/Profunctor/Cayley.hs
+++ b/src/Data/Profunctor/Cayley.hs
@@ -1,10 +1,9 @@
-{-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Trustworthy #-}
-#endif
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2014 Edward Kmett
+-- Copyright   :  (C) 2014-2015 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -21,10 +20,15 @@
 import Control.Comonad
 import Data.Profunctor
 import Data.Profunctor.Monad
+import Data.Profunctor.Traversing
 import Data.Profunctor.Unsafe
 import Prelude hiding ((.), id)
 
--- static arrows
+-- | Static arrows. Lifted by 'Applicative'.
+--
+-- 'Cayley' has a polymorphic kind since @5.6@.
+
+-- Cayley :: (k3 -> Type) -> (k1 -> k2 -> k3) -> (k1 -> k2 -> Type)
 newtype Cayley f p a b = Cayley { runCayley :: f (p a b) }
 
 instance Functor f => ProfunctorFunctor (Cayley f) where
@@ -51,10 +55,29 @@
   first'  = Cayley . fmap first' . runCayley
   second' = Cayley . fmap second' . runCayley
 
+instance (Functor f, Costrong p) => Costrong (Cayley f p) where
+  unfirst (Cayley fp) = Cayley (fmap unfirst fp)
+  unsecond (Cayley fp) = Cayley (fmap unsecond fp)
+
 instance (Functor f, Choice p) => Choice (Cayley f p) where
   left'   = Cayley . fmap left' . runCayley
   right'  = Cayley . fmap right' . runCayley
 
+instance (Functor f, Cochoice p) => Cochoice (Cayley f p) where
+  unleft (Cayley fp) = Cayley (fmap unleft fp)
+  {-# INLINE unleft #-}
+  unright (Cayley fp) = Cayley (fmap unright fp)
+  {-# INLINE unright #-}
+
+instance (Functor f, Closed p) => Closed (Cayley f p) where
+  closed = Cayley . fmap closed . runCayley
+
+instance (Functor f, Traversing p) => Traversing (Cayley f p) where
+  traverse' = Cayley . fmap traverse' . runCayley
+
+instance (Functor f, Mapping p) => Mapping (Cayley f p) where
+  map' = Cayley . fmap map' . runCayley
+
 instance (Applicative f, Category p) => Category (Cayley f p) where
   id = Cayley $ pure id
   Cayley fpbc . Cayley fpab = Cayley $ liftA2 (.) fpbc fpab
@@ -71,7 +94,7 @@
   right = Cayley . fmap right . runCayley
   Cayley ab +++ Cayley cd = Cayley $ liftA2 (+++) ab cd
   Cayley ac ||| Cayley bc = Cayley $ liftA2 (|||) ac bc
-  
+
 instance (Applicative f, ArrowLoop p) => ArrowLoop (Cayley f p) where
   loop = Cayley . fmap loop . runCayley
 
@@ -80,3 +103,43 @@
 
 instance (Applicative f, ArrowPlus p) => ArrowPlus (Cayley f p) where
   Cayley f <+> Cayley g = Cayley (liftA2 (<+>) f g)
+
+mapCayley :: (forall a. f a -> g a) -> Cayley f p x y -> Cayley g p x y
+mapCayley f (Cayley g) = Cayley (f g)
+
+-- instance Adjunction f g => ProfunctorAdjunction (Cayley f) (Cayley g) where
+
+{-
+newtype Uncayley p a = Uncayley (p () a)
+
+instance Profunctor p => Functor (Uncayley p) where
+  fmap f (Uncayley p) = Uncayley (rmap f p)
+
+smash :: Strong p => Cayley (Uncayley p) (->) a b -> p a b
+smash (Cayley (Uncayley pab)) = dimap ((,)()) (uncurry id) (first' pab)
+
+unsmash :: Closed p => p a b -> Cayley (Uncayley p) (->) a b
+unsmash = Cayley . Uncayley . curry' . lmap snd
+
+type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
+
+-- pastro and street's strong tambara module
+class (Strong p, Closed p) => Stronger p
+
+-- only a true iso for Stronger p and q, no?
+_Smash :: (Strong p, Closed q) => Iso
+  (Cayley (Uncayley p) (->) a b)
+  (Cayley (Uncayley q) (->) c d)
+  (p a b)
+  (q c d)
+_Smash = dimap hither (fmap yon) where
+  hither (Cayley (Uncayley pab)) = dimap ((,)()) (uncurry id) (first' pab)
+  yon = Cayley . Uncayley . curry' . lmap snd
+
+fsmash :: (forall x y. p x y -> q x y) -> Cayley (Uncayley p) (->) a b -> Cayley (Uncayley q) (->) a b
+fsmash f (Cayley (Uncayley puab)) = Cayley (Uncayley (f puab))
+
+-- | proposition 4.3 from pastro and street is that fsmash and funsmash form an equivalence of categories
+funsmash :: (Closed p, Strong q) => (forall x y. Cayley (Uncayley p) (->) x y -> Cayley (Uncayley q) (->) x y) -> p a b -> q a b
+funsmash k = smash . k . unsmash
+-}
diff --git a/src/Data/Profunctor/Choice.hs b/src/Data/Profunctor/Choice.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Choice.hs
@@ -0,0 +1,445 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Safe #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2014-2015 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  Rank2Types
+--
+----------------------------------------------------------------------------
+module Data.Profunctor.Choice
+  (
+  -- * Strength
+    Choice(..)
+  , TambaraSum(..)
+  , tambaraSum, untambaraSum
+  , PastroSum(..)
+  -- * Costrength
+  , Cochoice(..)
+  , CotambaraSum(..)
+  , cotambaraSum, uncotambaraSum
+  , CopastroSum(..)
+  ) where
+
+import Control.Applicative hiding (WrappedArrow(..))
+import Control.Arrow
+import Control.Category
+import Control.Comonad
+import Data.Bifunctor.Joker (Joker(..))
+import Data.Bifunctor.Product (Product(..))
+import Data.Bifunctor.Sum (Sum(..))
+import Data.Bifunctor.Tannen (Tannen(..))
+import Data.Monoid hiding (Product, Sum)
+import Data.Profunctor.Adjunction
+import Data.Profunctor.Monad
+import Data.Profunctor.Strong
+import Data.Profunctor.Types
+import Data.Profunctor.Unsafe
+import Data.Tagged
+import Prelude hiding (id,(.))
+
+------------------------------------------------------------------------------
+-- Choice
+------------------------------------------------------------------------------
+
+-- | The generalization of 'Costar' of 'Functor' that is strong with respect
+-- to 'Either'.
+--
+-- Note: This is also a notion of strength, except with regards to another monoidal
+-- structure that we can choose to equip Hask with: the cocartesian coproduct.
+class Profunctor p => Choice p where
+  -- | Laws:
+  --
+  -- @
+  -- 'left'' ≡ 'dimap' swapE swapE '.' 'right'' where
+  --   swapE :: 'Either' a b -> 'Either' b a
+  --   swapE = 'either' 'Right' 'Left'
+  -- 'rmap' 'Left' ≡ 'lmap' 'Left' '.' 'left''
+  -- 'lmap' ('right' f) '.' 'left'' ≡ 'rmap' ('right' f) '.' 'left''
+  -- 'left'' '.' 'left'' ≡ 'dimap' assocE unassocE '.' 'left'' where
+  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
+  --   assocE ('Left' ('Left' a)) = 'Left' a
+  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
+  --   assocE ('Right' c) = 'Right' ('Right' c)
+  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
+  --   unassocE ('Left' a) = 'Left' ('Left' a)
+  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
+  --   unassocE ('Right' ('Right' c)) = 'Right' c
+  -- @
+  left'  :: p a b -> p (Either a c) (Either b c)
+  left' =  dimap (either Right Left) (either Right Left) . right'
+
+  -- | Laws:
+  --
+  -- @
+  -- 'right'' ≡ 'dimap' swapE swapE '.' 'left'' where
+  --   swapE :: 'Either' a b -> 'Either' b a
+  --   swapE = 'either' 'Right' 'Left'
+  -- 'rmap' 'Right' ≡ 'lmap' 'Right' '.' 'right''
+  -- 'lmap' ('left' f) '.' 'right'' ≡ 'rmap' ('left' f) '.' 'right''
+  -- 'right'' '.' 'right'' ≡ 'dimap' unassocE assocE '.' 'right'' where
+  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
+  --   assocE ('Left' ('Left' a)) = 'Left' a
+  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
+  --   assocE ('Right' c) = 'Right' ('Right' c)
+  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
+  --   unassocE ('Left' a) = 'Left' ('Left' a)
+  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
+  --   unassocE ('Right' ('Right' c)) = 'Right' c
+  -- @
+  right' :: p a b -> p (Either c a) (Either c b)
+  right' =  dimap (either Right Left) (either Right Left) . left'
+
+  {-# MINIMAL left' | right' #-}
+
+instance Choice (->) where
+  left' ab (Left a) = Left (ab a)
+  left' _ (Right c) = Right c
+  {-# INLINE left' #-}
+  right' = fmap
+  {-# INLINE right' #-}
+
+instance Monad m => Choice (Kleisli m) where
+  left' = left
+  {-# INLINE left' #-}
+  right' = right
+  {-# INLINE right' #-}
+
+instance Applicative f => Choice (Star f) where
+  left' (Star f) = Star $ either (fmap Left . f) (pure . Right)
+  {-# INLINE left' #-}
+  right' (Star f) = Star $ either (pure . Left) (fmap Right . f)
+  {-# INLINE right' #-}
+
+-- | 'extract' approximates 'costrength'
+instance Comonad w => Choice (Cokleisli w) where
+  left' = left
+  {-# INLINE left' #-}
+  right' = right
+  {-# INLINE right' #-}
+
+instance Choice Tagged where
+  left' (Tagged b) = Tagged (Left b)
+  {-# INLINE left' #-}
+  right' (Tagged b) = Tagged (Right b)
+  {-# INLINE right' #-}
+
+instance ArrowChoice p => Choice (WrappedArrow p) where
+  left' (WrapArrow k) = WrapArrow (left k)
+  {-# INLINE left' #-}
+  right' (WrapArrow k) = WrapArrow (right k)
+  {-# INLINE right' #-}
+
+instance Monoid r => Choice (Forget r) where
+  left' (Forget k) = Forget (either k (const mempty))
+  {-# INLINE left' #-}
+  right' (Forget k) = Forget (either (const mempty) k)
+  {-# INLINE right' #-}
+
+instance Functor f => Choice (Joker f) where
+  left' (Joker fb) = Joker (fmap Left fb)
+  {-# INLINE left' #-}
+  right' (Joker fb) = Joker (fmap Right fb)
+  {-# INLINE right' #-}
+
+instance (Choice p, Choice q) => Choice (Product p q) where
+  left' (Pair p q) = Pair (left' p) (left' q)
+  {-# INLINE left' #-}
+  right' (Pair p q) = Pair (right' p) (right' q)
+  {-# INLINE right' #-}
+
+instance (Choice p, Choice q) => Choice (Sum p q) where
+  left' (L2 p) = L2 (left' p)
+  left' (R2 q) = R2 (left' q)
+  {-# INLINE left' #-}
+  right' (L2 p) = L2 (right' p)
+  right' (R2 q) = R2 (right' q)
+  {-# INLINE right' #-}
+
+instance (Functor f, Choice p) => Choice (Tannen f p) where
+  left' (Tannen fp) = Tannen (fmap left' fp)
+  {-# INLINE left' #-}
+  right' (Tannen fp) = Tannen (fmap right' fp)
+  {-# INLINE right' #-}
+
+instance Choice p => Choice (Tambara p) where
+  left' (Tambara f) = Tambara $ dimap hither yon $ left' f where
+    hither :: (Either a b, c) -> Either (a, c) (b, c)
+    hither (Left y, s) = Left (y, s)
+    hither (Right z, s) = Right (z, s)
+
+    yon :: Either (a, c) (b, c) -> (Either a b, c)
+    yon (Left (y, s)) = (Left y, s)
+    yon (Right (z, s)) = (Right z, s)
+
+
+----------------------------------------------------------------------------
+-- * TambaraSum
+----------------------------------------------------------------------------
+
+-- | TambaraSum is cofreely adjoins strength with respect to Either.
+--
+-- Note: this is not dual to 'Data.Profunctor.Tambara.Tambara'. It is 'Data.Profunctor.Tambara.Tambara' with respect to a different tensor.
+newtype TambaraSum p a b = TambaraSum { runTambaraSum :: forall c. p (Either a c) (Either b c) }
+
+instance ProfunctorFunctor TambaraSum where
+  promap f (TambaraSum p) = TambaraSum (f p)
+
+instance ProfunctorComonad TambaraSum where
+  proextract (TambaraSum p)   = dimap Left fromEither p
+  produplicate (TambaraSum p) = TambaraSum (TambaraSum $ dimap hither yon p) where
+    hither :: Either (Either a b) c -> Either a (Either b c)
+    hither (Left (Left x))   = Left x
+    hither (Left (Right y))  = Right (Left y)
+    hither (Right z)         = Right (Right z)
+
+    yon    :: Either a (Either b c) -> Either (Either a b) c
+    yon    (Left x)          = Left (Left x)
+    yon    (Right (Left y))  = Left (Right y)
+    yon    (Right (Right z)) = Right z
+
+instance Profunctor p => Profunctor (TambaraSum p) where
+  dimap f g (TambaraSum p) = TambaraSum $ dimap (left f) (left g) p
+  {-# INLINE dimap #-}
+
+instance Profunctor p => Choice (TambaraSum p) where
+  left' p = runTambaraSum $ produplicate p
+  {-# INLINE left' #-}
+
+instance Category p => Category (TambaraSum p) where
+  id = TambaraSum id
+  TambaraSum p . TambaraSum q = TambaraSum (p . q)
+
+instance Profunctor p => Functor (TambaraSum p a) where
+  fmap = rmap
+
+-- |
+-- @
+-- 'tambaraSum' '.' 'untambaraSum' ≡ 'id'
+-- 'untambaraSum' '.' 'tambaraSum' ≡ 'id'
+-- @
+tambaraSum :: Choice p => (p :-> q) -> p :-> TambaraSum q
+tambaraSum f p = TambaraSum $ f $ left' p
+
+-- |
+-- @
+-- 'tambaraSum' '.' 'untambaraSum' ≡ 'id'
+-- 'untambaraSum' '.' 'tambaraSum' ≡ 'id'
+-- @
+untambaraSum :: Profunctor q => (p :-> TambaraSum q) -> p :-> q
+untambaraSum f p = dimap Left fromEither $ runTambaraSum $ f p
+
+fromEither :: Either a a -> a
+fromEither = either id id
+
+----------------------------------------------------------------------------
+-- * PastroSum
+----------------------------------------------------------------------------
+
+-- | PastroSum -| TambaraSum
+--
+-- PastroSum freely constructs strength with respect to Either.
+data PastroSum p a b where
+  PastroSum :: (Either y z -> b) -> p x y -> (a -> Either x z) -> PastroSum p a b
+
+instance Functor (PastroSum p a) where
+  fmap f (PastroSum l m r) = PastroSum (f . l) m r
+
+instance Profunctor (PastroSum p) where
+  dimap f g (PastroSum l m r) = PastroSum (g . l) m (r . f)
+  lmap f (PastroSum l m r) = PastroSum l m (r . f)
+  rmap g (PastroSum l m r) = PastroSum (g . l) m r
+  w #. PastroSum l m r = PastroSum (w #. l) m r
+  PastroSum l m r .# w = PastroSum l m (r .# w)
+
+instance ProfunctorAdjunction PastroSum TambaraSum where
+  counit (PastroSum f (TambaraSum g) h) = dimap h f g
+  unit p = TambaraSum $ PastroSum id p id
+
+instance ProfunctorFunctor PastroSum where
+  promap f (PastroSum l m r) = PastroSum l (f m) r
+
+instance ProfunctorMonad PastroSum where
+  proreturn p = PastroSum fromEither p Left
+  projoin (PastroSum l (PastroSum m n o) q) = PastroSum lm n oq where
+    oq a = case q a of
+      Left b -> Left <$> o b
+      Right z -> Right (Right z)
+    lm (Left x) = l $ Left $ m $ Left x
+    lm (Right (Left y)) = l $ Left $ m $ Right y
+    lm (Right (Right z)) = l $ Right z
+
+instance Choice (PastroSum p) where
+  left' (PastroSum l m r) = PastroSum l' m r' where
+    r' = either (fmap Left . r) (Right . Right)
+    l' (Left y)          = Left (l (Left y))
+    l' (Right (Left z))  = Left (l (Right z))
+    l' (Right (Right c)) = Right c
+  right' (PastroSum l m r) = PastroSum l' m r' where
+    r' = either (Right . Left) (fmap Right . r)
+    l' (Right (Left c))  = Left c
+    l' (Right (Right z)) = Right (l (Right z))
+    l' (Left y)          = Right (l (Left y))
+
+--------------------------------------------------------------------------------
+-- * Costrength for Either
+--------------------------------------------------------------------------------
+
+class Profunctor p => Cochoice p where
+  -- | Laws:
+  --
+  -- @
+  -- 'unleft' ≡ 'unright' '.' 'dimap' swapE swapE where
+  --   swapE :: 'Either' a b -> 'Either' b a
+  --   swapE = 'either' 'Right' 'Left'
+  -- 'rmap' ('either' 'id' 'absurd') ≡ 'unleft' '.' 'lmap' ('either' 'id' 'absurd')
+  -- 'unfirst' '.' 'rmap' ('second' f) ≡ 'unfirst' '.' 'lmap' ('second' f)
+  -- 'unleft' '.' 'unleft' ≡ 'unleft' '.' 'dimap' assocE unassocE where
+  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
+  --   assocE ('Left' ('Left' a)) = 'Left' a
+  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
+  --   assocE ('Right' c) = 'Right' ('Right' c)
+  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
+  --   unassocE ('Left' a) = 'Left' ('Left' a)
+  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
+  --   unassocE ('Right' ('Right' c)) = 'Right' c
+  -- @
+  unleft  :: p (Either a d) (Either b d) -> p a b
+  unleft = unright . dimap (either Right Left) (either Right Left)
+
+  -- | Laws:
+  --
+  -- @
+  -- 'unright' ≡ 'unleft' '.' 'dimap' swapE swapE where
+  --   swapE :: 'Either' a b -> 'Either' b a
+  --   swapE = 'either' 'Right' 'Left'
+  -- 'rmap' ('either' 'absurd' 'id') ≡ 'unright' '.' 'lmap' ('either' 'absurd' 'id')
+  -- 'unsecond' '.' 'rmap' ('first' f) ≡ 'unsecond' '.' 'lmap' ('first' f)
+  -- 'unright' '.' 'unright' ≡ 'unright' '.' 'dimap' unassocE assocE where
+  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
+  --   assocE ('Left' ('Left' a)) = 'Left' a
+  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
+  --   assocE ('Right' c) = 'Right' ('Right' c)
+  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
+  --   unassocE ('Left' a) = 'Left' ('Left' a)
+  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
+  --   unassocE ('Right' ('Right' c)) = 'Right' c
+  -- @
+  unright :: p (Either d a) (Either d b) -> p a b
+  unright = unleft . dimap (either Right Left) (either Right Left)
+
+  {-# MINIMAL unleft | unright #-}
+
+instance Cochoice (->) where
+  unleft f = go . Left where go = either id (go . Right) . f
+  unright f = go . Right where go = either (go . Left) id . f
+
+instance Applicative f => Cochoice (Costar f) where
+  unleft (Costar f) = Costar (go . fmap Left)
+    where go = either id (go . pure . Right) . f
+
+-- NB: Another instance that's highly questionable
+instance Traversable f => Cochoice (Star f) where
+  unright (Star f) = Star (go . Right)
+    where go = either (go . Left) id . sequence . f
+
+instance (Functor f, Cochoice p) => Cochoice (Tannen f p) where
+  unleft (Tannen fp) = Tannen (fmap unleft fp)
+  {-# INLINE unleft #-}
+  unright (Tannen fp) = Tannen (fmap unright fp)
+  {-# INLINE unright #-}
+
+instance (Cochoice p, Cochoice q) => Cochoice (Product p q) where
+  unleft (Pair p q) = Pair (unleft p) (unleft q)
+  unright (Pair p q) = Pair (unright p) (unright q)
+
+instance (Cochoice p, Cochoice q) => Cochoice (Sum p q) where
+  unleft (L2 p) = L2 (unleft p)
+  unleft (R2 q) = R2 (unleft q)
+  unright (L2 p) = L2 (unright p)
+  unright (R2 q) = R2 (unright q)
+
+instance Cochoice (Forget r) where
+  unleft (Forget f) = Forget (f . Left)
+  unright (Forget f) = Forget (f . Right)
+
+----------------------------------------------------------------------------
+-- * CotambaraSum
+----------------------------------------------------------------------------
+
+-- | 'CotambaraSum' cofreely constructs costrength with respect to 'Either' (aka 'Choice')
+data CotambaraSum q a b where
+    CotambaraSum :: Cochoice r => (r :-> q) -> r a b -> CotambaraSum q a b
+
+instance Profunctor (CotambaraSum p) where
+  lmap f (CotambaraSum n p) = CotambaraSum n (lmap f p)
+  rmap g (CotambaraSum n p) = CotambaraSum n (rmap g p)
+  dimap f g (CotambaraSum n p) = CotambaraSum n (dimap f g p)
+
+instance ProfunctorFunctor CotambaraSum where
+  promap f (CotambaraSum n p) = CotambaraSum (f . n) p
+
+instance ProfunctorComonad CotambaraSum where
+  proextract (CotambaraSum n p)  = n p
+  produplicate (CotambaraSum n p) = CotambaraSum id (CotambaraSum n p)
+
+instance Cochoice (CotambaraSum p) where
+  unleft (CotambaraSum n p) = CotambaraSum n (unleft p)
+  unright (CotambaraSum n p) = CotambaraSum n (unright p)
+
+instance Functor (CotambaraSum p a) where
+  fmap = rmap
+
+-- |
+-- @
+-- 'cotambaraSum' '.' 'uncotambaraSum' ≡ 'id'
+-- 'uncotambaraSum' '.' 'cotambaraSum' ≡ 'id'
+-- @
+cotambaraSum :: Cochoice p => (p :-> q) -> p :-> CotambaraSum q
+cotambaraSum f = CotambaraSum f
+
+-- |
+-- @
+-- 'cotambaraSum' '.' 'uncotambaraSum' ≡ 'id'
+-- 'uncotambaraSum' '.' 'cotambaraSum' ≡ 'id'
+-- @
+uncotambaraSum :: Profunctor q => (p :-> CotambaraSum q) -> p :-> q
+uncotambaraSum f p = proextract (f p)
+
+----------------------------------------------------------------------------
+-- * Copastro
+----------------------------------------------------------------------------
+
+-- | CopastroSum -| CotambaraSum
+--
+-- 'CopastroSum' freely constructs costrength with respect to 'Either' (aka 'Choice')
+newtype CopastroSum p a b = CopastroSum { runCopastroSum :: forall r. Cochoice r => (forall x y. p x y -> r x y) -> r a b }
+
+instance Functor (CopastroSum p a) where
+  fmap f (CopastroSum h) = CopastroSum $ \ n -> rmap f (h n)
+
+instance Profunctor (CopastroSum p) where
+  dimap f g (CopastroSum h) = CopastroSum $ \ n -> dimap f g (h n)
+  lmap f (CopastroSum h) = CopastroSum $ \ n -> lmap f (h n)
+  rmap g (CopastroSum h) = CopastroSum $ \ n -> rmap g (h n)
+
+instance ProfunctorAdjunction CopastroSum CotambaraSum where
+ unit p = CotambaraSum id (proreturn p)
+ counit (CopastroSum h) = proextract (h id)
+
+instance ProfunctorFunctor CopastroSum where
+  promap f (CopastroSum h) = CopastroSum $ \n -> h (n . f)
+
+instance ProfunctorMonad CopastroSum where
+  proreturn p = CopastroSum $ \n -> n p
+  projoin p = CopastroSum $ \c -> runCopastroSum p (\x -> runCopastroSum x c)
+
+instance Cochoice (CopastroSum p) where
+  unleft (CopastroSum p) = CopastroSum $ \n -> unleft (p n)
+  unright (CopastroSum p) = CopastroSum $ \n -> unright (p n)
diff --git a/src/Data/Profunctor/Closed.hs b/src/Data/Profunctor/Closed.hs
--- a/src/Data/Profunctor/Closed.hs
+++ b/src/Data/Profunctor/Closed.hs
@@ -1,31 +1,47 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE Trustworthy #-}
-#endif
-
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2014-2018 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
 module Data.Profunctor.Closed
   ( Closed(..)
   , Closure(..)
   , close
   , unclose
   , Environment(..)
+  , curry'
   ) where
 
 import Control.Applicative
 import Control.Arrow
 import Control.Category
 import Control.Comonad
+import Data.Bifunctor.Product (Product(..))
+import Data.Bifunctor.Sum (Sum(..))
+import Data.Bifunctor.Tannen (Tannen(..))
+import Data.Coerce (Coercible, coerce)
 import Data.Distributive
-import Data.Monoid
-import Data.Profunctor
 import Data.Profunctor.Adjunction
 import Data.Profunctor.Monad
+import Data.Profunctor.Strong
+import Data.Profunctor.Types
 import Data.Profunctor.Unsafe
+import Data.Semigroup hiding (Product, Sum)
 import Data.Tagged
+import Data.Tuple
 import Prelude hiding ((.),id)
 
 --------------------------------------------------------------------------------
@@ -36,6 +52,13 @@
 --
 -- A closed profunctor allows the closed structure to pass through.
 class Profunctor p => Closed p where
+  -- | Laws:
+  --
+  -- @
+  -- 'lmap' ('.' f) '.' 'closed' ≡ 'rmap' ('.' f) '.' 'closed'
+  -- 'closed' '.' 'closed' ≡ 'dimap' 'uncurry' 'curry' '.' 'closed'
+  -- 'dimap' 'const' ('$'()) '.' 'closed' ≡ 'id'
+  -- @
   closed :: p a b -> p (x -> a) (x -> b)
 
 instance Closed Tagged where
@@ -45,10 +68,10 @@
   closed = (.)
 
 instance Functor f => Closed (Costar f) where
-  closed (Costar fab) = Costar $ \fxa x -> fab (fmap ($x) fxa)
+  closed (Costar fab) = Costar $ \fxa x -> fab (fmap ($ x) fxa)
 
 instance Functor f => Closed (Cokleisli f) where
-  closed (Cokleisli fab) = Cokleisli $ \fxa x -> fab (fmap ($x) fxa)
+  closed (Cokleisli fab) = Cokleisli $ \fxa x -> fab (fmap ($ x) fxa)
 
 instance Distributive f => Closed (Star f) where
   closed (Star afb) = Star $ \xa -> distribute $ \x -> afb (xa x)
@@ -56,9 +79,22 @@
 instance (Distributive f, Monad f) => Closed (Kleisli f) where
   closed (Kleisli afb) = Kleisli $ \xa -> distribute $ \x -> afb (xa x)
 
+instance (Closed p, Closed q) => Closed (Product p q) where
+  closed (Pair p q) = Pair (closed p) (closed q)
+
+instance (Closed p, Closed q) => Closed (Sum p q) where
+  closed (L2 p) = L2 (closed p)
+  closed (R2 q) = R2 (closed q)
+
+instance (Functor f, Closed p) => Closed (Tannen f p) where
+  closed (Tannen fp) = Tannen (fmap closed fp)
+
 -- instance Monoid r => Closed (Forget r) where
 --  closed _ = Forget $ \_ -> mempty
 
+curry' :: Closed p => p (a, b) c -> p a (b -> c)
+curry' = lmap (,) . closed
+
 --------------------------------------------------------------------------------
 -- * Closure
 --------------------------------------------------------------------------------
@@ -73,18 +109,22 @@
   dimap f g (Closure p) = Closure $ dimap (fmap f) (fmap g) p
   lmap f (Closure p) = Closure $ lmap (fmap f) p
   rmap f (Closure p) = Closure $ rmap (fmap f) p
-  w #. Closure p = Closure $ fmap w #. p
-  Closure p .# w = Closure $ p .# fmap w
 
+  (#.) :: forall a b c q. Coercible c b => q b c -> Closure p a b -> Closure p a c
+  _ #. Closure p = Closure $ fmap (coerce (id :: c -> c) :: b -> c) #. p
+
+  (.#) :: forall a b c q. Coercible b a => Closure p b c -> q a b -> Closure p a c
+  Closure p .# _ = Closure $ p .# fmap (coerce (id :: b -> b) :: a -> b)
+
 instance ProfunctorFunctor Closure where
   promap f (Closure p) = Closure (f p)
 
 instance ProfunctorComonad Closure where
-  proextract = dimap const ($ ()) . runClosure
+  proextract p = dimap const ($ ()) $ runClosure p
   produplicate (Closure p) = Closure $ Closure $ dimap uncurry curry p
 
 instance Profunctor p => Closed (Closure p) where
-  closed = runClosure . produplicate
+  closed p = runClosure $ produplicate p
 
 instance Strong p => Strong (Closure p) where
   first' (Closure p) = Closure $ dimap hither yon $ first' p
@@ -123,9 +163,14 @@
   empty = zeroArrow
   f <|> g = f <+> g
 
-instance (Profunctor p, Arrow p, Monoid b) => Monoid (Closure p a b) where
+instance (Profunctor p, Arrow p, Semigroup b) => Semigroup (Closure p a b) where
+  (<>) = liftA2 (<>)
+
+instance (Profunctor p, Arrow p, Semigroup b, Monoid b) => Monoid (Closure p a b) where
   mempty = pure mempty
-  mappend = liftA2 mappend
+#if !(MIN_VERSION_base(4,11,0))
+  mappend = (<>)
+#endif
 
 -- |
 -- @
@@ -150,7 +195,10 @@
 data Environment p a b where
   Environment :: ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
 
-instance Profunctor p => Profunctor (Environment p) where
+instance Functor (Environment p a) where
+  fmap f (Environment l m r) = Environment (f . l) m r
+
+instance Profunctor (Environment p) where
   dimap f g (Environment l m r) = Environment (g . l) m (r . f)
   lmap f (Environment l m r) = Environment l m (r . f)
   rmap g (Environment l m r) = Environment (g . l) m r
@@ -169,3 +217,8 @@
 instance ProfunctorAdjunction Environment Closure where
   counit (Environment g (Closure p) f) = dimap f g p
   unit p = Closure (Environment id p id)
+
+instance Closed (Environment p) where
+  closed (Environment l m r) = Environment l' m r' where
+    r' wa (z,w) = r (wa w) z
+    l' zx2y x = l (\z -> zx2y (z,x))
diff --git a/src/Data/Profunctor/Codensity.hs b/src/Data/Profunctor/Codensity.hs
deleted file mode 100644
--- a/src/Data/Profunctor/Codensity.hs
+++ /dev/null
@@ -1,54 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE TypeFamilies #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE Trustworthy #-}
-#endif
------------------------------------------------------------------------------
--- |
--- Copyright   :  (C) 2014 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  provisional
--- Portability :  Rank2Types, TFs
---
-----------------------------------------------------------------------------
-module Data.Profunctor.Codensity
-  ( Codensity(..)
-  , decomposeCodensity
-  ) where
-
-import Control.Category
-import Data.Profunctor.Unsafe
-import Data.Profunctor.Composition
-import Prelude hiding (id,(.))
-
--- | This represents the right Kan extension of a 'Profunctor' @p@ along itself. This provides a generalization of the \"difference list\" trick to profunctors.
-newtype Codensity p a b = Codensity { runCodensity :: forall x. p x a -> p x b }
-
-instance Profunctor p => Profunctor (Codensity p) where
-  dimap ca bd f = Codensity (rmap bd . runCodensity f . rmap ca)
-  {-# INLINE dimap #-}
-  lmap ca f = Codensity (runCodensity f . rmap ca)
-  {-# INLINE lmap #-}
-  rmap bd f = Codensity (rmap bd . runCodensity f)
-  {-# INLINE rmap #-}
-  bd #. f = Codensity (\p -> bd #. runCodensity f p)
-  {-# INLINE ( #. ) #-}
-  f .# ca = Codensity (\p -> runCodensity f (ca #. p))
-  {-# INLINE (.#) #-}
-
-instance Profunctor p => Functor (Codensity p a) where
-  fmap bd f = Codensity (rmap bd . runCodensity f)
-  {-# INLINE fmap #-}
-
-instance Category (Codensity p) where
-  id = Codensity id
-  {-# INLINE id #-}
-  Codensity f . Codensity g = Codensity (f . g)
-  {-# INLINE (.) #-}
-
-decomposeCodensity :: Procompose (Codensity p) p a b -> p a b
-decomposeCodensity (Procompose (Codensity pp) p) = pp p
-{-# INLINE decomposeCodensity #-}
diff --git a/src/Data/Profunctor/Composition.hs b/src/Data/Profunctor/Composition.hs
--- a/src/Data/Profunctor/Composition.hs
+++ b/src/Data/Profunctor/Composition.hs
@@ -1,17 +1,15 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE Safe #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Profunctor.Composition
--- Copyright   :  (C) 2014 Edward Kmett
+-- Copyright   :  (C) 2014-2015 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -28,6 +26,9 @@
   , idl
   , idr
   , assoc
+  -- * Categories as monoid objects
+  , eta
+  , mu
   -- * Generalized Composition
   , stars, kleislis
   , costars, cokleislis
@@ -43,10 +44,10 @@
 import Data.Functor.Compose
 import Data.Profunctor
 import Data.Profunctor.Adjunction
-import Data.Profunctor.Closed
 import Data.Profunctor.Monad
 import Data.Profunctor.Rep
 import Data.Profunctor.Sieve
+import Data.Profunctor.Traversing
 import Data.Profunctor.Unsafe
 import Prelude hiding ((.),id)
 
@@ -61,6 +62,10 @@
 -- see Dan Piponi's article:
 --
 -- <http://blog.sigfpe.com/2011/07/profunctors-in-haskell.html>
+--
+-- 'Procompose' has a polymorphic kind since @5.6@.
+
+-- Procompose :: (k1 -> k2 -> Type) -> (k3 -> k1 -> Type) -> (k3 -> k2 -> Type)
 data Procompose p q d c where
   Procompose :: p x c -> q d x -> Procompose p q d c
 
@@ -83,9 +88,9 @@
   rmap k (Procompose f g) = Procompose (rmap k f) g
   {-# INLINE lmap #-}
   k #. Procompose f g     = Procompose (k #. f) g
-  {-# INLINE ( #. ) #-}
+  {-# INLINE (#.) #-}
   Procompose f g .# k     = Procompose f (g .# k)
-  {-# INLINE ( .# ) #-}
+  {-# INLINE (.#) #-}
 
 instance Profunctor p => Functor (Procompose p q a) where
   fmap k (Procompose f g) = Procompose (rmap k f) g
@@ -127,9 +132,19 @@
   closed (Procompose x y) = Procompose (closed x) (closed y)
   {-# INLINE closed #-}
 
+instance (Traversing p, Traversing q) => Traversing (Procompose p q) where
+  traverse' (Procompose p q) = Procompose (traverse' p) (traverse' q)
+  {-# INLINE traverse' #-}
+
+instance (Mapping p, Mapping q) => Mapping (Procompose p q) where
+  map' (Procompose p q) = Procompose (map' p) (map' q)
+  {-# INLINE map' #-}
+
 instance (Corepresentable p, Corepresentable q) => Costrong (Procompose p q) where
   unfirst = unfirstCorep
+  {-# INLINE unfirst #-}
   unsecond = unsecondCorep
+  {-# INLINE unsecond #-}
 
 -- * Lax identity
 
@@ -227,7 +242,16 @@
 ----------------------------------------------------------------------------
 -- * Rift
 ----------------------------------------------------------------------------
--- | This represents the right Kan lift of a 'Profunctor' @q@ along a 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where the only object is the category Hask, 1-morphisms are profunctors composed and compose with Profunctor composition, and 2-morphisms are just natural transformations.
+
+-- | This represents the right Kan lift of a 'Profunctor' @q@ along a
+-- 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where
+-- the only object is the category Hask, 1-morphisms are profunctors composed
+-- and compose with Profunctor composition, and 2-morphisms are just natural
+-- transformations.
+--
+-- 'Rift' has a polymorphic kind since @5.6@.
+
+-- Rift :: (k3 -> k2 -> Type) -> (k1 -> k2 -> Type) -> (k1 -> k3 -> Type)
 newtype Rift p q a b = Rift { runRift :: forall x. p b x -> q a x }
 
 instance ProfunctorFunctor (Rift p) where
@@ -245,7 +269,7 @@
   rmap bd f = Rift (runRift f . lmap bd)
   {-# INLINE rmap #-}
   bd #. f = Rift (\p -> runRift f (p .# bd))
-  {-# INLINE ( #. ) #-}
+  {-# INLINE (#.) #-}
   f .# ca = Rift (\p -> runRift f p .# ca)
   {-# INLINE (.#) #-}
 
@@ -272,3 +296,16 @@
   unit q = Rift $ \p -> Procompose p q
 
 --instance (ProfunctorAdjunction f g, ProfunctorAdjunction f' g') => ProfunctorAdjunction (ProfunctorCompose f' f) (ProfunctorCompose g g') where
+
+----------------------------------------------------------------------------
+-- * Monoids
+----------------------------------------------------------------------------
+
+
+-- | a 'Category' that is also a 'Profunctor' is a 'Monoid' in @Prof@
+
+eta :: (Profunctor p, Category p) => (->) :-> p
+eta f = rmap f id
+
+mu :: Category p => Procompose p p :-> p
+mu (Procompose f g) = f . g
diff --git a/src/Data/Profunctor/Mapping.hs b/src/Data/Profunctor/Mapping.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Mapping.hs
@@ -0,0 +1,158 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE Safe #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2015-2018 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Data.Profunctor.Mapping
+  ( Mapping(..)
+  , CofreeMapping(..)
+  , FreeMapping(..)
+  -- * Traversing in terms of Mapping
+  , wanderMapping
+  -- * Closed in terms of Mapping
+  , traverseMapping
+  , closedMapping
+  ) where
+
+import Control.Arrow (Kleisli(..))
+import Data.Bifunctor.Tannen
+import Data.Distributive
+import Data.Functor.Compose
+import Data.Functor.Identity
+import Data.Profunctor.Choice
+import Data.Profunctor.Closed
+import Data.Profunctor.Monad
+import Data.Profunctor.Strong
+import Data.Profunctor.Traversing
+import Data.Profunctor.Types
+import Data.Profunctor.Unsafe
+
+class (Traversing p, Closed p) => Mapping p where
+  -- | Laws:
+  --
+  -- @
+  -- 'map'' '.' 'rmap' f ≡ 'rmap' ('fmap' f) '.' 'map''
+  -- 'map'' '.' 'map'' ≡ 'dimap' 'Data.Functor.Compose.Compose' 'Data.Functor.Compose.getCompose' '.' 'map''
+  -- 'dimap' 'Data.Functor.Identity.Identity' 'Data.Functor.Identity.runIdentity' '.' 'map'' ≡ 'id'
+  -- @
+  map' :: Functor f => p a b -> p (f a) (f b)
+  map' = roam fmap
+
+  roam :: ((a -> b) -> s -> t)
+       -> p a b -> p s t
+  roam f = dimap (\s -> Bar $ \ab -> f ab s) lent . map'
+
+newtype Bar t b a = Bar
+  { runBar :: (a -> b) -> t }
+  deriving Functor
+
+lent :: Bar t a a -> t
+lent m = runBar m id
+
+instance Mapping (->) where
+  map' = fmap
+  roam f = f
+
+instance (Monad m, Distributive m) => Mapping (Kleisli m) where
+  map' (Kleisli f) = Kleisli (collect f)
+  roam f = Kleisli #. genMap f .# runKleisli
+
+genMap :: Distributive f => ((a -> b) -> s -> t) -> (a -> f b) -> s -> f t
+genMap abst afb s = fmap (\ab -> abst ab s) (distribute afb)
+
+-- see <https://github.com/ekmett/distributive/issues/12>
+instance (Applicative m, Distributive m) => Mapping (Star m) where
+  map' (Star f) = Star (collect f)
+  roam f = Star #. genMap f .# runStar
+
+instance (Functor f, Mapping p) => Mapping (Tannen f p) where
+  map' = Tannen . fmap map' . runTannen
+
+wanderMapping :: Mapping p => (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
+wanderMapping f = roam ((runIdentity .) #. f .# (Identity .))
+
+traverseMapping :: (Mapping p, Functor f) => p a b -> p (f a) (f b)
+traverseMapping = map'
+
+closedMapping :: Mapping p => p a b -> p (x -> a) (x -> b)
+closedMapping = map'
+
+newtype CofreeMapping p a b = CofreeMapping { runCofreeMapping :: forall f. Functor f => p (f a) (f b) }
+
+instance Profunctor p => Profunctor (CofreeMapping p) where
+  lmap f (CofreeMapping p) = CofreeMapping (lmap (fmap f) p)
+  rmap g (CofreeMapping p) = CofreeMapping (rmap (fmap g) p)
+  dimap f g (CofreeMapping p) = CofreeMapping (dimap (fmap f) (fmap g) p)
+
+instance Profunctor p => Strong (CofreeMapping p) where
+  second' = map'
+
+instance Profunctor p => Choice (CofreeMapping p) where
+  right' = map'
+
+instance Profunctor p => Closed (CofreeMapping p) where
+  closed = map'
+
+instance Profunctor p => Traversing (CofreeMapping p) where
+  traverse' = map'
+  wander f = roam $ (runIdentity .) #. f .# (Identity .)
+
+instance Profunctor p => Mapping (CofreeMapping p) where
+  -- !@(#*&() Compose isn't representational in its second arg or we could use #. and .#
+  map' (CofreeMapping p) = CofreeMapping (dimap Compose getCompose p)
+  roam f (CofreeMapping p) =
+     CofreeMapping $
+       dimap (Compose #. fmap (\s -> Bar $ \ab -> f ab s)) (fmap lent .# getCompose) p
+
+instance ProfunctorFunctor CofreeMapping where
+  promap f (CofreeMapping p) = CofreeMapping (f p)
+
+instance ProfunctorComonad CofreeMapping where
+  proextract (CofreeMapping p) = runIdentity #. p .# Identity
+  produplicate (CofreeMapping p) = CofreeMapping (CofreeMapping (dimap Compose getCompose p))
+
+-- | @FreeMapping -| CofreeMapping@
+data FreeMapping p a b where
+  FreeMapping :: Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b
+
+instance Functor (FreeMapping p a) where
+  fmap f (FreeMapping l m r) = FreeMapping (f . l) m r
+
+instance Profunctor (FreeMapping p) where
+  lmap f (FreeMapping l m r) = FreeMapping l m (r . f)
+  rmap g (FreeMapping l m r) = FreeMapping (g . l) m r
+  dimap f g (FreeMapping l m r) = FreeMapping (g . l) m (r . f)
+  g #. FreeMapping l m r = FreeMapping (g #. l) m r
+  FreeMapping l m r .# f = FreeMapping l m (r .# f)
+
+instance Strong (FreeMapping p) where
+  second' = map'
+
+instance Choice (FreeMapping p) where
+  right' = map'
+
+instance Closed (FreeMapping p) where
+  closed = map'
+
+instance Traversing (FreeMapping p) where
+  traverse' = map'
+  wander f = roam ((runIdentity .) #. f .# (Identity .))
+
+instance Mapping (FreeMapping p) where
+  map' (FreeMapping l m r) = FreeMapping (fmap l .# getCompose) m (Compose #. fmap r)
+
+instance ProfunctorFunctor FreeMapping where
+  promap f (FreeMapping l m r) = FreeMapping l (f m) r
+
+instance ProfunctorMonad FreeMapping where
+  proreturn p = FreeMapping runIdentity p Identity
+  projoin (FreeMapping l (FreeMapping l' m r') r) = FreeMapping ((l . fmap l') .# getCompose) m (Compose #. (fmap r' . r))
diff --git a/src/Data/Profunctor/Monad.hs b/src/Data/Profunctor/Monad.hs
--- a/src/Data/Profunctor/Monad.hs
+++ b/src/Data/Profunctor/Monad.hs
@@ -1,16 +1,88 @@
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Safe #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2014-2015 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
 module Data.Profunctor.Monad where
 
-import Data.Profunctor
+import Control.Comonad
+import Data.Bifunctor.Tannen
+import Data.Bifunctor.Product
+import Data.Bifunctor.Sum
+import Data.Profunctor.Types
 
+-- | 'ProfunctorFunctor' has a polymorphic kind since @5.6@.
+
+-- ProfunctorFunctor :: ((Type -> Type -> Type) -> (k1 -> k2 -> Type)) -> Constraint
 class ProfunctorFunctor t where
-  promap    :: Profunctor p => (p :-> q) -> t p :-> t q
+  -- | Laws:
+  --
+  -- @
+  -- 'promap' f '.' 'promap' g ≡ 'promap' (f '.' g)
+  -- 'promap' 'id' ≡ 'id'
+  -- @
+  promap :: Profunctor p => (p :-> q) -> t p :-> t q
 
+instance Functor f => ProfunctorFunctor (Tannen f) where
+  promap f (Tannen g) = Tannen (fmap f g)
+
+instance ProfunctorFunctor (Product p) where
+  promap f (Pair p q) = Pair p (f q)
+
+instance ProfunctorFunctor (Sum p) where
+  promap _ (L2 p) = L2 p
+  promap f (R2 q) = R2 (f q)
+
+-- | Laws:
+--
+-- @
+-- 'promap' f '.' 'proreturn' ≡ 'proreturn' '.' f
+-- 'projoin' '.' 'proreturn' ≡ 'id'
+-- 'projoin' '.' 'promap' 'proreturn' ≡ 'id'
+-- 'projoin' '.' 'projoin' ≡ 'projoin' '.' 'promap' 'projoin'
+-- @
+
+-- ProfunctorMonad :: ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> Constraint
 class ProfunctorFunctor t => ProfunctorMonad t where
   proreturn :: Profunctor p => p :-> t p
   projoin   :: Profunctor p => t (t p) :-> t p
 
+instance Monad f => ProfunctorMonad (Tannen f) where
+  proreturn = Tannen . return
+  projoin (Tannen m) = Tannen $ m >>= runTannen
+
+instance ProfunctorMonad (Sum p) where
+  proreturn = R2
+  projoin (L2 p) = L2 p
+  projoin (R2 m) = m
+
+-- | Laws:
+--
+-- @
+-- 'proextract' '.' 'promap' f ≡ f '.' 'proextract'
+-- 'proextract' '.' 'produplicate' ≡ 'id'
+-- 'promap' 'proextract' '.' 'produplicate' ≡ 'id'
+-- 'produplicate' '.' 'produplicate' ≡ 'promap' 'produplicate' '.' 'produplicate'
+-- @
+
+-- ProfunctorComonad :: ((Type -> Type -> Type) -> (Type -> Type -> Type)) -> Constraint
 class ProfunctorFunctor t => ProfunctorComonad t where
   proextract :: Profunctor p => t p :-> p
   produplicate :: Profunctor p => t p :-> t (t p)
+
+instance Comonad f => ProfunctorComonad (Tannen f) where
+  proextract = extract . runTannen
+  produplicate (Tannen w) = Tannen $ extend Tannen w
+
+instance ProfunctorComonad (Product p) where
+  proextract (Pair _ q) = q
+  produplicate pq@(Pair p _) = Pair p pq
diff --git a/src/Data/Profunctor/Monoid.hs b/src/Data/Profunctor/Monoid.hs
deleted file mode 100644
--- a/src/Data/Profunctor/Monoid.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-module Data.Profunctor.Monoid where
-
-import Control.Category
-import Data.Profunctor
-import Data.Profunctor.Composition
-
--- | a 'Category' that is also a 'Profunctor' is a 'Monoid' in @Prof@
-
-eta :: (Profunctor p, Category p) => (->) :-> p
-eta f = rmap f id
-
-mu :: Category p => Procompose p p :-> p
-mu (Procompose f g) = f . g
diff --git a/src/Data/Profunctor/Ran.hs b/src/Data/Profunctor/Ran.hs
--- a/src/Data/Profunctor/Ran.hs
+++ b/src/Data/Profunctor/Ran.hs
@@ -1,13 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE Safe #-}
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2013-2014 Edward Kmett and Dan Doel
+-- Copyright   :  (C) 2013-2015 Edward Kmett and Dan Doel
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -21,6 +19,8 @@
   , precomposeRan
   , curryRan
   , uncurryRan
+  , Codensity(..)
+  , decomposeCodensity
   ) where
 
 import Control.Category
@@ -30,7 +30,19 @@
 import Data.Profunctor.Unsafe
 import Prelude hiding (id,(.))
 
--- | This represents the right Kan extension of a 'Profunctor' @q@ along a 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where the only object is the category Hask, 1-morphisms are profunctors composed and compose with Profunctor composition, and 2-morphisms are just natural transformations.
+--------------------------------------------------------------------------------
+-- * Ran
+--------------------------------------------------------------------------------
+
+-- | This represents the right Kan extension of a 'Profunctor' @q@ along a
+-- 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where
+-- the only object is the category Hask, 1-morphisms are profunctors composed
+-- and compose with Profunctor composition, and 2-morphisms are just natural
+-- transformations.
+--
+-- 'Ran' has a polymorphic kind since @5.6@.
+
+-- Ran :: (k1 -> k2 -> Type) -> (k1 -> k3 -> Type) -> (k2 -> k3 -> Type)
 newtype Ran p q a b = Ran { runRan :: forall x. p x a -> q x b }
 
 instance ProfunctorFunctor (Ran p) where
@@ -48,7 +60,7 @@
   rmap bd f = Ran (rmap bd . runRan f)
   {-# INLINE rmap #-}
   bd #. f = Ran (\p -> bd #. runRan f p)
-  {-# INLINE ( #. ) #-}
+  {-# INLINE (#.) #-}
   f .# ca = Ran (\p -> runRan f (ca #. p))
   {-# INLINE (.#) #-}
 
@@ -81,3 +93,42 @@
 uncurryRan :: (p :-> Ran q r) -> Procompose p q :-> r
 uncurryRan f (Procompose p q) = runRan (f p) q
 {-# INLINE uncurryRan #-}
+
+--------------------------------------------------------------------------------
+-- * Codensity
+--------------------------------------------------------------------------------
+
+-- | This represents the right Kan extension of a 'Profunctor' @p@ along
+-- itself. This provides a generalization of the \"difference list\" trick to
+-- profunctors.
+--
+-- 'Codensity' has a polymorphic kind since @5.6@.
+
+-- Codensity :: (k1 -> k2 -> Type) -> (k2 -> k2 -> Type)
+newtype Codensity p a b = Codensity { runCodensity :: forall x. p x a -> p x b }
+
+instance Profunctor p => Profunctor (Codensity p) where
+  dimap ca bd f = Codensity (rmap bd . runCodensity f . rmap ca)
+  {-# INLINE dimap #-}
+  lmap ca f = Codensity (runCodensity f . rmap ca)
+  {-# INLINE lmap #-}
+  rmap bd f = Codensity (rmap bd . runCodensity f)
+  {-# INLINE rmap #-}
+  bd #. f = Codensity (\p -> bd #. runCodensity f p)
+  {-# INLINE (#.) #-}
+  f .# ca = Codensity (\p -> runCodensity f (ca #. p))
+  {-# INLINE (.#) #-}
+
+instance Profunctor p => Functor (Codensity p a) where
+  fmap bd f = Codensity (rmap bd . runCodensity f)
+  {-# INLINE fmap #-}
+
+instance Category (Codensity p) where
+  id = Codensity id
+  {-# INLINE id #-}
+  Codensity f . Codensity g = Codensity (f . g)
+  {-# INLINE (.) #-}
+
+decomposeCodensity :: Procompose (Codensity p) p a b -> p a b
+decomposeCodensity (Procompose (Codensity pp) p) = pp p
+{-# INLINE decomposeCodensity #-}
diff --git a/src/Data/Profunctor/Rep.hs b/src/Data/Profunctor/Rep.hs
--- a/src/Data/Profunctor/Rep.hs
+++ b/src/Data/Profunctor/Rep.hs
@@ -1,14 +1,13 @@
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE Safe #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Profunctor.Rep
@@ -30,6 +29,7 @@
   , Corepresentable(..)
   , cotabulated
   , unfirstCorep, unsecondCorep
+  , closedCorep
   -- * Prep -| Star
   , Prep(..)
   , prepAdj
@@ -47,6 +47,7 @@
 import Control.Applicative
 import Control.Arrow
 import Control.Comonad
+import Control.Monad ((>=>))
 import Data.Functor.Identity
 import Data.Profunctor
 import Data.Profunctor.Sieve
@@ -59,6 +60,12 @@
 -- @p d c@ is isomorphic to @d -> f c@.
 class (Sieve p (Rep p), Strong p) => Representable p where
   type Rep p :: * -> *
+  -- | Laws:
+  --
+  -- @
+  -- 'tabulate' '.' 'sieve' ≡ 'id'
+  -- 'sieve' '.' 'tabulate' ≡ 'id'
+  -- @
   tabulate :: (d -> Rep p c) -> p d c
 
 -- | Default definition for 'first'' given that p is 'Representable'.
@@ -89,7 +96,14 @@
   tabulate = Forget . (getConst .)
   {-# INLINE tabulate #-}
 
+{- TODO: coproducts and products
+instance (Representable p, Representable q) => Representable (Bifunctor.Product p q)
+  type Rep (Bifunctor.Product p q) = Functor.Product p q
 
+instance (Corepresentable p, Corepresentable q) => Corepresentable (Bifunctor.Product p q) where
+  type Rep (Bifunctor.Product p q) = Functor.Sum p q
+-}
+
 type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)
 
 -- | 'tabulate' and 'sieve' form two halves of an isomorphism.
@@ -107,18 +121,28 @@
 -- @p d c@ is isomorphic to @f d -> c@.
 class (Cosieve p (Corep p), Costrong p) => Corepresentable p where
   type Corep p :: * -> *
+  -- | Laws:
+  --
+  -- @
+  -- 'cotabulate' '.' 'cosieve' ≡ 'id'
+  -- 'cosieve' '.' 'cotabulate' ≡ 'id'
+  -- @
   cotabulate :: (Corep p d -> c) -> p d c
 
--- | Default definition for 'unfirst' given that p is 'Corepresentable'.
+-- | Default definition for 'unfirst' given that @p@ is 'Corepresentable'.
 unfirstCorep :: Corepresentable p => p (a, d) (b, d) -> p a b
 unfirstCorep p = cotabulate f
   where f fa = b where (b, d) = cosieve p ((\a -> (a, d)) <$> fa)
 
--- | Default definition for 'unsecond' given that p is 'Corepresentable'.
+-- | Default definition for 'unsecond' given that @p@ is 'Corepresentable'.
 unsecondCorep :: Corepresentable p => p (d, a) (d, b) -> p a b
 unsecondCorep p = cotabulate f
   where f fa = b where (d, b) = cosieve p ((,) d <$> fa)
 
+-- | Default definition for 'closed' given that @p@ is 'Corepresentable'
+closedCorep :: Corepresentable p => p a b -> p (x -> a) (x -> b)
+closedCorep p = cotabulate $ \fs x -> cosieve p (fmap ($ x) fs)
+
 instance Corepresentable (->) where
   type Corep (->) = Identity
   cotabulate f = f . Identity
@@ -156,6 +180,10 @@
 --
 -- This gives rise to a monad in @Prof@, @('Star'.'Prep')@, and
 -- a comonad in @[Hask,Hask]@ @('Prep'.'Star')@
+--
+-- 'Prep' has a polymorphic kind since @5.6@.
+
+-- Prep :: (Type -> k -> Type) -> (k -> Type)
 data Prep p a where
   Prep :: x -> p x a -> Prep p a
 
@@ -168,8 +196,10 @@
     go (xf',xa') = sieve pf xf' <*> sieve pa xa'
 
 instance (Monad (Rep p), Representable p) => Monad (Prep p) where
+#if !(MIN_VERSION_base(4,11,0))
   return a = Prep () $ tabulate $ const $ return a
-  Prep xa pa >>= f = Prep xa $ tabulate $ \xa' -> sieve pa xa' >>= \a -> case f a of
+#endif
+  Prep xa pa >>= f = Prep xa $ tabulate $ sieve pa >=> \a -> case f a of
     Prep xb pb -> sieve pb xb
 
 prepAdj :: (forall a. Prep p a -> g a) -> p :-> Star g
@@ -188,6 +218,9 @@
 -- * Coprep
 --------------------------------------------------------------------------------
 
+-- | 'Prep' has a polymorphic kind since @5.6@.
+
+-- Coprep :: (k -> Type -> Type) -> (k -> Type)
 newtype Coprep p a = Coprep { runCoprep :: forall r. p a r -> r }
 
 instance Profunctor p => Functor (Coprep p) where
diff --git a/src/Data/Profunctor/Sieve.hs b/src/Data/Profunctor/Sieve.hs
--- a/src/Data/Profunctor/Sieve.hs
+++ b/src/Data/Profunctor/Sieve.hs
@@ -1,12 +1,8 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
 {-# LANGUAGE Trustworthy #-}
-#endif
 -----------------------------------------------------------------------------
 -- |
 -- Copyright   :  (C) 2015 Edward Kmett
diff --git a/src/Data/Profunctor/Strong.hs b/src/Data/Profunctor/Strong.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Strong.hs
@@ -0,0 +1,472 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Safe #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2014-2015 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  Rank2Types
+--
+----------------------------------------------------------------------------
+module Data.Profunctor.Strong
+  (
+  -- * Strength
+    Strong(..)
+  , uncurry'
+  , strong
+  , Tambara(..)
+  , tambara, untambara
+  , Pastro(..)
+  , pastro, unpastro
+  -- * Costrength
+  , Costrong(..)
+  , Cotambara(..)
+  , cotambara, uncotambara
+  , Copastro(..)
+  ) where
+
+import Control.Applicative hiding (WrappedArrow(..))
+import Control.Arrow
+import Control.Category
+import Control.Comonad
+import Control.Monad (liftM)
+import Control.Monad.Fix
+import Data.Bifunctor.Clown (Clown(..))
+import Data.Bifunctor.Product (Product(..))
+import Data.Bifunctor.Sum (Sum(..))
+import Data.Bifunctor.Tannen (Tannen(..))
+import Data.Functor.Contravariant (Contravariant(..))
+import Data.Profunctor.Adjunction
+import Data.Profunctor.Monad
+import Data.Profunctor.Types
+import Data.Profunctor.Unsafe
+import Data.Semigroup hiding (Product, Sum)
+import Data.Tagged
+import Data.Tuple
+import Prelude hiding (id,(.))
+
+------------------------------------------------------------------------------
+-- Strong
+------------------------------------------------------------------------------
+
+-- | Generalizing 'Star' of a strong 'Functor'
+--
+-- /Note:/ Every 'Functor' in Haskell is strong with respect to @(,)@.
+--
+-- This describes profunctor strength with respect to the product structure
+-- of Hask.
+--
+-- <http://www.riec.tohoku.ac.jp/~asada/papers/arrStrMnd.pdf>
+--
+class Profunctor p => Strong p where
+  -- | Laws:
+  --
+  -- @
+  -- 'first'' ≡ 'dimap' 'swap' 'swap' '.' 'second''
+  -- 'lmap' 'fst' ≡ 'rmap' 'fst' '.' 'first''
+  -- 'lmap' ('second'' f) '.' 'first'' ≡ 'rmap' ('second'' f) '.' 'first''
+  -- 'first'' '.' 'first'' ≡ 'dimap' assoc unassoc '.' 'first'' where
+  --   assoc ((a,b),c) = (a,(b,c))
+  --   unassoc (a,(b,c)) = ((a,b),c)
+  -- @
+  first' :: p a b  -> p (a, c) (b, c)
+  first' = dimap swap swap . second'
+
+  -- | Laws:
+  --
+  -- @
+  -- 'second'' ≡ 'dimap' 'swap' 'swap' '.' 'first''
+  -- 'lmap' 'snd' ≡ 'rmap' 'snd' '.' 'second''
+  -- 'lmap' ('first'' f) '.' 'second'' ≡ 'rmap' ('first'' f) '.' 'second''
+  -- 'second'' '.' 'second'' ≡ 'dimap' unassoc assoc '.' 'second'' where
+  --   assoc ((a,b),c) = (a,(b,c))
+  --   unassoc (a,(b,c)) = ((a,b),c)
+  -- @
+  second' :: p a b -> p (c, a) (c, b)
+  second' = dimap swap swap . first'
+
+  {-# MINIMAL first' | second' #-}
+
+uncurry' :: Strong p => p a (b -> c) -> p (a, b) c
+uncurry' = rmap (\(f,x) -> f x) . first'
+{-# INLINE uncurry' #-}
+
+strong :: Strong p => (a -> b -> c) -> p a b -> p a c
+strong f x = dimap (\a -> (a, a)) (\(b, a) -> f a b) (first' x)
+
+instance Strong (->) where
+  first' ab ~(a, c) = (ab a, c)
+  {-# INLINE first' #-}
+  second' ab ~(c, a) = (c, ab a)
+  {-# INLINE second' #-}
+
+instance Monad m => Strong (Kleisli m) where
+  first' (Kleisli f) = Kleisli $ \ ~(a, c) -> do
+     b <- f a
+     return (b, c)
+  {-# INLINE first' #-}
+  second' (Kleisli f) = Kleisli $ \ ~(c, a) -> do
+     b <- f a
+     return (c, b)
+  {-# INLINE second' #-}
+
+instance Functor m => Strong (Star m) where
+  first' (Star f) = Star $ \ ~(a, c) -> (\b' -> (b', c)) <$> f a
+  {-# INLINE first' #-}
+  second' (Star f) = Star $ \ ~(c, a) -> (,) c <$> f a
+  {-# INLINE second' #-}
+
+-- | 'Arrow' is 'Strong' 'Category'
+instance Arrow p => Strong (WrappedArrow p) where
+  first' (WrapArrow k) = WrapArrow (first k)
+  {-# INLINE first' #-}
+  second' (WrapArrow k) = WrapArrow (second k)
+  {-# INLINE second' #-}
+
+instance Strong (Forget r) where
+  first' (Forget k) = Forget (k . fst)
+  {-# INLINE first' #-}
+  second' (Forget k) = Forget (k . snd)
+  {-# INLINE second' #-}
+
+instance Contravariant f => Strong (Clown f) where
+  first' (Clown fa) = Clown (contramap fst fa)
+  {-# INLINE first' #-}
+  second' (Clown fa) = Clown (contramap snd fa)
+  {-# INLINE second' #-}
+
+instance (Strong p, Strong q) => Strong (Product p q) where
+  first' (Pair p q) = Pair (first' p) (first' q)
+  {-# INLINE first' #-}
+  second' (Pair p q) = Pair (second' p) (second' q)
+  {-# INLINE second' #-}
+
+instance (Strong p, Strong q) => Strong (Sum p q) where
+  first' (L2 p) = L2 (first' p)
+  first' (R2 q) = R2 (first' q)
+  {-# INLINE first' #-}
+  second' (L2 p) = L2 (second' p)
+  second' (R2 q) = R2 (second' q)
+  {-# INLINE second' #-}
+
+instance (Functor f, Strong p) => Strong (Tannen f p) where
+  first' (Tannen fp) = Tannen (fmap first' fp)
+  {-# INLINE first' #-}
+  second' (Tannen fp) = Tannen (fmap second' fp)
+  {-# INLINE second' #-}
+
+----------------------------------------------------------------------------
+-- * Tambara
+----------------------------------------------------------------------------
+
+-- | 'Tambara' cofreely makes any 'Profunctor' 'Strong'.
+newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }
+
+instance Profunctor p => Profunctor (Tambara p) where
+  dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p
+  {-# INLINE dimap #-}
+
+instance ProfunctorFunctor Tambara where
+  promap f (Tambara p) = Tambara (f p)
+
+instance ProfunctorComonad Tambara where
+  proextract (Tambara p) = dimap (\a -> (a,())) fst p
+  produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p) where
+    hither :: ((a, b), c) -> (a, (b, c))
+    hither ~(~(x,y),z) = (x,(y,z))
+
+    yon    :: (a, (b, c)) -> ((a, b), c)
+    yon    ~(x,~(y,z)) = ((x,y),z)
+
+instance Profunctor p => Strong (Tambara p) where
+  first' p = runTambara $ produplicate p
+  {-# INLINE first' #-}
+
+instance Category p => Category (Tambara p) where
+  id = Tambara id
+  Tambara p . Tambara q = Tambara (p . q)
+
+instance Arrow p => Arrow (Tambara p) where
+  arr f = Tambara $ arr $ first f
+  first (Tambara f) = Tambara (arr go . first f . arr go) where
+    go :: ((a, b), c) -> ((a, c), b)
+    go ~(~(x,y),z) = ((x,z),y)
+
+instance ArrowChoice p => ArrowChoice (Tambara p) where
+  left (Tambara f) = Tambara (arr yon . left f . arr hither) where
+    hither :: (Either a b, c) -> Either (a, c) (b, c)
+    hither (Left y, s) = Left (y, s)
+    hither (Right z, s) = Right (z, s)
+
+    yon :: Either (a, c) (b, c) -> (Either a b, c)
+    yon (Left (y, s)) = (Left y, s)
+    yon (Right (z, s)) = (Right z, s)
+
+instance ArrowApply p => ArrowApply (Tambara p) where
+  app = Tambara $ app . arr (\((Tambara f, x), s) -> (f, (x, s)))
+
+instance ArrowLoop p => ArrowLoop (Tambara p) where
+  loop (Tambara f) = Tambara (loop (arr go . f . arr go)) where
+    go :: ((a, b), c) -> ((a, c), b)
+    go ~(~(x,y),z) = ((x,z),y)
+
+instance ArrowZero p => ArrowZero (Tambara p) where
+  zeroArrow = Tambara zeroArrow
+
+instance ArrowPlus p => ArrowPlus (Tambara p) where
+  Tambara f <+> Tambara g = Tambara (f <+> g)
+
+instance Profunctor p => Functor (Tambara p a) where
+  fmap = rmap
+
+instance (Profunctor p, Arrow p) => Applicative (Tambara p a) where
+  pure x = arr (const x)
+  f <*> g = arr (uncurry id) . (f &&& g)
+
+instance (Profunctor p, ArrowPlus p) => Alternative (Tambara p a) where
+  empty = zeroArrow
+  f <|> g = f <+> g
+
+instance ArrowPlus p => Semigroup (Tambara p a b) where
+  f <> g = f <+> g
+
+instance ArrowPlus p => Monoid (Tambara p a b) where
+  mempty = zeroArrow
+#if !(MIN_VERSION_base(4,11,0))
+  mappend = (<>)
+#endif
+
+-- |
+-- @
+-- 'tambara' ('untambara' f) ≡ f
+-- 'untambara' ('tambara' f) ≡ f
+-- @
+tambara :: Strong p => (p :-> q) -> p :-> Tambara q
+tambara f p = Tambara $ f $ first' p
+
+-- |
+-- @
+-- 'tambara' ('untambara' f) ≡ f
+-- 'untambara' ('tambara' f) ≡ f
+-- @
+untambara :: Profunctor q => (p :-> Tambara q) -> p :-> q
+untambara f p = dimap (\a -> (a,())) fst $ runTambara $ f p
+
+----------------------------------------------------------------------------
+-- * Pastro
+----------------------------------------------------------------------------
+
+-- | Pastro -| Tambara
+--
+-- @
+-- Pastro p ~ exists z. Costar ((,)z) `Procompose` p `Procompose` Star ((,)z)
+-- @
+--
+-- 'Pastro' freely makes any 'Profunctor' 'Strong'.
+data Pastro p a b where
+  Pastro :: ((y, z) -> b) -> p x y -> (a -> (x, z)) -> Pastro p a b
+
+instance Functor (Pastro p a) where
+  fmap f (Pastro l m r) = Pastro (f . l) m r
+
+instance Profunctor (Pastro p) where
+  dimap f g (Pastro l m r) = Pastro (g . l) m (r . f)
+  lmap f (Pastro l m r) = Pastro l m (r . f)
+  rmap g (Pastro l m r) = Pastro (g . l) m r
+  w #. Pastro l m r = Pastro (w #. l) m r
+  Pastro l m r .# w = Pastro l m (r .# w)
+
+instance ProfunctorFunctor Pastro where
+  promap f (Pastro l m r) = Pastro l (f m) r
+
+instance ProfunctorMonad Pastro where
+  proreturn p = Pastro fst p $ \a -> (a,())
+  projoin (Pastro l (Pastro m n o) p) = Pastro lm n op where
+    op a = case p a of
+      (b, f) -> case o b of
+         (c, g) -> (c, (f, g))
+    lm (d, (f, g)) = l (m (d, g), f)
+
+instance ProfunctorAdjunction Pastro Tambara where
+  counit (Pastro g (Tambara p) f) = dimap f g p
+  unit p = Tambara (Pastro id p id)
+
+instance Strong (Pastro p) where
+  first' (Pastro l m r) = Pastro l' m r' where
+    r' (a,c) = case r a of
+      (x,z) -> (x,(z,c))
+    l' (y,(z,c)) = (l (y,z), c)
+  second' (Pastro l m r) = Pastro l' m r' where
+    r' (c,a) = case r a of
+      (x,z) -> (x,(c,z))
+    l' (y,(c,z)) = (c,l (y,z))
+
+-- |
+-- @
+-- 'pastro' ('unpastro' f) ≡ f
+-- 'unpastro' ('pastro' f) ≡ f
+-- @
+pastro :: Strong q => (p :-> q) -> Pastro p :-> q
+pastro f (Pastro r g l) = dimap l r (first' (f g))
+
+-- |
+-- @
+-- 'pastro' ('unpastro' f) ≡ f
+-- 'unpastro' ('pastro' f) ≡ f
+-- @
+unpastro :: (Pastro p :-> q) -> p :-> q
+unpastro f p = f (Pastro fst p (\a -> (a, ())))
+
+--------------------------------------------------------------------------------
+-- * Costrength for (,)
+--------------------------------------------------------------------------------
+
+-- | Analogous to 'ArrowLoop', 'loop' = 'unfirst'
+class Profunctor p => Costrong p where
+  -- | Laws:
+  --
+  -- @
+  -- 'unfirst' ≡ 'unsecond' '.' 'dimap' 'swap' 'swap'
+  -- 'lmap' (,()) ≡ 'unfirst' '.' 'rmap' (,())
+  -- 'unfirst' '.' 'lmap' ('second' f) ≡ 'unfirst' '.' 'rmap' ('second' f)
+  -- 'unfirst' '.' 'unfirst' = 'unfirst' '.' 'dimap' assoc unassoc where
+  --   assoc ((a,b),c) = (a,(b,c))
+  --   unassoc (a,(b,c)) = ((a,b),c)
+  -- @
+  unfirst  :: p (a, d) (b, d) -> p a b
+  unfirst = unsecond . dimap swap swap
+
+  -- | Laws:
+  --
+  -- @
+  -- 'unsecond' ≡ 'unfirst' '.' 'dimap' 'swap' 'swap'
+  -- 'lmap' ((),) ≡ 'unsecond' '.' 'rmap' ((),)
+  -- 'unsecond' '.' 'lmap' ('first' f) ≡ 'unsecond' '.' 'rmap' ('first' f)
+  -- 'unsecond' '.' 'unsecond' = 'unsecond' '.' 'dimap' unassoc assoc where
+  --   assoc ((a,b),c) = (a,(b,c))
+  --   unassoc (a,(b,c)) = ((a,b),c)
+  -- @
+  unsecond :: p (d, a) (d, b) -> p a b
+  unsecond = unfirst . dimap swap swap
+
+  {-# MINIMAL unfirst | unsecond #-}
+
+instance Costrong (->) where
+  unfirst f a = b where (b, d) = f (a, d)
+  unsecond f a = b where (d, b) = f (d, a)
+
+instance Functor f => Costrong (Costar f) where
+  unfirst (Costar f) = Costar f'
+    where f' fa = b where (b, d) = f ((\a -> (a, d)) <$> fa)
+  unsecond (Costar f) = Costar f'
+    where f' fa = b where (d, b) = f ((,) d <$> fa)
+
+instance Costrong Tagged where
+  unfirst (Tagged bd) = Tagged (fst bd)
+  unsecond (Tagged db) = Tagged (snd db)
+
+instance ArrowLoop p => Costrong (WrappedArrow p) where
+  unfirst (WrapArrow k) = WrapArrow (loop k)
+
+instance MonadFix m => Costrong (Kleisli m) where
+  unfirst (Kleisli f) = Kleisli (liftM fst . mfix . f')
+    where f' x y = f (x, snd y)
+
+instance Functor f => Costrong (Cokleisli f) where
+  unfirst (Cokleisli f) = Cokleisli f'
+    where f' fa = b where (b, d) = f ((\a -> (a, d)) <$> fa)
+
+instance (Functor f, Costrong p) => Costrong (Tannen f p) where
+  unfirst (Tannen fp) = Tannen (fmap unfirst fp)
+  unsecond (Tannen fp) = Tannen (fmap unsecond fp)
+
+instance (Costrong p, Costrong q) => Costrong (Product p q) where
+  unfirst (Pair p q) = Pair (unfirst p) (unfirst q)
+  unsecond (Pair p q) = Pair (unsecond p) (unsecond q)
+
+instance (Costrong p, Costrong q) => Costrong (Sum p q) where
+  unfirst (L2 p) = L2 (unfirst p)
+  unfirst (R2 q) = R2 (unfirst q)
+  unsecond (L2 p) = L2 (unsecond p)
+  unsecond (R2 q) = R2 (unsecond q)
+
+----------------------------------------------------------------------------
+-- * Cotambara
+----------------------------------------------------------------------------
+
+-- | Cotambara cofreely constructs costrength
+data Cotambara q a b where
+    Cotambara :: Costrong r => (r :-> q) -> r a b -> Cotambara q a b
+
+instance Profunctor (Cotambara p) where
+  lmap f (Cotambara n p) = Cotambara n (lmap f p)
+  rmap g (Cotambara n p) = Cotambara n (rmap g p)
+  dimap f g (Cotambara n p) = Cotambara n (dimap f g p)
+
+instance ProfunctorFunctor Cotambara where
+  promap f (Cotambara n p) = Cotambara (f . n) p
+
+instance ProfunctorComonad Cotambara where
+  proextract (Cotambara n p)  = n p
+  produplicate (Cotambara n p) = Cotambara id (Cotambara n p)
+
+instance Costrong (Cotambara p) where
+  unfirst (Cotambara n p) = Cotambara n (unfirst p)
+
+instance Functor (Cotambara p a) where
+  fmap = rmap
+
+-- |
+-- @
+-- 'cotambara' '.' 'uncotambara' ≡ 'id'
+-- 'uncotambara' '.' 'cotambara' ≡ 'id'
+-- @
+cotambara :: Costrong p => (p :-> q) -> p :-> Cotambara q
+cotambara f = Cotambara f
+
+-- |
+-- @
+-- 'cotambara' '.' 'uncotambara' ≡ 'id'
+-- 'uncotambara' '.' 'cotambara' ≡ 'id'
+-- @
+uncotambara :: Profunctor q => (p :-> Cotambara q) -> p :-> q
+uncotambara f p = proextract (f p)
+
+----------------------------------------------------------------------------
+-- * Copastro
+----------------------------------------------------------------------------
+
+-- | Copastro -| Cotambara
+--
+-- Copastro freely constructs costrength
+newtype Copastro p a b = Copastro { runCopastro :: forall r. Costrong r => (forall x y. p x y -> r x y) -> r a b }
+
+instance Functor (Copastro p a) where
+  fmap f (Copastro h) = Copastro $ \ n -> rmap f (h n)
+
+instance Profunctor (Copastro p) where
+  dimap f g (Copastro h) = Copastro $ \ n -> dimap f g (h n)
+  lmap f (Copastro h) = Copastro $ \ n -> lmap f (h n)
+  rmap g (Copastro h) = Copastro $ \ n -> rmap g (h n)
+
+instance ProfunctorAdjunction Copastro Cotambara where
+ unit p = Cotambara id (proreturn p)
+ counit (Copastro h) = proextract (h id)
+
+instance ProfunctorFunctor Copastro where
+  promap f (Copastro h) = Copastro $ \n -> h (n . f)
+
+instance ProfunctorMonad Copastro where
+  proreturn p = Copastro $ \n -> n p
+  projoin p = Copastro $ \c -> runCopastro p (\x -> runCopastro x c)
+
+instance Costrong (Copastro p) where
+  unfirst (Copastro p) = Copastro $ \n -> unfirst (p n)
+  unsecond (Copastro p) = Copastro $ \n -> unsecond (p n)
diff --git a/src/Data/Profunctor/Tambara.hs b/src/Data/Profunctor/Tambara.hs
deleted file mode 100644
--- a/src/Data/Profunctor/Tambara.hs
+++ /dev/null
@@ -1,261 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ <= 708
-{-# LANGUAGE Trustworthy #-}
-#endif
------------------------------------------------------------------------------
--- |
--- Copyright   :  (C) 2014 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  provisional
--- Portability :  Rank2Types
---
-----------------------------------------------------------------------------
-module Data.Profunctor.Tambara
-  ( Tambara(..)
-  , tambara, untambara
-  , Pastro(..)
-  , Cotambara(..)
-  , cotambara, uncotambara
-  , Copastro(..)
-  ) where
-
-import Control.Applicative
-import Control.Arrow
-import Control.Category
-import Data.Monoid
-import Data.Profunctor
-import Data.Profunctor.Adjunction
-import Data.Profunctor.Monad
-import Data.Profunctor.Unsafe
-import Prelude hiding (id,(.))
-
-----------------------------------------------------------------------------
--- * Tambara
-----------------------------------------------------------------------------
-
-newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }
-
-instance Profunctor p => Profunctor (Tambara p) where
-  dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p
-  {-# INLINE dimap #-}
-
-instance ProfunctorFunctor Tambara where
-  promap f (Tambara p) = Tambara (f p)
-
-instance ProfunctorComonad Tambara where
-  proextract (Tambara p) = dimap (\a -> (a,())) fst p
-  produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p) where
-    hither :: ((a, b), c) -> (a, (b, c))
-    hither ~(~(x,y),z) = (x,(y,z))
-
-    yon    :: (a, (b, c)) -> ((a, b), c)
-    yon    ~(x,~(y,z)) = ((x,y),z)
-
-instance Profunctor p => Strong (Tambara p) where
-  first' = runTambara . produplicate
-  {-# INLINE first' #-}
-
-instance Choice p => Choice (Tambara p) where
-  left' (Tambara f) = Tambara $ dimap hither yon $ left' f where
-    hither :: (Either a b, c) -> Either (a, c) (b, c)
-    hither (Left y, s) = Left (y, s)
-    hither (Right z, s) = Right (z, s)
-
-    yon :: Either (a, c) (b, c) -> (Either a b, c)
-    yon (Left (y, s)) = (Left y, s)
-    yon (Right (z, s)) = (Right z, s)
-
-instance Category p => Category (Tambara p) where
-  id = Tambara id
-  Tambara p . Tambara q = Tambara (p . q)
-
-instance Arrow p => Arrow (Tambara p) where
-  arr f = Tambara $ arr $ first f
-  first (Tambara f) = Tambara (arr go . first f . arr go) where
-    go :: ((a, b), c) -> ((a, c), b)
-    go ~(~(x,y),z) = ((x,z),y)
-
-instance ArrowChoice p => ArrowChoice (Tambara p) where
-  left (Tambara f) = Tambara (arr yon . left f . arr hither) where
-    hither :: (Either a b, c) -> Either (a, c) (b, c)
-    hither (Left y, s) = Left (y, s)
-    hither (Right z, s) = Right (z, s)
-
-    yon :: Either (a, c) (b, c) -> (Either a b, c)
-    yon (Left (y, s)) = (Left y, s)
-    yon (Right (z, s)) = (Right z, s)
-
-instance ArrowApply p => ArrowApply (Tambara p) where
-  app = Tambara $ app . arr (\((Tambara f, x), s) -> (f, (x, s)))
-
-instance ArrowLoop p => ArrowLoop (Tambara p) where
-  loop (Tambara f) = Tambara (loop (arr go . f . arr go)) where
-    go :: ((a, b), c) -> ((a, c), b)
-    go ~(~(x,y),z) = ((x,z),y)
-
-instance ArrowZero p => ArrowZero (Tambara p) where
-  zeroArrow = Tambara zeroArrow
-
-instance ArrowPlus p => ArrowPlus (Tambara p) where
-  Tambara f <+> Tambara g = Tambara (f <+> g)
-
-instance Profunctor p => Functor (Tambara p a) where
-  fmap = rmap
-
-instance (Profunctor p, Arrow p) => Applicative (Tambara p a) where
-  pure x = arr (const x)
-  f <*> g = arr (uncurry id) . (f &&& g)
-
-instance (Profunctor p, ArrowPlus p) => Alternative (Tambara p a) where
-  empty = zeroArrow
-  f <|> g = f <+> g
-
-instance (Profunctor p, ArrowPlus p) => Monoid (Tambara p a b) where
-  mempty = zeroArrow
-  mappend f g = f <+> g
-
--- |
--- @
--- 'tambara' '.' 'untambara' ≡ 'id'
--- 'untambara' '.' 'tambara' ≡ 'id'
--- @
-tambara :: Strong p => (p :-> q) -> p :-> Tambara q
-tambara f p = Tambara $ f $ first' p
-
--- |
--- @
--- 'tambara' '.' 'untambara' ≡ 'id'
--- 'untambara' '.' 'tambara' ≡ 'id'
--- @
-untambara :: Profunctor q => (p :-> Tambara q) -> p :-> q
-untambara f p = dimap (\a -> (a,())) fst $ runTambara $ f p
-
-----------------------------------------------------------------------------
--- * Pastro
-----------------------------------------------------------------------------
-
--- | Pastro -| Tambara
---
--- @
--- Pastro p ~ exists z. Costar ((,)z) `Procompose` p `Procompose` Star ((,)z)
--- @
-data Pastro p a b where
-  Pastro :: ((y, z) -> b) -> p x y -> (a -> (x, z)) -> Pastro p a b
-
-instance Profunctor p => Profunctor (Pastro p) where
-  dimap f g (Pastro l m r) = Pastro (g . l) m (r . f)
-  lmap f (Pastro l m r) = Pastro l m (r . f)
-  rmap g (Pastro l m r) = Pastro (g . l) m r
-  w #. Pastro l m r = Pastro (w #. l) m r
-  Pastro l m r .# w = Pastro l m (r .# w)
-
-instance ProfunctorFunctor Pastro where
-  promap f (Pastro l m r) = Pastro l (f m) r
-
-instance ProfunctorMonad Pastro where
-  proreturn p = Pastro fst p $ \a -> (a,())
-  projoin (Pastro l (Pastro m n o) p) = Pastro lm n op where
-    op a = case p a of
-      (b, f) -> case o b of
-         (c, g) -> (c, (f, g))
-    lm (d, (f, g)) = l (m (d, g), f)
-
-instance ProfunctorAdjunction Pastro Tambara where
-  counit (Pastro g (Tambara p) f) = dimap f g p
-  unit p = Tambara (Pastro id p id)
-
-----------------------------------------------------------------------------
--- * Cotambara
-----------------------------------------------------------------------------
-
--- | Cotambara is freely adjoins respect for cocartesian structure to a profunctor
---
--- Note: this is not dual to 'Tambara'. It is 'Tambara' with respect to a different tensor.
-newtype Cotambara p a b = Cotambara { runCotambara :: forall c. p (Either a c) (Either b c) }
-
-instance ProfunctorFunctor Cotambara where
-  promap f (Cotambara p) = Cotambara (f p)
-
-instance ProfunctorComonad Cotambara where
-  proextract (Cotambara p)   = dimap Left (\(Left a) -> a) p
-  produplicate (Cotambara p) = Cotambara (Cotambara $ dimap hither yon p) where
-    hither :: Either (Either a b) c -> Either a (Either b c)
-    hither (Left (Left x))   = Left x
-    hither (Left (Right y))  = Right (Left y)
-    hither (Right z)         = Right (Right z)
-
-    yon    :: Either a (Either b c) -> Either (Either a b) c
-    yon    (Left x)          = Left (Left x)
-    yon    (Right (Left y))  = Left (Right y)
-    yon    (Right (Right z)) = Right z
-
-instance Profunctor p => Profunctor (Cotambara p) where
-  dimap f g (Cotambara p) = Cotambara $ dimap (left f) (left g) p
-  {-# INLINE dimap #-}
-
-instance Profunctor p => Choice (Cotambara p) where
-  left' = runCotambara . produplicate
-  {-# INLINE left' #-}
-
-instance Category p => Category (Cotambara p) where
-  id = Cotambara id
-  Cotambara p . Cotambara q = Cotambara (p . q)
-
-instance Profunctor p => Functor (Cotambara p a) where
-  fmap = rmap
-
--- |
--- @
--- 'cotambara' '.' 'uncotambara' ≡ 'id'
--- 'uncotambara' '.' 'cotambara' ≡ 'id'
--- @
-cotambara :: Choice p => (p :-> q) -> p :-> Cotambara q
-cotambara f p = Cotambara $ f $ left' p
-
--- |
--- @
--- 'cotambara' '.' 'uncotambara' ≡ 'id'
--- 'uncotambara' '.' 'cotambara' ≡ 'id'
--- @
-uncotambara :: Profunctor q => (p :-> Cotambara q) -> p :-> q
-uncotambara f p = dimap Left (\(Left a) -> a) $ runCotambara $ f p
-
-----------------------------------------------------------------------------
--- * Copastro
-----------------------------------------------------------------------------
-
--- | Copastro -| Cotambara
-data Copastro p a b where
-  Copastro :: (Either y z -> b) -> p x y -> (a -> Either x z) -> Copastro p a b
-
-instance Profunctor p => Profunctor (Copastro p) where
-  dimap f g (Copastro l m r) = Copastro (g . l) m (r . f)
-  lmap f (Copastro l m r) = Copastro l m (r . f)
-  rmap g (Copastro l m r) = Copastro (g . l) m r
-  w #. Copastro l m r = Copastro (w #. l) m r
-  Copastro l m r .# w = Copastro l m (r .# w)
-
-instance ProfunctorAdjunction Copastro Cotambara where
-  counit (Copastro f (Cotambara g) h) = dimap h f g
-  unit p = Cotambara $ Copastro id p id
-
-instance ProfunctorFunctor Copastro where
-  promap f (Copastro l m r) = Copastro l (f m) r
-
-instance ProfunctorMonad Copastro where
-  proreturn p = Copastro (\(Left a)-> a) p Left
-  projoin (Copastro l (Copastro m n o) q) = Copastro lm n oq where
-    oq a = case q a of
-      Left b -> case o b of
-        Left c -> Left c
-        Right z -> Right (Left z)
-      Right z -> Right (Right z)
-    lm (Left x) = l $ Left $ m $ Left x
-    lm (Right (Left y)) = l $ Left $ m $ Right y
-    lm (Right (Right z)) = l $ Right z
diff --git a/src/Data/Profunctor/Trace.hs b/src/Data/Profunctor/Trace.hs
deleted file mode 100644
--- a/src/Data/Profunctor/Trace.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Profunctor.Trace
--- Copyright   :  (C) 2011-2012 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  provisional
--- Portability :  GADTs
---
-----------------------------------------------------------------------------
-module Data.Profunctor.Trace
-  ( Trace(..)
-  ) where
-
--- | Coend of 'Data.Profunctor.Profunctor' from @Hask -> Hask@.
-data Trace f where
-  Trace :: f a a -> Trace f
diff --git a/src/Data/Profunctor/Traversing.hs b/src/Data/Profunctor/Traversing.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Traversing.hs
@@ -0,0 +1,189 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE Safe #-}
+module Data.Profunctor.Traversing
+  ( Traversing(..)
+  , CofreeTraversing(..)
+  , FreeTraversing(..)
+  -- * Profunctor in terms of Traversing
+  , dimapWandering
+  , lmapWandering
+  , rmapWandering
+  -- * Strong in terms of Traversing
+  , firstTraversing
+  , secondTraversing
+  -- * Choice in terms of Traversing
+  , leftTraversing
+  , rightTraversing
+  ) where
+
+import Control.Applicative
+import Control.Arrow (Kleisli(..))
+import Data.Bifunctor.Tannen
+import Data.Functor.Compose
+import Data.Functor.Identity
+import Data.Orphans ()
+import Data.Profunctor.Choice
+import Data.Profunctor.Monad
+import Data.Profunctor.Strong
+import Data.Profunctor.Types
+import Data.Profunctor.Unsafe
+import Data.Traversable
+import Data.Tuple (swap)
+
+firstTraversing :: Traversing p => p a b -> p (a, c) (b, c)
+firstTraversing = dimap swap swap . traverse'
+
+secondTraversing :: Traversing p => p a b -> p (c, a) (c, b)
+secondTraversing = traverse'
+
+swapE :: Either a b -> Either b a
+swapE = either Right Left
+
+-- | A definition of 'dimap' for 'Traversing' instances that define
+-- an explicit 'wander'.
+dimapWandering :: Traversing p => (a' -> a) -> (b -> b') -> p a b -> p a' b'
+dimapWandering f g = wander (\afb a' -> g <$> afb (f a'))
+
+-- | 'lmapWandering' may be a more efficient implementation
+-- of 'lmap' than the default produced from 'dimapWandering'.
+lmapWandering :: Traversing p => (a -> b) -> p b c -> p a c
+lmapWandering f = wander (\afb a' -> afb (f a'))
+
+-- | 'rmapWandering' is the same as the default produced from
+-- 'dimapWandering'.
+rmapWandering :: Traversing p => (b -> c) -> p a b -> p a c
+rmapWandering g = wander (\afb a' -> g <$> afb a')
+
+leftTraversing :: Traversing p => p a b -> p (Either a c) (Either b c)
+leftTraversing = dimap swapE swapE . traverse'
+
+rightTraversing :: Traversing p => p a b -> p (Either c a) (Either c b)
+rightTraversing = traverse'
+
+newtype Bazaar a b t = Bazaar { runBazaar :: forall f. Applicative f => (a -> f b) -> f t }
+  deriving Functor
+
+instance Applicative (Bazaar a b) where
+  pure a = Bazaar $ \_ -> pure a
+  mf <*> ma = Bazaar $ \k -> runBazaar mf k <*> runBazaar ma k
+
+instance Profunctor (Bazaar a) where
+  dimap f g m = Bazaar $ \k -> g <$> runBazaar m (fmap f . k)
+
+sell :: a -> Bazaar a b b
+sell a = Bazaar $ \k -> k a
+
+newtype Baz t b a = Baz { runBaz :: forall f. Applicative f => (a -> f b) -> f t }
+  deriving Functor
+
+-- bsell :: a -> Baz b b a
+-- bsell a = Baz $ \k -> k a
+
+-- aar :: Bazaar a b t -> Baz t b a
+-- aar (Bazaar f) = Baz f
+
+sold :: Baz t a a -> t
+sold m = runIdentity (runBaz m Identity)
+
+instance Foldable (Baz t b) where
+  foldMap = foldMapDefault
+
+instance Traversable (Baz t b) where
+  traverse f bz = fmap (\m -> Baz (runBazaar m)) . getCompose . runBaz bz $ \x -> Compose $ sell <$> f x
+
+instance Profunctor (Baz t) where
+  dimap f g m = Baz $ \k -> runBaz m (fmap f . k . g)
+
+-- | Note: Definitions in terms of 'wander' are much more efficient!
+class (Choice p, Strong p) => Traversing p where
+  -- | Laws:
+  --
+  -- @
+  -- 'traverse'' ≡ 'wander' 'traverse'
+  -- 'traverse'' '.' 'rmap' f ≡ 'rmap' ('fmap' f) '.' 'traverse''
+  -- 'traverse'' '.' 'traverse'' ≡ 'dimap' 'Compose' 'getCompose' '.' 'traverse''
+  -- 'dimap' 'Identity' 'runIdentity' '.' 'traverse'' ≡ 'id'
+  -- @
+  traverse' :: Traversable f => p a b -> p (f a) (f b)
+  traverse' = wander traverse
+
+  -- | This combinator is mutually defined in terms of 'traverse''
+  wander :: (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
+  wander f pab = dimap (\s -> Baz $ \afb -> f afb s) sold (traverse' pab)
+
+  {-# MINIMAL wander | traverse' #-}
+
+instance Traversing (->) where
+  traverse' = fmap
+  wander f ab = runIdentity #. f (Identity #. ab)
+
+instance Monoid m => Traversing (Forget m) where
+  traverse' (Forget h) = Forget (foldMap h)
+  wander f (Forget h) = Forget (getConst . f (Const . h))
+
+instance Monad m => Traversing (Kleisli m) where
+  traverse' (Kleisli m) = Kleisli (mapM m)
+  wander f (Kleisli amb) = Kleisli $ unwrapMonad #. f (WrapMonad #. amb)
+
+instance Applicative m => Traversing (Star m) where
+  traverse' (Star m) = Star (traverse m)
+  wander f (Star amb) = Star (f amb)
+
+instance (Functor f, Traversing p) => Traversing (Tannen f p) where
+  traverse' = Tannen . fmap traverse' . runTannen
+
+newtype CofreeTraversing p a b = CofreeTraversing { runCofreeTraversing :: forall f. Traversable f => p (f a) (f b) }
+
+instance Profunctor p => Profunctor (CofreeTraversing p) where
+  lmap f (CofreeTraversing p) = CofreeTraversing (lmap (fmap f) p)
+  rmap g (CofreeTraversing p) = CofreeTraversing (rmap (fmap g) p)
+  dimap f g (CofreeTraversing p) = CofreeTraversing (dimap (fmap f) (fmap g) p)
+
+instance Profunctor p => Strong (CofreeTraversing p) where
+  second' = traverse'
+
+instance Profunctor p => Choice (CofreeTraversing p) where
+  right' = traverse'
+
+instance Profunctor p => Traversing (CofreeTraversing p) where
+  -- !@(#*&() Compose isn't representational in its second arg or we could use #. and .#
+  traverse' (CofreeTraversing p) = CofreeTraversing (dimap Compose getCompose p)
+
+instance ProfunctorFunctor CofreeTraversing where
+  promap f (CofreeTraversing p) = CofreeTraversing (f p)
+
+instance ProfunctorComonad CofreeTraversing where
+  proextract (CofreeTraversing p) = runIdentity #. p .# Identity
+  produplicate (CofreeTraversing p) = CofreeTraversing (CofreeTraversing (dimap Compose getCompose p))
+
+-- | @FreeTraversing -| CofreeTraversing@
+data FreeTraversing p a b where
+  FreeTraversing :: Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b
+
+instance Functor (FreeTraversing p a) where
+  fmap f (FreeTraversing l m r) = FreeTraversing (f . l) m r
+
+instance Profunctor (FreeTraversing p) where
+  lmap f (FreeTraversing l m r) = FreeTraversing l m (r . f)
+  rmap g (FreeTraversing l m r) = FreeTraversing (g . l) m r
+  dimap f g (FreeTraversing l m r) = FreeTraversing (g . l) m (r . f)
+  g #. FreeTraversing l m r = FreeTraversing (g #. l) m r
+  FreeTraversing l m r .# f = FreeTraversing l m (r .# f)
+
+instance Strong (FreeTraversing p) where
+  second' = traverse'
+
+instance Choice (FreeTraversing p) where
+  right' = traverse'
+
+instance Traversing (FreeTraversing p) where
+  traverse' (FreeTraversing l m r) = FreeTraversing (fmap l .# getCompose) m (Compose #. fmap r)
+
+instance ProfunctorFunctor FreeTraversing where
+  promap f (FreeTraversing l m r) = FreeTraversing l (f m) r
+
+instance ProfunctorMonad FreeTraversing where
+  proreturn p = FreeTraversing runIdentity p Identity
+  projoin (FreeTraversing l (FreeTraversing l' m r') r) = FreeTraversing ((l . fmap l') .# getCompose) m (Compose #. (fmap r' . r))
diff --git a/src/Data/Profunctor/Types.hs b/src/Data/Profunctor/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Types.hs
@@ -0,0 +1,263 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# LANGUAGE Trustworthy #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2011-2015 Edward Kmett,
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- For a good explanation of profunctors in Haskell see Dan Piponi's article:
+--
+-- <http://blog.sigfpe.com/2011/07/profunctors-in-haskell.html>
+--
+-- For more information on strength and costrength, see:
+--
+-- <http://comonad.com/reader/2008/deriving-strength-from-laziness/>
+----------------------------------------------------------------------------
+module Data.Profunctor.Types
+  ( Profunctor(dimap, lmap, rmap)
+  , Star(..)
+  , Costar(..)
+  , WrappedArrow(..)
+  , Forget(..)
+  , (:->)
+  ) where
+
+import Control.Applicative hiding (WrappedArrow(..))
+import Control.Arrow
+import Control.Category
+import Control.Comonad
+import Control.Monad (MonadPlus(..), (>=>))
+import Data.Coerce (Coercible, coerce)
+import Data.Distributive
+import Data.Foldable
+import Data.Functor.Contravariant
+import Data.Profunctor.Unsafe
+import Data.Traversable
+import Prelude hiding (id,(.))
+
+#if !(MIN_VERSION_base(4,11,0))
+import Data.Semigroup (Semigroup(..))
+#endif
+
+infixr 0 :->
+
+-- | (':->') has a polymorphic kind since @5.6@.
+
+-- (:->) :: forall k1 k2. (k1 -> k2 -> Type) -> (k1 -> k2 -> Type) -> Type
+type p :-> q = forall a b. p a b -> q a b
+
+------------------------------------------------------------------------------
+-- Star
+------------------------------------------------------------------------------
+
+-- | Lift a 'Functor' into a 'Profunctor' (forwards).
+--
+-- 'Star' has a polymorphic kind since @5.6@.
+
+-- Star :: (k -> Type) -> (Type -> k -> Type)
+newtype Star f d c = Star { runStar :: d -> f c }
+
+instance Functor f => Profunctor (Star f) where
+  dimap ab cd (Star bfc) = Star (fmap cd . bfc . ab)
+  {-# INLINE dimap #-}
+  lmap k (Star f) = Star (f . k)
+  {-# INLINE lmap #-}
+  rmap k (Star f) = Star (fmap k . f)
+  {-# INLINE rmap #-}
+  -- We cannot safely overload (#.) because we didn't write the 'Functor'.
+  p .# _ = coerce p
+  {-# INLINE (.#) #-}
+
+instance Functor f => Functor (Star f a) where
+  fmap = rmap
+  {-# INLINE fmap #-}
+
+instance Applicative f => Applicative (Star f a) where
+  pure a = Star $ \_ -> pure a
+  Star ff <*> Star fx = Star $ \a -> ff a <*> fx a
+  Star ff  *> Star fx = Star $ \a -> ff a  *> fx a
+  Star ff <*  Star fx = Star $ \a -> ff a <*  fx a
+
+instance Alternative f => Alternative (Star f a) where
+  empty = Star $ \_ -> empty
+  Star f <|> Star g = Star $ \a -> f a <|> g a
+
+instance Monad f => Monad (Star f a) where
+  Star m >>= f = Star $ \ e -> do
+    a <- m e
+    runStar (f a) e
+
+instance MonadPlus f => MonadPlus (Star f a) where
+  mzero = Star $ \_ -> mzero
+  Star f `mplus` Star g = Star $ \a -> f a `mplus` g a
+
+instance Distributive f => Distributive (Star f a) where
+  distribute fs = Star $ \a -> collect (($ a) .# runStar) fs
+
+instance Monad f => Category (Star f) where
+  id = Star return
+  Star f . Star g = Star $ g >=> f
+
+instance Contravariant f => Contravariant (Star f a) where
+  contramap f (Star g) = Star (contramap f . g)
+  {-# INLINE contramap #-}
+
+------------------------------------------------------------------------------
+-- Costar
+------------------------------------------------------------------------------
+
+-- | Lift a 'Functor' into a 'Profunctor' (backwards).
+--
+-- 'Costar' has a polymorphic kind since @5.6@.
+
+-- Costar :: (k -> Type) -> k -> Type -> Type
+newtype Costar f d c = Costar { runCostar :: f d -> c }
+
+instance Functor f => Profunctor (Costar f) where
+  dimap ab cd (Costar fbc) = Costar (cd . fbc . fmap ab)
+  {-# INLINE dimap #-}
+  lmap k (Costar f) = Costar (f . fmap k)
+  {-# INLINE lmap #-}
+  rmap k (Costar f) = Costar (k . f)
+  {-# INLINE rmap #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  {-# INLINE (#.) #-}
+  -- We cannot overload (.#) because we didn't write the 'Functor'.
+
+instance Distributive (Costar f d) where
+  distribute fs = Costar $ \gd -> fmap (($ gd) .# runCostar) fs
+
+instance Functor (Costar f a) where
+  fmap k (Costar f) = Costar (k . f)
+  {-# INLINE fmap #-}
+  a <$ _ = Costar $ \_ -> a
+  {-# INLINE (<$) #-}
+
+instance Applicative (Costar f a) where
+  pure a = Costar $ \_ -> a
+  Costar ff <*> Costar fx = Costar $ \a -> ff a (fx a)
+  _ *> m = m
+  m <* _ = m
+
+instance Monad (Costar f a) where
+  return = pure
+  Costar m >>= f = Costar $ \ x -> runCostar (f (m x)) x
+
+------------------------------------------------------------------------------
+-- Wrapped Profunctors
+------------------------------------------------------------------------------
+
+-- | Wrap an arrow for use as a 'Profunctor'.
+--
+-- 'WrappedArrow' has a polymorphic kind since @5.6@.
+
+-- WrappedArrow :: (k1 -> k2 -> Type) -> (k1 -> k2 -> Type)
+newtype WrappedArrow p a b = WrapArrow { unwrapArrow :: p a b }
+
+instance Category p => Category (WrappedArrow p) where
+  WrapArrow f . WrapArrow g = WrapArrow (f . g)
+  {-# INLINE (.) #-}
+  id = WrapArrow id
+  {-# INLINE id #-}
+
+instance Arrow p => Arrow (WrappedArrow p) where
+  arr = WrapArrow . arr
+  {-# INLINE arr #-}
+  first = WrapArrow . first . unwrapArrow
+  {-# INLINE first #-}
+  second = WrapArrow . second . unwrapArrow
+  {-# INLINE second #-}
+  WrapArrow a *** WrapArrow b = WrapArrow (a *** b)
+  {-# INLINE (***) #-}
+  WrapArrow a &&& WrapArrow b = WrapArrow (a &&& b)
+  {-# INLINE (&&&) #-}
+
+instance ArrowZero p => ArrowZero (WrappedArrow p) where
+  zeroArrow = WrapArrow zeroArrow
+  {-# INLINE zeroArrow #-}
+
+instance ArrowChoice p => ArrowChoice (WrappedArrow p) where
+  left = WrapArrow . left . unwrapArrow
+  {-# INLINE left #-}
+  right = WrapArrow . right . unwrapArrow
+  {-# INLINE right #-}
+  WrapArrow a +++ WrapArrow b = WrapArrow (a +++ b)
+  {-# INLINE (+++) #-}
+  WrapArrow a ||| WrapArrow b = WrapArrow (a ||| b)
+  {-# INLINE (|||) #-}
+
+instance ArrowApply p => ArrowApply (WrappedArrow p) where
+  app = WrapArrow $ app . arr (first unwrapArrow)
+  {-# INLINE app #-}
+
+instance ArrowLoop p => ArrowLoop (WrappedArrow p) where
+  loop = WrapArrow . loop . unwrapArrow
+  {-# INLINE loop #-}
+
+instance Arrow p => Profunctor (WrappedArrow p) where
+  lmap = (^>>)
+  {-# INLINE lmap #-}
+  rmap = (^<<)
+  {-# INLINE rmap #-}
+  -- We cannot safely overload (#.) or (.#) because we didn't write the 'Arrow'.
+
+------------------------------------------------------------------------------
+-- Forget
+------------------------------------------------------------------------------
+
+-- | 'Forget' has a polymorphic kind since @5.6@.
+
+-- Forget :: Type -> Type -> k -> Type
+newtype Forget r a b = Forget { runForget :: a -> r }
+
+instance Profunctor (Forget r) where
+  dimap f _ (Forget k) = Forget (k . f)
+  {-# INLINE dimap #-}
+  lmap f (Forget k) = Forget (k . f)
+  {-# INLINE lmap #-}
+  rmap _ (Forget k) = Forget k
+  {-# INLINE rmap #-}
+
+instance Functor (Forget r a) where
+  fmap _ (Forget k) = Forget k
+  {-# INLINE fmap #-}
+
+instance Foldable (Forget r a) where
+  foldMap _ _ = mempty
+  {-# INLINE foldMap #-}
+
+instance Traversable (Forget r a) where
+  traverse _ (Forget k) = pure (Forget k)
+  {-# INLINE traverse #-}
+
+instance Contravariant (Forget r a) where
+  contramap _ (Forget k) = Forget k
+  {-# INLINE contramap #-}
+
+-- | Via @Semigroup r => (a -> r)@
+--
+-- @since 5.6.2
+instance Semigroup r => Semigroup (Forget r a b) where
+  Forget f <> Forget g = Forget (f <> g)
+  {-# INLINE (<>) #-}
+
+-- | Via @Monoid r => (a -> r)@
+--
+-- @since 5.6.2
+instance Monoid r => Monoid (Forget r a b) where
+  mempty = Forget mempty
+  {-# INLINE mempty #-}
+#if !(MIN_VERSION_base(4,11,0))
+  mappend (Forget f) (Forget g) = Forget (mappend f g)
+  {-# INLINE mappend #-}
+#endif
diff --git a/src/Data/Profunctor/Unsafe.hs b/src/Data/Profunctor/Unsafe.hs
--- a/src/Data/Profunctor/Unsafe.hs
+++ b/src/Data/Profunctor/Unsafe.hs
@@ -1,13 +1,8 @@
-{-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 708
 {-# LANGUAGE Trustworthy #-}
-#elif __GLASGOW_HASKELL >= 704
-{-# LANGUAGE Unsafe #-}
-#endif
 {-# LANGUAGE ScopedTypeVariables #-}
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2011-2013 Edward Kmett
+-- Copyright   :  (C) 2011-2018 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -38,20 +33,16 @@
 import Control.Category
 import Control.Comonad (Cokleisli(..))
 import Control.Monad (liftM)
+import Data.Bifunctor.Biff (Biff(..))
 import Data.Bifunctor.Clown (Clown(..))
 import Data.Bifunctor.Joker (Joker(..))
+import Data.Bifunctor.Product (Product(..))
+import Data.Bifunctor.Sum (Sum(..))
+import Data.Bifunctor.Tannen (Tannen(..))
+import Data.Coerce (Coercible, coerce)
 import Data.Functor.Contravariant (Contravariant(..))
 import Data.Tagged
-import Prelude hiding (id,(.),sequence)
-
-#if __GLASGOW_HASKELL__ >= 708
-import Data.Coerce
-#else
-import Unsafe.Coerce
-#endif
-
-{-# ANN module "Hlint: ignore Redundant lambda" #-}
-{-# ANN module "Hlint: ignore Collapse lambdas" #-}
+import Prelude hiding (id,(.))
 
 infixr 9 #.
 infixl 8 .#
@@ -137,14 +128,10 @@
   -- The semantics of this function with respect to bottoms
   -- should match the default definition:
   --
-  -- @('Profuctor.Unsafe.#.') ≡ \\f -> \\p -> p \`seq\` 'rmap' f p@
-#if __GLASGOW_HASKELL__ >= 708
-  ( #. ) :: Coercible c b => (b -> c) -> p a b -> p a c
-#else
-  ( #. ) :: (b -> c) -> p a b -> p a c
-#endif
-  ( #. ) = \f -> \p -> p `seq` rmap f p
-  {-# INLINE ( #. ) #-}
+  -- @('Profuctor.Unsafe.#.') ≡ \\_ -> \\p -> p \`seq\` 'rmap' 'coerce' p@
+  (#.) :: forall a b c q. Coercible c b => q b c -> p a b -> p a c
+  (#.) = \_ -> \p -> p `seq` rmap (coerce (id :: c -> c) :: b -> c) p
+  {-# INLINE (#.) #-}
 
   -- | Strictly map the first argument argument
   -- contravariantly with a function that is assumed
@@ -167,18 +154,12 @@
   -- will only call this with a second argument that is
   -- operationally identity.
   --
-  -- @('.#') ≡ \\p -> p \`seq\` \\f -> 'lmap' f p@
-#if __GLASGOW_HASKELL__ >= 708
-  ( .# ) :: Coercible b a => p b c -> (a -> b) -> p a c
-#else
-  ( .# ) :: p b c -> (a -> b) -> p a c
-#endif
-  ( .# ) = \p -> p `seq` \f -> lmap f p
-  {-# INLINE ( .# ) #-}
+  -- @('.#') ≡ \\p -> p \`seq\` \\f -> 'lmap' 'coerce' p@
+  (.#) :: forall a b c q. Coercible b a => p b c -> q a b -> p a c
+  (.#) = \p -> p `seq` \_ -> lmap (coerce (id :: b -> b) :: a -> b) p
+  {-# INLINE (.#) #-}
 
-#if __GLASGOW_HASKELL__ >= 708
   {-# MINIMAL dimap | (lmap, rmap) #-}
-#endif
 
 instance Profunctor (->) where
   dimap ab cd bc = cd . bc . ab
@@ -187,15 +168,10 @@
   {-# INLINE lmap #-}
   rmap = (.)
   {-# INLINE rmap #-}
-#if __GLASGOW_HASKELL__ >= 708
-  ( #. ) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
-  ( .# ) pbc _ = coerce pbc
-#else
-  ( #. ) _ = unsafeCoerce
-  ( .# ) pbc _ = unsafeCoerce pbc
-#endif
-  {-# INLINE ( #. ) #-}
-  {-# INLINE ( .# ) #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  (.#) pbc _ = coerce pbc
+  {-# INLINE (#.) #-}
+  {-# INLINE (.#) #-}
 
 instance Profunctor Tagged where
   dimap _ f (Tagged s) = Tagged (f s)
@@ -204,14 +180,10 @@
   {-# INLINE lmap #-}
   rmap = fmap
   {-# INLINE rmap #-}
-#if __GLASGOW_HASKELL__ >= 708
-  ( #. ) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
-#else
-  ( #. ) _ = unsafeCoerce
-#endif
-  {-# INLINE ( #. ) #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  {-# INLINE (#.) #-}
   Tagged s .# _ = Tagged s
-  {-# INLINE ( .# ) #-}
+  {-# INLINE (.#) #-}
 
 instance Monad m => Profunctor (Kleisli m) where
   dimap f g (Kleisli h) = Kleisli (liftM g . h . f)
@@ -221,12 +193,8 @@
   rmap k (Kleisli f) = Kleisli (liftM k . f)
   {-# INLINE rmap #-}
   -- We cannot safely overload (#.) because we didn't provide the 'Monad'.
-#if __GLASGOW_HASKELL__ >= 708
-  ( .# ) pbc _ = coerce pbc
-#else
-  ( .# ) pbc _ = unsafeCoerce pbc
-#endif
-  {-# INLINE ( .# ) #-}
+  (.#) pbc _ = coerce pbc
+  {-# INLINE (.#) #-}
 
 instance Functor w => Profunctor (Cokleisli w) where
   dimap f g (Cokleisli h) = Cokleisli (g . h . fmap f)
@@ -236,12 +204,8 @@
   rmap k (Cokleisli f) = Cokleisli (k . f)
   {-# INLINE rmap #-}
   -- We cannot safely overload (.#) because we didn't provide the 'Functor'.
-#if __GLASGOW_HASKELL__ >= 708
-  ( #. ) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
-#else
-  ( #. ) _ = unsafeCoerce
-#endif
-  {-# INLINE ( #. ) #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  {-# INLINE (#.) #-}
 
 instance Contravariant f => Profunctor (Clown f) where
   lmap f (Clown fa) = Clown (contramap f fa)
@@ -258,3 +222,49 @@
   {-# INLINE rmap #-}
   dimap _ g (Joker fb) = Joker (fmap g fb)
   {-# INLINE dimap #-}
+
+instance (Profunctor p, Functor f, Functor g) => Profunctor (Biff p f g) where
+  lmap f (Biff p) = Biff (lmap (fmap f) p)
+  rmap g (Biff p) = Biff (rmap (fmap g) p)
+  dimap f g (Biff p) = Biff (dimap (fmap f) (fmap g) p)
+
+instance (Profunctor p, Profunctor q) => Profunctor (Product p q) where
+  lmap  f   (Pair p q) = Pair (lmap f p) (lmap f q)
+  {-# INLINE lmap #-}
+  rmap    g (Pair p q) = Pair (rmap g p) (rmap g q)
+  {-# INLINE rmap #-}
+  dimap f g (Pair p q) = Pair (dimap f g p) (dimap f g q)
+  {-# INLINE dimap #-}
+  (#.) f (Pair p q) = Pair (f #. p) (f #. q)
+  {-# INLINE (#.) #-}
+  (.#) (Pair p q) f = Pair (p .# f) (q .# f)
+  {-# INLINE (.#) #-}
+
+instance (Profunctor p, Profunctor q) => Profunctor (Sum p q) where
+  lmap f (L2 x) = L2 (lmap f x)
+  lmap f (R2 y) = R2 (lmap f y)
+  {-# INLINE lmap #-}
+  rmap g (L2 x) = L2 (rmap g x)
+  rmap g (R2 y) = R2 (rmap g y)
+  {-# INLINE rmap #-}
+  dimap f g (L2 x) = L2 (dimap f g x)
+  dimap f g (R2 y) = R2 (dimap f g y)
+  {-# INLINE dimap #-}
+  f #. L2 x = L2 (f #. x)
+  f #. R2 y = R2 (f #. y)
+  {-# INLINE (#.) #-}
+  L2 x .# f = L2 (x .# f)
+  R2 y .# f = R2 (y .# f)
+  {-# INLINE (.#) #-}
+
+instance (Functor f, Profunctor p) => Profunctor (Tannen f p) where
+  lmap f (Tannen h) = Tannen (lmap f <$> h)
+  {-# INLINE lmap #-}
+  rmap g (Tannen h) = Tannen (rmap g <$> h)
+  {-# INLINE rmap #-}
+  dimap f g (Tannen h) = Tannen (dimap f g <$> h)
+  {-# INLINE dimap #-}
+  (#.) f (Tannen h) = Tannen ((f #.) <$> h)
+  {-# INLINE (#.) #-}
+  (.#) (Tannen h) f = Tannen ((.# f) <$> h)
+  {-# INLINE (.#) #-}
diff --git a/src/Data/Profunctor/Yoneda.hs b/src/Data/Profunctor/Yoneda.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Profunctor/Yoneda.hs
@@ -0,0 +1,231 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Trustworthy #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2017 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  Rank2Types, TFs
+--
+----------------------------------------------------------------------------
+module Data.Profunctor.Yoneda
+  ( Yoneda(..), extractYoneda, duplicateYoneda
+  , Coyoneda(..), returnCoyoneda, joinCoyoneda
+  ) where
+
+import Control.Category
+import Data.Coerce (Coercible, coerce)
+import Data.Profunctor
+import Data.Profunctor.Monad
+import Data.Profunctor.Traversing
+import Data.Profunctor.Unsafe
+import Prelude hiding (id,(.))
+
+--------------------------------------------------------------------------------
+-- * Yoneda
+--------------------------------------------------------------------------------
+
+-- | This is the cofree profunctor given a data constructor of kind @* -> * -> *@
+newtype Yoneda p a b = Yoneda { runYoneda :: forall x y. (x -> a) -> (b -> y) -> p x y }
+
+-- Yoneda is a comonad on |*| -> Nat(|*|,*), we don't need the profunctor constraint to extract or duplicate
+-- |
+-- @
+-- 'projoin' '.' 'extractYoneda' ≡ 'id'
+-- 'extractYoneda' '.' 'projoin' ≡ 'id'
+-- 'projoin' ≡ 'extractYoneda'
+-- @
+extractYoneda :: Yoneda p a b -> p a b
+extractYoneda p = runYoneda p id id
+
+-- |
+-- @
+-- 'projoin' '.' 'duplicateYoneda' ≡ 'id'
+-- 'duplicateYoneda' '.' 'projoin' ≡ 'id'
+-- 'duplicateYoneda' = 'proreturn'
+-- @
+duplicateYoneda :: Yoneda p a b -> Yoneda (Yoneda p) a b
+duplicateYoneda p = Yoneda $ \l r -> dimap l r p
+
+instance Profunctor (Yoneda p) where
+  dimap l r p = Yoneda $ \l' r' -> runYoneda p (l . l') (r' . r)
+  {-# INLINE dimap #-}
+  lmap l p = Yoneda $ \l' r -> runYoneda p (l . l') r
+  {-# INLINE lmap #-}
+  rmap r p = Yoneda $ \l r' -> runYoneda p l (r' . r)
+  {-# INLINE rmap #-}
+  (.#) p _ = coerce p
+  {-# INLINE (.#) #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  {-# INLINE (#.) #-}
+
+instance Functor (Yoneda p a) where
+  fmap f p = Yoneda $ \l r -> runYoneda p l (r . f)
+  {-# INLINE fmap #-}
+
+instance ProfunctorFunctor Yoneda where
+  promap f p = Yoneda $ \l r -> f (runYoneda p l r)
+  {-# INLINE promap #-}
+
+instance ProfunctorComonad Yoneda where
+  proextract p = runYoneda p id id
+  {-# INLINE proextract #-}
+  produplicate p = Yoneda $ \l r -> dimap l r p
+  {-# INLINE produplicate #-}
+
+instance ProfunctorMonad Yoneda where
+  proreturn p = Yoneda $ \l r -> dimap l r p
+  {-# INLINE proreturn #-}
+  projoin p = runYoneda p id id
+  {-# INLINE projoin #-}
+
+instance (Category p, Profunctor p) => Category (Yoneda p) where
+  id = Yoneda $ \l r -> dimap l r id
+  {-# INLINE id #-}
+  p . q = Yoneda $ \ l r -> runYoneda p id r . runYoneda q l id
+  {-# INLINE (.) #-}
+
+instance Strong p => Strong (Yoneda p) where
+  first' = proreturn . first' . extractYoneda
+  {-# INLINE first' #-}
+  second' = proreturn . second' . extractYoneda
+  {-# INLINE second' #-}
+
+instance Choice p => Choice (Yoneda p) where
+  left' = proreturn . left' . extractYoneda
+  {-# INLINE left' #-}
+  right' = proreturn . right' . extractYoneda
+  {-# INLINE right' #-}
+
+instance Costrong p => Costrong (Yoneda p) where
+  unfirst = proreturn . unfirst . extractYoneda
+  {-# INLINE unfirst #-}
+  unsecond = proreturn . unsecond . extractYoneda
+  {-# INLINE unsecond #-}
+
+instance Cochoice p => Cochoice (Yoneda p) where
+  unleft = proreturn . unleft . extractYoneda
+  {-# INLINE unleft #-}
+  unright = proreturn . unright . extractYoneda
+  {-# INLINE unright #-}
+
+instance Closed p => Closed (Yoneda p) where
+  closed = proreturn . closed . extractYoneda
+  {-# INLINE closed #-}
+
+instance Mapping p => Mapping (Yoneda p) where
+  map' = proreturn . map' . extractYoneda
+  {-# INLINE map' #-}
+
+instance Traversing p => Traversing (Yoneda p) where
+  traverse' = proreturn . traverse' . extractYoneda
+  {-# INLINE traverse' #-}
+  wander f = proreturn . wander f . extractYoneda
+  {-# INLINE wander #-}
+
+--------------------------------------------------------------------------------
+-- * Coyoneda
+--------------------------------------------------------------------------------
+
+data Coyoneda p a b where
+  Coyoneda :: (a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
+
+-- Coyoneda is a Monad on |*| -> Nat(|*|,*), we don't need the profunctor constraint to extract or duplicate
+
+-- |
+-- @
+-- 'returnCoyoneda' '.' 'proextract' ≡ 'id'
+-- 'proextract' '.' 'returnCoyoneda' ≡ 'id'
+-- 'produplicate' ≡ 'returnCoyoneda'
+-- @
+returnCoyoneda :: p a b -> Coyoneda p a b
+returnCoyoneda = Coyoneda id id
+
+-- |
+-- @
+-- 'joinCoyoneda' '.' 'produplicate' ≡ 'id'
+-- 'produplicate' '.' 'joinCoyoneda' ≡ 'id'
+-- 'joinCoyoneda' ≡ 'proextract'
+-- @
+joinCoyoneda :: Coyoneda (Coyoneda p) a b -> Coyoneda p a b
+joinCoyoneda (Coyoneda l r p) = dimap l r p
+
+instance Functor (Coyoneda p a) where
+  fmap f (Coyoneda l r' p) = Coyoneda l (f . r') p
+
+instance Profunctor (Coyoneda p) where
+  dimap l r (Coyoneda l' r' p) = Coyoneda (l' . l) (r . r') p
+  {-# INLINE dimap #-}
+  lmap l (Coyoneda l' r p) = Coyoneda (l' . l) r p
+  {-# INLINE lmap #-}
+  rmap r (Coyoneda l r' p) = Coyoneda l (r . r') p
+  {-# INLINE rmap #-}
+  (.#) p _ = coerce p
+  {-# INLINE (.#) #-}
+  (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b
+  {-# INLINE (#.) #-}
+
+instance ProfunctorFunctor Coyoneda where
+  promap f (Coyoneda l r p) = Coyoneda l r (f p)
+  {-# INLINE promap #-}
+
+instance ProfunctorComonad Coyoneda where
+  proextract (Coyoneda l r p) = dimap l r p
+  {-# INLINE proextract #-}
+  produplicate = Coyoneda id id
+  {-# INLINE produplicate #-}
+
+instance ProfunctorMonad Coyoneda where
+  proreturn = returnCoyoneda
+  {-# INLINE proreturn #-}
+  projoin = joinCoyoneda
+  {-# INLINE projoin #-}
+
+instance (Category p, Profunctor p) => Category (Coyoneda p) where
+  id = Coyoneda id id id
+  {-# INLINE id #-}
+  Coyoneda lp rp p . Coyoneda lq rq q = Coyoneda lq rp (p . rmap (lp . rq) q)
+  {-# INLINE (.) #-}
+
+instance Strong p => Strong (Coyoneda p) where
+  first' = returnCoyoneda . first' . proextract
+  {-# INLINE first' #-}
+  second' = returnCoyoneda . second' . proextract
+  {-# INLINE second' #-}
+
+instance Choice p => Choice (Coyoneda p) where
+  left' = returnCoyoneda . left' . proextract
+  {-# INLINE left' #-}
+  right' = returnCoyoneda . right' . proextract
+  {-# INLINE right' #-}
+
+instance Costrong p => Costrong (Coyoneda p) where
+  unfirst = returnCoyoneda . unfirst . proextract
+  {-# INLINE unfirst #-}
+  unsecond = returnCoyoneda . unsecond . proextract
+  {-# INLINE unsecond #-}
+
+instance Cochoice p => Cochoice (Coyoneda p) where
+  unleft = returnCoyoneda . unleft . proextract
+  {-# INLINE unleft #-}
+  unright = returnCoyoneda . unright . proextract
+  {-# INLINE unright #-}
+
+instance Closed p => Closed (Coyoneda p) where
+  closed = returnCoyoneda . closed . proextract
+  {-# INLINE closed #-}
+
+instance Mapping p => Mapping (Coyoneda p) where
+  map' = returnCoyoneda . map' . proextract
+  {-# INLINE map' #-}
+
+instance Traversing p => Traversing (Coyoneda p) where
+  traverse' = returnCoyoneda . traverse' . proextract
+  {-# INLINE traverse' #-}
+  wander f = returnCoyoneda . wander f . proextract
+  {-# INLINE wander #-}