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

module Proarrow.Monoid where

import Data.Kind (Constraint, Type)
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), par)
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), act)
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), arr, dimapDefault, obj, type (+->))
import Proarrow.Object.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , HasBinaryCoproducts (..)
  , HasBiproducts (..)
  , HasCoproducts
  , codiag
  )
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), HasProducts, PROD (..), Prod (..), diag, (&&&))
import Proarrow.Object.Dual (CompactClosed (..), StarAutonomous (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..), HasZeroObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Constant (Constant)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))

type Monoid :: forall {k}. k -> Constraint
class (Monoidal k, Ob m) => Monoid (m :: k) where
  mempty :: Unit ~> m
  mappend :: m ** m ~> m

combine :: (Monoid m) => Unit ~> m -> Unit ~> m -> Unit ~> m
combine :: forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g = (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m) -> (Unit ~> (m ** m)) -> Unit ~> m
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
. (Unit ~> m
f (Unit ~> m) -> (Unit ~> m) -> (Unit ** Unit) ~> (m ** m)
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)
`par` Unit ~> m
g) ((Unit ** Unit) ~> (m ** m))
-> (Unit ~> (Unit ** Unit)) -> Unit ~> (m ** m)
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
. Unit ~> (Unit ** Unit)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv

class (Monoid m) => CommutativeMonoid (m :: k)

instance (P.Monoid m) => Monoid (m :: Type) where
  mempty :: Unit ~> m
mempty () = m
forall a. Monoid a => a
P.mempty
  mappend :: (m ** m) ~> m
mappend = (m -> m -> m) -> (m, m) -> m
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry m -> m -> m
forall a. Semigroup a => a -> a -> a
(P.<>)

newtype GenElt x m = GenElt (x ~> m)

instance (Monoid m, Cartesian k) => P.Semigroup (GenElt x (m :: k)) where
  GenElt x ~> m
f <> :: GenElt x m -> GenElt x m -> GenElt x m
<> GenElt x ~> m
g = (x ~> m) -> GenElt x m
forall {k} (x :: k) (m :: k). (x ~> m) -> GenElt x m
GenElt ((m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m) -> (x ~> (m ** m)) -> x ~> m
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
. (x ~> m
f (x ~> m) -> (x ~> m) -> x ~> (m && m)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& x ~> m
g))
instance (Monoid m, Cartesian k, Ob x) => P.Monoid (GenElt x (m :: k)) where
  mempty :: GenElt x m
mempty = (x ~> m) -> GenElt x m
forall {k} (x :: k) (m :: k). (x ~> m) -> GenElt x m
GenElt (Unit ~> m
TerminalObject ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty (TerminalObject ~> m) -> (x ~> TerminalObject) -> x ~> m
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
. (x ~> TerminalObject) -> x ~> TerminalObject
forall {k} (p :: k +-> k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> p a b
arr x ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)

instance (HasCoproducts k, Ob a) => Monoid (COPR (a :: k)) where
  mempty :: Unit ~> 'COPR a
mempty = Id InitialObject a -> Coprod Id ('COPR InitialObject) ('COPR a)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((InitialObject ~> a) -> Id InitialObject a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id InitialObject ~> a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)
  mappend :: ('COPR a ** 'COPR a) ~> 'COPR a
mappend = Id (a || a) a -> Coprod Id ('COPR (a || a)) ('COPR a)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (((a || a) ~> a) -> Id (a || a) a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (a || a) ~> a
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag)

memptyAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Monoid a, Ob n) => n ~> Act a n
memptyAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
n ~> Act a n
memptyAct = (Unit ~> a) -> (n ~> n) -> Act Unit n ~> Act a n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (m :: m). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n) (Act Unit n ~> Act a n) -> (n ~> Act Unit n) -> n ~> Act a n
forall (b :: c) (c :: c) (a :: c). (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 m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m

mappendAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Monoid a, Ob n) => Act a (Act a n) ~> Act a n
mappendAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
Act a (Act a n) ~> Act a n
mappendAct = ((a ** a) ~> a) -> (n ~> n) -> Act (a ** a) n ~> Act a n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (m :: m). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n) (Act (a ** a) n ~> Act a n)
-> (Act a (Act a n) ~> Act (a ** a) n)
-> Act a (Act a n) ~> Act a n
forall (b :: c) (c :: c) (a :: c). (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 m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @m @c @a @a @n

type ModuleObject :: forall {m} {c}. m -> c -> Constraint
class (MonoidalAction m c, Monoid a, Ob n) => ModuleObject (a :: m) (n :: c) where
  action :: Act a n ~> n

type Comonoid :: forall {k}. k -> Constraint
class (Monoidal k, Ob c) => Comonoid (c :: k) where
  counit :: c ~> Unit
  comult :: c ~> c ** c

instance Comonoid (a :: Type) where
  counit :: a ~> Unit
counit a
_ = ()
  comult :: a ~> (a ** a)
comult a
a = (a
a, a
a)

instance Comonoid '() where
  counit :: '() ~> Unit
counit = '() ~> Unit
Unit '() '()
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ()). Ob a => Unit a a
id
  comult :: '() ~> ('() ** '())
