diff --git a/.ghci b/.ghci
deleted file mode 100644
--- a/.ghci
+++ /dev/null
@@ -1,1 +0,0 @@
-:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h
diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
 dist
+dist-newstyle
 docs
 wiki
 TAGS
@@ -11,3 +12,24 @@
 *.hi
 *~
 *#
+.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.*
+/default.nix
+/shell.nix
+/result
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
--- a/.travis.yml
+++ /dev/null
@@ -1,8 +0,0 @@
-language: haskell
-notifications:
-  irc:
-    channels:
-      - "irc.freenode.org#haskell-lens"
-    skip_join: true
-    template:
-      - "\x0313kan-extensions\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,97 @@
+5.2.8 [2026.01.10]
+------------------
+* Add `MonadThrow` instance for `Codensity`.
+* Remove unused `array`, `containers`, and `tagged` dependencies.
+
+5.2.7 [2025.06.17]
+------------------
+* Make the implementations of `(.>)` and `(*>)` for `Data.Functor.Yoneda` more
+  stack-efficient.
+
+5.2.6 [2024.05.04]
+------------------
+* Drop support for GHC 8.2 and earlier.
+* Generalize instances in `Control.Monad.Codensity` to be of the form:
+
+  ```hs
+  instance (f ~~ f', MonadFail f') => MonadFail (Codensity (f :: k -> TYPE rep))
+  ```
+
+  This avoids having to constrain `k ~ Type` and `rep ~ LiftedRep`, which could potentially harm type inference.
+* Explicitly implement `liftA2` in the `Applicative` instance for `Data.Functor.Day.Curried`.
+* Add an `Adjunction` instance for `Data.Functor.Day`.
+* Add `Adjunction` and `Divisible` instances for `Data.Functor.Contravariant.Day`.
+* Add an `Apply` instance for `Data.Functor.Day.Curried`.
+
+5.2.5 [2022.06.26]
+------------------
+* Only require a `Functor` constraint in the `Eq` and `Ord` instances for
+  `Coyoneda` when building against `transformers-0.4.*`.
+
+5.2.4 [2022.05.07]
+------------------
+* Allow building with `transformers-0.6.*` and `mtl-2.3.*`.
+
+5.2.3 [2021.07.27]
+------------------
+* Add `shift` and `reset` to `Control.Monad.Codensity`.
+
+5.2.2 [2021.02.17]
+------------------
+* Add `hoistCoyoneda` to `Data.Functor.Contravariant.Coyoneda`.
+
+5.2.1 [2020.10.01]
+------------------
+* Allow building with GHC 9.0.
+
+5.2 [2018.07.03]
+----------------
+* Make `Codensity` levity polymorphic.
+* Add the `Data.Functor.Invariant.Day` module, which combines the covariant and
+  contravariant versions of `Day`. As a result, `kan-extensions` now depends on
+  the `invariant` package.
+* Add a `wrapCodensity` function.
+* More efficient `Eq1`, `Ord1`, and `Adjunction` instances for `Coyoneda`.
+* Add `INLINE` pragmas on more functions.
+* Allow building with `containers-0.6`.
+
+5.1 [2018.01.28]
+----------------
+* Make `Density`, `Codensity`, `Kan` and `Lan` polykinded.
+* Add `Eq1`, `Ord1`, `Read1` and `Show1` instances for `Coyoneda` and `Yoneda`.
+* Change contexts of `Eq` and `Ord` instances of `Coyoneda` and `Yoneda`
+  (and the `Show` instance for `Coyoneda`) to require lifted class instances,
+  e.g. `Eq1 f, Eq a`.
+* Allow `free-5`.
+
+5.0.2
+-----
+* Added `hoistCoyoneda`
+
+5.0.1
+-----
+* Removed some redundant constraints
+
+5
+-----
+* Move `Data.Functor.Kan.Rift` to `Data.Functor.Day.Curried`
+
+4.2.3
+-----
+* Builds clean on GHC 7.10
+
+4.2.2
+-----
+* `semigroupoids` 5 support
+
+4.2.1
+---
+* Add `liftRift` and `lowerRift`
+
+4.2
+---
+* Remove pointed dependency
+
 4.1.1
 ---
 * Added `Applicative` instance for `Day`
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2008-2013 Edward Kmett
+Copyright 2008-2016 Edward Kmett
 
 All rights reserved.
 
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,7 +1,7 @@
 kan-extensions
 ==============
 
