{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Algebraic (module Exports, type (:+*+:), type (:*+*:)) where

import Pandora.Paradigm.Algebraic.Functor as Exports
import Pandora.Paradigm.Algebraic.Exponential as Exports
import Pandora.Paradigm.Algebraic.Product as Exports
import Pandora.Paradigm.Algebraic.Sum as Exports
import Pandora.Paradigm.Algebraic.Zero as Exports
import Pandora.Paradigm.Algebraic.One as Exports

import Pandora.Core.Interpreted (Interpreted ((<~)))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--), (<-|---)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U))

instance (Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) u) => Semimonoidal (<--) (:*:) (:*:) (t <:*:> u) where
	mult :: ((<:*:>) t u a :*: (<:*:>) t u b) <-- (<:*:>) t u (a :*: b)
mult = ((<:*:>) t u (a :*: b) -> (<:*:>) t u a :*: (<:*:>) t u b)
-> ((<:*:>) t u a :*: (<:*:>) t u b) <-- (<:*:>) t u (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<:*:>) t u (a :*: b) -> (<:*:>) t u a :*: (<:*:>) t u b)
 -> ((<:*:>) t u a :*: (<:*:>) t u b) <-- (<:*:>) t u (a :*: b))
-> ((<:*:>) t u (a :*: b) -> (<:*:>) t u a :*: (<:*:>) t u b)
-> ((<:*:>) t u a :*: (<:*:>) t u b) <-- (<:*:>) t u (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U t (a :*: b) :*: u (a :*: b)
lrxys) ->
		-- TODO: I need matrix transposing here
		let ((t a
lxs :*: t b
lys) :*: (u a
rxs :*: u b
rys)) = (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) (t (a :*: b) -> t a :*: t b)
-> (t (a :*: b) :*: (u a :*: u b))
-> (t a :*: t b) :*: (u a :*: u b)
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-- (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((u a :*: u b) <-- u (a :*: b)) -> u (a :*: b) -> u a :*: u b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) (u (a :*: b) -> u a :*: u b)
-> (t (a :*: b) :*: u (a :*: b)) -> t (a :*: b) :*: (u a :*: u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t (a :*: b) :*: u (a :*: b)
lrxys in
		(t a :*: u a) -> (<:*:>) t u a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U (t a
lxs t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
rxs) (<:*:>) t u a -> (<:*:>) t u b -> (<:*:>) t u a :*: (<:*:>) t u b
forall s a. s -> a -> s :*: a
:*: (t b :*: u b) -> (<:*:>) t u b
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U (t b
lys t b -> u b -> t b :*: u b
forall s a. s -> a -> s :*: a
:*: u b
rys)

instance (Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => Semimonoidal (-->) (:*:) (:*:) (t <:*:> u) where
	mult :: ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :*: b)
mult = (((<:*:>) t u a :*: (<:*:>) t u b) -> (<:*:>) t u (a :*: b))
-> ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((<:*:>) t u a :*: (<:*:>) t u b) -> (<:*:>) t u (a :*: b))
 -> ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :*: b))
-> (((<:*:>) t u a :*: (<:*:>) t u b) -> (<:*:>) t u (a :*: b))
-> ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U (t a
xls :*: u a
xrs) :*: T_U (t b
yls :*: u b
yrs)) -> (t (a :*: b) :*: u (a :*: b)) -> (<:*:>) t u (a :*: b)
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t (a :*: b) :*: u (a :*: b)) -> (<:*:>) t u (a :*: b))
-> (t (a :*: b) :*: u (a :*: b)) -> (<:*:>) t u (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) (t a
xls t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yls) t (a :*: b) -> u (a :*: b) -> t (a :*: b) :*: u (a :*: b)
forall s a. s -> a -> s :*: a
:*: (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((u a :*: u b) --> u (a :*: b)) -> (u a :*: u b) -> u (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) (u a
xrs u a -> u b -> u a :*: u b
forall s a. s -> a -> s :*: a
:*: u b
yrs)

instance (Semimonoidal (-->) (:*:) (:+:) t, Semimonoidal (-->) (:*:) (:+:) u) => Semimonoidal (-->) (:*:) (:+:) (t <:*:> u) where
	mult :: ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :+: b)
mult = (((<:*:>) t u a :*: (<:*:>) t u b) -> (<:*:>) t u (a :+: b))
-> ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :+: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((<:*:>) t u a :*: (<:*:>) t u b) -> (<:*:>) t u (a :+: b))
 -> ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :+: b))