comult = '() ~> ('() ** '())
Unit '() '()
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ()). Ob a => Unit a a
id

instance (HasProducts k, Ob a) => Comonoid (PR (a :: k)) where
  counit :: 'PR a ~> Unit
counit = (a ~> TerminalObject) -> Prod (~>) ('PR a) ('PR TerminalObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  comult :: 'PR a ~> ('PR a ** 'PR a)
comult = (a ~> (a && a)) -> Prod (~>) ('PR a) ('PR (a && a))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag

counitAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Comonoid a, Ob n) => Act a n ~> n
counitAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> n
counitAct = forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m (Act Unit n ~> n) -> (Act a n ~> Act Unit n) -> Act a n ~> n
forall (b :: c) (c :: c) (a :: c). (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
. (a ~> Unit) -> (n ~> n) -> Act a n ~> Act Unit n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (c :: m). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n)

comultAct :: forall {m} {c} (a :: m) (n :: c). (MonoidalAction m c, Comonoid a, Ob n) => Act a n ~> Act a (Act a n)
comultAct :: forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> Act a (Act a n)
comultAct = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @m @c @a @a @n (Act (a ** a) n ~> Act a (Act a n))
-> (Act a n ~> Act (a ** a) n) -> Act a n ~> Act a (Act a n)
forall (b :: c) (c :: c) (a :: c). (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
. (a ~> (a ** a)) -> (n ~> n) -> Act a n ~> Act (a ** a) n
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (c :: m). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a) (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @n)

type data MONOIDK (m :: k) = M
data Mon a b where
  Mon :: Unit ~> m -> Mon (M :: MONOIDK m) M
instance (Monoid m) => Profunctor (Mon :: CAT (MONOIDK m)) where
  dimap :: forall (c :: MONOIDK m) (a :: MONOIDK m) (b :: MONOIDK m)
       (d :: MONOIDK m).
(c ~> a) -> (b ~> d) -> Mon a b -> Mon c d
dimap = (c ~> a) -> (b ~> d) -> Mon a b -> Mon c d
Mon c a -> Mon b d -> Mon a b -> Mon c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
((Ob a, Ob b) => r) -> Mon a b -> r
\\ Mon{} = r
(Ob a, Ob b) => r
r
instance (Monoid m) => Promonad (Mon :: CAT (MONOIDK m)) where
  id :: forall (a :: MONOIDK m). Ob a => Mon a a
id = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f . :: forall (b :: MONOIDK m) (c :: MONOIDK m) (a :: MONOIDK m).
Mon b c -> Mon a b -> Mon a c
. Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)

-- | A monoid as a one object category.
instance (Monoid m) => CategoryOf (MONOIDK m) where
  type (~>) = Mon
  type Ob a = a P.~ M

instance (Monoid m) => HasInitialObject (MONOIDK m) where
  type InitialObject = M
  initiate :: forall (a :: MONOIDK m). Ob a => InitialObject ~> a
initiate = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (Monoid m) => HasTerminalObject (MONOIDK m) where
  type TerminalObject = M
  terminate :: forall (a :: MONOIDK m). Ob a => a ~> TerminalObject
terminate = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (Monoid m) => HasBinaryProducts (MONOIDK m) where
  type a && b = M
  withObProd :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @M @M Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(a && b) ~> a
