{-# 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
  , mkAdjunctionUnit
  , mkAdjunctionCounit

  , leftAdjunct
  , rightAdjunct
  , adjunctionUnit
  , adjunctionCounit

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

  -- * Adjunctions from universal morphisms
  , initialPropAdjunction
  , terminalPropAdjunction

  -- * Universal morphisms from adjunctions
  , adjunctionInitialProp
  , adjunctionTerminalProp

  -- * Examples
  , precomposeAdj
  , postcomposeAdj
  , contAdj

) where

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

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
  { Adjunction c d f g -> f
leftAdjoint  :: f
  , Adjunction c d f g -> g
rightAdjoint :: g
  , Adjunction c d f g -> Profunctors c d (Costar f) (Star g)
leftAdjunctN  :: Profunctors c d (Costar f) (Star g)
  , Adjunction c d f g -> Profunctors c d (Star g) (Costar f)
rightAdjunctN :: Profunctors c d (Star g) (Costar f)
  }

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 :: 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 = f
-> g
-> Profunctors c d (Costar f) (Star g)
-> Profunctors c d (Star g) (Costar f)
-> Adjunction c d f g
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 ((Hom c :.: (Opposite f :***: Id c))
-> (Hom d :.: (Opposite (Id d) :***: g))
-> (forall z.
    Obj (Op d :**: c) z
    -> Component
         (Hom c :.: (Opposite f :***: Id c))
         (Hom d :.: (Opposite (Id d) :***: g))
         z)
-> Nat
     (Op d :**: c)
     (->)
     (Hom c :.: (Opposite f :***: Id c))
     (Hom d :.: (Opposite (Id d) :***: 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 (f -> Costar f
forall f. Functor f => f -> Costar f
Costar f
f) (g -> Star g
forall f. Functor f => f -> Star f
Star g
g) (\(Op a :**: _) -> Obj d b1 -> c (f :% b1) b2 -> d b1 (g :% b2)
forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)
l d b1 a1
Obj d b1
a)) ((Hom d :.: (Opposite (Id d) :***: g))
-> (Hom c :.: (Opposite f :***: Id c))
-> (forall z.
    Obj (Op d :**: c) z
    -> Component
         (Hom d :.: (Opposite (Id d) :***: g))
         (Hom c :.: (Opposite f :***: Id c))
         z)
-> Nat
     (Op d :**: c)
     (->)
     (Hom d :.: (Opposite (Id d) :***: g))
     (Hom c :.: (Opposite f :***: Id c))
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 (g -> Star g
forall f. Functor f => f -> Star f
Star g
g) (f -> Costar f
forall f. Functor f => f -> Costar f
Costar f
f) (\(_ :**: b) -> Obj c a2 -> d b1 (g :% a2) -> c (f :% b1) a2
forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
r Obj c a2
c a2 b2
b))

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 :: 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 = 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
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 g -> Dom g (f :% a) b -> Cod g (g :% (f :% a)) (g :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% c (f :% a) b
Dom g (f :% a) b
h) d (g :% (f :% a)) (g :% b) -> d a (g :% (f :% a)) -> d a (g :% b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj d a -> Component (Id d) (g :.: f) a
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 -> Obj c b -> Component (f :.: g) (Id c) b
forall a. Obj c a -> Component (f :.: g) (Id c) a
coun Obj c b
b c (f :% (g :% b)) b -> c (f :% a) (f :% (g :% b)) -> c (f :% a) 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 f -> Dom f a (g :% b) -> Cod f (f :% a) (f :% (g :% b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% d a (g :% b)
Dom f a (g :% b)
h))

mkAdjunctionUnit :: (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 b. Obj c b -> d a (g :% b) -> c (f :% a) b)
  -> Adjunction c d f g
mkAdjunctionUnit :: f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionUnit f
f g
g forall a. Obj d a -> Component (Id d) (g :.: f) a
un forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
adj = 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
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 g -> Dom g (f :% a) b -> Cod g (g :% (f :% a)) (g :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% c (f :% a) b
Dom g (f :% a) b
h) d (g :% (f :% a)) (g :% b) -> d a (g :% (f :% a)) -> d a (g :% b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj d a -> Component (Id d) (g :.: f) a
forall a. Obj d a -> Component (Id d) (g :.: f) a
un Obj d a
a) forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b
adj

mkAdjunctionCounit :: (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. Obj c a -> Component (f :.: g) (Id c) a)
  -> Adjunction c d f g
mkAdjunctionCounit :: f
-> g
-> (forall a b. Obj d a -> c (f :% a) b -> d a (g :% b))
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionCounit f
f g
g forall a b. Obj d a -> c (f :% a) b -> d a (g :% b)
adj forall a. Obj c a -> Component (f :.: g) (Id c) a
coun = 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
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 -> Obj c b -> Component (f :.: g) (Id c) b
forall a. Obj c a -> Component (f :.: g) (Id c) a
coun Obj c b
b c (f :% (g :% b)) b -> c (f :% a) (f :% (g :% b)) -> c (f :% a) 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 f -> Dom f a (g :% b) -> Cod f (f :% a) (f :% (g :% b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% d a (g :% b)
Dom f a (g :% b)
h))

leftAdjunct :: Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct :: 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 = (Nat
  (Op d :**: c)
  (->)
  (Hom c :.: (Opposite f :***: Id c))
  (Hom d :.: (Opposite (Id d) :***: g))
Profunctors c d (Costar f) (Star g)
l Nat
  (Op d :**: c)
  (->)
  (Hom c :.: (Opposite f :***: Id c))
  (Hom d :.: (Opposite (Id d) :***: g))
-> (:**:) (Op d) c (a, b) (a, b)
-> ((Hom c :.: (Opposite f :***: Id c)) :% (a, b))
-> (Hom d :.: (Opposite (Id d) :***: g)) :% (a, b)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (Obj d a -> Op d a a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj d a
a Op d a a -> c b b -> (:**:) (Op d) c (a, b) (a, b)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: c (f :% a) b -> c b b
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 :: 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 = (Nat
  (Op d :**: c)
  (->)
  (Hom d :.: (Opposite (Id d) :***: g))
  (Hom c :.: (Opposite f :***: Id c))
Profunctors c d (Star g) (Costar f)
r Nat
  (Op d :**: c)
  (->)
  (Hom d :.: (Opposite (Id d) :***: g))
  (Hom c :.: (Opposite f :***: Id c))
-> (:**:) (Op d) c (a, b) (a, b)
-> ((Hom d :.: (Opposite (Id d) :***: g)) :% (a, b))
-> (Hom c :.: (Opposite f :***: Id c)) :% (a, b)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! (d a a -> Op d a a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (d a (g :% b) -> d a a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src d a (g :% b)
h) Op d a a -> Obj c b -> (:**:) (Op d) c (a, b) (a, b)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c b
b)) d a (g :% b)
h

adjunctionUnit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit :: 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)
_) = Id d
-> (g :.: f)
-> (forall z. Obj d z -> Component (Id d) (g :.: f) z)
-> Nat d d (Id d) (g :.: 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 Id d
forall (k :: * -> * -> *). Id k
Id (g
g g -> f -> g :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (\Obj d z
a -> Adjunction c d f g
-> Obj d z -> c (f :% z) (f :% z) -> d z (g :% (f :% z))
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 f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d z
Dom f z z
a))
adjunctionCounit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit :: 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)
_) = (f :.: g)
-> Id c
-> (forall z. Obj c z -> Component (f :.: g) (Id c) z)
-> Nat c c (f :.: g) (Id c)
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 f -> g -> f :.: g
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) Id c
forall (k :: * -> * -> *). Id k
Id (\Obj c z
b -> Adjunction c d f g
-> Obj c z -> d (g :% z) (g :% z) -> c (f :% (g :% z)) z
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 g -> Dom g z z -> Cod g (g :% z) (g :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c z
Dom g z z
b))

