{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, FlexibleContexts, ScopedTypeVariables, RankNTypes, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Adjunction
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Adjunction (

  -- * Adjunctions
    Adjunction(..)
  , mkAdjunction
  , mkAdjunctionUnits
  , mkAdjunctionInit
  , mkAdjunctionTerm

  , leftAdjunct
  , rightAdjunct
  , adjunctionUnit
  , adjunctionCounit

  -- * Adjunctions as a category
  , idAdj
  , composeAdj
  , AdjArrow(..)

  -- * Examples
  , precomposeAdj
  , postcomposeAdj
  , contAdj

) where

import Data.Category
import Data.Category.Functor
import Data.Category.Product
import Data.Category.NaturalTransformation

data Adjunction c d f g = (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => Adjunction
  { forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> f
leftAdjoint  :: f
  , forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> g
rightAdjoint :: g
  , forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Profunctors c d (Costar f) (Star g)
leftAdjunctN  :: Profunctors c d (Costar f) (Star g)
  , forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Profunctors c d (Star g) (Costar f)
rightAdjunctN :: Profunctors c d (Star g) (Costar f)
  }

-- | Make an adjunction from the hom-set isomorphism.
mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g
  -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
  -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
  -> Adjunction c d f g
mkAdjunction :: forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction f
f g
g forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)
l forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
r = forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Functor f, Functor g, Category c, Category d, Dom f ~ d,
 Cod f ~ c, Dom g ~ c, Cod g ~ d) =>
f
-> g
-> Profunctors c d (Costar f) (Star g)
-> Profunctors c d (Star g) (Costar f)
-> Adjunction c d f g
Adjunction f
f g
g (forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall f. Functor f => f -> Costar f
Costar f
f) (forall f. Functor f => f -> Star f
Star g
g) (\(Op d b1 a1
a :**: c a2 b2
_) -> forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)
l d b1 a1
a)) (forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall f. Functor f => f -> Star f
Star g
g) (forall f. Functor f => f -> Costar f
Costar f
f) (\(Op d a1 b1
_ :**: c a2 b2
b) -> forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
r c a2 b2
b))

-- | Make an adjunction from the unit and counit.
mkAdjunctionUnits :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g
  -> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
  -> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
  -> Adjunction c d f g
mkAdjunctionUnits :: forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits f
f g
g forall a. Obj d a -> Component (Id d) (g :.: f) a
un forall a. Obj c a -> Component (f :.: g) (Id c) a
coun = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction f
f g
g (\Obj d a
a c (f :% a) b
h -> (g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% c (f :% a) b
h) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall a. Obj d a -> Component (Id d) (g :.: f) a
un Obj d a
a) (\Obj c b
b d a (g :% b)
h -> forall a. Obj c a -> Component (f :.: g) (Id c) a
coun Obj c b
b forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% d a (g :% b)
h))

-- | Make an adjunction from an initial universal property.
mkAdjunctionInit :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g
  -> (forall a. Obj d a -> d a (g :% (f :% a)))
  -> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
  -> Adjunction c d f g
mkAdjunctionInit :: forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit f
f g
g forall a. Obj d a -> d a (g :% (f :% a))
un forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
adj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction f
f g
g (\Obj d a
a c (f :% a) b
h -> (g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% c (f :% a) b
h) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall a. Obj d a -> d a (g :% (f :% a))
un Obj d a
a) forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
adj

-- | Make an adjunction from a terminal universal property.
mkAdjunctionTerm :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g
  -> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
  -> (forall b. Obj c b -> c (f :% (g :% b)) b)
  -> Adjunction c d f g
mkAdjunctionTerm :: forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall b. Obj c b -> c (f :% (g :% b)) b)
-> Adjunction c d f g
mkAdjunctionTerm f
f g
g forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)
adj forall b. Obj c b -> c (f :% (g :% b)) b
coun = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction f
f g
g forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)
adj (\Obj c b
b d a (g :% b)
h -> forall b. Obj c b -> c (f :% (g :% b)) b
coun Obj c b
b forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% d a (g :% b)
h))

leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct (Adjunction f
_ g
_ Profunctors c d (Costar f) (Star g)
l Profunctors c d (Star g) (Costar f)
_) Obj d a
a c (f :% a) b
h = (Profunctors c d (Costar f) (Star g)
l forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj d a
a forall (c1 :: * -> * -> *) f g (c2 :: * -> * -> *) a2 b2.
c1 f g -> c2 a2 b2 -> (:**:) c1 c2 (f, a2) (g, b2)
:**: forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c (f :% a) b
h)) c (f :% a) b
h
rightAdjunct :: Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct (Adjunction f
_ g
_ Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
r) Obj c b
b d a (g :% b)
h = (Profunctors c d (Star g) (Costar f)
r forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src d a (g :% b)
h) forall (c1 :: * -> * -> *) f g (c2 :: * -> * -> *) a2 b2.
c1 f g -> c2 a2 b2 -> (:**:) c1 c2 (f, a2) (g, b2)
:**: Obj c b
b)) d a (g :% b)
h

adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall (k :: * -> * -> *). Id k
Id (g
g forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (\Obj d z
a -> forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f g
adj Obj d z
a (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d z
a))
adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) forall (k :: * -> * -> *). Id k
Id (\Obj c z
b -> forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f g
adj Obj c z
b (g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
b))