fst @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  snd :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(a && b) ~> b
snd @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f &&& :: forall (a :: MONOIDK m) (x :: MONOIDK m) (y :: MONOIDK m).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)
instance (Monoid m) => HasBinaryCoproducts (MONOIDK m) where
  type a || b = M
  withObCoprod :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @M @M Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
a ~> (a || b)
lft @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rgt :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @M @M = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f ||| :: forall (x :: MONOIDK m) (a :: MONOIDK m) (y :: MONOIDK m).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)

instance (CommutativeMonoid m) => MonoidalProfunctor (Mon :: CAT (MONOIDK m)) where
  par0 :: Mon Unit Unit
par0 = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f par :: forall (x1 :: MONOIDK m) (x2 :: MONOIDK m) (y1 :: MONOIDK m)
       (y2 :: MONOIDK m).
Mon x1 x2 -> Mon y1 y2 -> Mon (x1 ** y1) (x2 ** y2)
`par` Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)
instance (CommutativeMonoid m) => Monoidal (MONOIDK m) where
  type Unit = M
  type M ** M = M
  withOb2 :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: MONOIDK m). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  leftUnitorInv :: forall (a :: MONOIDK m). Ob a => a ~> (Unit ** a)
leftUnitorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rightUnitor :: forall (a :: MONOIDK m). Ob a => (a ** Unit) ~> a
rightUnitor = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rightUnitorInv :: forall (a :: MONOIDK m). Ob a => a ~> (a ** Unit)
rightUnitorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  associator :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  associatorInv :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => SymMonoidal (MONOIDK m) where
  swap :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

instance (CommutativeMonoid m) => StarAutonomous (MONOIDK m) where
  type Dual (M :: MONOIDK m) = M
  dual :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(a ~> b) -> Dual b ~> Dual a
dual f :: a ~> b
f@Mon{} = a ~> b
Dual b ~> Dual a
f
  dualInv :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv Dual a ~> Dual b
f = b ~> a
Dual a ~> Dual b
f
  linDist :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (a ** b) ~> Dual c
_ = a ~> Dual (b ** c)
Mon M M
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MONOIDK m). Ob a => Mon a a
id
  linDistInv :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv a ~> Dual (b ** c)
_ = (a ** b) ~> Dual c
Mon M M
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MONOIDK m). Ob a => Mon a a
id
instance (CommutativeMonoid m) => CompactClosed (MONOIDK m) where
  distribDual :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  dualUnit :: Dual Unit ~> Unit
dualUnit = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => Closed (MONOIDK m) where
  type a ~~> b = M
  withObExp :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Mon Unit ~> m
m) = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
m
  apply :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

instance (Comonoid c) => Monoid (OP c) where
  mempty :: Unit ~> 'OP c
mempty = (c ~> Unit) -> Op (~>) ('OP Unit) ('OP c)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  mappend :: ('OP c ** 'OP c) ~> 'OP c
mappend = (c ~> (c ** c)) -> Op (~>) ('OP (c ** c)) ('OP c)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

instance (Monoid c) => Comonoid (OP c) where
  counit :: 'OP c ~> Unit
counit = (Unit ~> c) -> Op (~>) ('OP c) ('OP Unit)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op Unit ~> c
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  comult :: 'OP c ~> ('OP c ** 'OP c)
comult = ((c ** c) ~> c) -> Op (~>) ('OP c) ('OP (c ** c))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (c ** c) ~> c
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend

instance (HasZeroObject k, HasBiproducts k, Ob (a :: k), Ob b) => P.Semigroup (Id a b) where
  Id a ~> b
f <> :: Id a b -> Id a b -> Id a b
<> Id a ~> b
g = (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> (a ~> b) -> a ~> b
forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> a ~> b
forall k (a :: k) (b :: k).
HasBiproducts k =>
(a ~> b) -> (a ~> b) -> a ~> b
sum a ~> b
f a ~> b
g)
instance (HasZeroObject k, HasBiproducts k, Ob (a :: k), Ob b) => P.Monoid (Id a b) where
  mempty :: Id a b
