module Proarrow.Category.Bicategory.MonoidalAsBi where

import Prelude (type (~))

import Proarrow.Category.Bicategory (Adjunction (..), Bicategory (..), Comonad (..), Monad (..))
import Proarrow.Category.Bicategory.Kan (LeftKanExtension (..), RightKanExtension (..), RightKanLift (..), LeftKanLift (..))
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..))
import Proarrow.Category.Monoidal (SymMonoidal)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, obj)
import Proarrow.Monoid qualified as M
import Proarrow.Object.Coexponential (Coclosed (..), coeval, coevalUniv)
import Proarrow.Object.Exponential (Closed (..), curry, eval)
import Proarrow.Object.Exponential qualified as M
import Proarrow.Object.Dual qualified as M
import Proarrow.Category.Equipment.Limit (HasLimits (..), HasColimits (..))

type MonK :: Kind -> CAT ()
newtype MonK k i j = MK k
type instance UN MK (MK k) = k

type Mon2 :: forall {k} {i} {j}. CAT (MonK k i j)
data Mon2 a b where
  Mon2 :: a ~> b -> Mon2 (MK a) (MK b)
  deriving (CategoryOf (MonK k i j)
(CategoryOf (MonK k i j), CategoryOf (MonK k i j)) =>
(forall (c :: MonK k i j) (a :: MonK k i j) (b :: MonK k i j)
        (d :: MonK k i j).
 (c ~> a) -> (b ~> d) -> Mon2 a b -> Mon2 c d)
-> (forall (a :: MonK k i j) (b :: MonK k i j) r.
    ((Ob a, Ob b) => r) -> Mon2 a b -> r)
-> Profunctor Mon2
forall {j} {k} (p :: PRO j k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: j) (a :: j) (b :: k) (d :: k).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
forall k (i :: ()) (j :: ()).
CategoryOf k =>
CategoryOf (MonK k i j)
forall k (i :: ()) (j :: ()) (a :: MonK k i j) (b :: MonK k i j) r.
CategoryOf k =>
((Ob a, Ob b) => r) -> Mon2 a b -> r
forall k (i :: ()) (j :: ()) (c :: MonK k i j) (a :: MonK k i j)
       (b :: MonK k i j) (d :: MonK k i j).
CategoryOf k =>
(c ~> a) -> (b ~> d) -> Mon2 a b -> Mon2 c d
forall (a :: MonK k i j) (b :: MonK k i j) r.
((Ob a, Ob b) => r) -> Mon2 a b -> r
forall (c :: MonK k i j) (a :: MonK k i j) (b :: MonK k i j)
       (d :: MonK k i j).
(c ~> a) -> (b ~> d) -> Mon2 a b -> Mon2 c d
$cdimap :: forall k (i :: ()) (j :: ()) (c :: MonK k i j) (a :: MonK k i j)
       (b :: MonK k i j) (d :: MonK k i j).
CategoryOf k =>
(c ~> a) -> (b ~> d) -> Mon2 a b -> Mon2 c d
dimap :: forall (c :: MonK k i j) (a :: MonK k i j) (b :: MonK k i j)
       (d :: MonK k i j).
(c ~> a) -> (b ~> d) -> Mon2 a b -> Mon2 c d
$c\\ :: forall k (i :: ()) (j :: ()) (a :: MonK k i j) (b :: MonK k i j) r.
CategoryOf k =>
((Ob a, Ob b) => r) -> Mon2 a b -> r
\\ :: forall (a :: MonK k i j) (b :: MonK k i j) r.
((Ob a, Ob b) => r) -> Mon2 a b -> r
Profunctor, Profunctor Mon2
Profunctor Mon2 =>
(forall (a :: MonK k i j). Ob a => Mon2 a a)
-> (forall (b :: MonK k i j) (c :: MonK k i j) (a :: MonK k i j).
    Mon2 b c -> Mon2 a b -> Mon2 a c)
-> Promonad Mon2
forall k (i :: ()) (j :: ()). CategoryOf k => Profunctor Mon2
forall k (i :: ()) (j :: ()) (a :: MonK k i j).
(CategoryOf k, Ob a) =>
Mon2 a a
forall k (i :: ()) (j :: ()) (b :: MonK k i j) (c :: MonK k i j)
       (a :: MonK k i j).
CategoryOf k =>
Mon2 b c -> Mon2 a b -> Mon2 a c
forall {k} (p :: PRO k k).
Profunctor p =>
(forall (a :: k). Ob a => p a a)
-> (forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c)
-> Promonad p
forall (a :: MonK k i j). Ob a => Mon2 a a
forall (b :: MonK k i j) (c :: MonK k i j) (a :: MonK k i j).
Mon2 b c -> Mon2 a b -> Mon2 a c
$cid :: forall k (i :: ()) (j :: ()) (a :: MonK k i j).
(CategoryOf k, Ob a) =>
Mon2 a a
id :: forall (a :: MonK k i j). Ob a => Mon2 a a
$c. :: forall k (i :: ()) (j :: ()) (b :: MonK k i j) (c :: MonK k i j)
       (a :: MonK k i j).
CategoryOf k =>
Mon2 b c -> Mon2 a b -> Mon2 a c
. :: forall (b :: MonK k i j) (c :: MonK k i j) (a :: MonK k i j).
Mon2 b c -> Mon2 a b -> Mon2 a c
Promonad) via (~>)