idAdj :: Category k => Adjunction k k (Id k) (Id k)
idAdj :: forall (k :: * -> * -> *).
Category k =>
Adjunction k k (Id k) (Id k)
idAdj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction forall (k :: * -> * -> *). Id k
Id forall (k :: * -> * -> *). Id k
Id (\Obj k a
_ k (Id k :% a) b
f -> k (Id k :% a) b
f) (\Obj k b
_ k a (Id k :% b)
f -> k a (Id k :% b)
f)

composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
composeAdj :: forall (d :: * -> * -> *) (e :: * -> * -> *) f g (c :: * -> * -> *)
       f' g'.
Adjunction d e f g
-> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
composeAdj l :: Adjunction d e f g
l@(Adjunction f
f g
g Profunctors d e (Costar f) (Star g)
_ Profunctors d e (Star g) (Costar f)
_) r :: Adjunction c d f' g'
r@(Adjunction f'
f' g'
g' Profunctors c d (Costar f') (Star g')
_ Profunctors c d (Star g') (Costar f')
_) = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction (f'
f' forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (g
g forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g'
g')
  (\Obj e a
a -> forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction d e f g
l Obj e a
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct Adjunction c d f' g'
r (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj e a
a)) (\Obj c b
b -> forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction c d f' g'
r Obj c b
b forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct Adjunction d e f g
l (g'
g' forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c b
b))


data AdjArrow c d where
  AdjArrow :: (Category c, Category d) => Adjunction c d f g -> AdjArrow c d

-- | The category with categories as objects and adjunctions as arrows.
instance Category AdjArrow where

  src :: forall (a :: * -> * -> *) (b :: * -> * -> *).
AdjArrow a b -> Obj AdjArrow a
src (AdjArrow Adjunction{}) = forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Category c, Category d) =>
Adjunction c d f g -> AdjArrow c d
AdjArrow forall (k :: * -> * -> *).
Category k =>
Adjunction k k (Id k) (Id k)
idAdj
  tgt :: forall (a :: * -> * -> *) (b :: * -> * -> *).
AdjArrow a b -> Obj AdjArrow b
tgt (AdjArrow Adjunction{}) = forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Category c, Category d) =>
Adjunction c d f g -> AdjArrow c d
AdjArrow forall (k :: * -> * -> *).
Category k =>
Adjunction k k (Id k) (Id k)
idAdj

  AdjArrow Adjunction b c f g
x . :: forall (b :: * -> * -> *) (c :: * -> * -> *) (a :: * -> * -> *).
AdjArrow b c -> AdjArrow a b -> AdjArrow a c
. AdjArrow Adjunction a b f g
y = forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Category c, Category d) =>
Adjunction c d f g -> AdjArrow c d
AdjArrow (forall (d :: * -> * -> *) (e :: * -> * -> *) f g (c :: * -> * -> *)
       f' g'.
Adjunction d e f g
-> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
composeAdj Adjunction b c f g
x Adjunction a b f g
y)



precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
precomposeAdj :: forall (e :: * -> * -> *) (c :: * -> * -> *) (d :: * -> * -> *) f
       g.
Category e =>
Adjunction c d f g
-> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
precomposeAdj adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits
  (forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
Precompose g
g)
  (forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
Precompose f
f)
  (\nh :: Obj (Nat d e) a
nh@(Nat a
h a
_ forall z. Obj d z -> Component a a z
_) -> forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv a
h g
g f
f forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj (Nat d e) a
nh forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv a
h)
  (\nh :: Obj (Nat c e) a
nh@(Nat a
h a
_ forall z. Obj c z -> Component a a z
_) -> forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp a
h forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj (Nat c e) a
nh forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc a
h f
f g
g)

postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
postcomposeAdj :: forall (e :: * -> * -> *) (c :: * -> * -> *) (d :: * -> * -> *) f
       g.
Category e =>
Adjunction c d f g
-> Adjunction
     (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
postcomposeAdj adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits
  (forall (c :: * -> * -> *) f.
(Category c, Functor f) =>
f -> Postcompose f c
Postcompose f
f)
  (forall (c :: * -> * -> *) f.
(Category c, Functor f) =>
f -> Postcompose f c
Postcompose g
g)
  (\nh :: Obj (Nat e d) a
nh@(Nat a
h a
_ forall z. Obj e z -> Component a a z
_) -> forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc g
g f
f a
h forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Obj (Nat e d) a
nh) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
idPostcompInv a
h)
  (\nh :: Obj (Nat e c) a
nh@(Nat a
h a
_ forall z. Obj e z -> Component a a z
_) -> forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp a
h forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Obj (Nat e c) a
nh) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv f
f g
g a
h)

contAdj :: Adjunction (Op (->)) (->) (Opposite ((->) :-*: r) :.: OpOpInv (->)) ((->) :-*: r)
contAdj :: forall r.
Adjunction
  (Op (->))
  (->)
  (Opposite ((->) :-*: r) :.: OpOpInv (->))
  ((->) :-*: r)
contAdj = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunction
  (forall f. Functor f => f -> Opposite f
Opposite (forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X forall a. Obj (->) a
obj) forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). OpOpInv k
OpOpInv)
  (forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X forall a. Obj (->) a
obj)
  (\Obj (->) a
_ -> \(Op b -> (a -> r)
f) -> \a
b b
a -> b -> (a -> r)
f b
a a
b)
  (\Obj (Op (->)) b
_ -> \a -> (((->) :-*: r) :% b)
f -> forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (\b
b a
a -> a -> (((->) :-*: r) :% b)
f a
a b
b))