-- Each pair (FY, unit_Y) is an initial morphism from Y to G.
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionInitialProp :: Adjunction c d f g -> Obj d y -> InitialUniversal y g (f :% y)
adjunctionInitialProp 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)
_) Obj d y
y = g
-> Obj (Dom g) (f :% y)
-> Cod g y (g :% (f :% y))
-> (forall y.
    Obj (Dom g) y -> Cod g y (g :% y) -> Dom g (f :% y) y)
-> InitialUniversal y g (f :% y)
forall u a x.
Functor u =>
u
-> Obj (Dom u) a
-> Cod u x (u :% a)
-> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y)
-> InitialUniversal x u a
initialUniversal g
g (f
f f -> Dom f y y -> Cod f (f :% y) (f :% y)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d y
Dom f y y
y) (Adjunction c d f g -> Nat d d (Id d) (g :.: f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj Nat d d (Id d) (g :.: f)
-> Obj d y -> d (Id d :% y) ((g :.: f) :% y)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj d y
y) (Adjunction c d f g -> Obj c y -> d y (g :% y) -> c (f :% y) y
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)

-- Each pair (GX, counit_X) is a terminal morphism from F to X.
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
adjunctionTerminalProp :: Adjunction c d f g -> Obj c x -> TerminalUniversal x f (g :% x)
adjunctionTerminalProp 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)
_) Obj c x
x = f
-> Obj (Dom f) (g :% x)
-> Cod f (f :% (g :% x)) x
-> (forall y.
    Obj (Dom f) y -> Cod f (f :% y) x -> Dom f y (g :% x))