-[![Build Status](https://secure.travis-ci.org/ekmett/kan-extensions.png?branch=master)](http://travis-ci.org/ekmett/kan-extensions)
+[![Hackage](https://img.shields.io/hackage/v/kan-extensions.svg)](https://hackage.haskell.org/package/kan-extensions) [![Build Status](https://github.com/ekmett/kan-extensions/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/kan-extensions/actions?query=workflow%3AHaskell-CI)
 
 This package provides tools for working with various Kan extensions and Kan lifts in Haskell.
 
diff --git a/kan-extensions.cabal b/kan-extensions.cabal
--- a/kan-extensions.cabal
+++ b/kan-extensions.cabal
@@ -1,30 +1,40 @@
 name:          kan-extensions
 category:      Data Structures, Monads, Comonads, Functors
-version:       4.1.1
+version:       5.2.8
 license:       BSD3
-cabal-version: >= 1.6
+cabal-version: >= 1.10
 license-file:  LICENSE
 author:        Edward A. Kmett
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
 stability:     provisional
 homepage:      http://github.com/ekmett/kan-extensions/
 bug-reports:   http://github.com/ekmett/kan-extensions/issues
-copyright:     Copyright (C) 2008-2013 Edward A. Kmett
-synopsis:      Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads
-description:   Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads
+copyright:     Copyright (C) 2008-2016 Edward A. Kmett
+synopsis:      Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
+description:   Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads.
 build-type:    Simple
+tested-with:   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.7
+             , GHC == 9.8.4
+             , GHC == 9.10.3
+             , GHC == 9.12.2
+             , GHC == 9.14.1
 
 extra-source-files:
-  .travis.yml
   .gitignore
-  .ghci
   .vim.custom
   CHANGELOG.markdown
   README.markdown
 
 source-repository head
   type: git
-  location: git://github.com/ekmett/kan-extensions.git
+  location: https://github.com/ekmett/kan-extensions.git
 
 library
   hs-source-dirs: src
@@ -40,19 +50,18 @@
     TypeFamilies
 
   build-depends:
-    adjunctions   >= 4.2     && < 5,
-    array         >= 0.3.0.2 && < 0.6,
-    base          >= 4       && < 5,
-    comonad       >= 4       && < 5,
-    containers    >= 0.4     && < 0.6,
-    contravariant >= 1       && < 2,
-    distributive  >= 0.2.2   && < 1,
-    free          >= 4       && < 5,
-    mtl           >= 2.0.1   && < 2.3,
-    pointed       >= 4       && < 5,
-    semigroupoids >= 4       && < 5,
-    tagged        >= 0.7.2   && < 1,
-    transformers  >= 0.2     && < 0.5
+    adjunctions         >= 4.2     && < 5,
+    base                >= 4.11    && < 5,
+    comonad             >= 4       && < 6,
+    contravariant       >= 1       && < 2,
+    distributive        >= 0.2.2   && < 1,
+    exceptions          >= 0.10    && < 0.11,
+    invariant           >= 0.1     && < 1,
+    free                >= 4       && < 6,
+    mtl                 >= 2.2.1   && < 2.4,
+    profunctors         >= 5       && < 6,
+    semigroupoids       >= 5.2.2   && < 7,
+    transformers        >= 0.5     && < 0.7
 
   exposed-modules:
     Control.Comonad.Density
@@ -62,12 +71,15 @@
     Data.Functor.Contravariant.Yoneda
     Data.Functor.Contravariant.Coyoneda
     Data.Functor.Day
+    Data.Functor.Day.Curried
+    Data.Functor.Invariant.Day
     Data.Functor.Kan.Lan
-    Data.Functor.Kan.Lift
     Data.Functor.Kan.Ran
-    Data.Functor.Kan.Rift
     Data.Functor.Yoneda
     Data.Functor.Coyoneda
 
-  ghc-options: -Wall
+  ghc-options: -Wall -Wcompat -Wnoncanonical-monad-instances -Wno-trustworthy-safe
+  if !impl(ghc >= 8.8)
+    ghc-options: -Wnoncanonical-monadfail-instances
 
+  default-language: Haskell2010
diff --git a/src/Control/Comonad/Density.hs b/src/Control/Comonad/Density.hs
--- a/src/Control/Comonad/Density.hs
+++ b/src/Control/Comonad/Density.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE MultiParamTypeClasses, GADTs #-}
 {-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Comonad.Density
--- Copyright   :  (C) 2008-2011 Edward Kmett
+-- Copyright   :  (C) 2008-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -15,7 +14,7 @@
 --
 -- The 'Density' 'Comonad' for a 'Functor' (aka the 'Comonad generated by a 'Functor')
 -- The 'Density' term dates back to Dubuc''s 1974 thesis. The term
--- 'Monad' genererated by a 'Functor' dates back to 1972 in Street''s
+-- 'Monad' generated by a 'Functor' dates back to 1972 in Street''s
 -- ''Formal Theory of Monads''.
 --
 -- The left Kan extension of a 'Functor' along itself (@'Lan' f f@) forms a 'Comonad'. This is
@@ -28,7 +27,9 @@
   , densityToLan, lanToDensity
   ) where
 
+#if !(MIN_VERSION_base(4,18,0))
 import Control.Applicative
+#endif
 import Control.Comonad
 import Control.Comonad.Trans.Class
 import Data.Functor.Apply
diff --git a/src/Control/Monad/Co.hs b/src/Control/Monad/Co.hs
--- a/src/Control/Monad/Co.hs
+++ b/src/Control/Monad/Co.hs
@@ -3,13 +3,10 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE PolyKinds #-}
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2011 Edward Kmett
+-- Copyright   :  (C) 2011-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -29,7 +26,7 @@
 -- which is a 'Monad' in @Hask^op@ to a 'Monad' in 'Hask'.
 --
 -- For any @r@, the 'Contravariant' functor / presheaf @(-> r)@ :: Hask^op -> Hask is adjoint to the \"same\"
--- 'Contravariant' functor @(-> r) :: Hask -> Hask^op@. So we can sandwhich a
+-- 'Contravariant' functor @(-> r) :: Hask -> Hask^op@. So we can sandwich a
 -- Monad in Hask^op in the middle to obtain @w (a -> r-) -> r+@, and then take a coend over
 -- @r@ to obtain @forall r. w (a -> r) -> r@. This gives rise to 'Co'. If we observe that
 -- we didn't care what the choices we made for @r@ were to finish this construction, we can
@@ -54,16 +51,17 @@
   , askW, asksW, traceW
   )where
 
-import Control.Applicative
 import Control.Comonad
 import Control.Comonad.Cofree
 import Control.Comonad.Density
 import Control.Comonad.Env.Class as Env
 import Control.Comonad.Store.Class
 import Control.Comonad.Traced.Class as Traced
+import Control.Monad ((<=<), liftM)
 import Control.Monad.Error.Class
+import qualified Control.Monad.Fail as Fail
 import Control.Monad.IO.Class
-import Control.Monad.Identity
+import Control.Monad.Identity (Identity(..))
 import Control.Monad.Reader.Class as Reader
 import Control.Monad.State.Class
 import Control.Monad.Trans.Class
@@ -81,7 +79,7 @@
 
 -- |
 -- @
--- 'Co' w a ~ 'Data.Functor.KanLift.Rift' w 'Identity' a
+-- 'Co' w a ~ 'Data.Functor.Kan.Rift.Rift' w 'Identity' a
 -- @
 newtype CoT w m a = CoT { runCoT :: forall r. w (a -> m r) -> m r }
 
@@ -99,9 +97,12 @@
   mf <*> ma = mf >>= \f -> fmap f ma
 
 instance Comonad w => Monad (CoT w m) where
-  return a = CoT (`extract` a)
+  return = pure
   CoT k >>= f = CoT (k . extend (\wa a -> runCoT (f a) wa))
 
+instance (Comonad w, Fail.MonadFail m) => Fail.MonadFail (CoT w m) where
+  fail msg = CoT $ \ _ -> Fail.fail msg
+
 instance Comonad w => MonadTrans (CoT w) where
   lift m = CoT (extract . fmap (m >>=))
 
@@ -126,22 +127,22 @@
 lowerCo1 :: Functor w => Co w () -> w a -> a
 lowerCo1 m = runIdentity . runCoT m . fmap (const . return)
 
-posW :: (ComonadStore s w, Monad m) => CoT w m s
+posW :: ComonadStore s w => CoT w m s
 posW = liftCoT0 pos
 
-peekW :: (ComonadStore s w, Monad m) => s -> CoT w m ()
+peekW :: ComonadStore s w => s -> CoT w m ()
 peekW s = liftCoT1 (peek s)
 
-peeksW :: (ComonadStore s w, Monad m) => (s -> s) -> CoT w m ()
+peeksW :: ComonadStore s w => (s -> s) -> CoT w m ()
 peeksW f = liftCoT1 (peeks f)
 
-askW :: (ComonadEnv e w, Monad m) => CoT w m e
+askW :: ComonadEnv e w => CoT w m e
 askW = liftCoT0 (Env.ask)
 
-asksW :: (ComonadEnv e w, Monad m) => (e -> a) -> CoT w m a
+asksW :: ComonadEnv e w => (e -> a) -> CoT w m a
 asksW f = liftCoT0 (Env.asks f)
 
-traceW :: (ComonadTraced e w, Monad m) => e -> CoT w m ()
+traceW :: ComonadTraced e w => e -> CoT w m ()
 traceW e = liftCoT1 (Traced.trace e)
 
 liftCoT0M :: (Comonad w, Monad m) => (forall a. w a -> m s) -> CoT w m s
@@ -153,7 +154,7 @@
 diter :: Functor f => a -> (a -> f a) -> Density (Cofree f) a
 diter x y = liftDensity . coiter y $ x
 
-dctrlM :: (Comonad w, Monad m) => (forall a. w a -> m (w a)) -> CoT (Density w) m ()
+dctrlM :: Monad m => (forall a. w a -> m (w a)) -> CoT (Density w) m ()
 dctrlM k = liftCoT1M (\(Density w a) -> liftM w (k a))
 
 instance (Comonad w, MonadReader e m) => MonadReader e (CoT w m) where
diff --git a/src/Control/Monad/Codensity.hs b/src/Control/Monad/Codensity.hs
--- a/src/Control/Monad/Codensity.hs
+++ b/src/Control/Monad/Codensity.hs
@@ -1,19 +1,21 @@
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE Trustworthy #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+#if __GLASGOW_HASKELL__ < 806
+{-# LANGUAGE TypeInType #-}
 #endif
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Monad.Codensity
--- Copyright   :  (C) 2008-2013 Edward Kmett
+-- Copyright   :  (C) 2008-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -27,11 +29,17 @@
   , codensityToAdjunction, adjunctionToCodensity
   , codensityToRan, ranToCodensity
   , codensityToComposedRep, composedRepToCodensity
+  , wrapCodensity
   , improve
+  -- ** Delimited continuations
+  , reset
+  , shift
   ) where
 
 import Control.Applicative
-import Control.Monad (ap, MonadPlus(..))
+import Control.Monad (MonadPlus(..))
+import Control.Monad.Catch (MonadThrow(..))
+import qualified Control.Monad.Fail as Fail
 import Control.Monad.Free
 import Control.Monad.IO.Class
 import Control.Monad.Reader.Class
@@ -42,9 +50,8 @@
 import Data.Functor.Kan.Ran
 import Data.Functor.Plus
 import Data.Functor.Rep
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-import Data.Typeable
-#endif
+import Data.Type.Equality (type (~~))
+import GHC.Exts (TYPE)
 
 -- |
 -- @'Codensity' f@ is the Monad generated by taking the right Kan extension
@@ -54,37 +61,52 @@
 -- repeated applications of @(>>=)@.
 --
 -- See \"Asymptotic Improvement of Computations over Free Monads\" by Janis
--- Voightländer for more information about this type.
+-- Voigtländer for more information about this type.
 --
--- <http://www.iai.uni-bonn.de/~jv/mpc08.pdf>
-newtype Codensity m a = Codensity
+-- <https://www.janis-voigtlaender.eu/papers/AsymptoticImprovementOfComputationsOverFreeMonads.pdf>
+newtype Codensity (m :: k -> TYPE rep) a = Codensity
+-- Note: we *could* generalize @a@ to @TYPE repa@, but the 'Functor'
+-- instance wouldn't carry that, so it doesn't really seem worth
+-- the complication.
   { runCodensity :: forall b. (a -> m b) -> m b
   }
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
-    deriving Typeable
-#endif
 
-instance Functor (Codensity k) where
-  fmap f (Codensity m) = Codensity (\k -> m (k . f))
+instance Functor (Codensity (k :: j -> TYPE rep)) where
+  fmap f (Codensity m) = Codensity (\k -> m (\x -> k (f x)))
   {-# INLINE fmap #-}
 
-instance Apply (Codensity f) where
-  (<.>) = ap
+instance Apply (Codensity (f :: k -> TYPE rep)) where
+  (<.>) = (<*>)
   {-# INLINE (<.>) #-}
 
-instance Applicative (Codensity f) where
+instance Applicative (Codensity (f :: k -> TYPE rep)) where
   pure x = Codensity (\k -> k x)
   {-# INLINE pure #-}
-  (<*>) = ap
+  Codensity f <*> Codensity g = Codensity (\bfr -> f (\ab -> g (\x -> bfr (ab x))))
   {-# INLINE (<*>) #-}
 
-instance Monad (Codensity f) where
-  return x = Codensity (\k -> k x)
+instance Monad (Codensity (f :: k -> TYPE rep)) where
+  return = pure
   {-# INLINE return #-}
   m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))
   {-# INLINE (>>=) #-}
 
-instance MonadIO m => MonadIO (Codensity m) where
+-- Writing instances like
+-- instance MonadFail f => MonadFail (Codensity f)
+-- leads to some hidden flexible instances. Haddock will show things like
+--
+-- MonadFail f => MonadFail (Codensity * LiftedRep f)
+--
+-- Since FlexibleInstances are bad for inference, we avoid them when
+-- we can by carefully pushing kind constraints to the left.
+
+instance (f ~~ f', Fail.MonadFail f')
+  => Fail.MonadFail (Codensity (f :: k -> TYPE rep)) where
+  fail msg = Codensity $ \ _ -> Fail.fail msg
+  {-# INLINE fail #-}
+
+instance (m ~~ m', MonadIO m')
+  => MonadIO (Codensity (m :: k -> TYPE rep)) where
   liftIO = lift . liftIO
   {-# INLINE liftIO #-}
 
@@ -92,11 +114,12 @@
   lift m = Codensity (m >>=)
   {-# INLINE lift #-}
 
-instance Alt v => Alt (Codensity v) where
+instance (v ~~ v', Alt v')
+  => Alt (Codensity (v :: k -> TYPE rep)) where
   Codensity m <!> Codensity n = Codensity (\k -> m k <!> n k)
   {-# INLINE (<!>) #-}
 
-instance Plus v => Plus (Codensity v) where
+instance (v ~~ v', Plus v') => Plus (Codensity (v :: k -> TYPE rep)) where
   zero = Codensity (const zero)
   {-# INLINE zero #-}
 
@@ -110,18 +133,19 @@
   mplus = (<!>)
 -}
 
-instance Alternative v => Alternative (Codensity v) where
+instance (v ~~ v', Alternative v')
+  => Alternative (Codensity (v :: k -> TYPE rep)) where
   empty = Codensity (\_ -> empty)
   {-# INLINE empty #-}
   Codensity m <|> Codensity n = Codensity (\k -> m k <|> n k)
   {-# INLINE (<|>) #-}
 
-instance MonadPlus v => MonadPlus (Codensity v) where
-  mzero = Codensity (\_ -> mzero)
-  {-# INLINE mzero #-}
-  Codensity m `mplus` Codensity n = Codensity (\k -> m k `mplus` n k)
-  {-# INLINE mplus #-}
+instance (v ~~ v', Alternative v')
+   => MonadPlus (Codensity (v :: k -> TYPE rep))
 
+instance MonadThrow m => MonadThrow (Codensity m) where
+  throwM = lift . throwM
+
 -- |
 -- This serves as the *left*-inverse (retraction) of 'lift'.
 --
@@ -136,8 +160,8 @@
 -- e.g. @'Codensity' ((->) s)) a ~ forall r. (a -> s -> r) -> s -> r@
 -- could support a full complement of @'MonadState' s@ actions, while @(->) s@
 -- is limited to @'MonadReader' s@ actions.
-lowerCodensity :: Monad m => Codensity m a -> m a
-lowerCodensity a = runCodensity a return
+lowerCodensity :: Applicative f => Codensity f a -> f a
+lowerCodensity a = runCodensity a pure
 {-# INLINE lowerCodensity #-}
 
 -- | The 'Codensity' monad of a right adjoint is isomorphic to the
@@ -196,16 +220,25 @@
 ranToCodensity (Ran m) = Codensity m
 {-# INLINE ranToCodensity #-}
 
-instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
+instance (m ~~ m', Functor f, MonadFree f m')
+  => MonadFree f (Codensity (m :: k -> TYPE rep)) where
   wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))
   {-# INLINE wrap #-}
 
-instance MonadReader r m => MonadState r (Codensity m) where
+instance (m ~~ m', MonadReader r m')
+  => MonadState r (Codensity (m :: k -> TYPE rep)) where
   get = Codensity (ask >>=)
   {-# INLINE get #-}
   put s = Codensity (\k -> local (const s) (k ()))
   {-# INLINE put #-}
 
+instance (m ~~ m', MonadReader r m')
+  => MonadReader r (Codensity (m :: k -> TYPE rep)) where
+  ask = Codensity (ask >>=)
+  {-# INLINE ask #-}
+  local f m = Codensity $ \c -> ask >>= \r -> local f . runCodensity m $ local (const r) . c
+  {-# INLINE local #-}
+
 -- | Right associate all binds in a computation that generates a free monad
 --
 -- This can improve the asymptotic efficiency of the result, while preserving
@@ -218,3 +251,27 @@
 improve :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
 improve m = lowerCodensity m
 {-# INLINE improve #-}
+
+
+-- | Wrap the remainder of the 'Codensity' action using the given
+-- function.
+--
+-- This function can be used to register cleanup actions that will be
+-- executed at the end.  Example:
+--
+-- > wrapCodensity (`finally` putStrLn "Done.")
+wrapCodensity :: (forall a. m a -> m a) -> Codensity m ()
+wrapCodensity f = Codensity (\k -> f (k ()))
+
+-- | @'reset' m@ delimits the continuation of any 'shift' inside @m@.
+--
+-- * @'reset' ('return' m) = 'return' m@
+reset :: Monad m => Codensity m a -> Codensity m a
+reset = lift . lowerCodensity
+
+-- | @'shift' f@ captures the continuation up to the nearest enclosing
+-- 'reset' and passes it to @f@:
+--
+-- * @'reset' ('shift' f >>= k) = 'reset' (f ('lowerCodensity' . k))@
+shift :: Applicative m => (forall b. (a -> m b) -> Codensity m b) -> Codensity m a
+shift f = Codensity $ lowerCodensity . f
diff --git a/src/Data/Functor/Contravariant/Coyoneda.hs b/src/Data/Functor/Contravariant/Coyoneda.hs
--- a/src/Data/Functor/Contravariant/Coyoneda.hs
+++ b/src/Data/Functor/Contravariant/Coyoneda.hs
@@ -1,16 +1,13 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Trustworthy #-}
-#endif
 
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2013 Edward Kmett
+-- Copyright   :  (C) 2013-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -24,6 +21,7 @@
   ( Coyoneda(..)
   , liftCoyoneda
   , lowerCoyoneda
+  , hoistCoyoneda
   ) where
 
 import Control.Arrow
@@ -71,3 +69,9 @@
 lowerCoyoneda :: Contravariant f => Coyoneda f a -> f a
 lowerCoyoneda (Coyoneda f m) = contramap f m
 {-# INLINE lowerCoyoneda #-}
+
+-- | Lift a natural transformation from @f@ to @g@ to a natural transformation
+-- from @Coyoneda f@ to @Coyoneda g@.
+hoistCoyoneda :: (forall a. f a -> g a) -> (Coyoneda f b -> Coyoneda g b)
+hoistCoyoneda f (Coyoneda g x) = Coyoneda g (f x)
+{-# INLINE hoistCoyoneda #-}
diff --git a/src/Data/Functor/Contravariant/Day.hs b/src/Data/Functor/Contravariant/Day.hs
--- a/src/Data/Functor/Contravariant/Day.hs
+++ b/src/Data/Functor/Contravariant/Day.hs
@@ -1,19 +1,12 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE Rank2Types #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-{-# LANGUAGE DeriveDataTypeable #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ <= 707
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE KindSignatures #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2013-2014 Edward Kmett, Gershom Bazerman and Derek Elkins
+-- Copyright   :  (C) 2013-2016 Edward Kmett, Gershom Bazerman and Derek Elkins
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -38,20 +31,16 @@
   , trans1, trans2
   ) where
 
-import Control.Applicative
+import Control.Arrow ((***))
 import Data.Functor.Contravariant
 import Data.Functor.Contravariant.Rep
+import Data.Functor.Contravariant.Adjunction
+import Data.Functor.Contravariant.Divisible
 import Data.Proxy
 import Data.Tuple (swap)
-#ifdef __GLASGOW_HASKELL__
-import Data.Typeable
-#endif
 
 -- | The Day convolution of two contravariant functors.
 data Day f g a = forall b c. Day (f b) (g c) (a -> (b, c))
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-  deriving Typeable
-#endif
 
 -- | Construct the Day convolution
 --
@@ -62,26 +51,14 @@
 day :: f a -> g b -> Day f g (a, b)
 day fa gb = Day fa gb id
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
-instance (Typeable1 f, Typeable1 g) => Typeable1 (Day f g) where
-    typeOf1 tfga = mkTyConApp dayTyCon [typeOf1 (fa tfga), typeOf1 (ga tfga)]
-        where fa :: t f (g :: * -> *) a -> f a
-              fa = undefined
-              ga :: t (f :: * -> *) g a -> g a
-              ga = undefined
-
-dayTyCon :: TyCon
-#if MIN_VERSION_base(4,4,0)
-dayTyCon = mkTyCon3 "contravariant" "Data.Functor.Contravariant.Day" "Day"
-#else
-dayTyCon = mkTyCon "Data.Functor.Contravariant.Day.Day"
-#endif
-
-#endif
-
 instance Contravariant (Day f g) where
   contramap f (Day fb gc abc) = Day fb gc (abc . f)
 
+instance (Divisible f, Divisible g) => Divisible (Day f g) where
+  divide h (Day f g l) (Day f' g' r) = Day (divided f f') (divided g g') (intertwine . (l *** r) . h)
+    where intertwine ((a, b), (c, d)) = ((a, c), (b, d))
+  conquer = Day conquer conquer (\a -> (a, a))
+
 instance (Representable f, Representable g) => Representable (Day f g) where
   type Rep (Day f g) = (Rep f, Rep g)
 
@@ -97,6 +74,9 @@
     Right (vf, vg) -> (Right vf, Right vg)
   {-# INLINE tabulate #-}
 
+instance (Adjunction f u, Adjunction f' u') => Adjunction (Day f f') (Day u u') where
+  unit a = Day (unit a) (unit a) (\(Day f f' g) -> (contramap (fst . g) f, contramap (snd . g) f'))
+  counit a = Day (counit a) (counit a) (\(Day u u' g) -> (contramap (fst . g) u, contramap (snd . g) u'))
 
 -- | Break apart the Day convolution of two contravariant functors.
 runDay :: (Contravariant f, Contravariant g) => Day f g a -> (f a, g a)
diff --git a/src/Data/Functor/Contravariant/Yoneda.hs b/src/Data/Functor/Contravariant/Yoneda.hs
--- a/src/Data/Functor/Contravariant/Yoneda.hs
+++ b/src/Data/Functor/Contravariant/Yoneda.hs
@@ -1,15 +1,12 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE UndecidableInstances #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
-#endif
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2013 Edward Kmett
+-- Copyright   :  (C) 2013-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
diff --git a/src/Data/Functor/Coyoneda.hs b/src/Data/Functor/Coyoneda.hs
--- a/src/Data/Functor/Coyoneda.hs
+++ b/src/Data/Functor/Coyoneda.hs
@@ -1,49 +1,44 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
-#endif
 
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2011-2013 Edward Kmett
+-- Copyright   :  (C) 2011-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  provisional
 -- Portability :  GADTs, MPTCs, fundeps
 --
+-- @'Coyoneda' f@ is the "free functor" over @f@.
 -- The co-Yoneda lemma for a covariant 'Functor' @f@ states that @'Coyoneda' f@
 -- is naturally isomorphic to @f@.
 ----------------------------------------------------------------------------
 module Data.Functor.Coyoneda
   ( Coyoneda(..)
-  , liftCoyoneda, lowerCoyoneda, lowerM
+  , liftCoyoneda, lowerCoyoneda, lowerM, hoistCoyoneda
   -- * as a Left Kan extension
   , coyonedaToLan, lanToCoyoneda
-  -- * as a Left Kan lift
-  , coyonedaToLift, liftToCoyoneda
   ) where
 
-import Control.Applicative
+import Control.Applicative as A
 import Control.Monad (MonadPlus(..), liftM)
 import Control.Monad.Fix
 import Control.Monad.Trans.Class
 import Control.Comonad
 import Control.Comonad.Trans.Class
 import Data.Distributive
-import Data.Function (on)
 import Data.Functor.Adjunction
 import Data.Functor.Bind
+import Data.Functor.Classes
 import Data.Functor.Extend
 import Data.Functor.Identity
 import Data.Functor.Kan.Lan
-import Data.Functor.Kan.Lift
 import Data.Functor.Plus
 import Data.Functor.Rep
 import Data.Foldable
@@ -60,54 +55,81 @@
 
 -- | @Coyoneda f@ is the left Kan extension of @f@ along the 'Identity' functor.
 --
+-- @Coyoneda f@ is always a functor, even if @f@ is not. In this case, it
+-- is called the /free functor over @f@/. Note the following categorical fine
+-- print: If @f@ is not a functor, @Coyoneda f@ is actually not the left Kan
+-- extension of @f@ along the 'Identity' functor, but along the inclusion
+-- functor from the discrete subcategory of /Hask/ which contains only identity
+-- functions as morphisms to the full category /Hask/. (This is because @f@,
+-- not being a proper functor, can only be interpreted as a categorical functor
+-- by restricting the source category to only contain identities.)
+--
 -- @
 -- 'coyonedaToLan' . 'lanToCoyoneda' ≡ 'id'
 -- 'lanToCoyoneda' . 'coyonedaToLan' ≡ 'id'
 -- @
 coyonedaToLan :: Coyoneda f a -> Lan Identity f a
 coyonedaToLan (Coyoneda ba fb) = Lan (ba . runIdentity) fb
+{-# INLINE coyonedaToLan #-}
 
 lanToCoyoneda :: Lan Identity f a -> Coyoneda f a
 lanToCoyoneda (Lan iba fb) = Coyoneda (iba . Identity) fb
-
-{-# RULES "coyonedaToLan/lanToCoyoneda=id" coyonedaToLan . lanToCoyoneda = id #-}
-{-# RULES "lanToCoyoneda/coyonedaToLan=id" lanToCoyoneda . coyonedaToLan = id #-}
-
--- | @'Coyoneda' f@ is the left Kan lift of @f@ along the 'Identity' functor.
---
--- @
--- 'coyonedaToLift' . 'liftToCoyoneda' ≡ 'id'
--- 'liftToCoyoneda' . 'coyonedaToLift' ≡ 'id'
--- @
-coyonedaToLift :: Coyoneda f a -> Lift Identity f a
-coyonedaToLift (Coyoneda ba fb) = Lift $ \ f2iz -> ba <$> runIdentity (f2iz fb)
-
-liftToCoyoneda :: Functor f => Lift Identity f a -> Coyoneda f a
-liftToCoyoneda (Lift m) = Coyoneda id (m Identity)
+{-# INLINE lanToCoyoneda #-}
 
-{-# RULES "coyonedaToLift/liftToCoyoneda=id" coyonedaToLift . liftToCoyoneda = id #-}
-{-# RULES "liftToCoyoneda/coyonedaToLift=id" liftToCoyoneda . coyonedaToLift = id #-}
+-- {-# RULES "coyonedaToLan/lanToCoyoneda=id" coyonedaToLan . lanToCoyoneda = id #-}
+-- {-# RULES "lanToCoyoneda/coyonedaToLan=id" lanToCoyoneda . coyonedaToLan = id #-}
 
 instance Functor (Coyoneda f) where
   fmap f (Coyoneda g v) = Coyoneda (f . g) v
   {-# INLINE fmap #-}
 
 instance Apply f => Apply (Coyoneda f) where
-  m <.> n = liftCoyoneda $ lowerCoyoneda m <.> lowerCoyoneda n
+  Coyoneda mf m <.> Coyoneda nf n =
+    liftCoyoneda $ (\mres nres -> mf mres (nf nres)) <$> m <.> n
   {-# INLINE (<.>) #-}
+  Coyoneda _ m .> Coyoneda g n = Coyoneda g (m .> n)
+  {-# INLINE (.>) #-}
+  Coyoneda f m <. Coyoneda _ n = Coyoneda f (m <. n)
+  {-# INLINE (<.) #-}
 
 instance Applicative f => Applicative (Coyoneda f) where
   pure = liftCoyoneda . pure
   {-# INLINE pure #-}
-  m <*> n = liftCoyoneda $ lowerCoyoneda m <*> lowerCoyoneda n
+  Coyoneda mf m <*> Coyoneda nf n =
+    liftCoyoneda $ (\mres nres -> mf mres (nf nres)) <$> m <*> n
   {-# INLINE (<*>) #-}
+  Coyoneda _ m *> Coyoneda g n = Coyoneda g (m *> n)
+  {-# INLINE (*>) #-}
+  Coyoneda f m <* Coyoneda _ n = Coyoneda f (m <* n)
+  {-# INLINE (<*) #-}
 
 instance Alternative f => Alternative (Coyoneda f) where
   empty = liftCoyoneda empty
   {-# INLINE empty #-}
   m <|> n = liftCoyoneda $ lowerCoyoneda m <|> lowerCoyoneda n
   {-# INLINE (<|>) #-}
+  some = liftCoyoneda . A.some . lowerCoyoneda
+  {-# INLINE some #-}
+  many = liftCoyoneda . A.many . lowerCoyoneda
+  {-# INLINE many #-}
 
+{-
+-- These are slightly optimized versions of the *default*
+-- `some` and `many` definitions for `Coyoneda`. I don't
+-- know if it's worth the clutter to expose them.
+someDefault (Coyoneda vf vb) = liftCoyoneda some_v
+  where
+    many_v = some_v <|> pure []
+    some_v = (:) . vf <$> vb <*> many_v
+{-# INLINE someDefault #-}
+
+manyDefault (Coyoneda vf vb) = liftCoyoneda many_v
+  where
+    many_v = some_v <|> pure []
+    some_v = (:) . vf <$> vb <*> many_v
+{-# INLINE many #-}
+-}
+
 instance Alt f => Alt (Coyoneda f) where
   m <!> n = liftCoyoneda $ lowerCoyoneda m <!> lowerCoyoneda n
   {-# INLINE (<!>) #-}
@@ -121,8 +143,9 @@
   {-# INLINE (>>-) #-}
 
 instance Monad m => Monad (Coyoneda m) where
-  return = Coyoneda id . return
-  {-# INLINE return #-}
+  (>>) = (*>)
+  {-# INLINE (>>) #-}
+
   Coyoneda f v >>= k = lift (v >>= lowerM . k . f)
   {-# INLINE (>>=) #-}
 
@@ -181,31 +204,48 @@
   collect f = liftCoyoneda . collect (lowerCoyoneda . f)
   {-# INLINE collect #-}
 
-instance (Functor f, Show (f a)) => Show (Coyoneda f a) where
-  showsPrec d (Coyoneda f a) = showParen (d > 10) $
-    showString "liftCoyoneda " . showsPrec 11 (fmap f a)
+instance (Functor f, Show1 f) => Show1 (Coyoneda f) where
+  liftShowsPrec sp sl d (Coyoneda f a) =
+    showsUnaryWith (liftShowsPrec sp sl) "liftCoyoneda" d (fmap f a)
+  {-# INLINE liftShowsPrec #-}
+
+instance (Read1 f) => Read1 (Coyoneda f) where
+  liftReadsPrec rp rl = readsData $
+    readsUnaryWith (liftReadsPrec rp rl) "liftCoyoneda" liftCoyoneda
+  {-# INLINE liftReadsPrec #-}
+
+instance (Functor f, Show1 f, Show a) => Show (Coyoneda f a) where
+  showsPrec = showsPrec1
   {-# INLINE showsPrec #-}
 
-#ifdef __GLASGOW_HASKELL__
-instance (Functor f, Read (f a)) => Read (Coyoneda f a) where
+instance Read (f a) => Read (Coyoneda f a) where
   readPrec = parens $ prec 10 $ do
     Ident "liftCoyoneda" <- lexP
     liftCoyoneda <$> step readPrec
   {-# INLINE readPrec #-}
-#endif
 
-instance (Functor f, Eq (f a)) => Eq (Coyoneda f a) where
-  (==) = (==) `on` lowerCoyoneda
+instance Eq1 f => Eq1 (Coyoneda f) where
+  liftEq eq (Coyoneda f xs) (Coyoneda g ys) =
+    liftEq (\x y -> eq (f x) (g y)) xs ys
+  {-# INLINE liftEq #-}
+
+instance Ord1 f => Ord1 (Coyoneda f) where
+  liftCompare cmp (Coyoneda f xs) (Coyoneda g ys) =
+    liftCompare (\x y -> cmp (f x) (g y)) xs ys
+  {-# INLINE liftCompare #-}
+
+instance (Eq1 f, Eq a) => Eq (Coyoneda f a) where
+  (==) = eq1
   {-# INLINE (==) #-}
 
-instance (Functor f, Ord (f a)) => Ord (Coyoneda f a) where
-  compare = compare `on` lowerCoyoneda
+instance (Ord1 f, Ord a) => Ord (Coyoneda f a) where
+  compare = compare1
   {-# INLINE compare #-}
 
 instance Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g) where
-  unit = liftCoyoneda . fmap liftCoyoneda . unit
+  unit = liftCoyoneda . leftAdjunct liftCoyoneda
   {-# INLINE unit #-}
-  counit = counit . fmap lowerCoyoneda . lowerCoyoneda
+  counit = rightAdjunct lowerCoyoneda . lowerCoyoneda
   {-# INLINE counit #-}
 
 -- | Yoneda \"expansion\"
@@ -254,3 +294,9 @@
 lowerM :: Monad f => Coyoneda f a -> f a
 lowerM (Coyoneda f m) = liftM f m
 {-# INLINE lowerM #-}
+
+-- | Lift a natural transformation from @f@ to @g@ to a natural transformation
+-- from @Coyoneda f@ to @Coyoneda g@.
+hoistCoyoneda :: (forall a. f a -> g a) -> (Coyoneda f b -> Coyoneda g b)
+hoistCoyoneda f (Coyoneda g x) = Coyoneda g (f x)
+{-# INLINE hoistCoyoneda #-}
diff --git a/src/Data/Functor/Day.hs b/src/Data/Functor/Day.hs
--- a/src/Data/Functor/Day.hs
+++ b/src/Data/Functor/Day.hs
@@ -1,12 +1,12 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
--- Copyright   :  (C) 2014 Edward Kmett
+-- Copyright   :  (C) 2014-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -35,45 +35,28 @@
   , intro1, intro2
   , elim1, elim2
   , trans1, trans2
+  , cayley, dayley
   ) where
 
 import Control.Applicative
+import Control.Category
+import Control.Comonad
+import Control.Comonad.Trans.Class
 import Data.Distributive
+import Data.Profunctor.Cayley (Cayley(..))
+import Data.Profunctor.Composition (Procompose(..))
+import Data.Functor.Adjunction
 import Data.Functor.Identity
 import Data.Functor.Rep
-#ifdef __GLASGOW_HASKELL__
-import Data.Typeable
-#endif
+import Prelude hiding (id,(.))
 
 -- | The Day convolution of two covariant functors.
---
--- @Day f g a -> h a@ is isomorphic to @f a -> Rift g h a@
 data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a)
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
-  deriving Typeable
-#endif
 
 -- | Construct the Day convolution
 day :: f (a -> b) -> g a -> Day f g b
 day fa gb = Day fa gb id
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707
-instance (Typeable1 f, Typeable1 g) => Typeable1 (Day f g) where
-    typeOf1 tfga = mkTyConApp dayTyCon [typeOf1 (fa tfga), typeOf1 (ga tfga)]
-        where fa :: t f (g :: * -> *) a -> f a
-              fa = undefined
-              ga :: t (f :: * -> *) g a -> g a
-              ga = undefined
-
-dayTyCon :: TyCon
-#if MIN_VERSION_base(4,4,0)
-dayTyCon = mkTyCon3 "contravariant" "Data.Functor.Day" "Day"
-#else
-dayTyCon = mkTyCon "Data.Functor.Day.Day"
-#endif
-
-#endif
-
 instance Functor (Day f g) where
   fmap f (Day fb gc bca) = Day fb gc $ \b c -> f (bca b c)
 
@@ -84,13 +67,36 @@
         (\(a,c) (b,d) -> u a b (v c d))
 
 instance (Representable f, Representable g) => Distributive (Day f g) where
-  distribute f = Day (tabulate id) (tabulate id) $ \x y -> fmap (\(Day m n o) -> o (index m x) (index n y)) f
+  distribute f = Day (tabulate id) (tabulate id) $ \x y ->
+    fmap (\(Day m n o) -> o (index m x) (index n y)) f
 
+  collect g f = Day (tabulate id) (tabulate id) $ \x y ->
+    fmap (\q -> case g q of Day m n o -> o (index m x) (index n y)) f
+
 instance (Representable f, Representable g) => Representable (Day f g) where
   type Rep (Day f g) = (Rep f, Rep g)
   tabulate f = Day (tabulate id) (tabulate id) (curry f)
   index (Day m n o) (x,y) = o (index m x) (index n y)
 
+instance (Adjunction f u, Adjunction f' u') => Adjunction (Day f f') (Day u u') where
+  unit a = Day (unit ()) (unit ()) (\f f' -> Day f f' (\() () -> a))
+  counit (Day f f' h) = case h a a' of Day u u' g -> g (indexAdjunction u f_) (indexAdjunction u' f_')
+    where
+      (a, f_) = splitL f
+      (a', f_') = splitL f'
+
+instance (Comonad f, Comonad g) => Comonad (Day f g) where
+  extract (Day fb gc bca) = bca (extract fb) (extract gc)
+  duplicate (Day fb gc bca) = Day (duplicate fb) (duplicate gc) (\fb' gc' -> Day fb' gc' bca)
+
+instance (ComonadApply f, ComonadApply g) => ComonadApply (Day f g) where
+  Day fa fb u <@> Day gc gd v =
+    Day ((,) <$> fa <@> gc) ((,) <$> fb <@> gd)
+        (\(a,c) (b,d) -> u a b (v c d))
+
+instance Comonad f => ComonadTrans (Day f) where
+  lower (Day fb gc bca) = bca (extract fb) <$> gc
+
 -- | Day convolution provides a monoidal product. The associativity
 -- of this monoid is witnessed by 'assoc' and 'disassoc'.
 --
@@ -161,7 +167,7 @@
 
 -- | Collapse via a monoidal functor.
 --
--- @ 
+-- @
 -- 'dap' ('day' f g) = f '<*>' g
 -- @
 dap :: Applicative f => Day f f a -> f a
@@ -186,3 +192,10 @@
 -- @
 trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
 trans2 gh (Day fb gc bca) = Day fb (gh gc) bca
+
+cayley :: Procompose (Cayley f p) (Cayley g q) a b -> Cayley (Day f g) (Procompose p q) a b
+cayley (Procompose (Cayley p) (Cayley q)) = Cayley $ Day p q Procompose
+
+-- | Proposition 4.1 from Pastro and Street
+dayley :: Category p => Procompose (Cayley f p) (Cayley g p) a b -> Cayley (Day f g) p a b
+dayley (Procompose (Cayley p) (Cayley q)) = Cayley $ Day p q (.)
diff --git a/src/Data/Functor/Day/Curried.hs b/src/Data/Functor/Day/Curried.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Day/Curried.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Copyright 	: 2013-2016 Edward Kmett and Dan Doel
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: rank N types
+--
+-- @'Day' f -| 'Curried' f@
+--
+-- @'Day' f ~ 'Compose' f@ when f preserves colimits / is a left adjoint. (Due in part to the
+-- strength of all functors in Hask.)
+--
+-- So by the uniqueness of adjoints, when f is a left adjoint, @'Curried' f ~ 'Rift' f@
+-------------------------------------------------------------------------------------------
+module Data.Functor.Day.Curried
+  (
+  -- * Right Kan lifts
+    Curried(..)
+  , toCurried, fromCurried, applied, unapplied
+  , adjointToCurried, curriedToAdjoint
+  , composedAdjointToCurried, curriedToComposedAdjoint
+  , liftCurried, lowerCurried, rap
+  ) where
+
+import qualified Control.Applicative as App
+import Data.Functor.Adjunction
+import Data.Functor.Day
+import Data.Functor.Identity
+import Data.Functor.Apply
+
+newtype Curried g h a =
+  Curried { runCurried :: forall r. g (a -> r) -> h r }
+
+instance Functor g => Functor (Curried g h) where
+  fmap f (Curried g) = Curried (g . fmap (.f))
+  {-# INLINE fmap #-}
+
+instance (Functor g, g ~ h) => Apply (Curried g h) where
+  Curried mf <.> Curried ma = Curried (ma . mf . fmap (.))
+  {-# INLINE (<.>) #-}
+  liftF2 f (Curried g) (Curried ma) = Curried (ma . g . fmap (\p q -> p . f q))
+  {-# INLINE liftF2 #-}
+
+instance (Functor g, g ~ h) => App.Applicative (Curried g h) where
+  pure a = Curried (fmap ($ a))
+  {-# INLINE pure #-}
+  Curried mf <*> Curried ma = Curried (ma . mf . fmap (.))
+  {-# INLINE (<*>) #-}
+  liftA2 f (Curried g) (Curried ma) = Curried (ma . g . fmap (\p q -> p . f q))
+  {-# INLINE liftA2 #-}
+
+-- | The natural isomorphism between @f@ and @Curried f f@.
+-- @
+-- 'lowerCurried' '.' 'liftCurried' ≡ 'id'
+-- 'liftCurried' '.' 'lowerCurried' ≡ 'id'
+-- @
+--
+-- @
+-- 'lowerCurried' ('liftCurried' x)     -- definition
+-- 'lowerCurried' ('Curried' ('<*>' x))   -- definition
+-- ('<*>' x) ('pure' 'id')          -- beta reduction
+-- 'pure' 'id' '<*>' x              -- Applicative identity law
+-- x
+-- @
+liftCurried :: Applicative f => f a -> Curried f f a
+liftCurried fa = Curried (<*> fa)
+{-# INLINE liftCurried #-}
+
+-- | Lower 'Curried' by applying 'pure' 'id' to the continuation.
+--
+-- See 'liftCurried'.
+lowerCurried :: Applicative f => Curried f g a -> g a
+lowerCurried (Curried f) = f (pure id)
+{-# INLINE lowerCurried #-}
+
+-- | Indexed applicative composition of right Kan lifts.
+rap :: Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b
+rap (Curried mf) (Curried ma) = Curried (ma . mf . fmap (.))
+{-# INLINE rap #-}
+
+-- | This is the counit of the @Day f -| Curried f@ adjunction
+applied :: Functor f => Day f (Curried f g) a -> g a
+applied (Day fb (Curried fg) bca) = fg (bca <$> fb)
+{-# INLINE applied #-}
+
+-- | This is the unit of the @Day f -| Curried f@ adjunction
+unapplied :: g a -> Curried f (Day f g) a
+unapplied ga = Curried $ \ fab -> Day fab ga id
+{-# INLINE unapplied #-}
+
+-- | The universal property of 'Curried'
+toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a
+toCurried h ka = Curried $ \gar -> h (Day gar ka id)
+{-# INLINE toCurried #-}
+
+-- |
+-- @
+-- 'toCurried' . 'fromCurried' ≡ 'id'
+-- 'fromCurried' . 'toCurried' ≡ 'id'
+-- @
+fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b
+fromCurried f (Day fc kd cdb) = runCurried (f kd) (cdb <$> fc)
+{-# INLINE fromCurried #-}
+
+-- | @Curried f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
+--
+-- @
+-- 'adjointToCurried' . 'curriedToAdjoint' ≡ 'id'
+-- 'curriedToAdjoint' . 'adjointToCurried' ≡ 'id'
+-- @
+adjointToCurried :: Adjunction f u => u a -> Curried f Identity a
+adjointToCurried ua = Curried (Identity . rightAdjunct (<$> ua))
+{-# INLINE adjointToCurried #-}
+
+-- | @Curried f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
+curriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a
+curriedToAdjoint (Curried m) = leftAdjunct (runIdentity . m) id
+{-# INLINE curriedToAdjoint #-}
+
+-- | @Curried f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
+--
+-- @
+-- 'curriedToComposedAdjoint' . 'composedAdjointToCurried' ≡ 'id'
+-- 'composedAdjointToCurried' . 'curriedToComposedAdjoint' ≡ 'id'
+-- @
+
+curriedToComposedAdjoint :: Adjunction f u => Curried f h a -> u (h a)
+curriedToComposedAdjoint (Curried m) = leftAdjunct m id
+{-# INLINE curriedToComposedAdjoint #-}
+
+-- | @Curried f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
+composedAdjointToCurried :: (Functor h, Adjunction f u) => u (h a) -> Curried f h a
+composedAdjointToCurried uha = Curried $ rightAdjunct (\b -> fmap b <$> uha)
+{-# INLINE composedAdjointToCurried #-}
+
diff --git a/src/Data/Functor/Invariant/Day.hs b/src/Data/Functor/Invariant/Day.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Functor/Invariant/Day.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE RankNTypes                #-}
+-----------------------------------------------------------------------------
+-- |
+-- Copyright   :  (C) 2018 Brian Mckenna
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- The Day convolution of two invariant functors is an invariant
+-- functor.
+--
+-- <http://ncatlab.org/nlab/show/Day+convolution>
+----------------------------------------------------------------------------
+
+module Data.Functor.Invariant.Day
+  ( Day(..)
+  , day
+  , assoc, disassoc
+  , swapped
+  , intro1, intro2
+  , elim1, elim2
+  , trans1, trans2
+  , toContravariant, toCovariant
+  ) where
+
+import qualified Data.Functor.Contravariant.Day as Contravariant
+import qualified Data.Functor.Day               as Covariant
+import           Data.Functor.Identity
+import           Data.Functor.Invariant
+
+-- | The Day convolution of two invariant functors.
+data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a) (a -> (b, c))
+
+instance Invariant (Day f g) where
+  invmap f g (Day fb gc bca abc) = Day fb gc ((f .) . bca) (abc . g)
+
+-- | Construct the Day convolution
+day :: f a -> g b -> Day f g (a, b)
+day fa gb = Day fa gb (,) id
+
+-- | Day convolution provides a monoidal product. The associativity
+-- of this monoid is witnessed by 'assoc' and 'disassoc'.
+--
+-- @
+-- 'assoc' . 'disassoc' = 'id'
+-- 'disassoc' . 'assoc' = 'id'
+-- 'invmap' f g '.' 'assoc' = 'assoc' '.' 'invmap' f g
+-- @
+assoc :: Day f (Day g h) a -> Day (Day f g) h a
+assoc (Day fb (Day gd he dec cde) bca abc) = flip (Day (Day fb gd (,) id) he) f g
+  where
+    f a =
+      let (b,c) = abc a
+          (d,e) = cde c
+      in ((b,d),e)
+    g (b,d) e =
+      bca b (dec d e)
+
+-- | Day convolution provides a monoidal product. The associativity
+-- of this monoid is witnessed by 'assoc' and 'disassoc'.
+--
+-- @
+-- 'assoc' . 'disassoc' = 'id'
+-- 'disassoc' . 'assoc' = 'id'
+-- 'invmap' f g '.' 'disassoc' = 'disassoc' '.' 'invmap' f g
+-- @
+disassoc :: Day (Day f g) h a -> Day f (Day g h) a
+disassoc (Day (Day fb gc deb bde) hd bca abc) = Day fb (Day gc hd (,) id) f g
+  where
+    f e (d,c) =
+      bca (deb e d) c
+    g a =
+      let (b,c) = abc a
+          (d,e) = bde b
+      in (d,(e,c))
+
+-- | The monoid for 'Day' convolution on the cartesian monoidal structure is symmetric.
+--
+-- @
+-- 'invmap' f g '.' 'swapped' = 'swapped' '.' 'invmap' f g
+-- @
+swapped :: Day f g a -> Day g f a
+swapped (Day fb gc bca abc) = Day gc fb (flip bca) (\a -> let (b, c) = abc a in (c, b))
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro1' '.' 'elim1' = 'id'
+-- 'elim1' '.' 'intro1' = 'id'
+-- @
+intro1 :: f a -> Day Identity f a
+intro1 fa = Day (Identity ()) fa (\_ a -> a) ((,) ())
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro2' '.' 'elim2' = 'id'
+-- 'elim2' '.' 'intro2' = 'id'
+-- @
+intro2 :: f a -> Day f Identity a
+intro2 fa = Day fa (Identity ()) const (flip (,) ())
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro1' '.' 'elim1' = 'id'
+-- 'elim1' '.' 'intro1' = 'id'
+-- @
+elim1 :: Invariant f => Day Identity f a -> f a
+elim1 (Day (Identity b) fc bca abc) = invmap (bca b) (snd . abc) fc
+
+-- | 'Identity' is the unit of 'Day' convolution
+--
+-- @
+-- 'intro2' '.' 'elim2' = 'id'
+-- 'elim2' '.' 'intro2' = 'id'
+-- @
+elim2 :: Invariant f => Day f Identity a -> f a
+elim2 (Day fb (Identity c) bca abc) = invmap (flip bca c) (fst . abc) fb
+
+-- | Apply a natural transformation to the left-hand side of a Day convolution.
+--
+-- This respects the naturality of the natural transformation you supplied:
+--
+-- @
+-- 'invmap' f g '.' 'trans1' fg = 'trans1' fg '.' 'invmap' f g
+-- @
+trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
+trans1 fg (Day fb hc bca abc) = Day (fg fb) hc bca abc
+
+-- | Apply a natural transformation to the right-hand side of a Day convolution.
+--
+-- This respects the naturality of the natural transformation you supplied:
+--
+-- @
+-- 'invmap' f g '.' 'trans2' fg = 'trans2' fg '.' 'invmap' f g
+-- @
+trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
+trans2 gh (Day fb gc bca abc) = Day fb (gh gc) bca abc
+
+-- | Drop the covariant part of the Day convolution.
+toContravariant :: Day f g a -> Contravariant.Day f g a
+toContravariant (Day fb gc _ abc) = Contravariant.Day fb gc abc
+
+-- | Drop the contravariant part of the Day convolution.
+toCovariant :: Day f g a -> Covariant.Day f g a
+toCovariant (Day fb gc bca _) = Covariant.Day fb gc bca
diff --git a/src/Data/Functor/Kan/Lan.hs b/src/Data/Functor/Kan/Lan.hs
--- a/src/Data/Functor/Kan/Lan.hs
+++ b/src/Data/Functor/Kan/Lan.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE Rank2Types, GADTs #-}
 {-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE PolyKinds #-}
 -------------------------------------------------------------------------------------------
 -- |
--- Copyright 	: 2008-2013 Edward Kmett
+-- Copyright 	: 2008-2016 Edward Kmett
 -- License	: BSD
 --
 -- Maintainer	: Edward Kmett <ekmett@gmail.com>
@@ -25,7 +24,9 @@
   , composedAdjointToLan, lanToComposedAdjoint
   ) where
 
+#if !(MIN_VERSION_base(4,18,0))
 import Control.Applicative
+#endif
 import Data.Functor.Adjunction
 import Data.Functor.Apply
 import Data.Functor.Composition
diff --git a/src/Data/Functor/Kan/Lift.hs b/src/Data/Functor/Kan/Lift.hs
deleted file mode 100644
--- a/src/Data/Functor/Kan/Lift.hs
+++ /dev/null
@@ -1,150 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE GADTs #-}
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
--------------------------------------------------------------------------------------------
--- |
--- Copyright 	: 2013 Edward Kmett and Dan Doel
--- License	: BSD
---
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: rank N types
---
--- Left Kan lifts for functors over Hask, wherever they exist.
---
--- <http://ncatlab.org/nlab/show/Kan+lift>
--------------------------------------------------------------------------------------------
-module Data.Functor.Kan.Lift
-  (
-  -- * Left Kan lifts
-    Lift(..)
-  , toLift, fromLift, glift
-  , composeLift, decomposeLift
-  , adjointToLift, liftToAdjoint
-  , liftToComposedAdjoint, composedAdjointToLift
-  , repToLift, liftToRep
-  , liftToComposedRep, composedRepToLift
-  ) where
-
-import Data.Copointed
-import Data.Functor.Adjunction
-import Data.Functor.Composition
-import Data.Functor.Compose
-import Data.Functor.Identity
-import Data.Functor.Rep
-
--- * Left Kan Lift
-
--- |
--- > f => g . Lift g f
--- > (forall z. f => g . z) -> Lift g f => z -- couniversal
---
--- Here we use the universal property directly as how we extract from our definition of 'Lift'.
-newtype Lift g f a = Lift { runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a }
-
-instance Functor (Lift g h) where
-  fmap f (Lift g) = Lift (\x -> fmap f (g x))
-  {-# INLINE fmap #-}
-
-instance (Functor g, g ~ h) => Copointed (Lift g h) where
-  copoint x = runIdentity (runLift x (fmap Identity))
-  {-# INLINE copoint #-}
-
--- |
---
--- @f => g ('Lift' g f a)@
-glift :: Adjunction l g => k a -> g (Lift g k a)
-glift = leftAdjunct (\lka -> Lift (\k2gz -> rightAdjunct k2gz lka))
-{-# INLINE glift #-}
-
--- | The universal property of 'Lift'
-toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b
-toLift f l =  runLift l f
-{-# INLINE toLift #-}
-
--- | When the adjunction exists
---
--- @
--- 'fromLift' . 'toLift' ≡ 'id'
--- 'toLift' . 'fromLift' ≡ 'id'
--- @
-fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)
-fromLift f = fmap f . glift
-{-# INLINE fromLift #-}
-
--- |
---
--- @
--- 'composeLift' . 'decomposeLift' = 'id'
--- 'decomposeLift' . 'composeLift' = 'id'
--- @
-composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a
-composeLift (Lift m) = Lift $ \h -> m $ decompose . toLift (fmap Compose . decompose . h)
-{-# INLINE composeLift #-}
-
-decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a
-decomposeLift (Lift m) = Lift $ \h -> m (compose . fmap h . glift)
-{-# INLINE decomposeLift #-}
-
--- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.
---
--- @
--- 'adjointToLift' . 'liftToAdjoint' ≡ 'id'
--- 'liftToAdjoint' . 'adjointToLift' ≡ 'id'
--- @
-adjointToLift :: Adjunction f u => f a -> Lift u Identity a
-adjointToLift fa = Lift $ \k -> rightAdjunct (k . Identity) fa
-{-# INLINE adjointToLift #-}
-
-
--- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.
-liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a
-liftToAdjoint = toLift (unit . runIdentity)
-{-# INLINE liftToAdjoint #-}
-
--- |
---
--- @
--- 'repToLift' . 'liftToRep' ≡ 'id'
--- 'liftToRep' . 'repToLift' ≡ 'id'
--- @
-repToLift :: Representable u => Rep u -> a -> Lift u Identity a
-repToLift e a = Lift $ \k -> index (k (Identity a)) e
-{-# INLINE repToLift #-}
-
-liftToRep :: Representable u => Lift u Identity a -> (Rep u, a)
-liftToRep (Lift m) = m $ \(Identity a) -> tabulate $ \e -> (e, a)
-{-# INLINE liftToRep #-}
-
--- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.
---
--- @
--- 'liftToComposedAdjoint' . 'composedAdjointToLift' ≡ 'id'
--- 'composedAdjointToLift' . 'liftToComposedAdjoint' ≡ 'id'
--- @
-liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)
-liftToComposedAdjoint (Lift m) = decompose $ m (leftAdjunct Compose)
-{-# INLINE liftToComposedAdjoint #-}
-
--- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.
-composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a
-composedAdjointToLift = rightAdjunct glift
-{-# INLINE composedAdjointToLift #-}
-
--- |
---
--- @
--- 'liftToComposedRep' . 'composedRepToLift' ≡ 'id'
--- 'composedRepToLift' . 'liftToComposedRep' ≡ 'id'
--- @
-liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Rep u, h a)
-liftToComposedRep (Lift m) = decompose $ m $ \h -> tabulate $ \e -> Compose (e, h)
-{-# INLINE liftToComposedRep #-}
-
-composedRepToLift :: Representable u => Rep u -> h a -> Lift u h a
-composedRepToLift e ha = Lift $ \h2uz -> index (h2uz ha) e
-{-# INLINE composedRepToLift #-}
diff --git a/src/Data/Functor/Kan/Ran.hs b/src/Data/Functor/Kan/Ran.hs
--- a/src/Data/Functor/Kan/Ran.hs
+++ b/src/Data/Functor/Kan/Ran.hs
@@ -1,11 +1,9 @@
 {-# LANGUAGE Rank2Types, GADTs #-}
-{-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE Trustworthy #-}
-#endif
 -------------------------------------------------------------------------------------------
 -- |
--- Copyright 	: 2008-2013 Edward Kmett
+-- Copyright 	: 2008-2016 Edward Kmett
 -- License	: BSD
 --
 -- Maintainer	: Edward Kmett <ekmett@gmail.com>
@@ -37,8 +35,8 @@
 -- the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition
 -- from the universal property.
 --
--- Given a 'Functor' @h : C -> D@ and a 'Functor' @g : C -> C'@, we want to find extend @h@ /back/ along @g@
--- to give @Ran g h : C' -> C@, such that the natural transformation @'gran' :: Ran g h (g a) -> h a@ exists.
+-- Given a 'Functor' @h : C -> D@ and a 'Functor' @g : C -> C'@, we want to extend @h@ /back/ along @g@
+-- to give @Ran g h : C' -> D@, such that the natural transformation @'gran' :: Ran g h (g a) -> h a@ exists.
 --
 -- In some sense this is trying to approximate the inverse of @g@ by using one of
 -- its adjoints, because if the adjoint and the inverse both exist, they match!
@@ -52,7 +50,7 @@
 --
 -- The Right Kan extension is unique (up to isomorphism) by taking this as its universal property.
 --
--- That is to say given any @K : C' -> C@ such that we have a natural transformation from @k.g@ to @h@
+-- That is to say given any @K : C' -> D@ such that we have a natural transformation from @k.g@ to @h@
 -- @(forall x. k (g x) -> h x)@ there exists a canonical natural transformation from @k@ to @Ran g h@.
 -- @(forall x. k x -> Ran g h x)@.
 --
@@ -102,7 +100,7 @@
 -- 'fromRan' . 'toRan' ≡ 'id'
 -- @
 fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b
-fromRan s = flip runRan id . s
+fromRan s kgb = runRan (s kgb) id
 {-# INLINE fromRan #-}
 
 -- |
diff --git a/src/Data/Functor/Kan/Rift.hs b/src/Data/Functor/Kan/Rift.hs
deleted file mode 100644
--- a/src/Data/Functor/Kan/Rift.hs
+++ /dev/null
@@ -1,189 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE GADTs #-}
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
--------------------------------------------------------------------------------------------
--- |
--- Copyright 	: 2013 Edward Kmett and Dan Doel
--- License	: BSD
---
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: rank N types
---
--- Right and Left Kan lifts for functors over Hask, where they exist.
---
--- <http://ncatlab.org/nlab/show/Kan+lift>
--------------------------------------------------------------------------------------------
-module Data.Functor.Kan.Rift
-  (
-  -- * Right Kan lifts
-    Rift(..)
-  , toRift, fromRift, grift
-  , composeRift, decomposeRift
-  , adjointToRift, riftToAdjoint
-  , composedAdjointToRift, riftToComposedAdjoint
-  , rap
-  ) where
-
-import Control.Applicative
-import Data.Functor.Adjunction
-import Data.Functor.Composition
-import Data.Functor.Identity
-import Data.Pointed
-
--- * Right Kan Lift
-
--- |
---
--- @g . 'Rift' g f => f@
---
--- This could alternately be defined directly from the (co)universal propertly
--- in which case, we'd get 'toRift' = 'UniversalRift', but then the usage would
--- suffer.
---
--- @
--- data 'UniversalRift' g f a = forall z. 'Functor' z =>
---      'UniversalRift' (forall x. g (z x) -> f x) (z a)
--- @
---
--- We can witness the isomorphism between Rift and UniversalRift using:
---
--- @
--- riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a
--- riftIso1 (UniversalRift h z) = Rift $ \\g -> h $ fmap (\\k -> k \<$\> z) g
--- @
---
--- @
--- riftIso2 :: Rift g f a -> UniversalRift g f a
--- riftIso2 (Rift e) = UniversalRift e id
--- @
---
--- @
--- riftIso1 (riftIso2 (Rift h)) =
--- riftIso1 (UniversalRift h id) =          -- by definition
--- Rift $ \\g -> h $ fmap (\\k -> k \<$\> id) g -- by definition
--- Rift $ \\g -> h $ fmap id g               -- \<$\> = (.) and (.id)
--- Rift $ \\g -> h g                         -- by functor law
--- Rift h                                   -- eta reduction
--- @
---
--- The other direction is left as an exercise for the reader.
---
--- There are several monads that we can form from @Rift@.
---
--- When @g@ is corepresentable (e.g. is a right adjoint) then there exists @x@ such that @g ~ (->) x@, then it follows that
---
--- @
--- Rift g g a ~
--- forall r. (x -> a -> r) -> x -> r ~
--- forall r. (a -> x -> r) -> x -> r ~
--- forall r. (a -> g r) -> g r ~
--- Codensity g r
--- @
---
--- When @f@ is a left adjoint, so that @f -| g@ then
---
--- @
--- Rift f f a ~
--- forall r. f (a -> r) -> f r ~
--- forall r. (a -> r) -> g (f r) ~
--- forall r. (a -> r) -> Adjoint f g r ~
--- Yoneda (Adjoint f g r)
--- @
---
--- An alternative way to view that is to note that whenever @f@ is a left adjoint then @f -| 'Rift' f 'Identity'@, and since @'Rift' f f@ is isomorphic to @'Rift' f 'Identity' (f a)@, this is the 'Monad' formed by the adjunction.
---
--- @'Rift' 'Identity' m@ can be a 'Monad' for any 'Monad' @m@, as it is isomorphic to @'Yoneda' m@.
-
-newtype Rift g h a =
-  Rift { runRift :: forall r. g (a -> r) -> h r }
-
-instance Functor g => Functor (Rift g h) where
-  fmap f (Rift g) = Rift (g . fmap (.f))
-  {-# INLINE fmap #-}
-
-instance (Functor g, g ~ h) => Pointed (Rift g h) where
-  point a = Rift (fmap ($a))
-  {-# INLINE point #-}
-
-instance (Functor g, g ~ h) => Applicative (Rift g h) where
-  pure a = Rift (fmap ($a))
-  {-# INLINE pure #-}
-  Rift mf <*> Rift ma = Rift (ma . mf . fmap (.))
-  {-# INLINE (<*>) #-}
-
--- | Indexed applicative composition of right Kan lifts.
-rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b
-rap (Rift mf) (Rift ma) = Rift (ma . mf . fmap (.))
-{-# INLINE rap #-}
-
-grift :: Adjunction f u => f (Rift f k a) -> k a
-grift = rightAdjunct (\r -> leftAdjunct (runRift r) id)
-{-# INLINE grift #-}
-
--- | The universal property of 'Rift'
-toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a
-toRift h z = Rift $ \g -> h $ fmap (<$> z) g
-{-# INLINE toRift #-}
-
--- |
--- When @f -| u@, then @f -| Rift f Identity@ and
---
--- @
--- 'toRift' . 'fromRift' ≡ 'id'
--- 'fromRift' . 'toRift' ≡ 'id'
--- @
-fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b
-fromRift f = grift . fmap f
-{-# INLINE fromRift #-}
-
--- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
---
--- @
--- 'adjointToRift' . 'riftToAdjoint' ≡ 'id'
--- 'riftToAdjoint' . 'adjointToRift' ≡ 'id'
--- @
-adjointToRift :: Adjunction f u => u a -> Rift f Identity a
-adjointToRift ua = Rift (Identity . rightAdjunct (<$> ua))
-{-# INLINE adjointToRift #-}
-
--- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.
-riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a
-riftToAdjoint (Rift m) = leftAdjunct (runIdentity . m) id
-{-# INLINE riftToAdjoint #-}
-
--- |
---
--- @
--- 'composeRift' . 'decomposeRift' ≡ 'id'
--- 'decomposeRift' . 'composeRift' ≡ 'id'
--- @
-composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a
-composeRift (Rift f) = Rift (grift . fmap f . decompose)
-{-# INLINE composeRift #-}
-
-decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a
-decomposeRift (Rift f) = Rift $ \far -> Rift (f . compose . fmap (\rs -> fmap (rs.) far))
-{-# INLINE decomposeRift #-}
-
-
--- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
---
--- @
--- 'riftToComposedAdjoint' . 'composedAdjointToRift' ≡ 'id'
--- 'composedAdjointToRift' . 'riftToComposedAdjoint' ≡ 'id'
--- @
-
-riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)
-riftToComposedAdjoint (Rift m) = leftAdjunct m id
-{-# INLINE riftToComposedAdjoint #-}
-
--- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.
-composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a
-composedAdjointToRift uha = Rift $ rightAdjunct (\b -> fmap b <$> uha)
-{-# INLINE composedAdjointToRift #-}
-
diff --git a/src/Data/Functor/Yoneda.hs b/src/Data/Functor/Yoneda.hs
--- a/src/Data/Functor/Yoneda.hs
+++ b/src/Data/Functor/Yoneda.hs
@@ -1,18 +1,15 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Trustworthy #-}
-#endif
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Functor.Yoneda
--- Copyright   :  (C) 2011-2013 Edward Kmett
+-- Copyright   :  (C) 2011-2016 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -33,8 +30,6 @@
   , maxF, minF, maxM, minM
   -- * as a right Kan extension
   , yonedaToRan, ranToYoneda
-  -- * as a right Kan lift
-  , yonedaToRift, riftToYoneda
   ) where
 
 import Control.Applicative
@@ -46,13 +41,12 @@
 import Control.Comonad.Trans.Class
 import Data.Distributive
 import Data.Foldable
-import Data.Function (on)
 import Data.Functor.Adjunction
 import Data.Functor.Bind
+import Data.Functor.Classes
 import Data.Functor.Extend
 import Data.Functor.Identity
 import Data.Functor.Kan.Ran
-import Data.Functor.Kan.Rift
 import Data.Functor.Plus
 import Data.Functor.Rep
 import Data.Semigroup.Foldable
@@ -85,12 +79,15 @@
 -- @
 liftYoneda :: Functor f => f a -> Yoneda f a
 liftYoneda a = Yoneda (\f -> fmap f a)
+{-# INLINE liftYoneda #-}
 
 lowerYoneda :: Yoneda f a -> f a
 lowerYoneda (Yoneda f) = f id
+{-# INLINE lowerYoneda #-}
 
-{-# RULES "lower/lift=id" liftYoneda . lowerYoneda = id #-}
-{-# RULES "lift/lower=id" lowerYoneda . liftYoneda = id #-}
+-- TODO: coerce
+-- {-# RULES "lower/lift=id" liftYoneda . lowerYoneda = id #-}
+-- {-# RULES "lift/lower=id" lowerYoneda . liftYoneda = id #-}
 
 -- | @Yoneda f@ can be viewed as the right Kan extension of @f@ along the 'Identity' functor.
 --
@@ -100,83 +97,103 @@
 -- @
 yonedaToRan :: Yoneda f a -> Ran Identity f a
 yonedaToRan (Yoneda m) = Ran (m . fmap runIdentity)
+{-# INLINE yonedaToRan #-}
 
 ranToYoneda :: Ran Identity f a -> Yoneda f a
 ranToYoneda (Ran m) = Yoneda (m . fmap Identity)
-
-{-# RULES "yonedaToRan/ranToYoneda=id" yonedaToRan . ranToYoneda = id #-}
-{-# RULES "ranToYoneda/yonedaToRan=id" ranToYoneda . yonedaToRan = id #-}
-
--- | @Yoneda f@ can be viewed as the right Kan lift of @f@ along the 'Identity' functor.
---
--- @
--- 'yonedaToRift' . 'riftToYoneda' ≡ 'id'
--- 'riftToYoneda' . 'yonedaToRift' ≡ 'id'
--- @
-yonedaToRift :: Yoneda f a -> Rift Identity f a
-yonedaToRift m = Rift (runYoneda m . runIdentity)
-{-# INLINE yonedaToRift #-}
-
-riftToYoneda :: Rift Identity f a -> Yoneda f a
-riftToYoneda m = Yoneda (runRift m . Identity)
-{-# INLINE riftToYoneda #-}
+{-# INLINE ranToYoneda #-}
 
-{-# RULES "yonedaToRift/riftToYoneda=id" yonedaToRift . riftToYoneda = id #-}
-{-# RULES "riftToYoneda/yonedaToRift=id" riftToYoneda . yonedaToRift = id #-}
+-- {-# RULES "yonedaToRan/ranToYoneda=id" yonedaToRan . ranToYoneda = id #-}
+-- {-# RULES "ranToYoneda/yonedaToRan=id" ranToYoneda . yonedaToRan = id #-}
 
 instance Functor (Yoneda f) where
   fmap f m = Yoneda (\k -> runYoneda m (k . f))
+  {-# INLINE fmap #-}
 
 instance Apply f => Apply (Yoneda f) where
   Yoneda m <.> Yoneda n = Yoneda (\f -> m (f .) <.> n id)
+  {-# INLINE (<.>) #-}
+  Yoneda m .> Yoneda n = Yoneda (\f -> m id .> n f)
+  {-# INLINE (.>) #-}
 
 instance Applicative f => Applicative (Yoneda f) where
   pure a = Yoneda (\f -> pure (f a))
+  {-# INLINE pure #-}
   Yoneda m <*> Yoneda n = Yoneda (\f -> m (f .) <*> n id)
+  {-# INLINE (<*>) #-}
+  Yoneda m *> Yoneda n = Yoneda (\f -> m id *> n f)
+  {-# INLINE (*>) #-}
 
 instance Foldable f => Foldable (Yoneda f) where
   foldMap f = foldMap f . lowerYoneda
+  {-# INLINE foldMap #-}
 
 instance Foldable1 f => Foldable1 (Yoneda f) where
   foldMap1 f = foldMap1 f . lowerYoneda
+  {-# INLINE foldMap1 #-}
 
 instance Traversable f => Traversable (Yoneda f) where
   traverse f = fmap liftYoneda . traverse f . lowerYoneda
+  {-# INLINE traverse #-}
 
 instance Traversable1 f => Traversable1 (Yoneda f) where
   traverse1 f = fmap liftYoneda . traverse1 f . lowerYoneda
+  {-# INLINE traverse1 #-}
 
 instance Distributive f => Distributive (Yoneda f) where
   collect f = liftYoneda . collect (lowerYoneda . f)
+  {-# INLINE collect #-}
 
 instance Representable g => Representable (Yoneda g) where
   type Rep (Yoneda g) = Rep g
   tabulate = liftYoneda . tabulate
+  {-# INLINE tabulate #-}
   index = index . lowerYoneda
+  {-# INLINE index #-}
 
 instance Adjunction f g => Adjunction (Yoneda f) (Yoneda g) where
   unit = liftYoneda . fmap liftYoneda . unit
+  {-# INLINE unit #-}
   counit (Yoneda m) = counit (m lowerYoneda)
+  {-# INLINE counit #-}
 
--- instance Show1 f => Show1 (Yoneda f) where
+instance Show1 f => Show1 (Yoneda f) where
+  liftShowsPrec sp sl d (Yoneda f) =
+    showsUnaryWith (liftShowsPrec sp sl) "liftYoneda" d (f id)
+
+instance (Read1 f, Functor f) => Read1 (Yoneda f) where
+  liftReadsPrec rp rl = readsData $
+    readsUnaryWith (liftReadsPrec rp rl) "liftYoneda" liftYoneda
+
 instance Show (f a) => Show (Yoneda f a) where
   showsPrec d (Yoneda f) = showParen (d > 10) $
     showString "liftYoneda " . showsPrec 11 (f id)
 
--- instance Read1 f => Read1 (Yoneda f) where
-#ifdef __GLASGOW_HASKELL__
 instance (Functor f, Read (f a)) => Read (Yoneda f a) where
   readPrec = parens $ prec 10 $ do
      Ident "liftYoneda" <- lexP
      liftYoneda <$> step readPrec
-#endif
 
-instance Eq (f a) => Eq (Yoneda f a) where
-  (==) = (==) `on` lowerYoneda
+infixl 0 `on1`
+on1 :: (g a -> g b -> c) -> (forall x. f x -> g x) -> f a -> f b -> c
+(.*.) `on1` f = \x y -> f x .*. f y
 
-instance Ord (f a) => Ord (Yoneda f a) where
-  compare = compare `on` lowerYoneda
+instance Eq1 f => Eq1 (Yoneda f) where
+  liftEq eq = liftEq eq `on1` lowerYoneda
+  {-# INLINE liftEq #-}
 
+instance Ord1 f => Ord1 (Yoneda f) where
+  liftCompare cmp = liftCompare cmp `on1` lowerYoneda
+  {-# INLINE liftCompare #-}
+
+instance (Eq1 f, Eq a) => Eq (Yoneda f a) where
+  (==) = eq1
+  {-# INLINE (==) #-}
+
+instance (Ord1 f, Ord a) => Ord (Yoneda f a) where
+  compare = compare1
+  {-# INLINE compare #-}
+
 maxF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f a
 Yoneda f `maxF` Yoneda g = liftYoneda $ f id `max` g id
 -- {-# RULES "max/maxF" max = maxF #-}
@@ -199,40 +216,54 @@
 
 instance Alt f => Alt (Yoneda f) where
   Yoneda f <!> Yoneda g = Yoneda (\k -> f k <!> g k)
+  {-# INLINE (<!>) #-}
 
 instance Plus f => Plus (Yoneda f) where
   zero = Yoneda $ const zero
+  {-# INLINE zero #-}
 
 instance Alternative f => Alternative (Yoneda f) where
   empty = Yoneda $ const empty
+  {-# INLINE empty #-}
   Yoneda f <|> Yoneda g = Yoneda (\k -> f k <|> g k)
+  {-# INLINE (<|>) #-}
 
 instance Bind m => Bind (Yoneda m) where
   Yoneda m >>- k = Yoneda (\f -> m id >>- \a -> runYoneda (k a) f)
+  {-# INLINE (>>-) #-}
 
 instance Monad m => Monad (Yoneda m) where
-  return a = Yoneda (\f -> return (f a))
   Yoneda m >>= k = Yoneda (\f -> m id >>= \a -> runYoneda (k a) f)
+  {-# INLINE (>>=) #-}
 
 instance MonadFix m => MonadFix (Yoneda m) where
   mfix f = lift $ mfix (lowerYoneda . f)
+  {-# INLINE mfix #-}
 
 instance MonadPlus m => MonadPlus (Yoneda m) where
   mzero = Yoneda (const mzero)
+  {-# INLINE mzero #-}
   Yoneda f `mplus` Yoneda g = Yoneda (\k -> f k `mplus` g k)
+  {-# INLINE mplus #-}
 
 instance MonadTrans Yoneda where
   lift a = Yoneda (\f -> liftM f a)
+  {-# INLINE lift #-}
 
 instance (Functor f, MonadFree f m) => MonadFree f (Yoneda m) where
   wrap = lift . wrap . fmap lowerYoneda
+  {-# INLINE wrap #-}
 
 instance Extend w => Extend (Yoneda w) where
   extended k (Yoneda m) = Yoneda (\f -> extended (f . k . liftYoneda) (m id))
+  {-# INLINE extended #-}
 
 instance Comonad w => Comonad (Yoneda w) where
   extend k (Yoneda m) = Yoneda (\f -> extend (f . k . liftYoneda) (m id))
+  {-# INLINE extend #-}
   extract = extract . lowerYoneda
+  {-# INLINE extract #-}
 
 instance ComonadTrans Yoneda where
   lower = lowerYoneda
+  {-# INLINE lower #-}