{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Bicategory.MonoidalAsBi where

import Proarrow.Core (CAT, Promonad(..), CategoryOf(..), Profunctor(..), Is, UN, Kind)
import Proarrow.Monoid (Monoid(..), Comonoid (..))
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Bicategory (Bicategory (..), Monad(..), Comonad (..))


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 (b M.** a)
  Mon2 a ~> b
f o :: forall {k1 :: ()} (i :: ()) (j :: ()) (a :: MonK k i j)
       (b :: MonK k i j) (c :: MonK k j k1) (d :: MonK k j k1).
(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
g (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`M.par` a ~> b
f)
  (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). Obj a -> O I a ~> a
leftUnitor (Mon2 a ~> b
p) = ((b ** Unit) ~> b) -> Mon2 ('MK (b ** Unit)) ('MK b)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Obj b -> (b ** Unit) ~> b
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
M.rightUnitor a ~> b
Obj b
p)
  leftUnitorInv :: forall (i :: ()) (j :: ()) (a :: MonK k i j). Obj a -> a ~> O I a
leftUnitorInv (Mon2 a ~> b
p) = (b ~> (b ** Unit)) -> Mon2 ('MK b) ('MK (b ** Unit))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Obj b -> b ~> (b ** Unit)
forall (a :: k). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
M.rightUnitorInv a ~> b
Obj b
p)
  rightUnitor :: forall (i :: ()) (j :: ()) (a :: MonK k i j). Obj a -> O a I ~> a
rightUnitor (Mon2 a ~> b
p) = ((Unit ** b) ~> b) -> Mon2 ('MK (Unit ** b)) ('MK b)
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Obj b -> (Unit ** b) ~> b
forall (a :: k). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
M.leftUnitor a ~> b
Obj b
p)
  rightUnitorInv :: forall (i :: ()) (j :: ()) (a :: MonK k i j). Obj a -> a ~> O a I
rightUnitorInv (Mon2 a ~> b
p) = (b ~> (Unit ** b)) -> Mon2 ('MK b) ('MK (Unit ** b))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Obj b -> b ~> (Unit ** b)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
M.leftUnitorInv a ~> b
Obj b
p)
  associator :: forall {j1 :: ()} {k1 :: ()} (i :: ()) (j2 :: ())
       (a :: MonK k i j2) (b :: MonK k j2 j1) (c :: MonK k j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator (Mon2 a ~> b
p) (Mon2 a ~> b
q) (Mon2 a ~> b
r) = ((b ** (b ** b)) ~> ((b ** b) ** b))
-> Mon2 ('MK (b ** (b ** b))) ('MK ((b ** b) ** b))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Obj b -> Obj b -> Obj b -> (b ** (b ** b)) ~> ((b ** b) ** b)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
M.associatorInv a ~> b
Obj b
r a ~> b
Obj b
q a ~> b
Obj b
p)
  associatorInv :: forall {j1 :: ()} {k1 :: ()} (i :: ()) (j2 :: ())
       (a :: MonK k i j2) (b :: MonK k j2 j1) (c :: MonK k j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv (Mon2 a ~> b
p) (Mon2 a ~> b
q) (Mon2 a ~> b
r) = (((b ** b) ** b) ~> (b ** (b ** b)))
-> Mon2 ('MK ((b ** b) ** b)) ('MK (b ** (b ** b)))
forall {k} {i :: ()} {j :: ()} (a :: k) (b :: k).
(a ~> b) -> Mon2 ('MK a) ('MK b)
Mon2 (Obj b -> Obj b -> Obj b -> ((b ** b) ** b) ~> (b ** (b ** b))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
M.associator a ~> b
Obj b
r a ~> b
Obj b
q a ~> b
Obj b
p)

-- | Monoids in a monoidal category are monads when the monoidal category is seen as a bicategory.
instance 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
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
mappend

-- | Comonoids in a monoidal category are comonads when the monoidal category is seen as a bicategory.
instance 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
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)
comult