instance (CategoryOf k) => CategoryOf (MonK k i j) where
  type (~>) = Mon2
  type Ob a = (Is MK a, Ob (UN MK a))

-- | A monoidal category as a bicategory.
instance (M.Monoidal k) => Bicategory (MonK k) where
  type I = MK M.Unit
  type MK a `O` MK b = MK (a M.** b)
  iObj :: forall (i :: ()). Ob0 (MonK k) i => Obj I
iObj = (Unit ~> Unit) -> Mon2 ('MK Unit) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
M.par0
  Mon2 a ~> b
f o :: forall {i :: ()} (j :: ()) (k :: ()) (a :: MonK k j k)
       (b :: MonK k j k) (c :: MonK k i j) (d :: MonK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` Mon2 a ~> b
g = ((a ** a) ~> (b ** b)) -> Mon2 ('MK (a ** a)) ('MK (b ** b))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (a ~> b
f (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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)
`M.par` a ~> b
g)
  (Ob0 (MonK k) i, Ob0 (MonK k) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: ()) (j :: ()) (ps :: MonK k i j) (qs :: MonK k i j) r.
((Ob0 (MonK k) i, Ob0 (MonK k) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ Mon2 a ~> b
f = r
(Ob a, Ob b) => r
(Ob0 (MonK k) i, Ob0 (MonK k) j, Ob ps, Ob qs) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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 ~> b
f
  leftUnitor :: forall {i :: ()} {j :: ()} (a :: MonK k i j).
(Ob0 (MonK k) i, Ob0 (MonK k) j, Ob a) =>
O I a ~> a
leftUnitor = ((Unit ** UN 'MK a) ~> UN 'MK a)
-> Mon2 ('MK (Unit ** UN 'MK a)) ('MK (UN 'MK a))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Unit ** UN 'MK a) ~> UN 'MK a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
M.leftUnitor
  leftUnitorInv :: forall {i :: ()} {j :: ()} (a :: MonK k i j).
(Ob0 (MonK k) i, Ob0 (MonK k) j, Ob a) =>
a ~> O I a
leftUnitorInv = (UN 'MK a ~> (Unit ** UN 'MK a))
-> Mon2 ('MK (UN 'MK a)) ('MK (Unit ** UN 'MK a))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 UN 'MK a ~> (Unit ** UN 'MK a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
M.leftUnitorInv
  rightUnitor :: forall {i :: ()} {j :: ()} (a :: MonK k i j).
(Ob0 (MonK k) i, Ob0 (MonK k) j, Ob a) =>
O a I ~> a
rightUnitor = ((UN 'MK a ** Unit) ~> UN 'MK a)
-> Mon2 ('MK (UN 'MK a ** Unit)) ('MK (UN 'MK a))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (UN 'MK a ** Unit) ~> UN 'MK a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
M.rightUnitor
  rightUnitorInv :: forall {i :: ()} {j :: ()} (a :: MonK k i j).
(Ob0 (MonK k) i, Ob0 (MonK k) j, Ob a) =>
a ~> O a I
rightUnitorInv = (UN 'MK a ~> (UN 'MK a ** Unit))
-> Mon2 ('MK (UN 'MK a)) ('MK (UN 'MK a ** Unit))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 UN 'MK a ~> (UN 'MK a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
M.rightUnitorInv
  associator :: forall {h :: ()} {i :: ()} {j :: ()} {k :: ()} (a :: MonK k j k)
       (b :: MonK k i j) (c :: MonK k h i).
(Ob0 (MonK k) h, Ob0 (MonK k) i, Ob0 (MonK k) j, Ob0 (MonK k) k,
 Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @(MK a) @(MK b) @(MK c) = (((UN 'MK a ** UN 'MK b) ** UN 'MK c)
 ~> (UN 'MK a ** (UN 'MK b ** UN 'MK c)))
-> Mon2
     ('MK ((UN 'MK a ** UN 'MK b) ** UN 'MK c))
     ('MK (UN 'MK a ** (UN 'MK b ** UN 'MK c)))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
M.associator @k @a @b @c)
  associatorInv :: forall {h :: ()} {i :: ()} {j :: ()} {k :: ()} (a :: MonK k j k)
       (b :: MonK k i j) (c :: MonK k h i).
(Ob0 (MonK k) h, Ob0 (MonK k) i, Ob0 (MonK k) j, Ob0 (MonK k) k,
 Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @(MK a) @(MK b) @(MK c) = ((UN 'MK a ** (UN 'MK b ** UN 'MK c))
 ~> ((UN 'MK a ** UN 'MK b) ** UN 'MK c))
-> Mon2
     ('MK (UN 'MK a ** (UN 'MK b ** UN 'MK c)))
     ('MK ((UN 'MK a ** UN 'MK b) ** UN 'MK c))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
M.associatorInv @k @a @b @c)

-- | Monoids in a monoidal category are monads when the monoidal category is seen as a bicategory.
instance (M.Monoid m) => Monad (MK m) where
  eta :: I ~> 'MK m
eta = (Unit ~> m) -> Mon2 ('MK Unit) ('MK m)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
M.mempty
  mu :: O ('MK m) ('MK m) ~> 'MK m
mu = ((m ** m) ~> m) -> Mon2 ('MK (m ** m)) ('MK m)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
M.mappend

-- | Comonoids in a monoidal category are comonads when the monoidal category is seen as a bicategory.
instance (M.Comonoid m) => Comonad (MK m) where
  epsilon :: 'MK m ~> I
epsilon = (m ~> Unit) -> Mon2 ('MK m) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 m ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
M.counit
  delta :: 'MK m ~> O ('MK m) ('MK m)
delta = (m ~> (m ** m)) -> Mon2 ('MK m) ('MK (m ** m))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 m ~> (m ** m)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
M.comult

instance (M.Monoidal k) => HasCompanions (MonK k) (MonK k) where
  type Companion (MonK k) (MK a) = MK a
  mapCompanion :: forall {j :: ()} {k :: ()} (f :: MonK k j k) (g :: MonK k j k).
(f ~> g) -> Companion (MonK k) f ~> Companion (MonK k) g
mapCompanion (Mon2 a ~> b
f) = (a ~> b) -> Mon2 ('MK a) ('MK b)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 a ~> b
f
  compToId :: forall (k :: ()). Ob0 (MonK k) k => Companion (MonK k) I ~> I
compToId = (Unit ~> Unit) -> Mon2 ('MK Unit) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 Unit ~> Unit
forall k. Monoidal k => Obj Unit
M.unitObj
  compFromId :: forall (k :: ()). Ob0 (MonK k) k => I ~> Companion (MonK k) I
compFromId = (Unit ~> Unit) -> Mon2 ('MK Unit) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 Unit ~> Unit
forall k. Monoidal k => Obj Unit
M.unitObj
  compToCompose :: forall {i :: ()} {j :: ()} {k :: ()} (f :: MonK k j k)
       (g :: MonK k i j).
Obj f
-> Obj g
-> Companion (MonK k) (O f g)
   ~> O (Companion (MonK k) f) (Companion (MonK k) g)
compToCompose (Mon2 a ~> b
f) (Mon2 a ~> b
g) = ((b ** b) ~> (b ** b)) -> Mon2 ('MK (b ** b)) ('MK (b ** b))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (a ~> b
b ~> b
f (b ~> b) -> (b ~> b) -> (b ** b) ~> (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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)
`M.par` a ~> b
b ~> b
g)
  compFromCompose :: forall {j1 :: ()} {j2 :: ()} {k :: ()} (f :: MonK k j2 k)
       (g :: MonK k j1 j2).
Obj f
-> Obj g
-> O (Companion (MonK k) f) (Companion (MonK k) g)
   ~> Companion (MonK k) (O f g)
compFromCompose (Mon2 a ~> b
f) (Mon2 a ~> b
g) = ((b ** b) ~> (b ** b)) -> Mon2 ('MK (b ** b)) ('MK (b ** b))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (a ~> b
b ~> b
f (b ~> b) -> (b ~> b) -> (b ** b) ~> (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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)
`M.par` a ~> b
b ~> b
g)

instance (M.CompactClosed k, Ob (a :: k), b ~ M.Dual a) => Adjunction (MK a) (MK b) where
  unit :: I ~> O ('MK b) ('MK a)
unit = (Unit ~> (b ** a)) -> Mon2 ('MK Unit) ('MK (b ** a))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @a @b ((a ** b) ~> (b ** a)) -> (Unit ~> (a ** b)) -> Unit ~> (b ** a)
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
. forall (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
M.dualityUnit @a) ((Ob b, Ob b) => Mon2 ('MK Unit) ('MK (b ** a)))
-> (b ~> b) -> Mon2 ('MK Unit) ('MK (b ** a))
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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
M.dual @a
  counit :: O ('MK a) ('MK b) ~> I
counit = ((a ** b) ~> Unit) -> Mon2 ('MK (a ** b)) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k).
(SymMonoidal k, StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Bottom
forall {k} (a :: k).
(SymMonoidal k, StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Bottom
M.dualityCounit @a ((b ** a) ~> Unit) -> ((a ** b) ~> (b ** a)) -> (a ** b) ~> Unit
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
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @a @b) ((Ob b, Ob b) => Mon2 ('MK (a ** b)) ('MK Unit))
-> (b ~> b) -> Mon2 ('MK (a ** b)) ('MK 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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
M.dual @a

instance (M.CompactClosed k) => Equipment (MonK k) (MonK k) where
  type Conjoint (MonK k) (MK a) = MK (M.Dual a)
  mapConjoint :: forall {j :: ()} {k :: ()} (f :: MonK k j k) (g :: MonK k j k).
(f ~> g) -> Conjoint (MonK k) g ~> Conjoint (MonK k) f
mapConjoint (Mon2 a ~> b
f) = ((b ~~> Unit) ~> (a ~~> Unit))
-> Mon2 ('MK (b ~~> Unit)) ('MK (a ~~> Unit))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 ((a ~> b) -> Dual b ~> Dual a
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
M.dual' a ~> b
f)
  conjToId :: forall (k :: ()). Ob0 (MonK k) k => Conjoint (MonK k) I ~> I
conjToId = ((Unit ~~> Unit) ~> Unit) -> Mon2 ('MK (Unit ~~> Unit)) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
M.eval @M.Unit (((Unit ~~> Unit) ** Unit) ~> Unit)
-> ((Unit ~~> Unit) ~> ((Unit ~~> Unit) ** Unit))
-> (Unit ~~> Unit) ~> Unit
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
. forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
M.rightUnitorInv @_ @(M.Dual M.Unit)) ((Ob Unit, Ob Unit) => Mon2 ('MK (Unit ~~> Unit)) ('MK Unit))
-> (Unit ~> Unit) -> Mon2 ('MK (Unit ~~> Unit)) ('MK 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
\\ forall k. Monoidal k => Obj Unit
M.unitObj @k ((Ob (Unit ~~> Unit), Ob (Unit ~~> Unit)) =>
 Mon2 ('MK (Unit ~~> Unit)) ('MK Unit))
-> ((Unit ~~> Unit) ~> (Unit ~~> Unit))
-> Mon2 ('MK (Unit ~~> Unit)) ('MK 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
\\ (forall k. Monoidal k => Obj Unit
M.unitObj @k (Unit ~> Unit)
-> (Unit ~> Unit) -> (Unit ~~> Unit) ~> (Unit ~~> Unit)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall k. Monoidal k => Obj Unit
M.unitObj @k)
  conjFromId :: forall (k :: ()). Ob0 (MonK k) k => I ~> Conjoint (MonK k) I
conjFromId = (Unit ~> (Unit ~~> Unit)) -> Mon2 ('MK Unit) ('MK (Unit ~~> Unit))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 ((Unit ~> Unit) -> Unit ~> (Unit ~~> Unit)
forall {k} (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> (a ~~> b)
M.mkExponential Unit ~> Unit
forall k. Monoidal k => Obj Unit
M.unitObj)
  conjToCompose :: forall {k1 :: ()} {j :: ()} {k2 :: ()} (f :: MonK k j k2)
       (g :: MonK k k1 j).
Obj f
-> Obj g
-> Conjoint (MonK k) (O f g)
   ~> O (Conjoint (MonK k) g) (Conjoint (MonK k) f)
conjToCompose (Mon2 a ~> b
f) (Mon2 a ~> b
g) = (((b ** b) ~~> Unit) ~> ((b ~~> Unit) ** (b ~~> Unit)))
-> Mon2
     ('MK ((b ** b) ~~> Unit)) ('MK ((b ~~> Unit) ** (b ~~> Unit)))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 ((b ~> b) -> (b ~> b) -> Dual (b ** b) ~> (Dual b ** Dual b)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
CompactClosed k =>
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
M.distribDual' a ~> b
b ~> b
g a ~> b
b ~> b
f (((b ** b) ~~> Unit) ~> ((b ~~> Unit) ** (b ~~> Unit)))
-> (((b ** b) ~~> Unit) ~> ((b ** b) ~~> Unit))
-> ((b ** b) ~~> Unit) ~> ((b ~~> Unit) ** (b ~~> Unit))
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) ~> (b ** b)) -> Dual (b ** b) ~> Dual (b ** b)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
M.dual' (a ~> b
b ~> b
g (b ~> b) -> (b ~> b) -> (b ** b) ~> (b ** b)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
`M.swap'` a ~> b
b ~> b
f)))
  conjFromCompose :: forall {j1 :: ()} {j2 :: ()} {k :: ()} (f :: MonK k j2 k)
       (g :: MonK k j1 j2).