mempty = (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
forall k (a :: k) (b :: k). (HasZeroObject k, Ob a, Ob b) => a ~> b
zero
instance (HasZeroObject k, HasBiproducts k, Ob (a :: k), Ob b) => CommutativeMonoid (Id a b)

instance (Monoidal k, Monoid r) => MonoidalProfunctor (Rep (Constant r) :: k +-> k) where
  par0 :: Rep (Constant r) Unit Unit
par0 = (Unit ~> (Constant r @ Unit)) -> Rep (Constant r) Unit Unit
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep Unit ~> r
Unit ~> (Constant r @ Unit)
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Rep @_ @_ @x x1 ~> (Constant r @ x2)
l par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Rep (Constant r) x1 x2
-> Rep (Constant r) y1 y2 -> Rep (Constant r) (x1 ** y1) (x2 ** y2)
`par` Rep @_ @_ @y y1 ~> (Constant r @ y2)
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x @y (((x1 ** y1) ~> (Constant r @ (x2 ** y2)))
-> Rep (Constant r) (x1 ** y1) (x2 ** y2)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((r ** r) ~> r
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((r ** r) ~> r) -> ((x1 ** y1) ~> (r ** r)) -> (x1 ** y1) ~> r
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
. (x1 ~> r
x1 ~> (Constant r @ x2)
l (x1 ~> r) -> (y1 ~> r) -> (x1 ** y1) ~> (r ** r)
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)
`par` y1 ~> r
y1 ~> (Constant r @ y2)
r)))
instance (HasCoproducts k, Ob r) => MonoidalProfunctor (Coprod (Rep (Constant r)) :: COPROD k +-> COPROD k) where
  par0 :: Coprod (Rep (Constant r)) Unit Unit
par0 = Rep (Constant r) InitialObject InitialObject
-> Coprod
     (Rep (Constant r)) ('COPR InitialObject) ('COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((InitialObject ~> (Constant r @ InitialObject))
-> Rep (Constant r) InitialObject InitialObject
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep InitialObject ~> r
InitialObject ~> (Constant r @ InitialObject)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)
  Coprod @_ @_ @x (Rep a1 ~> (Constant r @ b1)
l) par :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (Rep (Constant r)) x1 x2
-> Coprod (Rep (Constant r)) y1 y2
-> Coprod (Rep (Constant r)) (x1 ** y1) (x2 ** y2)
`par` Coprod @_ @_ @y (Rep a1 ~> (Constant r @ b1)
r) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @x @y (Rep (Constant r) (a1 || a1) (b1 || b1)
-> Coprod (Rep (Constant r)) ('COPR (a1 || a1)) ('COPR (b1 || b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (((a1 || a1) ~> (Constant r @ (b1 || b1)))
-> Rep (Constant r) (a1 || a1) (b1 || b1)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (a1 ~> r
a1 ~> (Constant r @ b1)
l (a1 ~> r) -> (a1 ~> r) -> (a1 || a1) ~> r
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a1 ~> r
a1 ~> (Constant r @ b1)
r)))
instance (Monoidal k, Comonoid r) => MonoidalProfunctor (Corep (Constant r) :: k +-> k) where
  par0 :: Corep (Constant r) Unit Unit
par0 = ((Constant r @ Unit) ~> Unit) -> Corep (Constant r) Unit Unit
forall {j} {k} (f :: j +-> k) (a :: j) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep r ~> Unit
(Constant r @ Unit) ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  Corep @_ @x (Constant r @ x1) ~> x2
l par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Corep (Constant r) x1 x2
-> Corep (Constant r) y1 y2
-> Corep (Constant r) (x1 ** y1) (x2 ** y2)
`par` Corep @_ @y (Constant r @ y1) ~> y2
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x @y (((Constant r @ (x1 ** y1)) ~> (x2 ** y2))
-> Corep (Constant r) (x1 ** y1) (x2 ** y2)
forall {j} {k} (f :: j +-> k) (a :: j) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep ((r ~> x2
(Constant r @ x1) ~> x2
l (r ~> x2) -> (r ~> y2) -> (r ** r) ~> (x2 ** y2)
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)
`par` r ~> y2
(Constant r @ y1) ~> y2
r) ((r ** r) ~> (x2 ** y2)) -> (r ~> (r ** r)) -> r ~> (x2 ** y2)
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
. r ~> (r ** r)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult))