{-# LANGUAGE Rank2Types
           , MultiParamTypeClasses
           , FunctionalDependencies
           , TypeOperators
           , UndecidableInstances #-}

{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE EmptyCase #-}
#endif

-------------------------------------------------------------------------------------------
-- |
-- Copyright 	: 2008-2013 Edward Kmett
-- License	: BSD
--
-- Maintainer	: Edward Kmett <[email protected]>
-- Stability	: experimental
-- Portability	: rank 2 types, MPTCs, fundeps
--
-------------------------------------------------------------------------------------------
module Data.Functor.Adjunction
  ( Adjunction(..)
  , adjuncted
  , tabulateAdjunction
  , indexAdjunction
  , zapWithAdjunction
  , zipR, unzipR
  , unabsurdL, absurdL
  , cozipL, uncozipL
  , extractL, duplicateL
  , splitL, unsplitL
  ) where

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Control.Arrow ((&&&), (|||))
import Control.Monad.Free
#if __GLASGOW_HASKELL__ < 707
import Control.Monad.Instances ()
#endif
import Control.Monad.Trans.Identity
import Control.Monad.Trans.Reader
import Control.Monad.Trans.Writer
import Control.Comonad
import Control.Comonad.Cofree
import Control.Comonad.Trans.Env
import Control.Comonad.Trans.Traced

import Data.Functor.Identity
import Data.Functor.Compose
import Data.Functor.Product
import Data.Functor.Rep
import Data.Functor.Sum
import Data.Profunctor
import Data.Void
import GHC.Generics

-- | An adjunction between Hask and Hask.
--
-- Minimal definition: both 'unit' and 'counit' or both 'leftAdjunct'
-- and 'rightAdjunct', subject to the constraints imposed by the
-- default definitions that the following laws should hold.
--
-- > unit = leftAdjunct id
-- > counit = rightAdjunct id
-- > leftAdjunct f = fmap f . unit
-- > rightAdjunct f = counit . fmap f
--
-- Any implementation is required to ensure that 'leftAdjunct' and
-- 'rightAdjunct' witness an isomorphism from @Nat (f a, b)@ to
-- @Nat (a, g b)@
--
-- > rightAdjunct unit = id
-- > leftAdjunct counit = id
class (Functor f, Representable u) =>
      Adjunction f u | f -> u, u -> f where
#if __GLASGOW_HASKELL__ >= 708
  {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
#endif
  unit         :: a -> u (f a)
  counit       :: f (u a) -> a
  leftAdjunct  :: (f a -> b) -> a -> u b
  rightAdjunct :: (a -> u b) -> f a -> b

  unit           = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall a. a -> a
id
  counit         = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall a. a -> a
id
  leftAdjunct f a -> b
f  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
unit
  rightAdjunct a -> u b
f = forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f (u a) -> a
counit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> u b
f

-- | 'leftAdjunct' and 'rightAdjunct' form two halves of an isomorphism.
--
-- This can be used with the combinators from the @lens@ package.
--
-- @'adjuncted' :: 'Adjunction' f u => 'Iso'' (f a -> b) (a -> u b)@
adjuncted :: (Adjunction f u, Profunctor p, Functor g)
          => p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d))
adjuncted :: forall (f :: * -> *) (u :: * -> *) (p :: * -> * -> *) (g :: * -> *)
       a b c d.
(Adjunction f u, Profunctor p, Functor g) =>
p (a -> u b) (g (c -> u d)) -> p (f a -> b) (g (f c -> d))
adjuncted = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct)
{-# INLINE adjuncted #-}

-- | Every right adjoint is representable by its left adjoint
-- applied to a unit element
--
-- Use this definition and the primitives in
-- Data.Functor.Representable to meet the requirements of the
-- superclasses of Representable.
tabulateAdjunction :: Adjunction f u => (f () -> b) -> u b
tabulateAdjunction :: forall (f :: * -> *) (u :: * -> *) b.
Adjunction f u =>
(f () -> b) -> u b
tabulateAdjunction f () -> b
f = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct f () -> b
f ()

-- | This definition admits a default definition for the
-- 'index' method of 'Index", one of the superclasses of
-- Representable.
indexAdjunction :: Adjunction f u => u b -> f a -> b
indexAdjunction :: forall (f :: * -> *) (u :: * -> *) b a.
Adjunction f u =>
u b -> f a -> b
indexAdjunction = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const

zapWithAdjunction :: Adjunction f u => (a -> b -> c) -> u a -> f b -> c
zapWithAdjunction :: forall (f :: * -> *) (u :: * -> *) a b c.
Adjunction f u =>
(a -> b -> c) -> u a -> f b -> c
zapWithAdjunction a -> b -> c
f u a
ua = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\b
b -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> b -> c
f b
b) u a
ua)