-> (((<:*:>) t u a :*: (<:*:>) t u b) -> (<:*:>) t u (a :+: b))
-> ((<:*:>) t u a :*: (<:*:>) t u b) --> (<:*:>) t u (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(T_U (t a
xls :*: u a
xrs) :*: T_U (t b
yls :*: u b
yrs)) ->
		(forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (t :: * -> *) a b.
Semimonoidal (-->) (:*:) (:+:) t =>
(t a :*: t b) --> t (a :+: b)
mult @(-->) @(:*:) @(:+:) ((t a :*: t b) --> t (a :+: b)) -> (t a :*: t b) -> t (a :+: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (t a
xls t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yls)) t (a :+: b) -> u (a :+: b) -> (<:*:>) t u (a :+: b)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (t :: * -> *) a b.
Semimonoidal (-->) (:*:) (:+:) t =>
(t a :*: t b) --> t (a :+: b)
mult @(-->) @(:*:) @(:+:) ((u a :*: u b) --> u (a :+: b)) -> (u a :*: u b) -> u (a :+: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (u a
xrs u a -> u b -> u a :*: u b
forall s a. s -> a -> s :*: a
:*: u b
yrs))

instance (Monoidal (-->) (-->) (:*:) (:+:) t, Monoidal (-->) (-->) (:*:) (:+:) u)
	=> Monoidal (-->) (-->) (:*:) (:+:) (t <:*:> u) where
		unit :: Proxy (:*:) -> (Unit (:+:) --> a) --> (<:*:>) t u a
unit Proxy (:*:)
_ = ((Zero --> a) -> (<:*:>) t u a)
-> Straight (->) (Zero --> a) ((<:*:>) t u a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Zero --> a) -> (<:*:>) t u a)
 -> Straight (->) (Zero --> a) ((<:*:>) t u a))
-> ((Zero --> a) -> (<:*:>) t u a)
-> Straight (->) (Zero --> a) ((<:*:>) t u a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Zero --> a
_ -> t a
forall (t :: * -> *) a. Emptiable t => t a
empty t a -> u a -> (<:*:>) t u a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> u a
forall (t :: * -> *) a. Emptiable t => t a
empty

instance (Traversable (->) (->) t, Traversable (->) (->) u) => Traversable (->) (->) (t <:*:> u) where
	a -> u b
f <-/- :: (a -> u b) -> (<:*:>) t u a -> u ((<:*:>) t u b)
<-/- T_U (t a
xs :*: u a
ys) = (t b :*: u b) -> (<:*:>) t u b
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t b :*: u b) -> (<:*:>) t u b)
-> u (t b :*: u b) -> u ((<:*:>) t u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|--- t b -> u b -> t b :*: u b
forall s a. s -> a -> s :*: a
(:*:) (t b -> u b -> t b :*: u b) -> u (t b) -> u (u b -> t b :*: u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<-/- t a
xs u (u b -> t b :*: u b) -> u (u b) -> u (t b :*: u b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- a -> u b
f (a -> u b) -> u a -> u (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<-/- u a
ys

instance Traversable (->) (->) ((:*:) s) where
	a -> u b
f <-/- :: (a -> u b) -> (s :*: a) -> u (s :*: b)
<-/- s :*: a
x = ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*:) (b -> s :*: b) -> u b -> u (s :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f ((s :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract s :*: a
x)

instance Semimonoidal (-->) (:*:) (:*:) ((->) e) where
	mult :: ((e -> a) :*: (e -> b)) --> (e -> (a :*: b))
	mult :: ((e -> a) :*: (e -> b)) --> (e -> a :*: b)
mult = (((e -> a) :*: (e -> b)) -> e -> a :*: b)
-> ((e -> a) :*: (e -> b)) --> (e -> a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((e -> a) :*: (e -> b)) -> e -> a :*: b)
 -> ((e -> a) :*: (e -> b)) --> (e -> a :*: b))
-> (((e -> a) :*: (e -> b)) -> e -> a :*: b)
-> ((e -> a) :*: (e -> b)) --> (e -> a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(e -> a
g :*: e -> b
h) -> \e
x -> e -> a
g e
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: e -> b
h e
x

instance Monoidal (-->) (-->) (:*:) (:*:) ((->) e) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> (e -> a)
unit Proxy (:*:)
_ = (Straight (->) One a -> e -> a)
-> Straight (->) (Straight (->) One a) (e -> a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> e -> a)
 -> Straight (->) (Straight (->) One a) (e -> a))
-> (Straight (->) One a -> e -> a)
-> Straight (->) (Straight (->) One a) (e -> a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> e -> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (a -> e -> a)
-> (Straight (->) One a -> a) -> Straight (->) One a -> e -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

instance Semimonoidal (<--) (:*:) (:*:) ((->) e) where
	mult :: ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
	mult :: ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
mult = ((e -> a :*: b) -> (e -> a) :*: (e -> b))
-> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((e -> a :*: b) -> (e -> a) :*: (e -> b))
 -> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b))
-> ((e -> a :*: b) -> (e -> a) :*: (e -> b))
-> ((e -> a) :*: (e -> b)) <-- (e -> a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \e -> a :*: b
f -> (a :*: b) -> a
forall a b. (a :*: b) -> a
attached ((a :*: b) -> a) -> (e -> a :*: b) -> e -> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> a :*: b
f (e -> a) -> (e -> b) -> (e -> a) :*: (e -> b)
forall s a. s -> a -> s :*: a
:*: (a :*: b) -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((a :*: b) -> b) -> (e -> a :*: b) -> e -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> a :*: b
f

instance Semimonoidal (-->) (:*:) (:+:) ((:+:) e) where
	mult :: ((e :+: a) :*: (e :+: b)) --> (e :+: a :+: b)
	mult :: ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b))
mult = (((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b))
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b))
 -> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b)))