-> TerminalUniversal x f (g :% x)
forall u a x.
Functor u =>
u
-> Obj (Dom u) a
-> Cod u (u :% a) x
-> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a)
-> TerminalUniversal x u a
terminalUniversal f
f (g
g g -> Dom g x x -> Cod g (g :% x) (g :% x)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c x
Dom g x x
x) (Adjunction c d f g -> Nat c c (f :.: g) (Id 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 Nat c c (f :.: g) (Id c)
-> Obj c x -> c ((f :.: g) :% x) (Id c :% x)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj c x
x) (Adjunction c d f g -> Obj d y -> c (f :% y) x -> d y (g :% x)
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)



initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
initialPropAdjunction :: f
-> g
-> (forall y. Obj d y -> InitialUniversal y g (f :% y))
-> Adjunction c d f g
initialPropAdjunction f
f g
g forall y. Obj d y -> InitialUniversal y g (f :% y)
univ = 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
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
  (Representable ((a :*-: d) :.: g) (f :% a) -> d a (g :% (f :% a))
forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *).
   (Dom f ~ k, Cod f ~ (->)) =>
   f :% repObj
universalElement (Representable ((a :*-: d) :.: g) (f :% a) -> d a (g :% (f :% a)))
-> (d a a -> Representable ((a :*-: d) :.: g) (f :% a))
-> d a a
-> d a (g :% (f :% a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. d a a -> Representable ((a :*-: d) :.: g) (f :% a)
forall y. Obj d y -> InitialUniversal y g (f :% y)
univ)
  (\Obj c a
a -> Representable (((g :% a) :*-: d) :.: g) (f :% (g :% a))
-> Obj c a
-> ((((g :% a) :*-: d) :.: g) :% a)
-> c (f :% (g :% a)) a
forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *) z.
   (Dom f ~ k, Cod f ~ (->)) =>
   Obj k z -> (f :% z) -> k repObj z
represent (Obj d (g :% a) -> InitialUniversal (g :% a) g (f :% (g :% a))
forall y. Obj d y -> InitialUniversal y g (f :% y)
univ (g
g g -> Dom g a a -> Cod g (g :% a) (g :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c a
Dom g a a
a)) Obj c a
a (g
g g -> Dom g a a -> Cod g (g :% a) (g :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c a
Dom g a a
a))

terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)
  => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
terminalPropAdjunction :: f
-> g
-> (forall x. Obj c x -> TerminalUniversal x f (g :% x))
-> Adjunction c d f g
terminalPropAdjunction f
f g
g forall x. Obj c x -> TerminalUniversal x f (g :% x)
univ = 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
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
  (\Obj d a
a -> Op d (g :% (f :% a)) a -> d a (g :% (f :% a))
forall k k (k :: k -> k -> *) (a :: k) (b :: k). Op k a b -> k b a
unOp (Representable ((c :-*: (f :% a)) :.: Opposite f) (g :% (f :% a))
-> Obj (Op d) a
-> (((c :-*: (f :% a)) :.: Opposite f) :% a)
-> Op d (g :% (f :% a)) a
forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *) z.
   (Dom f ~ k, Cod f ~ (->)) =>
   Obj k z -> (f :% z) -> k repObj z
represent (Obj c (f :% a) -> TerminalUniversal (f :% a) f (g :% (f :% a))
forall x. Obj c x -> TerminalUniversal x f (g :% x)
univ (f
f f -> Dom f a a -> Cod f (f :% a) (f :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d a
Dom f a a
a)) (Obj d a -> Obj (Op d) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj d a
a) (f
f f -> Dom f a a -> Cod f (f :% a) (f :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj d a
Dom f a a
a)))
  (Representable ((c :-*: a) :.: Opposite f) (g :% a)
-> c (f :% (g :% a)) a
forall f repObj.
Representable f repObj
-> forall (k :: * -> * -> *).
   (Dom f ~ k, Cod f ~ (->)) =>
   f :% repObj
universalElement (Representable ((c :-*: a) :.: Opposite f) (g :% a)
 -> c (f :% (g :% a)) a)
-> (c a a -> Representable ((c :-*: a) :.: Opposite f) (g :% a))
-> c a a
-> c (f :% (g :% a)) a
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. c a a -> Representable ((c :-*: a) :.: Opposite f) (g :% a)
forall x. Obj c x -> TerminalUniversal x f (g :% x)
univ)


idAdj :: Category k => Adjunction k k (Id k) (Id k)
idAdj :: Adjunction k k (Id k) (Id k)
idAdj = Id k
-> Id k
-> (forall a b. Obj k a -> k (Id k :% a) b -> k a (Id k :% b))
-> (forall a b. Obj k b -> k a (Id k :% b) -> k (Id k :% a) b)
-> Adjunction k k (Id k) (Id k)
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 Id k
forall (k :: * -> * -> *). Id k
Id Id k
forall (k :: * -> * -> *). Id k
Id (\Obj k a
_ k (Id k :% a) b
f -> k a (Id k :% b)
k (Id k :% a) b
f) (\Obj k b
_ k a (Id k :% b)
f -> k a (Id k :% b)
k (Id k :% a) b
f)

composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
composeAdj :: 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')
_) = (f' :.: f)
-> (g :.: g')
-> (forall a b.
    Obj e a -> c ((f' :.: f) :% a) b -> e a ((g :.: g') :% b))
-> (forall a b.
    Obj c b -> e a ((g :.: g') :% b) -> c ((f' :.: f) :% a) b)
-> Adjunction c e (f' :.: f) (g :.: g')
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' f' -> f -> f' :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (g
g g -> g' -> g :.: g'
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g'
g')
  (\Obj e a
a -> Adjunction d e f g
-> Obj e a -> d (f :% a) (g' :% b) -> e a (g :% (g' :% b))
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 (d (f :% a) (g' :% b) -> e a (g :% (g' :% b)))
-> (c (f' :% (f :% a)) b -> d (f :% a) (g' :% b))
-> c (f' :% (f :% a)) b
-> e a (g :% (g' :% b))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Adjunction c d f' g'
-> Obj d (f :% a) -> c (f' :% (f :% a)) b -> d (f :% a) (g' :% b)
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 f -> Dom f a a -> Cod f (f :% a) (f :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj e a
Dom f a a
a)) (\Obj c b
b -> Adjunction c d f' g'
-> Obj c b -> d (f :% a) (g' :% b) -> c (f' :% (f :% a)) 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 (d (f :% a) (g' :% b) -> c (f' :% (f :% a)) b)
-> (e a (g :% (g' :% b)) -> d (f :% a) (g' :% b))
-> e a (g :% (g' :% b))
-> c (f' :% (f :% a)) b
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Adjunction d e f g
-> Obj d (g' :% b) -> e a (g :% (g' :% b)) -> d (f :% a) (g' :% 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 d e f g
l (g'
g' g' -> Dom g' b b -> Cod g' (g' :% b) (g' :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c b
Dom g' b 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 :: AdjArrow a b -> Obj AdjArrow a
src (AdjArrow (Adjunction f
_ g
_ Profunctors a b (Costar f) (Star g)
_ Profunctors a b (Star g) (Costar f)
_)) = Adjunction a a (Id a) (Id a) -> Obj AdjArrow a
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Category c, Category d) =>
Adjunction c d f g -> AdjArrow c d
AdjArrow Adjunction a a (Id a) (Id a)
forall (k :: * -> * -> *).
Category k =>
Adjunction k k (Id k) (Id k)
idAdj
  tgt :: AdjArrow a b -> Obj AdjArrow b
tgt (AdjArrow (Adjunction f
_ g
_ Profunctors a b (Costar f) (Star g)
_ Profunctors a b (Star g) (Costar f)
_)) = Adjunction b b (Id b) (Id b) -> Obj AdjArrow b
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Category c, Category d) =>
Adjunction c d f g -> AdjArrow c d
AdjArrow Adjunction b b (Id b) (Id b)
forall (k :: * -> * -> *).
Category k =>
Adjunction k k (Id k) (Id k)
idAdj

  AdjArrow Adjunction b c f g
x . :: AdjArrow b c -> AdjArrow a b -> AdjArrow a c
. AdjArrow Adjunction a b f g
y = Adjunction a c (f :.: f) (g :.: g) -> AdjArrow a c
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Category c, Category d) =>
Adjunction c d f g -> AdjArrow c d
AdjArrow (Adjunction b c f g
-> Adjunction a b f g -> Adjunction a c (f :.: f) (g :.: g)
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 :: 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)
_) = (FunctorCompose c d e :.: Tuple2 (Nat d e) (Nat c d) g)
-> (FunctorCompose d c e :.: Tuple2 (Nat c e) (Nat d c) f)
-> (forall a.
    Obj (Nat d e) a
    -> Component
         (Id (Nat d e))
         ((FunctorCompose d c e :.: Tuple2 (Nat c e) (Nat d c) f)
          :.: (FunctorCompose c d e :.: Tuple2 (Nat d e) (Nat c d) g))
         a)
-> (forall a.
    Obj (Nat c e) a
    -> Component
         ((FunctorCompose c d e :.: Tuple2 (Nat d e) (Nat c d) g)
          :.: (FunctorCompose d c e :.: Tuple2 (Nat c e) (Nat d c) f))
         (Id (Nat c e))
         a)
-> Adjunction
     (Nat c e)
     (Nat d e)
     (FunctorCompose c d e :.: Tuple2 (Nat d e) (Nat c d) g)
     (FunctorCompose d c e :.: Tuple2 (Nat c e) (Nat d c) 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
  (g -> Precompose g e
forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
Precompose g
g)
  (f -> Precompose f e
forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
Precompose f
f)
  (\nh :: Obj (Nat d e) a
nh@(Nat h _ _) -> a
-> g
-> f
-> Nat (Dom f) (Cod a) (a :.: (g :.: f)) ((a :.: g) :.: f)
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 Nat d e (a :.: (g :.: f)) ((a :.: g) :.: f)
-> Nat d e a (a :.: (g :.: f)) -> Nat d e a ((a :.: g) :.: 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 Obj (Nat d e) a
-> Nat d d (Id d) (g :.: f)
-> Nat d e (a :.: Id d) (a :.: (g :.: f))
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` Adjunction c d f g -> Nat d d (Id d) (g :.: f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj) Nat d e (a :.: Id d) (a :.: (g :.: f))
-> Nat d e a (a :.: Id d) -> Nat d e a (a :.: (g :.: f))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. a -> Nat (Dom a) (Cod a) a (a :.: Id (Dom a))
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 h _ _) -> a -> Nat (Dom a) (Cod a) (a :.: Id (Dom a)) a
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp a
h Nat c e (a :.: Id c) a
-> Nat c e ((a :.: f) :.: g) (a :.: Id c)
-> Nat c e ((a :.: f) :.: g) a
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 Obj (Nat c e) a
-> Nat c c (f :.: g) (Id c)
-> Nat c e (a :.: (f :.: g)) (a :.: Id c)
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` Adjunction c d f g -> Nat c c (f :.: g) (Id 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) Nat c e (a :.: (f :.: g)) (a :.: Id c)
-> Nat c e ((a :.: f) :.: g) (a :.: (f :.: g))
-> Nat c e ((a :.: f) :.: g) (a :.: Id c)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. a
-> f
-> g
-> Nat (Dom g) (Cod a) ((a :.: f) :.: g) (a :.: (f :.: g))
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 :: 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)
_) = (FunctorCompose e d c :.: Tuple1 (Nat d c) (Nat e d) f)
-> (FunctorCompose e c d :.: Tuple1 (Nat c d) (Nat e c) g)
-> (forall a.
    Obj (Nat e d) a
    -> Component
         (Id (Nat e d))
         ((FunctorCompose e c d :.: Tuple1 (Nat c d) (Nat e c) g)
          :.: (FunctorCompose e d c :.: Tuple1 (Nat d c) (Nat e d) f))
         a)
-> (forall a.
    Obj (Nat e c) a
    -> Component
         ((FunctorCompose e d c :.: Tuple1 (Nat d c) (Nat e d) f)
          :.: (FunctorCompose e c d :.: Tuple1 (Nat c d) (Nat e c) g))
         (Id (Nat e c))
         a)
-> Adjunction
     (Nat e c)
     (Nat e d)
     (FunctorCompose e d c :.: Tuple1 (Nat d c) (Nat e d) f)
     (FunctorCompose e c d :.: Tuple1 (Nat c d) (Nat e c) g)
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 -> Postcompose f e
forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Postcompose f e
Postcompose f
f)
  (g -> Postcompose g e
forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Postcompose f e
Postcompose g
g)
  (\nh :: Obj (Nat e d) a
nh@(Nat h _ _) -> g
-> f
-> a
-> Nat (Dom a) (Cod g) ((g :.: f) :.: a) (g :.: (f :.: a))
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 Nat e d ((g :.: f) :.: a) (g :.: (f :.: a))
-> Nat e d a ((g :.: f) :.: a) -> Nat e d a (g :.: (f :.: a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Adjunction c d f g -> Nat d d (Id d) (g :.: f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj Nat d d (Id d) (g :.: f)
-> Obj (Nat e d) a -> Nat e d (Id d :.: a) ((g :.: f) :.: a)
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) Nat e d (Id d :.: a) ((g :.: f) :.: a)
-> Nat e d a (Id d :.: a) -> Nat e d a ((g :.: f) :.: a)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. a -> Nat (Dom a) (Cod a) a (Id (Cod a) :.: a)
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 h _ _) -> a -> Nat (Dom a) (Cod a) (Id (Cod a) :.: a) a
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp a
h Nat e c (Id c :.: a) a
-> Nat e c (f :.: (g :.: a)) (Id c :.: a)
-> Nat e c (f :.: (g :.: a)) a
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Adjunction c d f g -> Nat c c (f :.: g) (Id 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 Nat c c (f :.: g) (Id c)
-> Obj (Nat e c) a -> Nat e c ((f :.: g) :.: a) (Id c :.: a)
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) Nat e c ((f :.: g) :.: a) (Id c :.: a)
-> Nat e c (f :.: (g :.: a)) ((f :.: g) :.: a)
-> Nat e c (f :.: (g :.: a)) (Id c :.: a)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f
-> g
-> a
-> Nat (Dom a) (Cod f) (f :.: (g :.: a)) ((f :.: g) :.: a)
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 :: Adjunction
  (Op (->))
  (->)
  (Opposite ((->) :-*: r) :.: OpOpInv (->))
  ((->) :-*: r)
contAdj = (Opposite ((->) :-*: r) :.: OpOpInv (->))
-> ((->) :-*: r)
-> (forall a b.
    Obj (->) a
    -> Op (->) ((Opposite ((->) :-*: r) :.: OpOpInv (->)) :% a) b
    -> a
    -> ((->) :-*: r) :% b)
-> (forall a b.
    Obj (Op (->)) b
    -> (a -> ((->) :-*: r) :% b)
    -> Op (->) ((Opposite ((->) :-*: r) :.: OpOpInv (->)) :% a) b)
-> Adjunction
     (Op (->))
     (->)
     (Opposite ((->) :-*: r) :.: OpOpInv (->))
     ((->) :-*: r)
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
  (((->) :-*: r) -> Opposite ((->) :-*: r)
forall f. Functor f => f -> Opposite f
Opposite (Obj (->) r -> (->) :-*: r
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X (\r
x -> r
x)) Opposite ((->) :-*: r)
-> OpOpInv (->) -> Opposite ((->) :-*: r) :.: OpOpInv (->)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: OpOpInv (->)
forall (k :: * -> * -> *). OpOpInv k
OpOpInv)
  (Obj (->) r -> (->) :-*: r
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X (\r
x -> r
x))
  (\Obj (->) a
_ -> \(Op f) -> \a
b b
a -> b -> a -> r
f b
a a
b)
  (\Obj (Op (->)) b
_ -> \a -> ((->) :-*: r) :% b
f -> (b -> a -> r) -> Op (->) (a -> r) b
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
a -> b -> r
f a
a b
b))