splitL :: Adjunction f u => f a -> (a, f ())
splitL :: forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f a -> (a, f ())
splitL = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct () forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,))

unsplitL :: Functor f => a -> f () -> f a
unsplitL :: forall (f :: * -> *) a. Functor f => a -> f () -> f a
unsplitL = forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$)

extractL :: Adjunction f u => f a -> a
extractL :: forall (f :: * -> *) (u :: * -> *) a. Adjunction f u => f a -> a
extractL = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f a -> (a, f ())
splitL

duplicateL :: Adjunction f u => f a -> f (f a)
duplicateL :: forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f a -> f (f a)
duplicateL f a
as = f a
as forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f a
as

-- | A right adjoint functor admits an intrinsic
-- notion of zipping
zipR :: Adjunction f u => (u a, u b) -> u (a, b)
zipR :: forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(u a, u b) -> u (a, b)
zipR = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall a b. (a, b) -> b
snd)

-- | Every functor in Haskell permits unzipping
unzipR :: Functor u => u (a, b) -> (u a, u b)
unzipR :: forall (u :: * -> *) a b. Functor u => u (a, b) -> (u a, u b)
unzipR = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd

absurdL :: Void -> f Void
absurdL :: forall (f :: * -> *). Void -> f Void
absurdL = forall a. Void -> a
absurd

-- | A left adjoint must be inhabited, or we can derive bottom.
unabsurdL :: Adjunction f u => f Void -> Void
unabsurdL :: forall (f :: * -> *) (u :: * -> *).
Adjunction f u =>
f Void -> Void
unabsurdL = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall a. Void -> a
absurd

-- | And a left adjoint must be inhabited by exactly one element
cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
cozipL :: forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
f (Either a b) -> Either (f a) (f b)
cozipL = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall a b. a -> Either a b
Left forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall a b. b -> Either a b
Right)

-- | Every functor in Haskell permits 'uncozipping'
uncozipL :: Functor f => Either (f a) (f b) -> f (Either a b)
uncozipL :: forall (f :: * -> *) a b.
Functor f =>
Either (f a) (f b) -> f (Either a b)
uncozipL = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right

-- Requires deprecated Impredicative types
-- limitR :: Adjunction f u => (forall a. u a) -> u (forall a. a)
-- limitR = leftAdjunct (rightAdjunct (\(x :: forall a. a) -> x))

instance Adjunction ((,) e) ((->) e) where
  leftAdjunct :: forall a b. ((e, a) -> b) -> a -> e -> b
leftAdjunct (e, a) -> b
f a
a e
e      = (e, a) -> b
f (e
e, a
a)
  rightAdjunct :: forall a b. (a -> e -> b) -> (e, a) -> b
rightAdjunct a -> e -> b
f ~(e
e, a
a) = a -> e -> b
f a
a e
e

instance Adjunction Identity Identity where
  leftAdjunct :: forall a b. (Identity a -> b) -> a -> Identity b
leftAdjunct Identity a -> b
f  = forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity
  rightAdjunct :: forall a b. (a -> Identity b) -> Identity a -> b
rightAdjunct a -> Identity b
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity

instance Adjunction f g =>
         Adjunction (IdentityT f) (IdentityT g) where
  unit :: forall a. a -> IdentityT g (IdentityT f a)
unit   = forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT
  counit :: forall a. IdentityT f (IdentityT g a) -> a
counit = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT

instance Adjunction w m =>
         Adjunction (EnvT e w) (ReaderT e m) where
  unit :: forall a. a -> ReaderT e m (EnvT e w a)
unit              = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e (w :: * -> *) a. e -> w a -> EnvT e w a
EnvT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct
  counit :: forall a. EnvT e w (ReaderT e m a) -> a
counit (EnvT e
e w (ReaderT e m a)
w) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT e
e) w (ReaderT e m a)
w

instance Adjunction m w =>
         Adjunction (WriterT s m) (TracedT s w) where
  unit :: forall a. a -> TracedT s w (WriterT s m a)
unit   = forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
TracedT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (\m a
ma s
s -> forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
a -> (a
a, s
s)) m a
ma))
  counit :: forall a. WriterT s m (TracedT s w a) -> a
counit = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(TracedT s w a
t, s
s) -> (forall a b. (a -> b) -> a -> b
$ s
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall m (w :: * -> *) a. TracedT m w a -> w (m -> a)
runTracedT TracedT s w a
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT

instance (Adjunction f g, Adjunction f' g') =>
         Adjunction (Compose f' f) (Compose g g') where
  unit :: forall a. a -> Compose g g' (Compose f' f a)
