{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE BlockArguments #-}
module FFunctor.Adjunction (Adjunction(..)) where


import Data.Coerce ( coerce, Coercible )
import Data.Kind (Constraint)

import Control.Monad.Trans.Identity
import Data.Functor.Day
import Data.Functor.Day.Curried

import Data.Functor.Kan.Lan
import Data.Functor.Kan.Ran
import Data.Functor.Precompose (Precompose(..))
import Data.Functor.Compose (Compose(..))

import qualified Data.Bifunctor.Sum as Bi
import qualified Data.Bifunctor.Product as Bi
import qualified Data.Bifunctor.Product.Extra as Bi

import qualified Data.Functor.Adjunction as Rank1
import qualified Control.Monad.Trans.Reader as Rank1
import qualified Control.Monad.Trans.Writer as Rank1
import qualified Control.Monad.Trans.State.Lazy as Rank1
import qualified Control.Comonad.Trans.Env as Rank1
import qualified Control.Comonad.Trans.Traced as Rank1
import qualified Control.Comonad.Trans.Store as Rank1

import FFunctor
import FFunctor.FCompose ( FCompose(..) )
import Data.Functor.Exp
import GHC.Generics ((:*:))

-- | An adjunction between \(\mathrm{Hask}^{\mathrm{Hask}}\) and \(\mathrm{Hask}^{\mathrm{Hask}}\).
type Adjunction :: FF -> FF -> Constraint
class (FFunctor ff, FFunctor uu) => Adjunction ff uu | ff -> uu, uu -> ff where
    {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}
    unit :: forall g. Functor g => g ~> uu (ff g)
    unit = (ff g ~> ff g) -> g ~> uu (ff g)
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
leftAdjunct ff g x -> ff g x
forall a. a -> a
ff g ~> ff g
id
    counit :: forall g. Functor g => ff (uu g) ~> g
    counit = (uu g ~> uu g) -> ff (uu g) ~> g
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
rightAdjunct uu g x -> uu g x
forall a. a -> a
uu g ~> uu g
id

    leftAdjunct :: forall g h. (Functor g, Functor h) => (ff g ~> h) -> (g ~> uu h)
    leftAdjunct ff g ~> h
ffg_h = (ff g ~> h) -> uu (ff g) x -> uu h x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ff g x -> h x
ff g ~> h
ffg_h (uu (ff g) x -> uu h x) -> (g x -> uu (ff g) x) -> g x -> uu h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> uu (ff g) x
g ~> uu (ff g)
forall (g :: * -> *). Functor g => g ~> uu (ff g)
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit
    rightAdjunct :: forall g h. (Functor g, Functor h) => (g ~> uu h) -> (ff g ~> h)
    rightAdjunct g ~> uu h
g_uuh = ff (uu h) x -> h x
ff (uu h) ~> h
forall (g :: * -> *). Functor g => ff (uu g) ~> g
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit (ff (uu h) x -> h x) -> (ff g x -> ff (uu h) x) -> ff g x -> h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g ~> uu h) -> ff g x -> ff (uu h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap g x -> uu h x
g ~> uu h
g_uuh

natCoerce :: forall f' f g g'. (Coercible f' f, Coercible g g') => (f ~> g) -> (f' ~> g')
natCoerce :: forall {k} (f' :: k -> *) (f :: k -> *) (g :: k -> *)
       (g' :: k -> *).
(Coercible f' f, Coercible g g') =>
(f ~> g) -> f' ~> g'
natCoerce f ~> g
fg =
    let f'g' :: forall x. f' x -> g' x
        f'g' :: forall (x :: k). f' x -> g' x
f'g' = (f x -> g x) -> f' x -> g' x
forall a b. Coercible a b => a -> b
coerce (f ~> g
fg @x)
    in f' x -> g' x
forall (x :: k). f' x -> g' x
f'g'

instance Adjunction IdentityT IdentityT where
    unit :: forall (g :: * -> *). Functor g => g ~> IdentityT (IdentityT g)
unit = g x -> IdentityT (IdentityT g) x
forall a b. Coercible a b => a -> b
coerce
    counit :: forall (g :: * -> *). Functor g => IdentityT (IdentityT g) ~> g
counit = IdentityT (IdentityT g) x -> g x
forall a b. Coercible a b => a -> b
coerce
    leftAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(IdentityT g ~> h) -> g ~> IdentityT h
leftAdjunct = (IdentityT g ~> h) -> g x -> IdentityT h x
(IdentityT g ~> h) -> g ~> IdentityT h
forall {k} (f' :: k -> *) (f :: k -> *) (g :: k -> *)
       (g' :: k -> *).
(Coercible f' f, Coercible g g') =>
(f ~> g) -> f' ~> g'
natCoerce 
    rightAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> IdentityT h) -> IdentityT g ~> h
rightAdjunct = (g ~> IdentityT h) -> IdentityT g x -> h x
(g ~> IdentityT h) -> IdentityT g ~> h
forall {k} (f' :: k -> *) (f :: k -> *) (g :: k -> *)
       (g' :: k -> *).
(Coercible f' f, Coercible g g') =>
(f ~> g) -> f' ~> g'
natCoerce

instance Functor f => Adjunction (Day f) (Curried f) where
    unit :: forall (g :: * -> *). Functor g => g ~> Curried f (Day f g)
unit = g x -> Curried f (Day f g) x
forall (g :: * -> *) a (f :: * -> *). g a -> Curried f (Day f g) a
unapplied
    counit :: forall (g :: * -> *). Functor g => Day f (Curried f g) ~> g
counit = Day f (Curried f g) x -> g x
forall (f :: * -> *) (g :: * -> *) a.
Functor f =>
Day f (Curried f g) a -> g a
applied

    leftAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(Day f g ~> h) -> g ~> Curried f h
leftAdjunct = (forall x. Day f g x -> h x) -> g x -> Curried f h x
forall (g :: * -> *) (k :: * -> *) (h :: * -> *) a.
(forall x. Day g k x -> h x) -> k a -> Curried g h a
toCurried
    rightAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> Curried f h) -> Day f g ~> h
rightAdjunct = (forall a. g a -> Curried f h a) -> Day f g x -> h x
forall (f :: * -> *) (k :: * -> *) (h :: * -> *) b.
Functor f =>
(forall a. k a -> Curried f h a) -> Day f k b -> h b
fromCurried

instance Functor f => Adjunction (Lan f) (Precompose f) where
    unit :: (Functor g) => g ~> Precompose f (Lan f g)
    unit :: forall (g :: * -> *). Functor g => g ~> Precompose f (Lan f g)
unit g x
g = Lan f g (f x) -> Precompose f (Lan f g) x
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
g (f a) -> Precompose f g a
Precompose (Lan f g (f x) -> Precompose f (Lan f g) x)
-> Lan f g (f x) -> Precompose f (Lan f g) x
forall a b. (a -> b) -> a -> b
$ (f x -> f x) -> g x -> Lan f g (f x)
forall {k} (g :: k -> *) (b :: k) a (h :: k -> *).
(g b -> a) -> h b -> Lan g h a
Lan f x -> f x
forall a. a -> a
id g x
g
    counit :: (Functor g) => Lan f (Precompose f g) ~> g
    counit :: forall (g :: * -> *). Functor g => Lan f (Precompose f g) ~> g
counit (Lan f b -> x
unF (Precompose g (f b)
gf)) = (f b -> x) -> g (f b) -> g x
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f b -> x
unF g (f b)
gf

instance Functor f => Adjunction (Precompose f) (Ran f) where
    unit :: (Functor g) => g ~> Ran f (Precompose f g)
    -- g ~> Ran f (g :.: f)
    -- ∀x. g x -> (∀y. (x -> f y) -> g (f y))
    unit :: forall (g :: * -> *). Functor g => g ~> Ran f (Precompose f g)
unit g x
g = (forall b. (x -> f b) -> Precompose f g b)
-> Ran f (Precompose f g) x
forall {k} (g :: k -> *) (h :: k -> *) a.
(forall (b :: k). (a -> g b) -> h b) -> Ran g h a
Ran ((forall b. (x -> f b) -> Precompose f g b)
 -> Ran f (Precompose f g) x)
-> (forall b. (x -> f b) -> Precompose f g b)
-> Ran f (Precompose f g) x
forall a b. (a -> b) -> a -> b
$ \x -> f b
toF -> g (f b) -> Precompose f g b
forall j k (f :: j -> k) (g :: k -> *) (a :: j).
g (f a) -> Precompose f g a
Precompose ((x -> f b) -> g x -> g (f b)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> f b
toF g x
g)

    counit :: (Functor g) => Precompose f (Ran f g) ~> g
    -- Ran f g :.: f ~> g
    -- ∀x. (∀y. (f x -> f y) -> g y) -> g x
    counit :: forall (g :: * -> *). Functor g => Precompose f (Ran f g) ~> g
counit (Precompose Ran f g (f x)
ffg) = Ran f g (f x) -> forall b. (f x -> f b) -> g b
forall {k} (g :: k -> *) (h :: k -> *) a.
Ran g h a -> forall (b :: k). (a -> g b) -> h b
runRan Ran f g (f x)
ffg f x -> f x
forall a. a -> a
id

instance (Adjunction ff uu, Adjunction gg vv) => Adjunction (FCompose ff gg) (FCompose vv uu) where
    unit :: Functor h => h ~> FCompose vv uu (FCompose ff gg h)
    unit :: forall (g :: * -> *).
Functor g =>
g ~> FCompose vv uu (FCompose ff gg g)
unit = (ff (gg h) ~> FCompose ff gg h)
-> FCompose vv uu (ff (gg h)) x
-> FCompose vv uu (FCompose ff gg h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> FCompose vv uu g x -> FCompose vv uu h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ff (gg h) x -> FCompose ff gg h x
ff (gg h) ~> FCompose ff gg h
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
ff (gg h) x -> FCompose ff gg h x
FCompose (FCompose vv uu (ff (gg h)) x
 -> FCompose vv uu (FCompose ff gg h) x)
-> (h x -> FCompose vv uu (ff (gg h)) x)
-> h x
-> FCompose vv uu (FCompose ff gg h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. vv (uu (ff (gg h))) x -> FCompose vv uu (ff (gg h)) x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
ff (gg h) x -> FCompose ff gg h x
FCompose (vv (uu (ff (gg h))) x -> FCompose vv uu (ff (gg h)) x)
-> (h x -> vv (uu (ff (gg h))) x)
-> h x
-> FCompose vv uu (ff (gg h)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (gg h ~> uu (ff (gg h))) -> vv (gg h) x -> vv (uu (ff (gg h))) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> vv g x -> vv h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap gg h x -> uu (ff (gg h)) x
gg h ~> uu (ff (gg h))
forall (g :: * -> *). Functor g => g ~> uu (ff g)
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit (vv (gg h) x -> vv (uu (ff (gg h))) x)
-> (h x -> vv (gg h) x) -> h x -> vv (uu (ff (gg h))) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h x -> vv (gg h) x
h ~> vv (gg h)
forall (g :: * -> *). Functor g => g ~> vv (gg g)
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit

    counit :: Functor h => FCompose ff gg (FCompose vv uu h) ~> h
    counit :: forall (g :: * -> *).
Functor g =>
FCompose ff gg (FCompose vv uu g) ~> g
counit = ff (uu h) x -> h x
ff (uu h) ~> h
forall (g :: * -> *). Functor g => ff (uu g) ~> g
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit (ff (uu h) x -> h x)
-> (FCompose ff gg (FCompose vv uu h) x -> ff (uu h) x)
-> FCompose ff gg (FCompose vv uu h) x
-> h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (gg (vv (uu h)) ~> uu h) -> ff (gg (vv (uu h))) x -> ff (uu h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap gg (vv (uu h)) x -> uu h x
gg (vv (uu h)) ~> uu h
forall (g :: * -> *). Functor g => gg (vv g) ~> g
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit (ff (gg (vv (uu h))) x -> ff (uu h) x)
-> (FCompose ff gg (FCompose vv uu h) x -> ff (gg (vv (uu h))) x)
-> FCompose ff gg (FCompose vv uu h) x
-> ff (uu h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FCompose ff gg (vv (uu h)) x -> ff (gg (vv (uu h))) x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
FCompose ff gg h x -> ff (gg h) x
getFCompose (FCompose ff gg (vv (uu h)) x -> ff (gg (vv (uu h))) x)
-> (FCompose ff gg (FCompose vv uu h) x
    -> FCompose ff gg (vv (uu h)) x)
-> FCompose ff gg (FCompose vv uu h) x
-> ff (gg (vv (uu h))) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FCompose vv uu h ~> vv (uu h))
-> FCompose ff gg (FCompose vv uu h) x
-> FCompose ff gg (vv (uu h)) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> FCompose ff gg g x -> FCompose ff gg h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap FCompose vv uu h x -> vv (uu h) x
FCompose vv uu h ~> vv (uu h)
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
FCompose ff gg h x -> ff (gg h) x
getFCompose

    leftAdjunct :: forall h k. (Functor h, Functor k)
      => (FCompose ff gg h ~> k) -> h ~> FCompose vv uu k
    leftAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(FCompose ff gg g ~> h) -> g ~> FCompose vv uu h
leftAdjunct FCompose ff gg h ~> k
lefty = vv (uu k) x -> FCompose vv uu k x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
ff (gg h) x -> FCompose ff gg h x
FCompose (vv (uu k) x -> FCompose vv uu k x)
-> (h x -> vv (uu k) x) -> h x -> FCompose vv uu k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (gg h ~> uu k) -> h ~> vv (uu k)
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(gg g ~> h) -> g ~> vv h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
leftAdjunct ((ff (gg h) ~> k) -> gg h ~> uu k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
leftAdjunct (FCompose ff gg h x -> k x
FCompose ff gg h ~> k
lefty (FCompose ff gg h x -> k x)
-> (ff (gg h) x -> FCompose ff gg h x) -> ff (gg h) x -> k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ff (gg h) x -> FCompose ff gg h x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
ff (gg h) x -> FCompose ff gg h x
FCompose))

    rightAdjunct :: (Functor h, Functor k)
      => (h ~> FCompose vv uu k) -> FCompose ff gg h ~> k
    rightAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> FCompose vv uu h) -> FCompose ff gg g ~> h
rightAdjunct h ~> FCompose vv uu k
righty = (gg h ~> uu k) -> ff (gg h) ~> k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
rightAdjunct ((h ~> vv (uu k)) -> gg h ~> uu k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> vv h) -> gg g ~> h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
rightAdjunct (FCompose vv uu k x -> vv (uu k) x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
FCompose ff gg h x -> ff (gg h) x
getFCompose (FCompose vv uu k x -> vv (uu k) x)
-> (h x -> FCompose vv uu k x) -> h x -> vv (uu k) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h x -> FCompose vv uu k x
h ~> FCompose vv uu k
righty)) (ff (gg h) x -> k x)
-> (FCompose ff gg h x -> ff (gg h) x) -> FCompose ff gg h x -> k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FCompose ff gg h x -> ff (gg h) x
forall (ff :: FF) (gg :: FF) (h :: * -> *) x.
FCompose ff gg h x -> ff (gg h) x
getFCompose

instance (Adjunction ff uu, Adjunction gg vv) => Adjunction (Bi.Sum ff gg) (Bi.Product uu vv) where
    unit :: (Functor h)
      => h ~> Bi.Product uu vv (Bi.Sum ff gg h)
    unit :: forall (g :: * -> *). Functor g => g ~> Product uu vv (Sum ff gg g)
unit h x
h = uu (Sum ff gg h) x
-> vv (Sum ff gg h) x -> Product uu vv (Sum ff gg h) x
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Bi.Pair ((ff h ~> Sum ff gg h) -> uu (ff h) x -> uu (Sum ff gg h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> uu g x -> uu h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap ff h x -> Sum ff gg h x
ff h ~> Sum ff gg h
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
Bi.L2 (h x -> uu (ff h) x
h ~> uu (ff h)
forall (g :: * -> *). Functor g => g ~> uu (ff g)
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit h x
h)) ((gg h ~> Sum ff gg h) -> vv (gg h) x -> vv (Sum ff gg h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> vv g x -> vv h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap gg h x -> Sum ff gg h x
gg h ~> Sum ff gg h
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
Bi.R2 (h x -> vv (gg h) x
h ~> vv (gg h)
forall (g :: * -> *). Functor g => g ~> vv (gg g)
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
g ~> uu (ff g)
unit h x
h))

    counit :: (Functor h)
      => Bi.Sum ff gg (Bi.Product uu vv h) ~> h
    counit :: forall (g :: * -> *). Functor g => Sum ff gg (Product uu vv g) ~> g
counit (Bi.L2 ff (Product uu vv h) x
ffP) = ff (uu h) x -> h x
ff (uu h) ~> h
forall (g :: * -> *). Functor g => ff (uu g) ~> g
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit ((Product uu vv h ~> uu h) -> ff (Product uu vv h) x -> ff (uu h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Product uu vv h x -> uu h x
Product uu vv h ~> uu h
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
Product p q a b -> p a b
Bi.proj1 ff (Product uu vv h) x
ffP)
    counit (Bi.R2 gg (Product uu vv h) x
ggP) = gg (vv h) x -> h x
gg (vv h) ~> h
forall (g :: * -> *). Functor g => gg (vv g) ~> g
forall (ff :: FF) (uu :: FF) (g :: * -> *).
(Adjunction ff uu, Functor g) =>
ff (uu g) ~> g
counit ((Product uu vv h ~> vv h) -> gg (Product uu vv h) x -> gg (vv h) x
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> gg g x -> gg h x
forall (ff :: FF) (g :: * -> *) (h :: * -> *) x.
(FFunctor ff, Functor g, Functor h) =>
(g ~> h) -> ff g x -> ff h x
ffmap Product uu vv h x -> vv h x
Product uu vv h ~> vv h
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
Product p q a b -> q a b
Bi.proj2 gg (Product uu vv h) x
ggP)

    leftAdjunct :: (Functor h, Functor k) => (Bi.Sum ff gg h ~> k) -> h ~> Bi.Product uu vv k
    leftAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(Sum ff gg g ~> h) -> g ~> Product uu vv h
leftAdjunct Sum ff gg h ~> k
lefty h x
h = uu k x -> vv k x -> Product uu vv k x
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Bi.Pair ((ff h ~> k) -> h ~> uu k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
leftAdjunct (Sum ff gg h x -> k x
Sum ff gg h ~> k
lefty (Sum ff gg h x -> k x)
-> (ff h x -> Sum ff gg h x) -> ff h x -> k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ff h x -> Sum ff gg h x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
Bi.L2) h x
h) ((gg h ~> k) -> h ~> vv k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(gg g ~> h) -> g ~> vv h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(ff g ~> h) -> g ~> uu h
leftAdjunct (Sum ff gg h x -> k x
Sum ff gg h ~> k
lefty (Sum ff gg h x -> k x)
-> (gg h x -> Sum ff gg h x) -> gg h x -> k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. gg h x -> Sum ff gg h x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
Bi.R2) h x
h)

    rightAdjunct :: (Functor h, Functor k) => (h ~> Bi.Product uu vv k) -> Bi.Sum ff gg h ~> k
    rightAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> Product uu vv h) -> Sum ff gg g ~> h
rightAdjunct h ~> Product uu vv k
righty (Bi.L2 ff h x
ff) = (h ~> uu k) -> ff h ~> k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
rightAdjunct (Product uu vv k x -> uu k x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
Product p q a b -> p a b
Bi.proj1 (Product uu vv k x -> uu k x)
-> (h x -> Product uu vv k x) -> h x -> uu k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h x -> Product uu vv k x
h ~> Product uu vv k
righty) ff h x
ff
    rightAdjunct h ~> Product uu vv k
righty (Bi.R2 gg h x
gg) = (h ~> vv k) -> gg h ~> k
forall (g :: * -> *) (h :: * -> *).
(Functor g, Functor h) =>
(g ~> vv h) -> gg g ~> h
forall (ff :: FF) (uu :: FF) (g :: * -> *) (h :: * -> *).
(Adjunction ff uu, Functor g, Functor h) =>
(g ~> uu h) -> ff g ~> h
rightAdjunct (Product uu vv k x -> vv k x
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
Product p q a b -> q a b
Bi.proj2 (Product uu vv k x -> vv k x)
-> (h x -> Product uu vv k x) -> h x -> vv k x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h x -> Product uu vv k x
h ~> Product uu vv k
righty) gg h x
gg

instance (Rank1.Adjunction f u) => Adjunction (Compose f) (Compose u) where
    unit :: (Functor g) => g ~> Compose u (Compose f g)
    unit :: forall (g :: * -> *). Functor g => g ~> Compose u (Compose f g)
unit g x
gx = u (Compose f g x) -> Compose u (Compose f g) x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (u (Compose f g x) -> Compose u (Compose f g) x)
-> (u (f (g x)) -> u (Compose f g x))
-> u (f (g x))
-> Compose u (Compose f g) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (g x) -> Compose f g x) -> u (f (g x)) -> u (Compose f g x)
forall a b. (a -> b) -> u a -> u b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (g x) -> Compose f g x
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (u (f (g x)) -> Compose u (Compose f g) x)
-> u (f (g x)) -> Compose u (Compose f g) x
forall a b. (a -> b) -> a -> b
$ g x -> u (f (g x))
forall a. a -> u (f a)
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
a -> u (f a)
Rank1.unit g x
gx
    counit :: (Functor g) => Compose f (Compose u g) ~> g
    counit :: forall (g :: * -> *). Functor g => Compose f (Compose u g) ~> g
counit = f (u (g x)) -> g x
forall a. f (u a) -> a
forall (f :: * -> *) (u :: * -> *) a.
Adjunction f u =>
f (u a) -> a
Rank1.counit (f (u (g x)) -> g x)
-> (Compose f (Compose u g) x -> f (u (g x)))
-> Compose f (Compose u g) x
-> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Compose u g x -> u (g x)) -> f (Compose u g x) -> f (u (g x))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Compose u g x -> u (g x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (f (Compose u g x) -> f (u (g x)))
-> (Compose f (Compose u g) x -> f (Compose u g x))
-> Compose f (Compose u g) x
-> f (u (g x))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f (Compose u g) x -> f (Compose u g x)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

instance Adjunction (Rank1.EnvT e) (Rank1.ReaderT e) where
    unit :: forall (g :: * -> *). Functor g => g ~> ReaderT e (EnvT e g)
unit g x
gx = (e -> EnvT e g x) -> ReaderT e (EnvT e g) x
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
Rank1.ReaderT \e
e -> e -> g x -> EnvT e g x
forall e (w :: * -> *) a. e -> w a -> EnvT e w a
Rank1.EnvT e
e g x
gx
    counit :: forall (g :: * -> *). Functor g => EnvT e (ReaderT e g) ~> g
counit (Rank1.EnvT e
e (Rank1.ReaderT e -> g x
f)) = e -> g x
f e
e

instance Adjunction (Rank1.TracedT m) (Rank1.WriterT m) where
    unit :: forall (g :: * -> *). Functor g => g ~> WriterT m (TracedT m g)
unit g x
gx = TracedT m g (x, m) -> WriterT m (TracedT m g) x
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
Rank1.WriterT (TracedT m g (x, m) -> WriterT m (TracedT m g) x)
-> TracedT m g (x, m) -> WriterT m (TracedT m g) x
forall a b. (a -> b) -> a -> b
$ g (m -> (x, m)) -> TracedT m g (x, m)
forall m (w :: * -> *) a. w (m -> a) -> TracedT m w a
Rank1.TracedT (g (m -> (x, m)) -> TracedT m g (x, m))
-> g (m -> (x, m)) -> TracedT m g (x, m)
forall a b. (a -> b) -> a -> b
$ (x -> m -> (x, m)) -> g x -> g (m -> (x, m))
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,) g x
gx

    counit :: forall (g :: * -> *). Functor g => TracedT m (WriterT m g) ~> g
counit (Rank1.TracedT (Rank1.WriterT g (m -> x, m)
gwx)) = ((m -> x, m) -> x) -> g (m -> x, m) -> g x
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(m -> x
f, m
m) -> m -> x
f m
m) g (m -> x, m)
gwx

instance Adjunction (Rank1.StoreT s) (Rank1.StateT s) where
    unit :: forall (g :: * -> *). Functor g => g ~> StateT s (StoreT s g)
unit g x
gx = (s -> StoreT s g (x, s)) -> StateT s (StoreT s g) x
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
Rank1.StateT ((s -> StoreT s g (x, s)) -> StateT s (StoreT s g) x)
-> (s -> StoreT s g (x, s)) -> StateT s (StoreT s g) x
forall a b. (a -> b) -> a -> b
$ g (s -> (x, s)) -> s -> StoreT s g (x, s)
forall s (w :: * -> *) a. w (s -> a) -> s -> StoreT s w a
Rank1.StoreT ((x -> s -> (x, s)) -> g x -> g (s -> (x, s))
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,) g x
gx)
    counit :: forall (g :: * -> *). Functor g => StoreT s (StateT s g) ~> g
counit (Rank1.StoreT (Rank1.StateT s -> g (s -> x, s)
state) s
s0) = ((s -> x, s) -> x) -> g (s -> x, s) -> g x
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(s -> x
f, s
m) -> s -> x
f s
m) (s -> g (s -> x, s)
state s
s0)

instance Functor f => Adjunction ((:*:) f) (Exp1 f) where 
  leftAdjunct :: (Functor f, Functor g, Functor h) => ((f :*: g) ~> h) -> g ~> Exp1 f h
  leftAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor f, Functor g, Functor h) =>
((f :*: g) ~> h) -> g ~> Exp1 f h
leftAdjunct = ((f :*: g) ~> h) -> g x -> Exp1 f h x
((f :*: g) ~> h) -> g ~> Exp1 f h
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Functor g =>
((f :*: g) ~> h) -> g ~> Exp1 f h
toExp1
  
  rightAdjunct :: (Functor f, Functor g, Functor h) => (g ~> Exp1 f h) -> (f :*: g) ~> h
  rightAdjunct :: forall (g :: * -> *) (h :: * -> *).
(Functor f, Functor g, Functor h) =>
(g ~> Exp1 f h) -> (f :*: g) ~> h
rightAdjunct = (g ~> Exp1 f h) -> (:*:) f g x -> h x
(g ~> Exp1 f h) -> (f :*: g) ~> h
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(g ~> Exp1 f h) -> (f :*: g) ~> h
fromExp1