module Data.Bifunctor.Monoidal
  ( -- * Semigroupal
    Semigroupal (..),

    -- * Unital
    Unital (..),

    -- * Monoidal
    Monoidal,
  )
where

--------------------------------------------------------------------------------

import Control.Applicative (Alternative (..), Applicative (..), pure, (<$>))
import Control.Category (Category (..))
import Control.Category.Cartesian (Cocartesian (..), Semicartesian (..))
import Control.Category.Tensor (Associative, Iso (..), Tensor (..))
import Control.Monad (Functor(..), Monad)
import Data.Biapplicative (Biapplicative (..), Bifunctor (..))
import Data.Bifunctor.Clown (Clown)
import Data.Bifunctor.Joker (Joker (..))
import Data.Either (Either, either)
import Data.Function (const, ($))
import Data.Profunctor (Forget (..), Profunctor (..), Star (..), Strong (..))
import Data.Semigroupoid (Semigroupoid (..))
import Data.These (These (..))
import Data.Tuple (fst, snd, uncurry)
import Data.Void (Void, absurd)
import Prelude (Either (..))

--------------------------------------------------------------------------------

-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is 'Semigroupal' if it supports a
-- natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\), which we call 'combine'.
--
-- === Laws
--
-- __Associativity:__
--
-- \[ 
-- \require{AMScd}
-- \begin{CD}
-- (F A B \bullet F C D) \bullet F X Y                      @>>{\alpha_{\mathcal{D}}}>                              F A B \bullet (F C D \bullet F X Y) \\
-- @VV{\phi_{AB,CD} \bullet 1}V                                                                                     @VV{1 \bullet \phi_{CD,FY}}V \\
-- F (A \otimes C) (B \otimes D) \bullet F X Y              @.                                                      F A B \bullet (F (C \otimes X) (D \otimes Y) \\
-- @VV{\phi_{(A \otimes C)(B \otimes D),XY}}V                                                                       @VV{\phi_{AB,(C \otimes X)(D \otimes Y)}}V \\
-- F ((A \otimes C) \otimes X)  ((B \otimes D) \otimes Y)   @>>{F \alpha_{\mathcal{C_1}}} \alpha_{\mathcal{C_2}}>   F (A \otimes (C \otimes X)) (B \otimes (D \otimes Y)) \\
-- \end{CD}
-- \]
--
-- @
-- 'combine' 'Control.Category..' 'Control.Category.Tensor.grmap' 'combine' 'Control.Category..' 'bwd' 'Control.Category.Tensor.assoc' ≡ 'fmap' ('bwd' 'Control.Category.Tensor.assoc') 'Control.Category..' 'combine' 'Control.Category..' 'Control.Category.Tensor.glmap' 'combine'
-- @
class (Associative cat t1, Associative cat t2, Associative cat to) => Semigroupal cat t1 t2 to f where
  -- | A natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\). 
  --
  -- ==== __Examples__
  --
  -- >>> :t combine @(->) @(,) @(,) @(,) @(,)
  -- combine @(->) @(,) @(,) @(,) @(,) :: ((x, y), (x', y')) -> ((x, x'), (y, y'))
  --
  -- >>> combine @(->) @(,) @(,) @(,) @(,) ((True, "Hello"), ((), "World"))
  -- ((True,()),("Hello","World"))
  --
  -- >>> combine @(->) @(,) @(,) @(,) @(->) (show, (>10)) (True, 11)
  -- ("True",True)
  combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))

instance Profunctor p => Semigroupal (->) (,) Either Either p where
  combine :: Either (p x y) (p x' y') -> p (x, x') (Either y y')
  combine :: forall x y x' y'.
Either (p x y) (p x' y') -> p (x, x') (Either y y')
combine = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. (a, b) -> a
fst forall a b. a -> Either a b
Left) (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. (a, b) -> b
snd forall a b. b -> Either a b
Right)

instance Semigroupal (->) (,) (,) (,) (,) where
  combine :: ((x, y), (x', y')) -> ((x, x'), (y, y'))
  combine :: forall x y x' y'. ((x, y), (x', y')) -> ((x, x'), (y, y'))
