{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Adjunction where

import Data.Kind (Constraint)
import Prelude (($))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), isObPar)
import Proarrow.Core (CAT, CategoryOf (..), Obj, PRO, Profunctor (..), Promonad (..), rmap, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Costar (Costar (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (RepCostar (..), Representable (..), repObj)
import Proarrow.Profunctor.Star (Star (..))
import Proarrow.Promonad (Procomonad (..))
import Proarrow.Category.Opposite (Op (..))

type Adjunction :: forall {j} {k}. PRO k j -> PRO j k -> Constraint

-- | Adjunctions between two profunctors.
class (Profunctor p, Profunctor q) => Adjunction (p :: PRO k j) (q :: PRO j k) where
  unit :: (Ob a) => (q :.: p) a a -- (~>) :~> q :.: p
  counit :: p :.: q :~> (~>)

unit' :: forall p q a b. (Adjunction p q) => a ~> b -> (q :.: p) a b
unit' :: forall {j} {i} (p :: PRO j i) (q :: PRO i j) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' a ~> b
f = (a ~> b) -> (:.:) q p a a -> (:.:) q p a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
f (forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO j i) (q :: PRO i j) (a :: i).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @p @q @a) ((Ob a, Ob b) => (:.:) q p a b) -> (a ~> b) -> (:.:) q p a b
forall (a :: i) (b :: i) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

leftAdjunct
  :: forall l r a b
   . (Adjunction l r, Representable l, Representable r, Ob a)
  => (l % a ~> b)
  -> r a b
leftAdjunct :: forall {k} {j} (l :: PRO k j) (r :: PRO j k) (a :: j) (b :: k).
(Adjunction l r, Representable l, Representable r, Ob a) =>
((l % a) ~> b) -> r a b
leftAdjunct (l % a) ~> b
f = case forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @l @r of r a b
r :.: l b a
l -> (b ~> b) -> r a b -> r a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((l % a) ~> b
f ((l % a) ~> b) -> (b ~> (l % a)) -> b ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. l b a -> b ~> (l % a)
forall (a :: k) (b :: j). l a b -> a ~> (l % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index l b a
l) r a b
r

rightAdjunct
  :: forall l r a b
   . (Adjunction l r, Representable l, Representable r, Ob b)
  => r a b
  -> (l % a ~> b)
rightAdjunct :: forall {k} {j} (l :: PRO k j) (r :: PRO j k) (a :: j) (b :: k).
(Adjunction l r, Representable l, Representable r, Ob b) =>
r a b -> (l % a) ~> b
rightAdjunct r a b
f = (:.:) l r (l % a) b -> (l % a) ~> b
(l :.: r) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @l (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @l @a a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) l (l % a) a -> r a b -> (:.:) l r (l % a) b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r a b
f) ((Ob a, Ob b) => (l % a) ~> b) -> r a b -> (l % a) ~> b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> r a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ r a b
f

unitFromRepUnit
  :: forall l r a. (Representable l, Representable r, Ob a) => (a ~> r % (l % a)) -> (r :.: l) a a
unitFromRepUnit :: forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i).
(Representable l, Representable r, Ob a) =>
(a ~> (r % (l % a))) -> (:.:) r l a a
unitFromRepUnit a ~> (r % (l % a))
f = (a ~> (r % (l % a))) -> r a (l % a)
forall (b :: j) (a :: i). Ob b => (a ~> (r % b)) -> r a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a ~> (r % (l % a))
f r a (l % a) -> l (l % a) a -> (:.:) r l a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((l % a) ~> (l % a)) -> l (l % a) a
forall (b :: i) (a :: j). Ob b => (a ~> (l % b)) -> l a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (l % a) ~> (l % a)
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (l % a), Ob (l % a)) => (:.:) r l a a)
-> ((l % a) ~> (l % a)) -> (:.:) r l a a
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: i +-> j) (a :: i).
(Representable p, Ob a) =>
Obj (p % a)
repObj @l @a

counitFromRepCounit
  :: forall l r. (Representable l, Representable r) => (forall c. (Ob c) => l % (r % c) ~> c) -> (l :.: r) :~> (~>)