Obj f
-> Obj g
-> O (Conjoint (MonK k) g) (Conjoint (MonK k) f)
   ~> Conjoint (MonK k) (O f g)
conjFromCompose (Mon2 a ~> b
f) (Mon2 a ~> b
g) = (((b ~~> Unit) ** (b ~~> Unit)) ~> ((b ** b) ~~> Unit))
-> Mon2
     ('MK ((b ~~> Unit) ** (b ~~> Unit))) ('MK ((b ** b) ~~> Unit))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 ((((b ** b) ~> (b ** b)) -> Dual (b ** b) ~> Dual (b ** b)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
M.dual' (a ~> b
b ~> b
f (b ~> b) -> (b ~> b) -> (b ** b) ~> (b ** b)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
`M.swap'` a ~> b
b ~> b
g)) (((b ** b) ~~> Unit) ~> ((b ** b) ~~> Unit))
-> (((b ~~> Unit) ** (b ~~> Unit)) ~> ((b ** b) ~~> Unit))
-> ((b ~~> Unit) ** (b ~~> Unit)) ~> ((b ** b) ~~> Unit)
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) -> (b ~> b) -> (Dual b ** Dual b) ~> Dual (b ** b)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
CompactClosed k =>
(a ~> a') -> (b ~> b') -> (Dual a' ** Dual b') ~> Dual (a ** b)
M.combineDual' a ~> b
b ~> b
g a ~> b
b ~> b
f)

instance (Closed k, Ob j) => HasLimits (MonK k) (MK (j :: k)) '() where
  type Limit (MK j) (MK d) = MK (j ~~> d)
  limitObj :: forall (d :: MonK k i '()). Ob d => Obj (Limit ('MK j) d)
limitObj @(MK d) = ((j ~~> UN 'MK d) ~> (j ~~> UN 'MK d))
-> Mon2 ('MK (j ~~> UN 'MK d)) ('MK (j ~~> UN 'MK d))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d Obj (UN 'MK d) -> (j ~> j) -> (j ~~> UN 'MK d) ~> (j ~~> UN 'MK d)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j)
  limit :: forall (d :: MonK k i '()).
Ob d =>
O (Companion (MonK k) (Limit ('MK j) d)) ('MK j)
~> Companion (MonK k) d
limit @(MK d) = (((j ~~> UN 'MK d) ** j) ~> UN 'MK d)
-> Mon2 ('MK ((j ~~> UN 'MK d) ** j)) ('MK (UN 'MK d))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @j @d)
  limitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()).
(Ob d, Ob p) =>
(O (Companion (MonK k) p) ('MK j) ~> Companion (MonK k) d)
-> p ~> Limit ('MK j) d
limitUniv @_ @(MK p) (Mon2 a ~> b
pj2d) = (UN 'MK p ~> (j ~~> UN 'MK d))
-> Mon2 ('MK (UN 'MK p)) ('MK (j ~~> UN 'MK d))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @p @j a ~> b
(UN 'MK p ** j) ~> UN 'MK d
pj2d)

instance (M.Monoidal k, Ob j) => HasColimits (MonK k) (MK (j :: k)) '() where
  type Colimit (MK j) (MK d) = MK (d M.** j)
  colimit :: forall (d :: MonK k i '()).
Ob d =>
O (Companion (MonK k) d) ('MK j)
~> Companion (MonK k) (Colimit ('MK j) d)
colimit @(MK d) = ((UN 'MK d ** j) ~> (UN 'MK d ** j))
-> Mon2 ('MK (UN 'MK d ** j)) ('MK (UN 'MK d ** j))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d Obj (UN 'MK d) -> (j ~> j) -> (UN 'MK d ** j) ~> (UN 'MK d ** j)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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)
`M.par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j)
  colimitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()).
(Ob d, Ob p) =>
(O (Companion (MonK k) d) ('MK j) ~> Companion (MonK k) p)
-> Colimit ('MK j) d ~> p
colimitUniv (Mon2 a ~> b
f) = (a ~> UN 'MK p) -> Mon2 ('MK a) ('MK (UN 'MK p))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 a ~> b
a ~> UN 'MK p
f

instance (Closed k, Ob (p ~~> q), Ob p, Ob q) => RightKanExtension (MK (p :: k)) (MK (q :: k)) where
  type Ran (MK p) (MK q) = MK (p ~~> q)
  ran :: O (Ran ('MK p) ('MK q)) ('MK p) ~> 'MK q
ran = (((p ~~> q) ** p) ~> q) -> Mon2 ('MK ((p ~~> q) ** p)) ('MK q)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @p @q)
  ranUniv :: forall (g :: MonK k d e).
Ob g =>
(O g ('MK p) ~> 'MK q) -> g ~> Ran ('MK p) ('MK q)
ranUniv @(MK g) (Mon2 a ~> b
f) = (UN 'MK g ~> (p ~~> q)) -> Mon2 ('MK (UN 'MK g)) ('MK (p ~~> q))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @g @p @q a ~> b
(UN 'MK g ** p) ~> q
f)

instance (Closed k, SymMonoidal k, Ob (p ~~> q), Ob p, Ob q) => RightKanLift (MK (p :: k)) (MK (q :: k)) where
  type Rift (MK p) (MK q) = MK (p ~~> q)
  rift :: O ('MK p) (Rift ('MK p) ('MK q)) ~> 'MK q
rift = ((p ** (p ~~> q)) ~> q) -> Mon2 ('MK (p ** (p ~~> q))) ('MK q)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @p @q (((p ~~> q) ** p) ~> q)
-> ((p ** (p ~~> q)) ~> ((p ~~> q) ** p)) -> (p ** (p ~~> q)) ~> q
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
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @p @(p ~~> q))
  riftUniv :: forall (g :: MonK k e d).
Ob g =>
(O ('MK p) g ~> 'MK q) -> g ~> Rift ('MK p) ('MK q)
riftUniv @(MK g) (Mon2 a ~> b
f) = (UN 'MK g ~> (p ~~> q)) -> Mon2 ('MK (UN 'MK g)) ('MK (p ~~> q))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @g @p @q (a ~> q
a ~> b
f (a ~> q) -> ((UN 'MK g ** p) ~> a) -> (UN 'MK g ** p) ~> q
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
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @g @p))

instance (Coclosed k, Ob (q <~~ p), Ob p, Ob q) => LeftKanExtension (MK (p :: k)) (MK (q :: k)) where
  type Lan (MK p) (MK q) = MK (q <~~ p)
  lan :: 'MK q ~> O (Lan ('MK p) ('MK q)) ('MK p)
lan = (q ~> ((q <~~ p) ** p)) -> Mon2 ('MK q) ('MK ((q <~~ p) ** p))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
forall {k} (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
coeval @q @p)
  lanUniv :: forall (g :: MonK k d e).
Ob g =>
('MK q ~> O g ('MK p)) -> Lan ('MK p) ('MK q) ~> g
lanUniv @(MK g) (Mon2 a ~> b
f) = ((q <~~ p) ~> UN 'MK g) -> Mon2 ('MK (q <~~ p)) ('MK (UN 'MK g))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k) (c :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
forall {k} (a :: k) (b :: k) (c :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv @q @p @g q ~> (UN 'MK g ** p)
a ~> b
f)

instance (Coclosed k, SymMonoidal k, Ob (q <~~ p), Ob p, Ob q) => LeftKanLift (MK (p :: k)) (MK (q :: k)) where
  type Lift (MK p) (MK q) = MK (q <~~ p)
  lift :: 'MK q ~> O ('MK p) (Lift ('MK p) ('MK q))
lift = (q ~> (p ** (q <~~ p))) -> Mon2 ('MK q) ('MK (p ** (q <~~ p)))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @(q <~~ p) @p (((q <~~ p) ** p) ~> (p ** (q <~~ p)))
-> (q ~> ((q <~~ p) ** p)) -> q ~> (p ** (q <~~ p))
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
. forall (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
forall {k} (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
coeval @q @p)
  liftUniv :: forall (g :: MonK k e d).
Ob g =>
('MK q ~> O ('MK p) g) -> Lift ('MK p) ('MK q) ~> g
liftUniv @(MK g) (Mon2 a ~> b
f) = ((q <~~ p) ~> UN 'MK g) -> Mon2 ('MK (q <~~ p)) ('MK (UN 'MK g))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k) (b :: k) (c :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
forall {k} (a :: k) (b :: k) (c :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv @q @p @g (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @p @g (b ~> (UN 'MK g ** p)) -> (q ~> b) -> q ~> (UN 'MK g ** p)
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
. q ~> b
a ~> b
f))