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

-- | Monoids and comonoids internal to a monoidal category: a 'Monoid' @m@ has @'mempty' :: 'Unit' '~>' m@
-- and @'mappend' :: m '**' m '~>' m@; dually a 'Comonoid' has 'counit' and 'comult'. Monoids in
-- 'Data.Kind.Type' are the Prelude monoids, and in a cartesian category every object is a comonoid.
module Proarrow.Monoid where

import Data.Kind (Constraint, Type)
import Data.Type.Nat (SNat (..), SNatI, snat)
import Prelude qualified as P

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Free (Elems, FREE, HasStructure (..), Lower, withLowerOb)
import Proarrow.Category.Instance.Free qualified as F
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , NFold
  , NFoldS
  , SymMonoidal (..)
  , Tensor
  , UnitF
  , swapInner
  , (**)
  , type (**!)
  )
import Proarrow.Category.Monoidal.Action (Act, ActionAt, CoprodAction, MonoidalAction (..), actHom)
import Proarrow.Category.Monoidal.Closed (Closed (..), Exp)
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Category.Monoidal.Strictified (Strictified (..), obj1)
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , HasBinaryCoproducts (..)
  , HasBiproducts (..)
  , HasCoproducts
  , codiag
  )
import Proarrow.Colimit.Initial (HasInitialObject (..), HasZeroObject (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Promonad (..), obj, (//), type (+->))
import Proarrow.Object (pattern Objs)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))
import Proarrow.Tools.Laws (Law (..), Laws (..), (===))

-- | A monoid object in a monoidal category: a unit and an (associative, unital) multiplication
-- for the object @m@. At @k = Type@ (with tensor @(,)@) this is the ordinary 'P.Monoid'.
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 :: CAT 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)
** 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 :: CAT 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

memptyS :: (Monoid m) => '[] ~> '[m]
memptyS :: forall {a} (m :: a). Monoid m => '[] ~> '[m]
memptyS = (Fold '[] ~> Fold '[m]) -> Strictified '[] '[m]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Unit ~> m
Fold '[] ~> Fold '[m]
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

mappendS :: (Monoid m) => '[m, m] ~> '[m]
mappendS :: forall {k} (m :: k). Monoid m => '[m, m] ~> '[m]
mappendS = (Fold '[m, m] ~> Fold '[m]) -> Strictified '[m, m] '[m]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (m ** m) ~> m
Fold '[m, m] ~> Fold '[m]
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend

-- | A law-only marker class for monoids whose multiplication commutes:
-- @'mappend' . 'swap' = 'mappend'@.
class (Monoid m, SymMonoidal k) => 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.<>)
instance CommutativeMonoid ()

instance Monoid TRU where
  mempty :: Unit ~> 'TRU
mempty = Unit ~> 'TRU
Booleans 'TRU 'TRU
Tru
  mappend :: ('TRU ** 'TRU) ~> 'TRU
mappend = ('TRU ** 'TRU) ~> 'TRU
Booleans 'TRU 'TRU
Tru
instance CommutativeMonoid TRU

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

instance (Monoid m, Comonoid (x :: 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 :: CAT 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 ** x) ~> (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)
** x ~> m
g) ((x ** x) ~> (m ** m)) -> (x ~> (x ** x)) -> x ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> (x ** x)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult)
instance (Monoid m, Comonoid (x :: k)) => 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
forall {k} (m :: k). Monoid m => Unit ~> m
mempty (Unit ~> m) -> (x ~> Unit) -> x ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit)

instance (HasCoproducts k, Ob a) => Monoid (COPR (a :: k)) where
  mempty :: Unit ~> COPR a
mempty = (InitialObject ~> a) -> Coprod (~>) (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
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 = ((a || a) ~> a) -> Coprod (~>) (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
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag

memptyAct :: forall {m} {c} t (a :: m) (n :: c). (MonoidalAction t, Monoid a, Ob n) => n ~> Act t a n
memptyAct :: forall {m} {c} (t :: (m, c) +-> c) (a :: m) (n :: c).
(MonoidalAction t, Monoid a, Ob n) =>
n ~> Act t a n
memptyAct = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, c) +-> c) (a :: m) (b :: m) (x :: c) (y :: c).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (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) ((t % '(Unit, n)) ~> (t % '(a, n)))
-> (n ~> (t % '(Unit, n))) -> n ~> (t % '(a, n))
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, c) +-> c) (x :: c).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @t

mappendAct
  :: forall {m} {c} t (a :: m) (n :: c). (MonoidalAction t, Monoid a, Ob n) => Act t a (Act t a n) ~> Act t a n
