{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Redundant map" #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Adjunction where

import Proarrow.Core (CAT, PRO, Profunctor(..), Promonad (..), CategoryOf(..), (:~>), (//), rmap)
import Proarrow.Functor (Functor(..))
import Data.Kind (Constraint)
import Proarrow.Profunctor.Composition ((:.:)(..))
import Proarrow.Profunctor.Identity (Id(..))
import Proarrow.Profunctor.Star (Star(..))
import Proarrow.Profunctor.Costar (Costar(..))

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 :~> (~>)

leftAdjunct
  :: forall l r a b. (Adjunction (Star l) (Star r), Functor r)
  => Ob a => (l a ~> b) -> (a ~> r b)
leftAdjunct :: forall {k} {k} (l :: k -> k) (r :: k -> k) (a :: k) (b :: k).
(Adjunction (Star l) (Star r), Functor r, Ob a) =>
(l a ~> b) -> a ~> r 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 k) (q :: PRO k k) (a :: k).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @(Star l) @(Star r) @a of Star a ~> r b
r :.: Star b ~> l a
l -> (b ~> b) -> r b ~> r b
forall (a :: k) (b :: k). (a ~> b) -> r a ~> r b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (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
. b ~> l a
l) (r b ~> r b) -> (a ~> r b) -> a ~> r 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 ~> r b
r

rightAdjunct
  :: forall l r a b. (Adjunction (Star l) (Star r), Functor l)
  => Ob b => (a ~> r b) -> (l a ~> b)
rightAdjunct :: forall {k} {k} (l :: k -> k) (r :: k -> k) (a :: k) (b :: k).
(Adjunction (Star l) (Star r), Functor l, Ob b) =>
(a ~> r b) -> l a ~> b
rightAdjunct a ~> r b
f = (:.:) (Star l) (Star r) (l a) b -> l a ~> b
(Star l :.: Star r) :~> (~>)
forall {j} {k} (p :: PRO k j) (q :: PRO j k).
Adjunction p q =>
(p :.: q) :~> (~>)
counit ((l a ~> l a) -> Star l (l a) a
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a ~> a) -> l a ~> l a
forall (a :: k) (b :: k). (a ~> b) -> l a ~> l b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map 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) Star l (l a) a -> Star r a b -> (:.:) (Star l) (Star r) (l a) b
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> r b) -> Star r a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star a ~> r b
f) ((Ob a, Ob (r b)) => l a ~> b) -> (a ~> r b) -> l a ~> b
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
\\ a ~> r b
f

unitFromStarUnit
  :: forall l r a. (Functor l, Ob a) => (a ~> r (l a)) -> (Star r :.: Star l) a a
unitFromStarUnit :: forall {k} {k2} (l :: k -> k2) (r :: k2 -> k) (a :: k).
(Functor l, Ob a) =>
(a ~> r (l a)) -> (:.:) (Star r) (Star l) a a
unitFromStarUnit a ~> r (l a)
f = (a ~> r (l a)) -> Star r a (l a)
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star a ~> r (l a)
f Star r a (l a) -> Star l (l a) a -> (:.:) (Star r) (Star l) a a
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: (l a ~> l a) -> Star l (l a) a
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star l a ~> l a
forall (a :: k2). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

counitFromStarCounit
  :: Functor l => (forall c. Ob c => l (r c) ~> c) -> (Star l :.: Star r) a b -> (a ~> b)
counitFromStarCounit :: forall {j} {k} (l :: j -> k) (r :: k -> j) (a :: k) (b :: k).
Functor l =>
(forall (c :: k). Ob c => l (r c) ~> c)
-> (:.:) (Star l) (Star r) a b -> a ~> b
counitFromStarCounit forall (c :: k). Ob c => l (r c) ~> c
f (Star a ~> l b
l :.: Star b ~> r b
r) = l (r b) ~> b
forall (c :: k). Ob c => l (r c) ~> c
f (l (r b) ~> b) -> (a ~> l (r 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 ~> r b) -> l b ~> l (r b)
forall (a :: j) (b :: j). (a ~> b) -> l a ~> l b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map b ~> r b
r (l b ~> l (r b)) -> (a ~> l b) -> a ~> l (r 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 ~> l b
l

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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 (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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 :: i). 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 i) (q :: PRO i j) (a :: i).
(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 k j) (q :: PRO j k) (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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 ~> (a -> (a, a))) -> (:.:) (Star ((->) a)) (Star ((,) a)) a a
forall {k} {k2} (l :: k -> k2) (r :: k2 -> k) (a :: k).
(Functor l, Ob a) =>
(a ~> r (l a)) -> (:.:) (Star r) (Star l) a a
unitFromStarUnit \a
a a
b -> (a
b, a
a)
  counit :: (Star ((,) a) :.: Star ((->) a)) :~> (~>)
counit = (forall c. Ob c => (a, a -> c) ~> c)
-> (:.:) (Star ((,) a)) (Star ((->) a)) a b -> a ~> b
forall {j} {k} (l :: j -> k) (r :: k -> j) (a :: k) (b :: k).
Functor l =>
(forall (c :: k). Ob c => l (r c) ~> c)
-> (:.:) (Star l) (Star r) a b -> a ~> b
counitFromStarCounit \(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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
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 {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: p b c
p