counitFromRepCounit :: forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j).
(Representable l, Representable r) =>
(forall (c :: k1). Ob c => (l % (r % c)) ~> c)
-> (l :.: r) :~> (~>)
counitFromRepCounit forall (c :: k1). Ob c => (l % (r % c)) ~> c
f (l a b
l :.: r b b
r) = (l % (r % b)) ~> b
forall (c :: k1). Ob c => (l % (r % c)) ~> c
f ((l % (r % b)) ~> b) -> (a ~> (l % (r % b))) -> a ~> b
forall (b :: k1) (c :: k1) (a :: k1).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k1) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @l (r b b -> b ~> (r % b)
forall (a :: j) (b :: k1). r a b -> a ~> (r % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index r b b
r) ((l % b) ~> (l % (r % b))) -> (a ~> (l % b)) -> a ~> (l % (r % b))
forall (b :: k1) (c :: k1) (a :: k1).
(b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. l a b -> a ~> (l % b)
forall (a :: k1) (b :: j). l a b -> a ~> (l % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index l a b
l ((Ob b, Ob b) => a ~> b) -> r b b -> a ~> b
forall (a :: j) (b :: k1) r. ((Ob a, Ob b) => r) -> r a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ r b b
r

instance (Functor f) => Adjunction (Star f) (Costar f) where
  unit :: forall (a :: j). Ob a => (:.:) (Costar f) (Star f) a a
unit = (f a ~> f a) -> Costar f a (f a)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar ((a ~> a) -> f a ~> f a
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) Costar f a (f a) -> Star f (f a) a -> (:.:) (Costar f) (Star f) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (f a ~> f a) -> Star f (f a) a
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a ~> a) -> f a ~> f a
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  counit :: (Star f :.: Costar f) :~> (~>)
counit (Star a ~> f b
f :.: Costar f b ~> b
g) = f b ~> b
g (f b ~> b) -> (a ~> f b) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> f b
f

instance (Representable f) => Adjunction f (RepCostar f) where
  unit :: forall (a :: k). Ob a => (:.:) (RepCostar f) f a a
unit @a = let fa :: (f % a) ~> (f % a)
fa = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> j) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f @a a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id in ((f % a) ~> (f % a)) -> RepCostar f a (f % a)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (f % a) ~> (f % a)
fa RepCostar f a (f % a) -> f (f % a) a -> (:.:) (RepCostar f) f a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((f % a) ~> (f % a)) -> f (f % a) a
forall (b :: k) (a :: j). Ob b => (a ~> (f % b)) -> f a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (f % a) ~> (f % a)
fa
  counit :: (f :.: RepCostar f) :~> (~>)
counit (f a b
f :.: RepCostar (f % b) ~> b
g) = (f % b) ~> b
g ((f % b) ~> b) -> (a ~> (f % b)) -> a ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. f a b -> a ~> (f % b)
forall (a :: j) (b :: k). f a b -> a ~> (f % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index f a b
f

instance (Functor f, Functor g, Adjunction (Star f) (Star g)) => Adjunction (Costar f) (Costar g) where
  unit :: forall a. (Ob a) => (Costar g :.: Costar f) a a
  unit :: forall (a :: j). Ob a => (:.:) (Costar g) (Costar f) a a
unit = (g a ~> g a) -> Costar g a (g a)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar g a ~> g a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Costar g a (g a)
-> Costar f (g a) a -> (:.:) (Costar g) (Costar f) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (f (g a) ~> a) -> Costar f (g a) a
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar ((:.:) (Star f) (Star g) (f (g a)) a -> f (g a) ~> a
(Star f :.: Star g) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit ((f (g a) ~> f (g a)) -> Star f (f (g a)) (g a)
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((g a ~> g a) -> f (g a) ~> f (g a)
forall (a :: k) (b :: k). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map g a ~> g a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) Star f (f (g a)) (g a)
-> Star g (g a) a -> (:.:) (Star f) (Star g) (f (g a)) a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (g a ~> g a) -> Star g (g a) a
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star g a ~> g a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id))
  counit :: forall a b. (Costar f :.: Costar g) a b -> a ~> b
  counit :: (Costar f :.: Costar g) :~> (~>)
counit (Costar f a ~> b
f :.: Costar g b ~> b
g) = case forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO j k) (q :: PRO k j) (a :: k).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @(Star f) @(Star g) @a of Star a ~> g b
g' :.: Star b ~> f a
f' -> g b ~> b
g (g b ~> b) -> (a ~> g b) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b ~> b) -> g b ~> g b
forall (a :: j) (b :: j). (a ~> b) -> g a ~> g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (f a ~> b
f (f a ~> b) -> (b ~> f a) -> b ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> f a
f') (g b ~> g b) -> (a ~> g b) -> a ~> g b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> g b
g'

instance (Adjunction l1 r1, Adjunction l2 r2) => Adjunction (l1 :.: l2) (r2 :.: r1) where
  unit :: forall a. (Ob a) => ((r2 :.: r1) :.: (l1 :.: l2)) a a
  unit :: forall (a :: k). Ob a => (:.:) (r2 :.: r1) (l1 :.: l2) a a
unit = case forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO j k) (q :: PRO k j) (a :: k).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @l2 @r2 @a of
    r2 a b