mappendAct :: forall {m} {c} (t :: (m, c) +-> c) (a :: m) (n :: c).
(MonoidalAction t, Monoid a, Ob n) =>
Act t a (Act t a n) ~> Act t a n
mappendAct = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, c) +-> c) (a :: m) (b :: m) (x :: c) (y :: c).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (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) ((t % '(a ** a, n)) ~> (t % '(a, n)))
-> ((t % '(a, t % '(a, n))) ~> (t % '(a ** a, n)))
-> (t % '(a, t % '(a, n))) ~> (t % '(a, n))
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
forall (t :: (m, c) +-> c) (a :: m) (b :: m) (x :: c).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
multiplicatorInv @t @a @a @n

-- | A comonoid object: an object that can be discarded ('counit') and copied ('comult').
type Comonoid :: forall {k}. k -> Constraint
class (Monoidal k, Ob c) => Comonoid (c :: k) where
  counit :: c ~> Unit
  comult :: c ~> c ** c

-- | A law-only marker for comonoids whose comultiplication cocommutes: @'swap' . 'comult' = 'comult'@.
-- Dual to 'CommutativeMonoid'.
class (Comonoid c, SymMonoidal k) => CocommutativeComonoid (c :: k)

counitS :: (Comonoid c) => '[c] ~> '[]
counitS :: forall {k} (c :: k). Comonoid c => '[c] ~> '[]
counitS = (Fold '[c] ~> Fold '[]) -> Strictified '[c] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str c ~> Unit
Fold '[c] ~> Fold '[]
forall {k} (c :: k). Comonoid c => c ~> Unit
counit

comultS :: (Comonoid c) => '[c] ~> '[c, c]
comultS :: forall {k} (c :: k). Comonoid c => '[c] ~> '[c, c]
comultS = (Fold '[c] ~> Fold '[c, c]) -> Strictified '[c] '[c, c]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str c ~> (c ** c)
Fold '[c] ~> Fold '[c, c]
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

-- | A comonoid structure on @c@ carried as a value. @Unit@ and @('**')@ are type families and so
-- cannot head a 'Comonoid' instance, yet the unit is a comonoid and, in a symmetric monoidal
-- category, so is a tensor of comonoids. 'unitComonoid' and 'tensorComonoid' say so at the value
-- level, so that 'Proarrow.Optic.MonoidalLens.withMonLens' can hand back the comonoid of a
-- composite residual (cf. 'Proarrow.Optic.Action.withAlgP', which passes algebras the same way).
type ComonoidOn :: forall {k}. k -> Type
data ComonoidOn (c :: k) = ComonoidOn {forall {k} (c :: k). ComonoidOn c -> c ~> Unit
counitOn :: c ~> Unit, forall {k} (c :: k). ComonoidOn c -> c ~> (c ** c)
comultOn :: c ~> c ** c}

-- | The comonoid structure of a 'Comonoid' instance, as a value.
comonoidOn :: forall {k} (c :: k). (Comonoid c) => ComonoidOn c
comonoidOn :: forall {k} (c :: k). Comonoid c => ComonoidOn c
comonoidOn = (c ~> Unit) -> (c ~> (c ** c)) -> ComonoidOn c
forall {k} (c :: k). (c ~> Unit) -> (c ~> (c ** c)) -> ComonoidOn c
ComonoidOn c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

-- | The unit is a comonoid, via the unitor.
unitComonoid :: forall {k}. (Monoidal k) => ComonoidOn (Unit :: k)
unitComonoid :: forall {k}. Monoidal k => ComonoidOn Unit
unitComonoid = (Unit ~> Unit) -> (Unit ~> (Unit ** Unit)) -> ComonoidOn Unit
forall {k} (c :: k). (c ~> Unit) -> (c ~> (c ** c)) -> ComonoidOn c
ComonoidOn Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @Unit)

-- | In a symmetric monoidal category the tensor of two comonoids is a comonoid: counit both
-- halves, or comultiply both halves and swap the inner pair.
tensorComonoid :: forall {k} (a :: k) b. (SymMonoidal k) => ComonoidOn a -> ComonoidOn b -> ComonoidOn (a ** b)
tensorComonoid :: forall {k} (a :: k) (b :: k).
SymMonoidal k =>
ComonoidOn a -> ComonoidOn b -> ComonoidOn (a ** b)
tensorComonoid (ComonoidOn ca :: a ~> Unit
ca@a ~> Unit
Objs a ~> (a ** a)
ma) (ComonoidOn cb :: b ~> Unit
cb@b ~> Unit
Objs b ~> (b ** b)
mb) =
  ((a ** b) ~> Unit)
-> ((a ** b) ~> ((a ** b) ** (a ** b))) -> ComonoidOn (a ** b)
forall {k} (c :: k). (c ~> Unit) -> (c ~> (c ** c)) -> ComonoidOn c
ComonoidOn (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @Unit ((Unit ** Unit) ~> Unit)
-> ((a ** b) ~> (Unit ** Unit)) -> (a ** b) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> Unit
ca (a ~> Unit) -> (b ~> Unit) -> (a ** b) ~> (Unit ** Unit)
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)
** b ~> Unit
cb)) (forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @a @a @b @b (((a ** a) ** (b ** b)) ~> ((a ** b) ** (a ** b)))
-> ((a ** b) ~> ((a ** a) ** (b ** b)))
-> (a ** b) ~> ((a ** b) ** (a ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> (a ** a)
ma (a ~> (a ** a))
-> (b ~> (b ** 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)
** b ~> (b ** b)
mb))

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

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

instance (Ob a) => Comonoid (a :: BOOL) where
  counit :: a ~> Unit
counit = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> a ~> Unit
Booleans 'FLS 'TRU
F2T
    Obj a
Booleans a a
Tru -> a ~> Unit
Booleans 'TRU 'TRU
Tru
  comult :: a ~> (a ** a)
comult = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> a ~> (a ** a)
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> a ~> (a ** a)
Booleans 'TRU 'TRU
Tru
instance (Ob a) => CocommutativeComonoid (a :: BOOL)

counitAct :: forall {m} {c} t (a :: m) (n :: c). (MonoidalAction t, Comonoid a, Ob n) => Act t a n ~> n
counitAct :: forall {m} {c} (t :: (m, c) +-> c) (a :: m) (n :: c).
(MonoidalAction t, Comonoid a, Ob n) =>
Act t a n ~> n
counitAct = forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, c) +-> c) (x :: c).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @t (Act t Unit n ~> n)
-> ((t % '(a, n)) ~> Act t Unit n) -> (t % '(a, n)) ~> n
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, c) +-> c) (a :: m) (b :: m) (x :: c) (y :: c).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (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} t (a :: m) (n :: c). (MonoidalAction t, Comonoid a, Ob n) => Act t a n ~> Act t a (Act t a n)
comultAct :: forall {m} {c} (t :: (m, c) +-> c) (a :: m) (n :: c).
(MonoidalAction t, Comonoid a, Ob n) =>
Act t a n ~> Act t a (Act t a n)
comultAct = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
forall (t :: (m, c) +-> c) (a :: m) (b :: m) (x :: c).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
multiplicator @t @a @a @n (Act t (a ** a) n ~> (t % '(a, t % '(a, n))))
-> ((t % '(a, n)) ~> Act t (a ** a) n)
-> (t % '(a, n)) ~> (t % '(a, t % '(a, n)))
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, c) +-> c) (a :: m) (b :: m) (x :: c) (y :: c).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (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)

-- | @'Supplies' c k@ says that every object of the category @k@ satisfies the constraint @c@,
-- e.g. @'Supplies' 'Comonoid' k@ for a category in which every object can be copied and discarded.
-- The constraint comes first (at a higher-rank kind) so that a partial application like
-- @'Supplies' 'Comonoid'@ has kind @Kind -> Constraint@ and can appear in a free category's
-- structure list ("Proarrow.Category.Instance.Free"). Instances are necessarily per-@c@ (an
-- instance variable cannot have a higher-rank kind); each follows the shape of the 'Comonoid' one.
type Supplies :: (forall j. j -> Constraint) -> Kind -> Constraint
class (forall (a :: k). (Ob a) => c a) => Supplies c k

instance (forall (a :: k). (Ob a) => Comonoid a) => Supplies Comonoid k

instance (forall (a :: k). (Ob a) => CocommutativeComonoid a) => Supplies CocommutativeComonoid k

instance (forall (a :: k). (Ob a) => Monoid a) => Supplies Monoid k

instance (forall (a :: k). (Ob a) => CommutativeMonoid a) => Supplies CommutativeMonoid k

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 (CocommutativeComonoid c) => CommutativeMonoid (OP c)

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 (CommutativeMonoid c) => CocommutativeComonoid (OP c)

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
  one :: Rep (Constant r) Unit Unit
one = (Unit ~> (Constant r @ Unit)) -> Rep (Constant r) Unit Unit
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
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 ** :: 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)
** 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} (b :: j) (f :: j +-> k) (a :: k).
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 :: CAT 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)
** y1 ~> r
y1 ~> (Constant r @ y2)
r)))
instance (HasCoproducts k, Ob r) => MonoidalProfunctor (Coprod (Rep (Constant r)) :: COPROD k +-> COPROD k) where
  one :: Coprod (Rep (Constant r)) Unit Unit
one = 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} (b :: j) (f :: j +-> k) (a :: k).
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) ** :: 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)
** 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} (b :: j) (f :: j +-> k) (a :: k).
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
  one :: Corep (Constant r) Unit Unit
one = ((Constant r @ Unit) ~> Unit) -> Corep (Constant r) Unit Unit
forall {j} {k} (a :: j) (f :: j +-> k) (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 ** :: 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)
** 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} (a :: j) (f :: j +-> k) (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)
** 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 :: CAT 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))

-- | Tensoring with a monoid, @m ** -@, is an applicative functor: the monoid's unit is @pure@ and
-- its multiplication is @<*>@. Rendered on the representable profunctor @'Rep' ('ActionAt' 'Tensor' m)@
-- (legs @a ~> m ** b@) this is a 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor',
-- the Writer applicative of the literature. (The 'Constant' instances above are the degenerate
-- case @b = Unit@.)
instance (SymMonoidal k, Monoid (m :: k)) => MonoidalProfunctor (Rep (ActionAt Tensor m) :: k +-> k) where
  one :: Rep (ActionAt Tensor m) Unit Unit
one = (Unit ~> (ActionAt Tensor m @ Unit))
-> Rep (ActionAt Tensor m) Unit Unit
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall {m} {c} (t :: (m, c) +-> c) (a :: m) (n :: c).
(MonoidalAction t, Monoid a, Ob n) =>
n ~> Act t a n
forall (t :: (k, k) +-> k) (a :: k) (n :: k).
(MonoidalAction t, Monoid a, Ob n) =>
n ~> Act t a n
memptyAct @Tensor @m @Unit)
  Rep @x2 x1 ~> (ActionAt Tensor m @ x2)
l ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Rep (ActionAt Tensor m) x1 x2
-> Rep (ActionAt Tensor m) y1 y2
-> Rep (ActionAt Tensor m) (x1 ** y1) (x2 ** y2)
** Rep @y2 y1 ~> (ActionAt Tensor m @ y2)
r =
    x1 ~> (ActionAt Tensor m @ x2)
x1 ~> (m ** x2)
l (x1 ~> (m ** x2))
-> ((Ob x1, Ob (m ** x2)) =>
    Rep (ActionAt Tensor m) (x1 ** y1) (x2 ** y2))
-> Rep (ActionAt Tensor m) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// y1 ~> (ActionAt Tensor m @ y2)
y1 ~> (m ** y2)
r (y1 ~> (m ** y2))
-> ((Ob y1, Ob (m ** y2)) =>
    Rep (ActionAt Tensor m) (x1 ** y1) (x2 ** y2))
-> Rep (ActionAt Tensor m) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x2 @y2 (((x1 ** y1) ~> (ActionAt Tensor m @ (x2 ** y2)))
-> Rep (ActionAt Tensor m) (x1 ** y1) (x2 ** y2)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @m ((m ** m) ~> m)
-> ((x2 ** y2) ~> (x2 ** y2))
-> ((m ** m) ** (x2 ** y2)) ~> (m ** (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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(x2 ** y2)) (((m ** m) ** (x2 ** y2)) ~> (m ** (x2 ** y2)))
-> ((x1 ** y1) ~> ((m ** m) ** (x2 ** y2)))
-> (x1 ** y1) ~> (m ** (x2 ** y2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @m @x2 @m @y2 (((m ** x2) ** (m ** y2)) ~> ((m ** m) ** (x2 ** y2)))
-> ((x1 ** y1) ~> ((m ** x2) ** (m ** y2)))
-> (x1 ** y1) ~> ((m ** m) ** (x2 ** y2))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x1 ~> (ActionAt Tensor m @ x2)
x1 ~> (m ** x2)
l (x1 ~> (m ** x2))
-> (y1 ~> (m ** y2)) -> (x1 ** y1) ~> ((m ** x2) ** (m ** 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)
** y1 ~> (ActionAt Tensor m @ y2)
y1 ~> (m ** y2)
r)))

instance
  (Monoidal k, HasCoproducts k, Ob (m :: k))
  => MonoidalProfunctor (Coprod (Rep (ActionAt Tensor m)) :: COPROD k +-> COPROD k)
  where
  one :: Coprod (Rep (ActionAt Tensor m)) Unit Unit
one = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @m @InitialObject (Rep (ActionAt Tensor m) InitialObject InitialObject
-> Coprod
     (Rep (ActionAt Tensor m)) (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 ~> (ActionAt Tensor m @ InitialObject))
-> Rep (ActionAt Tensor m) InitialObject InitialObject
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep InitialObject ~> (ActionAt Tensor m @ InitialObject)
InitialObject ~> (m ** InitialObject)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate))
  Coprod (Rep @x2 a1 ~> (ActionAt Tensor m @ b1)
l) ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (Rep (ActionAt Tensor m)) x1 x2
-> Coprod (Rep (ActionAt Tensor m)) y1 y2
-> Coprod (Rep (ActionAt Tensor m)) (x1 ** y1) (x2 ** y2)
** Coprod (Rep @y2 a1 ~> (ActionAt Tensor m @ b1)
r) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @x2 @y2 (Rep (ActionAt Tensor m) (a1 || a1) (b1 || b1)
-> Coprod
     (Rep (ActionAt Tensor m)) (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) ~> (ActionAt Tensor m @ (b1 || b1)))
-> Rep (ActionAt Tensor m) (a1 || a1) (b1 || b1)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m -> (b1 ~> (b1 || b1)) -> (m ** b1) ~> (m ** (b1 || b1))
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)
** forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @x2 @y2) ((m ** b1) ~> (m ** (b1 || b1)))
-> (a1 ~> (m ** b1)) -> a1 ~> (m ** (b1 || b1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> (ActionAt Tensor m @ b1)
a1 ~> (m ** b1)
l (a1 ~> (m ** (b1 || b1)))
-> (a1 ~> (m ** (b1 || b1))) -> (a1 || a1) ~> (m ** (b1 || b1))
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
||| (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m -> (b1 ~> (b1 || b1)) -> (m ** b1) ~> (m ** (b1 || b1))
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)
** forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @x2 @y2) ((m ** b1) ~> (m ** (b1 || b1)))
-> (a1 ~> (m ** b1)) -> a1 ~> (m ** (b1 || b1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> (ActionAt Tensor m @ b1)
a1 ~> (m ** b1)
r)))
instance (SymMonoidal k, Ob (m :: k)) => Strong Tensor (Rep (ActionAt Tensor m) :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
Rep (ActionAt Tensor m) x y
-> Rep (ActionAt Tensor m) (Act Tensor a x) (Act Tensor a y)
act @a (Rep @y x ~> (ActionAt Tensor m @ y)
p) =
    x ~> (ActionAt Tensor m @ y)
x ~> (m ** y)
p (x ~> (m ** y))
-> ((Ob x, Ob (m ** y)) =>
    Rep (ActionAt Tensor m) (a ** x) (a ** y))
-> Rep (ActionAt Tensor m) (a ** x) (a ** y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @y (((a ** x) ~> (ActionAt Tensor m @ (a ** y)))
-> Rep (ActionAt Tensor m) (a ** x) (a ** y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @m @a @y (((m ** a) ** y) ~> (m ** (a ** y)))
-> ((a ** x) ~> ((m ** a) ** y)) -> (a ** x) ~> (m ** (a ** y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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)
swap @k @a @m ((a ** m) ~> (m ** a))
-> (y ~> y) -> ((a ** m) ** y) ~> ((m ** a) ** y)
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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y) (((a ** m) ** y) ~> ((m ** a) ** y))
-> ((a ** x) ~> ((a ** m) ** y)) -> (a ** x) ~> ((m ** a) ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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)
associatorInv @k @a @m @y ((a ** (m ** y)) ~> ((a ** m) ** y))
-> ((a ** x) ~> (a ** (m ** y))) -> (a ** x) ~> ((a ** m) ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (x ~> (m ** y)) -> (a ** x) ~> (a ** (m ** y))
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)
** x ~> (ActionAt Tensor m @ y)
x ~> (m ** y)
p)))
instance (Monoidal k, HasCoproducts k, Monoid (m :: k)) => Strong CoprodAction (Rep (ActionAt Tensor m) :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
Rep (ActionAt Tensor m) x y
-> Rep
     (ActionAt Tensor m) (Act CoprodAction a x) (Act CoprodAction a y)
act @(COPR a) (Rep @y x ~> (ActionAt Tensor m @ y)
p) =
    x ~> (ActionAt Tensor m @ y)
x ~> (m ** y)
p (x ~> (m ** y))
-> ((Ob x, Ob (m ** y)) =>
    Rep (ActionAt Tensor m) (UN COPR a || x) (UN COPR a || y))
-> Rep (ActionAt Tensor m) (UN COPR a || x) (UN COPR a || y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @y (((UN COPR a || x) ~> (ActionAt Tensor m @ (UN COPR a || y)))
-> Rep (ActionAt Tensor m) (UN COPR a || x) (UN COPR a || y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m
-> (UN COPR a ~> (UN COPR a || y))
-> (m ** UN COPR a) ~> (m ** (UN COPR a || y))
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)
** forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @y) ((m ** UN COPR a) ~> (m ** (UN COPR a || y)))
-> (UN COPR a ~> (m ** UN COPR a))
-> UN COPR a ~> (m ** (UN COPR a || y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {c} (t :: (m, c) +-> c) (a :: m) (n :: c).
(MonoidalAction t, Monoid a, Ob n) =>
n ~> Act t a n
forall (t :: (k, k) +-> k) (a :: k) (n :: k).
(MonoidalAction t, Monoid a, Ob n) =>
n ~> Act t a n
memptyAct @Tensor @m @a (UN COPR a ~> (m ** (UN COPR a || y)))
-> (x ~> (m ** (UN COPR a || y)))
-> (UN COPR a || x) ~> (m ** (UN COPR a || y))
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
||| (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m
-> (y ~> (UN COPR a || y)) -> (m ** y) ~> (m ** (UN COPR a || y))
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)
** forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @y) ((m ** y) ~> (m ** (UN COPR a || y)))
-> (x ~> (m ** y)) -> x ~> (m ** (UN COPR a || y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> (ActionAt Tensor m @ y)
x ~> (m ** y)
p))

-- | The exponential by a comonoid, @m ~~> -@, is an applicative functor (the reader applicative):
-- @pure@ discards the argument with the counit and @<*>@ duplicates it with the comultiplication.
-- Rendered on @'Rep' ('Exp' m)@ (legs @a ~> (m ~~> b)@) this is a
-- 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor', so a
-- 'Proarrow.Optic.Grate.Grate' is a 'Proarrow.Optic.Kaleidoscope.Kaleidoscope'.
instance (Closed k, SymMonoidal k, Comonoid (m :: k)) => MonoidalProfunctor (Rep (Exp m) :: k +-> k) where
  one :: Rep (Exp m) Unit Unit
one = (Unit ~> (Exp m @ Unit)) -> Rep (Exp m) Unit Unit
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @Unit @m (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @Unit ((Unit ** Unit) ~> Unit)
-> ((Unit ** m) ~> (Unit ** Unit)) -> (Unit ** m) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @Unit Obj Unit -> (m ~> Unit) -> (Unit ** m) ~> (Unit ** Unit)
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)
** forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @m)))
  Rep @x2 @_ @x1 x1 ~> (Exp m @ x2)
l ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Rep (Exp m) x1 x2
-> Rep (Exp m) y1 y2 -> Rep (Exp m) (x1 ** y1) (x2 ** y2)
** Rep @y2 @_ @y1 y1 ~> (Exp m @ y2)
r =
    x1 ~> (Exp m @ x2)
x1 ~> (m ~~> x2)
l (x1 ~> (m ~~> x2))
-> ((Ob x1, Ob (m ~~> x2)) => Rep (Exp m) (x1 ** y1) (x2 ** y2))
-> Rep (Exp m) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      y1 ~> (Exp m @ y2)
y1 ~> (m ~~> y2)
r (y1 ~> (m ~~> y2))
-> ((Ob y1, Ob (m ~~> y2)) => Rep (Exp m) (x1 ** y1) (x2 ** y2))
-> Rep (Exp m) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x1 @y1
          ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x2 @y2
              ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @x2
                  ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @y2
                      ( ((x1 ** y1) ~> (Exp m @ (x2 ** y2)))
-> Rep (Exp m) (x1 ** y1) (x2 ** y2)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep
                          ( forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @(x1 ** y1) @m
                              ( (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @m @x2 (((m ~~> x2) ** m) ~> x2)
-> (((m ~~> y2) ** m) ~> y2)
-> (((m ~~> x2) ** m) ** ((m ~~> y2) ** m)) ~> (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)
** forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @m @y2)
                                  ((((m ~~> x2) ** m) ** ((m ~~> y2) ** m)) ~> (x2 ** y2))
-> (((x1 ** y1) ** m) ~> (((m ~~> x2) ** m) ** ((m ~~> y2) ** m)))
-> ((x1 ** y1) ** m) ~> (x2 ** y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @(m ~~> x2) @(m ~~> y2) @m @m
                                  ((((m ~~> x2) ** (m ~~> y2)) ** (m ** m))
 ~> (((m ~~> x2) ** m) ** ((m ~~> y2) ** m)))
-> (((x1 ** y1) ** m) ~> (((m ~~> x2) ** (m ~~> y2)) ** (m ** m)))
-> ((x1 ** y1) ** m) ~> (((m ~~> x2) ** m) ** ((m ~~> y2) ** m))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((x1 ~> (Exp m @ x2)
x1 ~> (m ~~> x2)
l (x1 ~> (m ~~> x2))
-> (y1 ~> (m ~~> y2)) -> (x1 ** y1) ~> ((m ~~> x2) ** (m ~~> 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)
** y1 ~> (Exp m @ y2)
y1 ~> (m ~~> y2)
r) ((x1 ** y1) ~> ((m ~~> x2) ** (m ~~> y2)))
-> (m ~> (m ** m))
-> ((x1 ** y1) ** m) ~> (((m ~~> x2) ** (m ~~> y2)) ** (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)
** forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @m)
                              )
                          )
                      )
                  )
              )
          )

instance (Closed k, HasCoproducts k, Ob (m :: k)) => MonoidalProfunctor (Coprod (Rep (Exp m)) :: COPROD k +-> COPROD k) where
  one :: Coprod (Rep (Exp m)) Unit Unit
one = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @InitialObject (Rep (Exp m) InitialObject InitialObject
-> Coprod (Rep (Exp m)) (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 ~> (Exp m @ InitialObject))
-> Rep (Exp m) InitialObject InitialObject
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep InitialObject ~> (Exp m @ InitialObject)
InitialObject ~> (m ~~> InitialObject)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate))
  Coprod (Rep @x2 a1 ~> (Exp m @ b1)
l) ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (Rep (Exp m)) x1 x2
-> Coprod (Rep (Exp m)) y1 y2
-> Coprod (Rep (Exp m)) (x1 ** y1) (x2 ** y2)
** Coprod (Rep @y2 a1 ~> (Exp m @ b1)
r) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @x2 @y2 (Rep (Exp m) (a1 || a1) (b1 || b1)
-> Coprod (Rep (Exp m)) (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) ~> (Exp m @ (b1 || b1)))
-> Rep (Exp m) (a1 || a1) (b1 || b1)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @x2 @y2 (b1 ~> (b1 || b1)) -> (m ~> m) -> (m ~~> b1) ~> (m ~~> (b1 || b1))
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 @m) ((m ~~> b1) ~> (m ~~> (b1 || b1)))
-> (a1 ~> (m ~~> b1)) -> a1 ~> (m ~~> (b1 || b1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> (Exp m @ b1)
a1 ~> (m ~~> b1)
l (a1 ~> (m ~~> (b1 || b1)))
-> (a1 ~> (m ~~> (b1 || b1))) -> (a1 || a1) ~> (m ~~> (b1 || b1))
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
||| (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @x2 @y2 (b1 ~> (b1 || b1)) -> (m ~> m) -> (m ~~> b1) ~> (m ~~> (b1 || b1))
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 @m) ((m ~~> b1) ~> (m ~~> (b1 || b1)))
-> (a1 ~> (m ~~> b1)) -> a1 ~> (m ~~> (b1 || b1))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> (Exp m @ b1)
a1 ~> (m ~~> b1)
r)))
instance (Closed k, SymMonoidal k, Ob (m :: k)) => Strong Tensor (Rep (Exp m) :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
Rep (Exp m) x y -> Rep (Exp m) (Act Tensor a x) (Act Tensor a y)
act @a (Rep @y @_ @x x ~> (Exp m @ y)
p) =
    x ~> (Exp m @ y)
x ~> (m ~~> y)
p (x ~> (m ~~> y))
-> ((Ob x, Ob (m ~~> y)) => Rep (Exp m) (a ** x) (a ** y))
-> Rep (Exp m) (a ** x) (a ** y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @x
        ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @y
            ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @y
                (((a ** x) ~> (Exp m @ (a ** y))) -> Rep (Exp m) (a ** x) (a ** y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @(a ** x) @m ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a
-> (((m ~~> y) ** m) ~> y) -> (a ** ((m ~~> y) ** m)) ~> (a ** y)
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)
** forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @m @y) ((a ** ((m ~~> y) ** m)) ~> (a ** y))
-> (((a ** x) ** m) ~> (a ** ((m ~~> y) ** m)))
-> ((a ** x) ** m) ~> (a ** y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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))
associator @k @a @(m ~~> y) @m (((a ** (m ~~> y)) ** m) ~> (a ** ((m ~~> y) ** m)))
-> (((a ** x) ** m) ~> ((a ** (m ~~> y)) ** m))
-> ((a ** x) ** m) ~> (a ** ((m ~~> y) ** m))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (x ~> (m ~~> y)) -> (a ** x) ~> (a ** (m ~~> y))
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)
** x ~> (Exp m @ y)
x ~> (m ~~> y)
p) ((a ** x) ~> (a ** (m ~~> y)))
-> (m ~> m) -> ((a ** x) ** m) ~> ((a ** (m ~~> y)) ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m))))
            )
        )