combine ((x
x, y
y), (x'
x', y'
y')) = ((x
x, x'
x'), (y
y, y'
y'))
  -- NOTE: This version could be used for a more general abstraction
  -- of products in a category:
  -- combine =
  --   let fwd' = fwd assoc
  --       bwd' = bwd assoc
  --   in second swap . swap . fwd' . swap . first (bwd' . first swap) . fwd'

instance Semigroupal (->) Either Either Either (,) where
  combine :: Either (x, y) (x', y') -> (Either x x', Either y y')
  combine :: forall x y x' y'.
Either (x, y) (x', y') -> (Either x x', Either y y')
combine = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a b. a -> Either a b
Left forall a b. a -> Either a b
Left) (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a b. b -> Either a b
Right forall a b. b -> Either a b
Right)

instance Semigroupal (->) Either Either Either Either where
  combine :: Either (Either x y) (Either x' y') -> Either (Either x x') (Either y y')
  combine :: forall x y x' y'.
Either (Either x y) (Either x' y')
-> Either (Either x x') (Either y y')
combine = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a b. a -> Either a b
Left forall a b. a -> Either a b
Left) (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a b. b -> Either a b
Right forall a b. b -> Either a b
Right)

instance Semigroupal (->) Either (,) (,) Either where
  combine :: (Either x y, Either x' y') -> Either (Either x x') (y, y')
  combine :: forall x y x' y'.