-> (((e :+: a) :*: (e :+: b)) -> e :+: (a :+: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :+: b))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Option e
_ :*: Option e
e' -> e -> e :+: (a :+: b)
forall o a. o -> o :+: a
Option e
e'
		Option e
_ :*: Adoption b
y -> (a :+: b) -> e :+: (a :+: b)
forall o a. a -> o :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- b -> a :+: b
forall o a. a -> o :+: a
Adoption b
y
		Adoption a
x :*: e :+: b
_ -> (a :+: b) -> e :+: (a :+: b)
forall o a. a -> o :+: a
Adoption ((a :+: b) -> e :+: (a :+: b)) -> (a :+: b) -> e :+: (a :+: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> a :+: b
forall o a. o -> o :+: a
Option a
x

instance Semimonoidal (-->) (:*:) (:*:) ((:+:) e) where
	mult :: ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b))
mult = (((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b))
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b))
 -> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b)))
-> (((e :+: a) :*: (e :+: b)) -> e :+: (a :*: b))
-> ((e :+: a) :*: (e :+: b)) --> (e :+: (a :*: b))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Adoption a
x :*: Adoption b
y -> (a :*: b) -> e :+: (a :*: b)
forall o a. a -> o :+: a
Adoption ((a :*: b) -> e :+: (a :*: b)) -> (a :*: b) -> e :+: (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y
		Option e
e :*: e :+: b
_ -> e -> e :+: (a :*: b)
forall o a. o -> o :+: a
Option e
e
		e :+: a
_ :*: Option e
e -> e -> e :+: (a :*: b)
forall o a. o -> o :+: a
Option e
e

instance Monoidal (-->) (-->) (:*:) (:*:) ((:+:) e) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> (e :+: a)
unit Proxy (:*:)
_ = (Straight (->) One a -> e :+: a)
-> Straight (->) (Straight (->) One a) (e :+: a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> e :+: a)
 -> Straight (->) (Straight (->) One a) (e :+: a))
-> (Straight (->) One a -> e :+: a)
-> Straight (->) (Straight (->) One a) (e :+: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> e :+: a
forall o a. a -> o :+: a
Adoption (a -> e :+: a)
-> (Straight (->) One a -> a) -> Straight (->) One a -> e :+: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

instance Semimonoidal (<--) (:*:) (:*:) ((:*:) s) where
	mult :: ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
mult = ((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
-> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
 -> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b)))
-> ((s :*: (a :*: b)) -> (s :*: a) :*: (s :*: b))
-> ((s :*: a) :*: (s :*: b)) <-- (s :*: (a :*: b))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(s
s :*: a
x :*: b
y) -> (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (s :*: a) -> (s :*: b) -> (s :*: a) :*: (s :*: b)
forall s a. s -> a -> s :*: a
:*: (s
s s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: b
y)

instance Monoidal (<--) (-->) (:*:) (:*:) ((:*:) s) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- (s :*: a)
unit Proxy (:*:)
_ = ((s :*: a) -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (s :*: a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((s :*: a) -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (s :*: a))
-> ((s :*: a) -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (s :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(s
_ :*: a
x) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

instance Comonad (->) ((:*:) s) where

instance Semimonoidal (<--) (:*:) (:*:) (Flip (:*:) a) where
	mult :: (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
mult = (Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
-> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
 -> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b))
-> (Flip (:*:) a (a :*: b) -> Flip (:*:) a a :*: Flip (:*:) a b)
-> (Flip (:*:) a a :*: Flip (:*:) a b) <-- Flip (:*:) a (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Flip ((a
sx :*: b
sy) :*: a
r)) -> (a :*: a) -> Flip (:*:) a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (a
sx a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
r) Flip (:*:) a a
-> Flip (:*:) a b -> Flip (:*:) a a :*: Flip (:*:) a b
forall s a. s -> a -> s :*: a
:*: (b :*: a) -> Flip (:*:) a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (b
sy b -> a -> b :*: a
forall s a. s -> a -> s :*: a
:*: a
r)

instance Monoidal (<--) (-->) (:*:) (:*:) (Flip (:*:) a) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Flip (:*:) a a
unit Proxy (:*:)
_ = (Flip (:*:) a a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Flip (:*:) a a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Flip (:*:) a a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Flip (:*:) a a))
-> (Flip (:*:) a a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Flip (:*:) a a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Flip (a
s :*: a
_)) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
s)

type (:+*+:) l r = (l :+: r) :*: (r :+: l)

type (:*+*:) l r = (l :*: r) :+: (r :*: l)