r2 :.: l2 b a
l2 ->
      l2 b a
l2 l2 b a
-> ((Ob b, Ob a) => (:.:) (r2 :.: r1) (l1 :.: l2) a a)
-> (:.:) (r2 :.: r1) (l1 :.: l2) a a
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO i j) (q :: PRO j i) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @l1 @r1 of
        r1 b b
r1 :.: l1 b b
l1 -> (r2 a b
r2 r2 a b -> r1 b b -> (:.:) r2 r1 a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r1 b b
r1) (:.:) r2 r1 a b
-> (:.:) l1 l2 b a -> (:.:) (r2 :.: r1) (l1 :.: l2) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (l1 b b
l1 l1 b b -> l2 b a -> (:.:) l1 l2 b a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: l2 b a
l2)
  counit :: ((l1 :.: l2) :.: (r2 :.: r1)) :~> (~>)
counit ((l1 a b
l1 :.: l2 b b
l2) :.: (r2 b b
r2 :.: r1 b b
r1)) = (:.:) l1 r1 a b -> a ~> b
(l1 :.: r1) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit ((b ~> b) -> l1 a b -> l1 a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((:.:) l2 r2 b b -> b ~> b
(l2 :.: r2) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (l2 b b
l2 l2 b b -> r2 b b -> (:.:) l2 r2 b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r2 b b
r2)) l1 a b
l1 l1 a b -> r1 b b -> (:.:) l1 r1 a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r1 b b
r1)

instance Adjunction (Star ((,) a)) (Star ((->) a)) where
  unit :: forall a. Ob a => (:.:) (Star ((->) a)) (Star ((,) a)) a a
unit = (a ~> (Star ((->) a) % (Star ((,) a) % a)))
-> (:.:) (Star ((->) a)) (Star ((,) a)) a a
forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i).
(Representable l, Representable r, Ob a) =>
(a ~> (r % (l % a))) -> (:.:) r l a a
unitFromRepUnit \a
a a
b -> (a
b, a
a)
  counit :: (Star ((,) a) :.: Star ((->) a)) :~> (~>)
counit = (forall c. Ob c => (Star ((,) a) % (Star ((->) a) % c)) ~> c)
-> (Star ((,) a) :.: Star ((->) a)) :~> (~>)
forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j).
(Representable l, Representable r) =>
(forall (c :: k1). Ob c => (l % (r % c)) ~> c)
-> (l :.: r) :~> (~>)
counitFromRepCounit \(a
a, a -> c
f) -> a -> c
f a
a

instance (CategoryOf k) => Adjunction (Id :: CAT k) Id where
  unit :: forall (a :: k). Ob a => (:.:) Id Id a a
unit = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Id a a -> Id a a -> (:.:) Id Id a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (Id :.: Id) :~> (~>)
counit (Id a ~> b
f :.: Id b ~> b
g) = b ~> b
g (b ~> b) -> (a ~> b) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f

instance Adjunction q p => Adjunction (Op p) (Op q) where
  unit :: forall (a :: OPPOSITE j). Ob a => (:.:) (Op q) (Op p) a a