(Either x y, Either x' y') -> Either (Either x x') (y, y')
combine = \case
    (Left x
x, Left x'
_)    -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left x
x
    (Left x
x, Right y'
_)   -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left x
x
    (Right y
_, Left x'
x')  -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right x'
x'
    (Right y
y, Right y'
y') -> forall a b. b -> Either a b
Right (y
y, y'
y')

instance Semigroupal (->) These (,) (,) Either where
  combine :: (Either x y, Either x' y') -> Either (These x x') (y, y')
  combine :: forall x y x' y'.
(Either x y, Either x' y') -> Either (These x x') (y, y')
combine = \case
    (Left x
x, Left x'
x')   -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> These a b
These x
x x'
x'
    (Left x
x, Right y'
_)   -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. a -> These a b
This x
x
    (Right y
_, Left x'
x')  -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a b. b -> These a b
That x'
x'
    (Right y
y, Right y'
y') -> forall a b. b -> Either a b
Right (y
y, y'
y')

instance Semigroupal (->) (,) (,) (,) (->) where
  combine :: (x -> y, x' -> y') -> (x, x') -> (y, y')
  combine :: forall x y x' y'. (x -> y, x' -> y') -> ((x, x') -> (y, y'))
combine = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap

instance Semigroupal (->) Either Either (,) (->) where
  combine :: (x -> y, x' -> y') -> Either x x' -> Either y y'
  combine :: forall x y x' y'.
(x -> y, x' -> y') -> (Either x x' -> Either y y')
combine (x -> y, x' -> y')
fs = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> a
fst (x -> y, x' -> y')
fs) (forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> b
snd (x -> y, x' -> y')
fs)

instance Applicative f => Semigroupal (->) (,) (,) (,) (Joker f) where
  combine :: (Joker f x y, Joker f x' y') -> Joker f (x, x') (y, y')
  combine :: forall x y x' y'.
(Joker f x y, Joker f x' y') -> Joker f (x, x') (y, y')
combine = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d e f.
Biapplicative p =>
(a -> b -> c) -> (d -> e -> f) -> p a d -> p b e -> p c f
biliftA2 (,) (,)

instance Alternative f => Semigroupal (->) Either Either (,) (Joker f) where
  combine :: (Joker f x y, Joker f x' y') -> Joker f (Either x x') (Either y y')
  combine :: forall x y x' y'.
(Joker f x y, Joker f x' y') -> Joker f (Either x x') (Either y y')
combine  = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d e f.
Biapplicative p =>
(a -> b -> c) -> (d -> e -> f) -> p a d -> p b e -> p c f
biliftA2 (\x
_ x'
x' -> forall a b. b -> Either a b
Right x'
x') (\y
_ y'
y' -> forall a b. b -> Either a b
Right y'
y')

instance Functor f => Semigroupal (->) Either Either Either (Joker f) where
  combine :: Either (Joker f x y) (Joker f x' y') -> Joker f (Either x x') (Either y y')
  combine :: forall x y x' y'.
Either (Joker f x y) (Joker f x' y')
-> Joker f (Either x x') (Either y y')
combine = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k1} {k2} (g :: k1 -> *) (a :: k2) (b :: k1).
Joker g a b -> g b
runJoker ) (forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k1} {k2} (g :: k1 -> *) (a :: k2) (b :: k1).
Joker g a b -> g b
runJoker)

instance Applicative f => Semigroupal (->) (,) (,) (,) (Clown f) where
  combine :: (Clown f x y, Clown f x' y') -> Clown f (x, x') (y, y')
  combine :: forall x y x' y'.
(Clown f x y, Clown f x' y') -> Clown f (x, x') (y, y')
combine = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d e f.
Biapplicative p =>
(a -> b -> c) -> (d -> e -> f) -> p a d -> p b e -> p c f
biliftA2 (,) (,)

instance Alternative f => Semigroupal (->) Either Either (,) (Clown f) where
  combine :: (Clown f x y, Clown f x' y') -> Clown f (Either x x') (Either y y')
  combine :: forall x y x' y'.
(Clown f x y, Clown f x' y') -> Clown f (Either x x') (Either y y')
combine = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d e f.
Biapplicative p =>
(a -> b -> c) -> (d -> e -> f) -> p a d -> p b e -> p c f
biliftA2 (\x
_ x'
x' -> forall a b. b -> Either a b
Right x'
x') (\y
_ y'
y' -> forall a b. b -> Either a b
Right y'
y')

instance Applicative f => Semigroupal (->) (,) (,) (,) (Star f) where
  combine :: (Star f x y, Star f x' y') -> Star f (x, x') (y, y')
  combine :: forall x y x' y'.
(Star f x y, Star f x' y') -> Star f (x, x') (y, y')
combine (Star x -> f y
fxy, Star x' -> f y'
fxy') = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ \(x
x, x'
x') -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (x -> f y
fxy x
x) (x' -> f y'
fxy' x'
x')

instance Functor f => Semigroupal (->) Either Either (,) (Star f) where
  combine :: (Star f x y, Star f x' y') -> Star f (Either x x') (Either y y')
  combine :: forall x y x' y'.
(Star f x y, Star f x' y') -> Star f (Either x x') (Either y y')
combine (Star x -> f y
fxy, Star x' -> f y'
fxy') = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. x -> f y
fxy) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. x' -> f y'
fxy')

instance Alternative f => Semigroupal (->) Either Either Either (Star f) where
  combine :: Either (Star f x y) (Star f x' y') -> Star f (Either x x') (Either y y')
  combine :: forall x y x' y'.
Either (Star f x y) (Star f x' y')
-> Star f (Either x x') (Either y y')
combine = \case
    Left (Star x -> f y
fxy)   -> forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. x -> f y
fxy) (forall a b. a -> b -> a
const forall (f :: * -> *) a. Alternative f => f a
empty)
    Right (Star x' -> f y'
fxy') -> forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall (f :: * -> *) a. Alternative f => f a
empty) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. x' -> f y'
fxy')

instance Alternative f => Semigroupal (->) (,) Either (,) (Star f) where
  combine :: (Star f x y, Star f x' y') -> Star f (x, x') (Either y y')
  combine :: forall x y x' y'.
(Star f x y, Star f x' y') -> Star f (x, x') (Either y y')
combine (Star x -> f y
f, Star x' -> f y'
g) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ \(x
x, x'
x') -> (forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x -> f y
f x
x) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x' -> f y'
g x'
x')

instance Alternative f => Semigroupal (->) (,) (,) (,) (Forget (f r)) where
  combine :: (Forget (f r) x y, Forget (f r) x' y') -> Forget (f r) (x, x') (y, y')
  combine :: forall x y x' y'.
(Forget (f r) x y, Forget (f r) x' y')
-> Forget (f r) (x, x') (y, y')
combine (Forget x -> f r
f, Forget x' -> f r
g) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget forall a b. (a -> b) -> a -> b
$ \(x
x, x'
x') -> x -> f r
f x
x forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> x' -> f r
g x'
x'

instance Semigroupal (->) Either Either (,) (Forget (f r)) where
  combine :: (Forget (f r) x y, Forget (f r) x' y') -> Forget (f r) (Either x x') (Either y y')
  combine :: forall x y x' y'.
(Forget (f r) x y, Forget (f r) x' y')
-> Forget (f r) (Either x x') (Either y y')
combine (Forget x -> f r
f, Forget x' -> f r
g) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either x -> f r
f x' -> f r
g

instance Alternative f => Semigroupal (->) Either Either Either (Forget (f r)) where
  combine :: Either (Forget (f r) x y) (Forget (f r) x' y') -> Forget (f r) (Either x x') (Either y y')
  combine :: forall x y x' y'.
Either (Forget (f r) x y) (Forget (f r) x' y')
-> Forget (f r) (Either x x') (Either y y')
combine = \case
    Left (Forget x -> f r
f)  -> forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either x -> f r
f (forall a b. a -> b -> a
const forall (f :: * -> *) a. Alternative f => f a
empty)
    Right (Forget x' -> f r
g) -> forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall (f :: * -> *) a. Alternative f => f a
empty) x' -> f r
g

instance Alternative f => Semigroupal (->) (,) Either (,) (Forget (f r)) where
  combine :: (Forget (f r) x y, Forget (f r) x' y') -> Forget (f r) (x, x') (Either y y')
  combine :: forall x y x' y'.
(Forget (f r) x y, Forget (f r) x' y')
-> Forget (f r) (x, x') (Either y y')
combine (Forget x -> f r
f, Forget x' -> f r
g) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget forall a b. (a -> b) -> a -> b
$ \(x
x, x'
x') -> x -> f r
f x
x forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> x' -> f r
g x'
x'

--------------------------------------------------------------------------------

-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is 'Unital' if it supports a morphism
-- \(\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C_1}}\ I_{\mathcal{C_2}}\), which we call 'introduce'.
class Unital cat i1 i2 io f where
  -- | @introduce@ maps from the identity in \(\mathcal{C_1} \times \mathcal{C_2}\) to the
  -- identity in \(\mathcal{D}\).
  --
  -- ==== __Examples__
  --
  -- >>> introduce @(->) @() @() @() @(,) ()
  -- ((),())
  --
  -- >>> :t introduce @(->) @Void @() @() @Either
  -- introduce @(->) @Void @() @() @Either :: () -> Either Void ()
  -- 
  -- >>> introduce @(->) @Void @() @() @Either ()
  -- Right ()
  introduce :: cat io (f i1 i2)

instance (Profunctor p, Category p) => Unital (->) () () () (StrongCategory p) where
  introduce :: () -> StrongCategory p () ()
  introduce :: () -> StrongCategory p () ()
introduce () = forall (p :: * -> * -> *) a b. p a b -> StrongCategory p a b
StrongCategory forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

instance Unital (->) () () () (,) where
  introduce :: () -> ((), ())
  introduce :: () -> ((), ())
introduce = forall (cat :: * -> * -> *) (t :: * -> * -> *) a.
Semicartesian cat t =>
cat a (t a a)
split

instance Unital (->) Void Void Void (,) where
  introduce :: Void -> (Void, Void)
  introduce :: Void -> (Void, Void)
introduce = forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Cocartesian cat t i =>
cat i a
spawn

instance Unital (->) Void Void Void Either where
  introduce :: Void -> Either Void Void
  introduce :: Void -> Either Void Void
introduce = forall (cat :: * -> * -> *) a b. Iso cat a b -> cat b a
bwd forall (cat :: * -> * -> *) (t :: * -> * -> *) i a.
Tensor cat t i =>
Iso cat (t a i) a
unitr

instance Unital (->) Void () () Either where
  introduce :: () -> Either Void ()
  introduce :: () -> Either Void ()
introduce = forall a b. b -> Either a b
Right

instance Unital (->) () () () (->) where
  introduce :: () -> () -> ()
  introduce :: () -> (() -> ())
introduce () () = ()

instance Unital (->) Void Void Void (->) where
  introduce :: Void -> Void -> Void
  introduce :: Void -> (Void -> Void)
introduce = forall a. Void -> a
absurd

instance (Unital (->) Void Void () (->)) where
  introduce :: () -> Void -> Void
  introduce :: () -> (Void -> Void)
introduce () = forall a. Void -> a
absurd

instance Applicative f => Unital (->) () () () (Joker f) where
  introduce :: () -> Joker f () ()
  introduce :: () -> Joker f () ()
introduce = forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Alternative f => Unital (->) Void Void () (Joker f) where
  introduce :: () -> Joker f Void Void
  introduce :: () -> Joker f Void Void
introduce () = forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker forall (f :: * -> *) a. Alternative f => f a
empty

instance Unital (->) Void Void Void (Joker f) where
  introduce :: Void -> Joker f Void Void
  introduce :: Void -> Joker f Void Void
introduce = forall a. Void -> a
absurd

instance Applicative f => Unital (->) () () () (Star f) where
  introduce :: () -> Star f () ()
  introduce :: () -> Star f () ()
introduce () = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Unital (->) Void Void () (Star f) where
  introduce :: () -> Star f Void Void
  introduce :: () -> Star f Void Void
introduce () = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a. Void -> a
absurd

instance Alternative f => Unital (->) Void Void Void (Star f) where
  introduce :: Void -> Star f Void Void
  introduce :: Void -> Star f Void Void
introduce = forall a. Void -> a
absurd

instance Alternative f => Unital (->) () Void () (Star f) where
  introduce :: () -> Star f () Void
  introduce :: () -> Star f () Void
introduce () = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (f :: * -> *) a. Alternative f => f a
empty

--------------------------------------------------------------------------------
-- Monoidal

-- | Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
-- A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is 'Monoidal' if it maps between \(\mathcal{C_1} \times \mathcal{C_2}\)
-- and \(\mathcal{D}\) while preserving their monoidal structure. Eg., a homomorphism of monoidal categories.
--
-- See <https://ncatlab.org/nlab/show/monoidal+functor NCatlab> for more details.
--
-- === Laws
--
-- __Right Unitality:__
--
-- \[ 
-- \require{AMScd}
-- \begin{CD}
-- F A B \bullet I_{\mathcal{D}}   @>{1 \bullet \phi}>>                                     F A B \bullet F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}}\\
-- @VV{\rho_{\mathcal{D}}}V                                                                 @VV{\phi AB,I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}}V \\
-- F A B                           @<<{F \rho_{\mathcal{C_{1}}} \rho_{\mathcal{C_{2}}}}<    F (A \otimes I_{\mathcal{C_{1}}}) (B \otimes I_{\mathcal{C_{2}}})
-- \end{CD}
-- \]
--
-- @
-- 'combine' 'Control.Category..' 'Control.Category.Tensor.grmap' 'introduce' ≡ 'bwd' 'unitr' 'Control.Category..' 'fwd' 'unitr'
-- @
--
-- __ Left Unitality__:
--
-- \[ 
-- \begin{CD}
-- I_{\mathcal{D}} \bullet F A B   @>{\phi \bullet 1}>>                                          F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} \bullet F A B\\
-- @VV{\lambda_{\mathcal{D}}}V                                                                   @VV{I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}},\phi AB}V \\
-- F A B                           @<<{F \lambda_{\mathcal{C_{1}}} \lambda_{\mathcal{C_{2}}}}<   F (I_{\mathcal{C_{1}}} \otimes A) (I_{\mathcal{C_{2}}} \otimes B)
-- \end{CD}
-- \]
--
-- @
-- 'combine' 'Control.Category..' 'Control.Category.Tensor.glmap' 'introduce' ≡ 'fmap' ('bwd' 'unitl') 'Control.Category..' 'fwd' 'unitl'
-- @
class ( Tensor cat t1 i1
      , Tensor cat t2 i2
      , Tensor cat to io
      , Semigroupal cat t1 t2 to f
      , Unital cat i1 i2 io f
      ) => Monoidal cat t1 i1 t2 i2 to io f