instance (Closed k, HasCoproducts k, Comonoid (m :: k)) => Strong CoprodAction (Rep (Exp m) :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
Rep (Exp m) x y
-> Rep (Exp m) (Act CoprodAction a x) (Act CoprodAction a y)
act @(COPR a) (Rep @y x ~> (Exp m @ y)
p) =
    x ~> (Exp m @ y)
x ~> (m ~~> y)
p (x ~> (m ~~> y))
-> ((Ob x, Ob (m ~~> y)) =>
    Rep (Exp m) (UN COPR a || x) (UN COPR a || y))
-> Rep (Exp m) (UN COPR a || x) (UN COPR a || y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @y
        ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @a
            ( forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @m @y
                ( ((UN COPR a || x) ~> (Exp m @ (UN COPR a || y)))
-> Rep (Exp m) (UN COPR a || x) (UN COPR a || y)
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep
                    ((forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @y (UN COPR a ~> (UN COPR a || y))
-> (m ~> m) -> (m ~~> UN COPR a) ~> (m ~~> (UN COPR a || y))
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 @m) ((m ~~> UN COPR a) ~> (m ~~> (UN COPR a || y)))
-> (UN COPR a ~> (m ~~> UN COPR a))
-> UN COPR a ~> (m ~~> (UN COPR a || y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @m (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @a ((UN COPR a ** Unit) ~> UN COPR a)
-> ((UN COPR a ** m) ~> (UN COPR a ** Unit))
-> (UN COPR a ** m) ~> UN COPR a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj (UN COPR a)
-> (m ~> Unit) -> (UN COPR a ** m) ~> (UN COPR a ** Unit)
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)
** forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @m)) (UN COPR a ~> (m ~~> (UN COPR a || y)))
-> (x ~> (m ~~> (UN COPR a || y)))
-> (UN COPR a || x) ~> (m ~~> (UN COPR a || y))
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
||| (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @y (y ~> (UN COPR a || y))
-> (m ~> m) -> (m ~~> y) ~> (m ~~> (UN COPR a || y))
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 @m) ((m ~~> y) ~> (m ~~> (UN COPR a || y)))
-> (x ~> (m ~~> y)) -> x ~> (m ~~> (UN COPR a || y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> (Exp m @ y)
x ~> (m ~~> y)
p)
                )
            )
        )

-- | The free-category structure for @'Supplies' 'Monoid'@: every object gets formal 'mappend'
-- ('Join') and 'mempty' ('Sprout') generators, interpreted by 'foldStructure' through the
-- target's own supply.
instance ('[Supplies Monoid, Monoidal] `Elems` cs) => HasStructure cs (p :: CAT k) (Supplies Monoid) where
  data Struct (Supplies Monoid) i o where
    Join :: (Ob a) => Struct (Supplies Monoid) (a **! a) a
    Sprout :: (Ob a) => Struct (Supplies Monoid) UnitF a
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(Supplies Monoid k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct (Supplies Monoid) a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Join @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall (m :: k'). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @(Lower f a))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Sprout @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall (m :: k'). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @(Lower f a))

instance P.Show (Struct (Supplies Monoid) a b) where
  showsPrec :: Int -> Struct (Supplies Monoid) a b -> ShowS
showsPrec Int
_ Struct (Supplies Monoid) a b
R:StructkcspSuppliesio1 k cs p a b
Join = String -> ShowS
P.showString String
"mappend"
  showsPrec Int
_ Struct (Supplies Monoid) a b
R:StructkcspSuppliesio1 k cs p a b
Sprout = String -> ShowS
P.showString String
"mempty"

-- | The free-category structure for @'Supplies' 'Comonoid'@, dually: formal 'comult' ('Fork') and
-- 'counit' ('Prune') generators for every object.
instance ('[Supplies Comonoid, Monoidal] `Elems` cs) => HasStructure cs (p :: CAT k) (Supplies Comonoid) where
  data Struct (Supplies Comonoid) i o where
    Fork :: (Ob a) => Struct (Supplies Comonoid) a (a **! a)
    Prune :: (Ob a) => Struct (Supplies Comonoid) a UnitF
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(Supplies Comonoid k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct (Supplies Comonoid) a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Fork @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall (c :: k'). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @(Lower f a))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Prune @a) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall (c :: k'). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @(Lower f a))

instance P.Show (Struct (Supplies Comonoid) a b) where
  showsPrec :: Int -> Struct (Supplies Comonoid) a b -> ShowS
showsPrec Int
_ Struct (Supplies Comonoid) a b
R:StructkcspSuppliesio k cs p a b
Fork = String -> ShowS
P.showString String
"comult"
  showsPrec Int
_ Struct (Supplies Comonoid) a b
R:StructkcspSuppliesio k cs p a b
Prune = String -> ShowS
P.showString String
"counit"

instance
  ('[Supplies Monoid, Monoidal] `Elems` cs, Ob (a :: FREE cs (p :: CAT k)))
  => Monoid (a :: FREE cs p)
  where
  mempty :: Unit ~> a
mempty = Struct (Supplies Monoid) UnitF a
-> Free UnitF UnitF -> Free UnitF a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St Struct (Supplies Monoid) UnitF a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct (Supplies Monoid) UnitF a
Sprout Free UnitF UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil
  mappend :: (a ** a) ~> a
mappend = Struct (Supplies Monoid) (a **! a) a
-> Free (a **! a) (a **! a) -> Free (a **! a) a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St Struct (Supplies Monoid) (a **! a) a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct (Supplies Monoid) (a **! a) a
Join Free (a **! a) (a **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil

-- | The free supply is commutative only up to interpretation ('FREE' has no equations); the marker
-- holds because every @'Proarrow.Category.Instance.Free.fold'@ of these arrows into a target lands in that target's commutative
-- monoid.
instance (Monoid (a :: FREE cs p), SymMonoidal (FREE cs p)) => CommutativeMonoid (a :: FREE cs p)

instance
  ('[Supplies Comonoid, Monoidal] `Elems` cs, Ob (a :: FREE cs (p :: CAT k)))
  => Comonoid (a :: FREE cs p)
  where
  counit :: a ~> Unit
counit = Struct (Supplies Comonoid) a UnitF -> Free a a -> Free a UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St Struct (Supplies Comonoid) a UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct (Supplies Comonoid) a UnitF
Prune Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil
  comult :: a ~> (a ** a)
comult = Struct (Supplies Comonoid) a (a **! a)
-> Free a a -> Free a (a **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
F.St Struct (Supplies Comonoid) a (a **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct (Supplies Comonoid) a (a **! a)
Fork Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
F.Nil

instance (Comonoid (a :: FREE cs p), SymMonoidal (FREE cs p)) => CocommutativeComonoid (a :: FREE cs p)

-- | Collapse an @n@-fold tensor power of a monoid with 'mappend', bottoming out at 'mempty'.
fanIn :: forall n a. (SNatI n, Monoid a) => NFold n a ~> a
fanIn :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
fanIn = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Unit ~> a
NFold n a ~> a
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  SS @n' -> forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a)
-> ((a ** NFold n1 a) ~> (a ** a)) -> (a ** NFold n1 a) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (NFold n1 a ~> a) -> (a ** NFold n1 a) ~> (a ** a)
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)
** forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
forall (n :: Nat) (a :: k). (SNatI n, Monoid a) => NFold n a ~> a
fanIn @n' @a)

-- | Dually, build an @n@-fold tensor power of a comonoid with 'comult', bottoming out at 'counit'.
fanOut :: forall n a. (SNatI n, Comonoid a) => a ~> NFold n a
fanOut :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
fanOut = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> a ~> Unit
a ~> NFold n a
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  SS @n' -> (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> NFold n1 a) -> (a ** a) ~> (a ** NFold n1 a)
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)
** forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
forall (n :: Nat) (a :: k). (SNatI n, Comonoid a) => a ~> NFold n a
fanOut @n' @a) ((a ** a) ~> (a ** NFold n1 a))
-> (a ~> (a ** a)) -> a ~> (a ** NFold n1 a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a

-- | The 'Proarrow.Category.Monoidal.Strictified.Strictified' counterpart of 'fanIn'.
fanInS :: forall n a. (SNatI n, Monoid a) => NFoldS n a ~> '[a]
fanInS :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
fanInS =
  case forall (n :: Nat). SNatI n => SNat n
snat @n of
    SNat n
SZ -> (Fold '[] ~> Fold '[a]) -> Strictified '[] '[a]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Unit ~> a
Fold '[] ~> Fold '[a]
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
    SS @n' -> forall (m :: k). Monoid m => '[m, m] ~> '[m]
forall {k} (m :: k). Monoid m => '[m, m] ~> '[m]
mappendS @a Strictified '[a, a] '[a]
-> Strictified (a : NFoldS n1 a) '[a, a]
-> Strictified (a : NFoldS n1 a) '[a]
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @a Strictified '[a] '[a]
-> Strictified (NFoldS n1 a) '[a]
-> Strictified ('[a] ** NFoldS n1 a) ('[a] ** '[a])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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)
** forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
forall (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
fanInS @n' @a)

-- | The 'Proarrow.Category.Monoidal.Strictified.Strictified' counterpart of 'fanOut'.
fanOutS :: forall n a. (SNatI n, Comonoid a) => '[a] ~> NFoldS n a
fanOutS :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
fanOutS =
  case forall (n :: Nat). SNatI n => SNat n
snat @n of
    SNat n
SZ -> (Fold '[a] ~> Fold '[]) -> Strictified '[a] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> Unit
Fold '[a] ~> Fold '[]
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
    SS @n' -> (forall (a :: k). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @a Strictified '[a] '[a]
-> Strictified '[a] (NFoldS n1 a)
-> Strictified ('[a] ** '[a]) ('[a] ** NFoldS n1 a)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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)
** forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
forall (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
fanOutS @n' @a) Strictified ('[a] ++ '[a]) (a : NFoldS n1 a)
-> Strictified '[a] ('[a] ++ '[a])
-> Strictified '[a] (a : NFoldS n1 a)
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => '[c] ~> '[c, c]
forall {k} (c :: k). Comonoid c => '[c] ~> '[c, c]
comultS @a

-- | In a category that supplies monoids, every object is one: 'mempty' is a unit for 'mappend' (up
-- to the unitors), and 'mappend' is associative (up to the associator).
instance Laws '[Monoidal, Supplies Monoid] where
  laws :: [Law '[Monoidal, Supplies Monoid]]
laws =
    [ String
-> LawBody '[Monoidal, Supplies Monoid]
-> Law '[Monoidal, Supplies Monoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"left unit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @Unit @a (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @a ((Unit ** a) ~> a) -> ((Unit ** a) ~> a) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a) -> ((Unit ** a) ~> (a ** a)) -> (Unit ** a) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @a (Unit ~> a) -> (a ~> a) -> (Unit ** a) ~> (a ** a)
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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a))
    , String
-> LawBody '[Monoidal, Supplies Monoid]
-> Law '[Monoidal, Supplies Monoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"right unit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @Unit (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @_ @a ((a ** Unit) ~> a) -> ((a ** Unit) ~> a) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a) -> ((a ** Unit) ~> (a ** a)) -> (a ** Unit) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (Unit ~> a) -> (a ** Unit) ~> (a ** a)
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)
** forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @a))
    , String
-> LawBody '[Monoidal, Supplies Monoid]
-> Law '[Monoidal, Supplies Monoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"associativity" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @a ((Ob (a ** a) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** a) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
P.$
          forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a)
-> (((a ** a) ** a) ~> (a ** a)) -> ((a ** a) ** a) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a) -> (a ~> a) -> ((a ** a) ** a) ~> (a ** a)
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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (((a ** a) ** a) ~> a) -> (((a ** a) ** a) ~> a) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a)
-> (((a ** a) ** a) ~> (a ** a)) -> ((a ** a) ** a) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a (a ~> a) -> ((a ** a) ~> a) -> (a ** (a ** a)) ~> (a ** a)
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)
** forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a) ((a ** (a ** a)) ~> (a ** a))
-> (((a ** a) ** a) ~> (a ** (a ** a)))
-> ((a ** a) ** a) ~> (a ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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))
associator @_ @a @a @a
    ]

-- | In a category that supplies comonoids, every object is one: 'counit' is a unit for 'comult', and
-- 'comult' is coassociative.
instance Laws '[Monoidal, Supplies Comonoid] where
  laws :: [Law '[Monoidal, Supplies Comonoid]]
laws =
    [ String
-> LawBody '[Monoidal, Supplies Comonoid]
-> Law '[Monoidal, Supplies Comonoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"left counit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @Unit @a (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @a (a ~> (Unit ** a)) -> (a ~> (Unit ** a)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @a (a ~> Unit) -> (a ~> a) -> (a ** a) ~> (Unit ** a)
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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((a ** a) ~> (Unit ** a)) -> (a ~> (a ** a)) -> a ~> (Unit ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a)
    , String
-> LawBody '[Monoidal, Supplies Comonoid]
-> Law '[Monoidal, Supplies Comonoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"right counit" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @Unit (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @a (a ~> (a ** Unit)) -> (a ~> (a ** Unit)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> Unit) -> (a ** a) ~> (a ** Unit)
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)
** forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @a) ((a ** a) ~> (a ** Unit)) -> (a ~> (a ** a)) -> a ~> (a ** Unit)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a)
    , String
-> LawBody '[Monoidal, Supplies Comonoid]
-> Law '[Monoidal, Supplies Comonoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"coassociativity" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @a ((Ob (a ** a) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** a) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
P.$
          forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @a @a (((a ** a) ** a) ~> (a ** (a ** a)))
-> (a ~> ((a ** a) ** a)) -> a ~> (a ** (a ** a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a (a ~> (a ** a)) -> (a ~> a) -> (a ** a) ~> ((a ** a) ** a)
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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((a ** a) ~> ((a ** a) ** a))
-> (a ~> (a ** a)) -> a ~> ((a ** a) ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a (a ~> (a ** (a ** a))) -> (a ~> (a ** (a ** a))) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a (a ~> a) -> (a ~> (a ** a)) -> (a ** a) ~> (a ** (a ** a))
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)
** forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a) ((a ** a) ~> (a ** (a ** a)))
-> (a ~> (a ** a)) -> a ~> (a ** (a ** a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a
    ]

-- | The supplied monoids are commutative: 'mappend' is unchanged by 'swap'.
instance Laws '[Monoidal, SymMonoidal, Supplies CommutativeMonoid] where
  laws :: [Law '[Monoidal, SymMonoidal, Supplies CommutativeMonoid]]
laws = [String
-> LawBody '[Monoidal, SymMonoidal, Supplies CommutativeMonoid]
-> Law '[Monoidal, SymMonoidal, Supplies CommutativeMonoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"commutativity" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @a (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a) -> ((a ** a) ~> a) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a) -> ((a ** a) ~> (a ** a)) -> (a ** a) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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)
swap @_ @a @a)]

-- | The supplied comonoids are cocommutative: 'comult' is unchanged by 'swap'.
instance Laws '[Monoidal, SymMonoidal, Supplies CocommutativeComonoid] where
  laws :: [Law '[Monoidal, SymMonoidal, Supplies CocommutativeComonoid]]
laws = [String
-> LawBody '[Monoidal, SymMonoidal, Supplies CocommutativeComonoid]
-> Law '[Monoidal, SymMonoidal, Supplies CocommutativeComonoid]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"cocommutativity" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @a (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a (a ~> (a ** a)) -> (a ~> (a ** a)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @a ((a ** a) ~> (a ** a)) -> (a ~> (a ** a)) -> a ~> (a ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a)]