module Proarrow.Category.Bicategory.MonoidalAsBi where

import Proarrow.Category.Bicategory (Adj (..), Bicategory (..), Comonad (..), Monad (..), flipLeftAdjoint, withAdj)
import Proarrow.Category.Bicategory.Kan
  ( LeftKanExtension (..)
  , LeftKanLift (..)
  , RightKanExtension (..)
  , RightKanLift (..)
  )
import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), IsOb, Tight, TightAdjoint, WithObO2 (..))
import Proarrow.Category.Equipment.Limit (HasColimits (..), HasLimits (..))
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.Functor (Functor (..))
import Proarrow.Monoid qualified as M
import Proarrow.Object.Coexponential (Coclosed (..), coeval, coevalUniv)
import Proarrow.Object.Dual qualified as M
import Proarrow.Object.Exponential (Closed (..))

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 :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (a :: k) (b :: j) 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 :: 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))

instance (CategoryOf k) => Functor (MK :: k -> MonK k i j) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> 'MK a ~> 'MK b
map = (a ~> b) -> 'MK a ~> 'MK b
(a ~> b) -> Mon2 ('MK a) ('MK b)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2

-- | 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)
  withOb2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: MonK k j k)
       (b :: MonK k i j) r.
(Ob a, Ob b, Ob0 (MonK k) i, Ob0 (MonK k) j, Ob0 (MonK k) k) =>
(Ob (O a b) => r) -> r
withOb2 @(MK a) @(MK b) Ob (O a b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (UN 'MK a ** UN 'MK b) => r
Ob (O a b) => r
r
  withOb0s :: forall {j :: ()} {k :: ()} (a :: MonK k j k) r.
Ob a =>
((Ob0 (MonK k) j, Ob0 (MonK k) k) => r) -> r
withOb0s (Ob0 (MonK k) j, Ob0 (MonK k) k) => r
r = r
(Ob0 (MonK k) j, Ob0 (MonK k) k) => r
r
  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 :: j +-> k) (a :: k) (b :: j) 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

dualAdj :: forall {k} a. (M.CompactClosed k, Ob (a :: k)) => Adj (MK (M.Dual a)) (MK a)
dualAdj :: forall {c :: ()} {d :: ()} {k} (a :: k).
(CompactClosed k, Ob a) =>
Adj ('MK (Dual a)) ('MK a)
dualAdj = Adj{adjUnit :: I ~> O ('MK a) ('MK (Dual a))
adjUnit = (Unit ~> (a ** Dual a)) -> Mon2 ('MK Unit) ('MK (a ** Dual a))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (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), adjCounit :: O ('MK (Dual a)) ('MK a) ~> I
adjCounit = ((Dual a ** a) ~> Unit) -> Mon2 ('MK (Dual a ** a)) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
M.dualityCounit @a)}

dualAdj' :: forall {k} a. (M.CompactClosed k, Ob (a :: k)) => Adj (MK a) (MK (M.Dual a))
dualAdj' :: forall {c :: ()} {d :: ()} {k} (a :: k).
(CompactClosed k, Ob a) =>
Adj ('MK a) ('MK (Dual a))
dualAdj' =
  Adj
    { adjUnit :: I ~> O ('MK (Dual a)) ('MK a)
adjUnit = (Unit ~> (Dual a ** a)) -> Mon2 ('MK Unit) ('MK (Dual a ** a))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @a @(M.Dual a) ((a ** Dual a) ~> (Dual a ** a))
-> (Unit ~> (a ** Dual a)) -> Unit ~> (Dual a ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: 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)
    , adjCounit :: O ('MK a) ('MK (Dual a)) ~> I
adjCounit = ((a ** Dual a) ~> Unit) -> Mon2 ('MK (a ** Dual a)) ('MK Unit)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
M.dualityCounit @a ((Dual a ** a) ~> Unit)
-> ((a ** Dual a) ~> (Dual a ** a)) -> (a ** Dual a) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @a @(M.Dual a))
    }

type Dual a = MK (M.Dual (UN MK a))

type instance IsOb Tight (MK a) = ()
type instance IsOb Cotight (MK a) = ()
type instance TightAdjoint a = Dual a
type instance CotightAdjoint a = Dual a
instance (M.Monoidal k) => WithObO2 Tight (MonK k) where
  withObO2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: MonK k j k)
       (b :: MonK k i j) r.
(Ob a, Ob b, IsOb Tight a, IsOb Tight b) =>
((IsOb Tight (O a b), Ob (O a b)) => r) -> r
withObO2 @(MK a) @(MK b) (IsOb Tight (O a b), Ob (O a b)) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (UN 'MK a ** UN 'MK b) => r
(IsOb Tight (O a b), Ob (O a b)) => r
r
instance (M.Monoidal k) => WithObO2 Cotight (MonK k) where
  withObO2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: MonK k j k)
       (b :: MonK k i j) r.
(Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) =>
((IsOb Cotight (O a b), Ob (O a b)) => r) -> r
withObO2 @(MK a) @(MK b) (IsOb Cotight (O a b), Ob (O a b)) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (UN 'MK a ** UN 'MK b) => r
(IsOb Cotight (O a b), Ob (O a b)) => r
r
instance (M.CompactClosed k) => Equipment (MonK k) where
  withCotightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r.
IsTight f =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint @f (Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
k = forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c) s.
Adj l r -> (Adjunction_ l r => s) -> s
forall (l :: MonK k j k1) (r :: MonK k k1 j) s.
Adj l r -> (Adjunction_ l r => s) -> s
withAdj @f Adj f ('MK (Dual (UN 'MK f)))
Adj ('MK (UN 'MK f)) ('MK (Dual (UN 'MK f)))
forall {c :: ()} {d :: ()} {k} (a :: k).
(CompactClosed k, Ob a) =>
Adj ('MK a) ('MK (Dual a))
dualAdj' r
(Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
Adjunction_ f ('MK (Dual (UN 'MK f))) => r
k
  withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r.
IsCotight f =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @f (Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
k = forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c) s.
Adj l r -> (Adjunction_ l r => s) -> s
forall (l :: MonK k k1 j) (r :: MonK k j k1) s.
Adj l r -> (Adjunction_ l r => s) -> s
withAdj @_ @f Adj ('MK (Dual (UN 'MK f))) f
Adj ('MK (Dual (UN 'MK f))) ('MK (UN 'MK f))
forall {c :: ()} {d :: ()} {k} (a :: k).
(CompactClosed k, Ob a) =>
Adj ('MK (Dual a)) ('MK a)
dualAdj r
(Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
Adjunction_ ('MK (Dual (UN 'MK f))) f => r
k

instance (M.CompactClosed k, Ob j) => HasLimits (MK (j :: k)) '() where
  type Limit (MK j) (MK d) = MK (j ~~> d)
  withObLimit :: forall (d :: MonK k i '()) r.
IsTight d =>
(IsTight (Limit ('MK j) d) => r) -> r
withObLimit @(MK d) IsTight (Limit ('MK j) d) => r
r = r
(Ob (j ~~> UN 'MK d), Ob (j ~~> UN 'MK d)) => r
IsTight (Limit ('MK j) d) => r
r ((Ob (j ~~> UN 'MK d), Ob (j ~~> UN 'MK d)) => r)
-> ((j ~~> UN 'MK d) ~> (j ~~> UN 'MK d)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: 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 '()).
IsTight d =>
O (Limit ('MK j) d) ('MK j) ~> 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 k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @_ @j @d)
  limitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()).
(IsTight d, Ob p) =>
(O p ('MK j) ~> 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 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.CompactClosed k, Ob j) => HasColimits (MK (j :: k) :: MonK k i0 i1) '() where
  type Colimit (MK j) (MK d) = MK (M.Dual j M.** d)
  withObColimit :: forall (d :: MonK k '() i1) r.
IsCotight d =>
(IsCotight (Colimit ('MK j) d) => r) -> r
withObColimit @(MK d) IsCotight (Colimit ('MK j) d) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @(M.Dual j) @d r
Ob (Dual j ** UN 'MK d) => r
IsCotight (Colimit ('MK j) d) => r
r
  colimit :: forall (d :: MonK k '() i1).
IsCotight d =>
O ('MK j) (Colimit ('MK j) d) ~> d
colimit @(MK d) = ((j ** (Dual j ** UN 'MK d)) ~> UN 'MK d)
-> Mon2 ('MK (j ** (Dual j ** UN 'MK d))) ('MK (UN 'MK d))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (((j ** Dual j) ~> Unit) -> ((j ** Dual j) ** UN 'MK d) ~> UN 'MK d
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
M.leftUnitorWith (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
M.dualityCounit @j ((Dual j ** j) ~> Unit)
-> ((j ** Dual j) ~> (Dual j ** j)) -> (j ** Dual j) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @j @(M.Dual j)) (((j ** Dual j) ** UN 'MK d) ~> UN 'MK d)
-> ((j ** (Dual j ** UN 'MK d)) ~> ((j ** Dual j) ** UN 'MK d))
-> (j ** (Dual j ** UN 'MK d)) ~> UN 'MK d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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 @j @(M.Dual j) @d)
  colimitUniv :: forall (d :: MonK k '() i1) (p :: MonK k '() i0).
(IsCotight d, Ob p) =>
(O ('MK j) p ~> d) -> p ~> Colimit ('MK j) d
colimitUniv @_ @p O ('MK j) p ~> d
f =
    forall {k} (kk :: CAT k) {j :: k} {k1 :: k} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
forall (kk :: CAT ()) {j :: ()} {k1 :: ()} (f :: kk j k1) r.
(Equipment kk, IsCotight f) =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint @_ @(Dual (MK j) :: MonK k i1 i0)
      (forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
forall (l :: MonK k i0 i1) (r :: MonK k i1 i0) (a :: MonK k '() i0)
       (b :: MonK k '() i1).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
flipLeftAdjoint @(Dual (Dual (MK j)) :: MonK k i0 i1) @(Dual (MK j)) (O ('MK j) p ~> d
Mon2 ('MK (j ** UN 'MK p)) ('MK (UN 'MK d))
f Mon2 ('MK (j ** UN 'MK p)) ('MK (UN 'MK d))
-> Mon2 ('MK (Dual (Dual j) ** UN 'MK p)) ('MK (j ** UN 'MK p))
-> Mon2 ('MK (Dual (Dual j) ** UN 'MK p)) ('MK (UN 'MK d))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: MonK k '() i1) (c :: MonK k '() i1)
       (a :: MonK k '() i1).
Mon2 b c -> Mon2 a b -> Mon2 a c
. ((Dual (Dual j) ~> j) -> Mon2 ('MK (Dual (Dual j))) ('MK j)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
M.doubleNeg @j) ('MK (Dual (Dual j)) ~> 'MK j)
-> ('MK (UN 'MK p) ~> 'MK (UN 'MK p))
-> O ('MK (Dual (Dual j))) ('MK (UN 'MK p))
   ~> O ('MK j) ('MK (UN 'MK p))
forall {s} (kk :: CAT s) {i :: s} (j :: s) (k :: s) (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
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` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: MonK k '() i0).
(CategoryOf (MonK k '() i0), Ob a) =>
Obj a
obj @p)))

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 k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @_ @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 k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @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 k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @_ @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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @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 k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @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 k (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
coeval @k @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 k (b :: k) (c :: k) (a :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv @k @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 k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @(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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
coeval @k @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 k (b :: k) (c :: k) (a :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv @k @p @g (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. q ~> b
a ~> b
f))