unit   = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)
  counit :: forall a. Compose f' f (Compose g g' a) -> a
counit = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

instance (Adjunction f g, Adjunction f' g') =>
         Adjunction (Sum f f') (Product g g') where
  unit :: forall a. a -> Product g g' (Sum f f' a)
unit a
a = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL a
a) (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR a
a)
  counit :: forall a. Sum f f' (Product g g' a) -> a
counit (InL f (Product g g' a)
l) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(Pair g a
x g' a
_) -> g a
x) f (Product g g' a)
l
  counit (InR f' (Product g g' a)
r) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(Pair g a
_ g' a
x) -> g' a
x) f' (Product g g' a)
r

instance Adjunction f u =>
         Adjunction (Free f) (Cofree u) where
  unit :: forall a. a -> Cofree u (Free f a)
unit a
a = forall (m :: * -> *) a. Monad m => a -> m a
return a
a forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall (f :: * -> *) (u :: * -> *) b.
Adjunction f u =>
(f () -> b) -> u b
tabulateAdjunction (\f ()
k -> forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (forall (f :: * -> *) (m :: * -> *) a.
MonadFree f m =>
f (m a) -> m a
wrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a. Functor f => a -> f () -> f a
unsplitL f ()
k) a
a)
  counit :: forall a. Free f (Cofree u a) -> a
counit (Pure Cofree u a
a) = forall (w :: * -> *) a. Comonad w => w a -> a
extract Cofree u a
a
  counit (Free f (Free f (Cofree u a))
k) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) (u :: * -> *) b a.
Adjunction f u =>
u b -> f a -> b
indexAdjunction f (Free f (Cofree u a))
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (w :: * -> *) a.
ComonadCofree f w =>
w a -> f (w a)
unwrap) (forall (f :: * -> *) (u :: * -> *) a. Adjunction f u => f a -> a
extractL f (Free f (Cofree u a))
k)

instance Adjunction V1 U1 where
  unit :: forall a. a -> U1 (V1 a)
unit a
_ = forall k (p :: k). U1 p
U1
  counit :: forall a. V1 (U1 a) -> a
counit = forall a b. V1 a -> b
absurdV1

absurdV1 :: V1 a -> b
#if __GLASGOW_HASKELL__ >= 708
absurdV1 :: forall a b. V1 a -> b
absurdV1 V1 a
x = case V1 a
x of {}
#else
absurdV1 x = x `seq` undefined
#endif

instance Adjunction Par1 Par1 where
  leftAdjunct :: forall a b. (Par1 a -> b) -> a -> Par1 b
leftAdjunct Par1 a -> b
f = forall p. p -> Par1 p
Par1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. p -> Par1 p
Par1
  rightAdjunct :: forall a b. (a -> Par1 b) -> Par1 a -> b
rightAdjunct a -> Par1 b
f = forall p. Par1 p -> p
unPar1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Par1 b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. Par1 p -> p
unPar1

instance Adjunction f g => Adjunction (Rec1 f) (Rec1 g) where
  unit :: forall a. a -> Rec1 g (Rec1 f a)
unit   = forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1
  counit :: forall a. Rec1 f (Rec1 g a) -> a
counit = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1

-- @i@ and @c@ indexes have to be the same due functional dependency.
-- But we want them to be different, therefore we rather not define this instance
{-
instance Adjunction f g => Adjunction (M1 i c f) (M1 i c g) where
  unit   = M1 . leftAdjunct M1
  counit = rightAdjunct unM1 . unM1
-}

instance (Adjunction f g, Adjunction f' g') => Adjunction (f' :.: f) (g :.: g') where
  unit :: forall a. a -> (:.:) g g' ((:.:) f' f a)
unit   = forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1)
  counit :: forall a. (:.:) f' f ((:.:) g g' a) -> a
counit = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1

instance (Adjunction f g, Adjunction f' g') => Adjunction (f :+: f') (g :*: g') where
  unit :: forall a. a -> (:*:) g g' ((:+:) f f' a)
unit a
a = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 a
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(f a -> b) -> a -> u b
leftAdjunct forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 a
a
  counit :: forall a. (:+:) f f' ((:*:) g g' a) -> a
counit (L1 f ((:*:) g g' a)
l) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(g a
x :*: g' a
_) -> g a
x) f ((:*:) g g' a)
l
  counit (R1 f' ((:*:) g g' a)
r) = forall (f :: * -> *) (u :: * -> *) a b.
Adjunction f u =>
(a -> u b) -> f a -> b
rightAdjunct (\(g a
_ :*: g' a
x) -> g' a
x) f' ((:*:) g g' a)
r