unit = case forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @q @p of p (UN 'OP a) b
q :.: q b (UN 'OP a)
p -> q b (UN 'OP a) -> Op q ('OP (UN 'OP a)) ('OP b)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op q b (UN 'OP a)
p Op q a ('OP b) -> Op p ('OP b) a -> (:.:) (Op q) (Op p) a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p (UN 'OP a) b -> Op p ('OP b) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op p (UN 'OP a) b
q
  counit :: (Op p :.: Op q) :~> (~>)
counit (Op p b1 a1
q :.: Op q b1 a1
p) = (b1 ~> a1) -> Op (~>) ('OP a1) ('OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((:.:) q p b1 a1 -> b1 ~> a1
(q :.: p) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (q b1 a1
p q b1 a1 -> p a1 a1 -> (:.:) q p b1 a1
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b1 a1
p a1 a1
q))

instance (Adjunction p q) => Promonad (q :.: p) where
  id :: forall (a :: k). Ob a => (:.:) q p a a
id = (:.:) q p a a
forall (a :: k). Ob a => (:.:) q p a a
forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit
  (q b b
q :.: p b c
p) . :: forall (b :: k) (c :: k) (a :: k).
(:.:) q p b c -> (:.:) q p a b -> (:.:) q p a c
. (q a b
q' :.: p b b
p') = (b ~> b) -> q a b -> q a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((:.:) p q b b -> b ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (p b b
p' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q)) q a b
q' q a b -> p b c -> (:.:) q p a c
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b c
p

instance (Adjunction p q) => Procomonad (p :.: q) where
  extract :: (p :.: q) :~> (~>)
extract = (:.:) p q a b -> a ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit
  duplicate :: (p :.: q) :~> ((p :.: q) :.: (p :.: q))
duplicate (p a b
p :.: q b b
q) = p a b
p p a b
-> ((Ob a, Ob b) => (:.:) (p :.: q) (p :.: q) a b)
-> (:.:) (p :.: q) (p :.: q) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case (:.:) q p b b
forall (a :: j). Ob a => (:.:) q p a a
forall {j} {k} (p :: PRO k j) (q :: PRO j k) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit of q b b
q' :.: p b b
p' -> (p a b
p p a b -> q b b -> (:.:) p q a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q') (:.:) p q a b -> (:.:) p q b b -> (:.:) (p :.: q) (p :.: q) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (p b b
p' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q)

instance
  (MonoidalProfunctor r, Adjunction l r, Representable l, Representable r, Monoidal j, Monoidal k)
  => MonoidalProfunctor (RepCostar l :: j +-> k)
  where
  par0 :: RepCostar l Unit Unit
par0 = ((l % Unit) ~> Unit) -> RepCostar l Unit Unit
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
forall (p :: PRO j k) (q :: j +-> k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit @l @r (((l % Unit) ~> (l % Unit)) -> l (l % Unit) Unit
forall (b :: k) (a :: j). Ob b => (a ~> (l % b)) -> l a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: PRO j k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @l @Unit Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) l (l % Unit) Unit -> r Unit Unit -> (:.:) l r (l % Unit) Unit
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: r Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0)) ((Ob Unit, Ob Unit) => RepCostar l Unit Unit)
-> (Unit ~> Unit) -> RepCostar l Unit Unit
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 :: Obj (Unit :: k))
  RepCostar @x1 (l % x1) ~> x2
fx par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
RepCostar l x1 x2
-> RepCostar l y1 y2 -> RepCostar l (x1 ** y1) (x2 ** y2)
`par` RepCostar @y1 (l % y1) ~> y2
fy =
    ((l % x1) ~> x2
fx ((l % x1) ~> x2)
-> ((l % y1) ~> y2) -> ((l % x1) ** (l % y1)) ~> (x2 ** y2)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (l % y1) ~> y2
fy) (((l % x1) ** (l % y1)) ~> (x2 ** y2))
-> ((Ob ((l % x1) ** (l % y1)), Ob (x2 ** y2)) =>
    RepCostar l (x1 ** y1) (x2 ** y2))
-> RepCostar l (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
forall {k} (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
isObPar @x1 @y1 ((Ob (x1 ** y1) => RepCostar l (x1 ** y1) (x2 ** y2))
 -> RepCostar l (x1 ** y1) (x2 ** y2))
-> (Ob (x1 ** y1) => RepCostar l (x1 ** y1) (x2 ** y2))
-> RepCostar l (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
      ((l % (x1 ** y1)) ~> (x2 ** y2))
-> RepCostar l (x1 ** y1) (x2 ** y2)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (forall {k} {j} (l :: PRO k j) (r :: PRO j k) (a :: j) (b :: k).
(Adjunction l r, Representable l, Representable r, Ob b) =>
r a b -> (l % a) ~> b
forall (l :: PRO j k) (r :: j +-> k) (a :: k) (b :: j).
(Adjunction l r, Representable l, Representable r, Ob b) =>
r a b -> (l % a) ~> b
rightAdjunct @l @r (forall {k} {j} (l :: PRO k j) (r :: PRO j k) (a :: j) (b :: k).
(Adjunction l r, Representable l, Representable r, Ob a) =>
((l % a) ~> b) -> r a b
forall (l :: PRO j k) (r :: j +-> k) (a :: k) (b :: j).
(Adjunction l r, Representable l, Representable r, Ob a) =>
((l % a) ~> b) -> r a b
leftAdjunct @l @r @x1 (l % x1) ~> x2
fx r x1 x2 -> r y1 y2 -> r (x1 ** y1) (x2 ** y2)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
r x1 x2 -> r y1 y2 -> r (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall {k} {j} (l :: PRO k j) (r :: PRO j k) (a :: j) (b :: k).
(Adjunction l r, Representable l, Representable r, Ob a) =>
((l % a) ~> b) -> r a b
forall (l :: PRO j k) (r :: j +-> k) (a :: k) (b :: j).
(Adjunction l r, Representable l, Representable r, Ob a) =>
((l % a) ~> b) -> r a b
leftAdjunct @l @r @y1 (l % y1) ~> y2
fy))