instance (Strong p, Semigroupoid p, Category p) => Monoidal (->) (,) () (,) () (,) () (StrongCategory p)
instance Monoidal (->) (,) () (,) () (,) () (,)
instance Monoidal (->) Either Void Either Void Either Void (,)
instance Monoidal (->) Either Void Either Void Either Void Either
instance Monoidal (->) Either Void (,) () (,) () Either
instance Monoidal (->) These Void (,) () (,) () Either
instance Monoidal (->) (,) () (,) () (,) () (->)
instance Monoidal (->) Either Void Either Void (,) () (->)
instance Applicative f => Monoidal (->) (,) () (,) () (,) () (Joker f)
instance Alternative f => Monoidal (->) Either Void Either Void (,) () (Joker f)
instance Functor f => Monoidal (->) Either Void Either Void Either Void (Joker f)
instance Applicative f => Monoidal (->) (,) () (,) () (,) () (Star f)
instance Functor f => Monoidal (->) Either Void Either Void (,) () (Star f)
instance Alternative f => Monoidal (->) Either Void Either Void Either Void (Star f)
instance Alternative f => Monoidal (->) (,) () Either Void (,) () (Star f)

newtype StrongCategory p a b = StrongCategory (p a b)
  deriving (forall a b. a -> StrongCategory p a b -> StrongCategory p a a
forall a b.
(a -> b) -> StrongCategory p a a -> StrongCategory p a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> StrongCategory p a b -> StrongCategory p a a
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> StrongCategory p a a -> StrongCategory p a b
<$ :: forall a b. a -> StrongCategory p a b -> StrongCategory p a a
$c<$ :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> StrongCategory p a b -> StrongCategory p a a
fmap :: forall a b.
(a -> b) -> StrongCategory p a a -> StrongCategory p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> StrongCategory p a a -> StrongCategory p a b
Functor, forall a. a -> StrongCategory p a a
forall a b.
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a a
forall a b.
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
forall a b.
StrongCategory p a (a -> b)
-> StrongCategory p a a -> StrongCategory p a b
forall a b c.
(a -> b -> c)
-> StrongCategory p a a
-> StrongCategory p a b
-> StrongCategory p a c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall {p :: * -> * -> *} {a}.
Applicative (p a) =>
Functor (StrongCategory p a)
forall (p :: * -> * -> *) a a.
Applicative (p a) =>
a -> StrongCategory p a a
forall (p :: * -> * -> *) a a b.
Applicative (p a) =>
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a a
forall (p :: * -> * -> *) a a b.
Applicative (p a) =>
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
forall (p :: * -> * -> *) a a b.
Applicative (p a) =>
StrongCategory p a (a -> b)
-> StrongCategory p a a -> StrongCategory p a b
forall (p :: * -> * -> *) a a b c.
Applicative (p a) =>
(a -> b -> c)
-> StrongCategory p a a
-> StrongCategory p a b
-> StrongCategory p a c
<* :: forall a b.
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a a
$c<* :: forall (p :: * -> * -> *) a a b.
Applicative (p a) =>
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a a
*> :: forall a b.
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
$c*> :: forall (p :: * -> * -> *) a a b.
Applicative (p a) =>
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
liftA2 :: forall a b c.
(a -> b -> c)
-> StrongCategory p a a
-> StrongCategory p a b
-> StrongCategory p a c
$cliftA2 :: forall (p :: * -> * -> *) a a b c.
Applicative (p a) =>
(a -> b -> c)
-> StrongCategory p a a
-> StrongCategory p a b
-> StrongCategory p a c
<*> :: forall a b.
StrongCategory p a (a -> b)
-> StrongCategory p a a -> StrongCategory p a b
$c<*> :: forall (p :: * -> * -> *) a a b.
Applicative (p a) =>
StrongCategory p a (a -> b)
-> StrongCategory p a a -> StrongCategory p a b
pure :: forall a. a -> StrongCategory p a a
$cpure :: forall (p :: * -> * -> *) a a.
Applicative (p a) =>
a -> StrongCategory p a a
Applicative, forall a. a -> StrongCategory p a a
forall a b.
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
forall a b.
StrongCategory p a a
-> (a -> StrongCategory p a b) -> StrongCategory p a b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall {p :: * -> * -> *} {a}.
Monad (p a) =>
Applicative (StrongCategory p a)
forall (p :: * -> * -> *) a a.
Monad (p a) =>
a -> StrongCategory p a a
forall (p :: * -> * -> *) a a b.
Monad (p a) =>
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
forall (p :: * -> * -> *) a a b.
Monad (p a) =>
StrongCategory p a a
-> (a -> StrongCategory p a b) -> StrongCategory p a b
return :: forall a. a -> StrongCategory p a a
$creturn :: forall (p :: * -> * -> *) a a.
Monad (p a) =>
a -> StrongCategory p a a
>> :: forall a b.
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
$c>> :: forall (p :: * -> * -> *) a a b.
Monad (p a) =>
StrongCategory p a a
-> StrongCategory p a b -> StrongCategory p a b
>>= :: forall a b.
StrongCategory p a a
-> (a -> StrongCategory p a b) -> StrongCategory p a b
$c>>= :: forall (p :: * -> * -> *) a a b.
Monad (p a) =>
StrongCategory p a a
-> (a -> StrongCategory p a b) -> StrongCategory p a b
Monad, forall a b c.
(a -> b) -> StrongCategory p b c -> StrongCategory p a c
forall b c a.
(b -> c) -> StrongCategory p a b -> StrongCategory p a c
forall a b c d.
(a -> b)
-> (c -> d) -> StrongCategory p b c -> StrongCategory p a d
forall a b c (q :: * -> * -> *).
Coercible b a =>
StrongCategory p b c -> q a b -> StrongCategory p a c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> StrongCategory p a b -> StrongCategory p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> StrongCategory p b c -> StrongCategory p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> StrongCategory p a b -> StrongCategory p a c
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> StrongCategory p b c -> StrongCategory p a d
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
StrongCategory p b c -> q a b -> StrongCategory p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> StrongCategory p a b -> StrongCategory p a c
forall (p :: * -> * -> *).
(forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d)
-> (forall a b c. (a -> b) -> p b c -> p a c)
-> (forall b c a. (b -> c) -> p a b -> p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> p a b -> p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    p b c -> q a b -> p a c)
-> Profunctor p
.# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
StrongCategory p b c -> q a b -> StrongCategory p a c
$c.# :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
StrongCategory p b c -> q a b -> StrongCategory p a c
#. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> StrongCategory p a b -> StrongCategory p a c
$c#. :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> StrongCategory p a b -> StrongCategory p a c
rmap :: forall b c a.
(b -> c) -> StrongCategory p a b -> StrongCategory p a c
$crmap :: forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> StrongCategory p a b -> StrongCategory p a c
lmap :: forall a b c.
(a -> b) -> StrongCategory p b c -> StrongCategory p a c
$clmap :: forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> StrongCategory p b c -> StrongCategory p a c
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> StrongCategory p b c -> StrongCategory p a d
$cdimap :: forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> StrongCategory p b c -> StrongCategory p a d
Profunctor, forall a. StrongCategory p a a
forall b c a.
StrongCategory p b c
-> StrongCategory p a b -> StrongCategory p a c
forall {k} (cat :: k -> k -> *).
(forall (a :: k). cat a a)
-> (forall (b :: k) (c :: k) (a :: k).
    cat b c -> cat a b -> cat a c)
-> Category cat
forall (p :: * -> * -> *) a. Category p => StrongCategory p a a
forall (p :: * -> * -> *) b c a.
Category p =>
StrongCategory p b c
-> StrongCategory p a b -> StrongCategory p a c
. :: forall b c a.
StrongCategory p b c
-> StrongCategory p a b -> StrongCategory p a c
$c. :: forall (p :: * -> * -> *) b c a.
Category p =>
StrongCategory p b c
-> StrongCategory p a b -> StrongCategory p a c
id :: forall a. StrongCategory p a a
$cid :: forall (p :: * -> * -> *) a. Category p => StrongCategory p a a
Category)

instance Semigroupoid p => Semigroupoid (StrongCategory p) where
  o :: StrongCategory p b c -> StrongCategory p a b -> StrongCategory p a c
  o :: forall j k1 i.
StrongCategory p j k1
-> StrongCategory p i j -> StrongCategory p i k1
o (StrongCategory p b c
f) (StrongCategory p a b
g) = forall (p :: * -> * -> *) a b. p a b -> StrongCategory p a b
StrongCategory (p b c
f forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` p a b
g)

instance (Strong p, Semigroupoid p) => Semigroupal (->) (,) (,) (,) (StrongCategory p) where
  combine :: (StrongCategory p x y, StrongCategory p x' y') -> StrongCategory p (x, x') (y, y')
  combine :: forall x y x' y'.
(StrongCategory p x y, StrongCategory p x' y')
-> StrongCategory p (x, x') (y, y')
combine (StrongCategory p x y
pxy, StrongCategory p x' y'
pxy') = forall (p :: * -> * -> *) a b. p a b -> StrongCategory p a b
StrongCategory forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p x y
pxy forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' p x' y'
pxy'