module Proarrow.Category.Enriched.Bipara where

import Data.Kind (Type)
import Prelude (($))

import Proarrow.Core (PRO, Kind, UN, Is, Profunctor(..), Promonad(..), CategoryOf (..), obj, (//))
import Proarrow.Category.Bicategory (Bicategory(I))
import Proarrow.Category.Bicategory.MonoidalAsBi (MonK(..), Mon2 (..))
import Proarrow.Category.Enriched (ECategory(..), V, Arr, type (%~>))
import Proarrow.Category.Instance.Prof (Prof(..))
import Proarrow.Category.Monoidal (Monoidal(..), first, second, swap', SymMonoidal)
import Proarrow.Profunctor.Day (DayUnit(..), Day (..))


type BIPARAK :: Kind -> () -> Kind
data BIPARAK k ext where
  BIPARA :: k -> BIPARAK k i
type instance UN BIPARA (BIPARA a) = a

type instance V (BIPARAK k) = MonK (PRO k k)
type instance Arr (MonK (PRO k k)) (BIPARA a) (BIPARA b) = MK (Bipara a b)

type Bipara :: k -> k -> k -> k -> Type
data Bipara a b p q where
  Bipara :: (Ob p, Ob q) => a ** p ~> q ** b -> Bipara a b p q

instance (Monoidal k, Ob a, Ob b) => Profunctor (Bipara (a :: k) b) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Bipara a b a b -> Bipara a b c d
dimap c ~> a
f b ~> d
g (Bipara (a ** a) ~> (b ** b)
h) = ((a ** c) ~> (d ** b)) -> Bipara a b c d
forall {k} (p :: k) (q :: k) (a :: k) (b :: k).
(Ob p, Ob q) =>
((a ** p) ~> (q ** b)) -> Bipara a b p q
Bipara (forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @b b ~> d
g ((b ** b) ~> (d ** b))
-> ((a ** c) ~> (b ** b)) -> (a ** c) ~> (d ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** a) ~> (b ** b)
h ((a ** a) ~> (b ** b))
-> ((a ** c) ~> (a ** a)) -> (a ** c) ~> (b ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @a c ~> a
f) ((Ob c, Ob a) => Bipara a b c d) -> (c ~> a) -> Bipara a b c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
f ((Ob b, Ob d) => Bipara a b c d) -> (b ~> d) -> Bipara a b c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
g
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Bipara a b a b -> r
\\ Bipara{} = r
(Ob a, Ob b) => r
r

-- | Bipara as a profunctor enriched category.
instance SymMonoidal k => ECategory (BIPARAK k) where

  type EOb a = (Is BIPARA a, Ob (UN BIPARA a))

  eid :: forall {exta} (a :: BIPARAK k exta). EOb a => I ~> (a %~> a)
  eid :: forall {exta :: ()} (a :: BIPARAK k exta). EOb a => I ~> (a %~> a)
eid = (DayUnit ~> Bipara (UN 'BIPARA a) (UN 'BIPARA a))
-> Mon2 ('MK DayUnit) ('MK (Bipara (UN 'BIPARA a) (UN 'BIPARA a)))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((DayUnit ~> Bipara (UN 'BIPARA a) (UN 'BIPARA a))
 -> Mon2 ('MK DayUnit) ('MK (Bipara (UN 'BIPARA a) (UN 'BIPARA a))))
-> (DayUnit ~> Bipara (UN 'BIPARA a) (UN 'BIPARA a))
-> Mon2 ('MK DayUnit) ('MK (Bipara (UN 'BIPARA a) (UN 'BIPARA a)))
forall a b. (a -> b) -> a -> b
$ (DayUnit :~> Bipara (UN 'BIPARA a) (UN 'BIPARA a))
-> Prof DayUnit (Bipara (UN 'BIPARA a) (UN 'BIPARA a))
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((DayUnit :~> Bipara (UN 'BIPARA a) (UN 'BIPARA a))
 -> Prof DayUnit (Bipara (UN 'BIPARA a) (UN 'BIPARA a)))
-> (DayUnit :~> Bipara (UN 'BIPARA a) (UN 'BIPARA a))
-> Prof DayUnit (Bipara (UN 'BIPARA a) (UN 'BIPARA a))
forall a b. (a -> b) -> a -> b
$ \(DayUnit a ~> Unit
f Unit ~> b
g) -> a ~> Unit
f (a ~> Unit)
-> ((Ob a, Ob Unit) => Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b)
-> Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// Unit ~> b
g (Unit ~> b)
-> ((Ob Unit, Ob b) => Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b)
-> Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// ((UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA a))
-> Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b
forall {k} (p :: k) (q :: k) (a :: k) (b :: k).
(Ob p, Ob q) =>
((a ** p) ~> (q ** b)) -> Bipara a b p q
Bipara (((UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA a))
 -> Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b)
-> ((UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA a))
-> Bipara (UN 'BIPARA a) (UN 'BIPARA a) a b
forall a b. (a -> b) -> a -> b
$ let a :: Obj (UN 'BIPARA a)
a = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(UN BIPARA a) in
    (Unit ~> b
g (Unit ~> b)
-> Obj (UN 'BIPARA a)
-> (Unit ** UN 'BIPARA a) ~> (b ** UN 'BIPARA a)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj (UN 'BIPARA a)
a) ((Unit ** UN 'BIPARA a) ~> (b ** UN 'BIPARA a))
-> ((UN 'BIPARA a ** a) ~> (Unit ** UN 'BIPARA a))
-> (UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN 'BIPARA a) -> UN 'BIPARA a ~> (Unit ** UN 'BIPARA a)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv Obj (UN 'BIPARA a)
a (UN 'BIPARA a ~> (Unit ** UN 'BIPARA a))
-> ((UN 'BIPARA a ** a) ~> UN 'BIPARA a)
-> (UN 'BIPARA a ** a) ~> (Unit ** UN 'BIPARA a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN 'BIPARA a) -> (UN 'BIPARA a ** Unit) ~> UN 'BIPARA a
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor Obj (UN 'BIPARA a)
a ((UN 'BIPARA a ** Unit) ~> UN 'BIPARA a)
-> ((UN 'BIPARA a ** a) ~> (UN 'BIPARA a ** Unit))
-> (UN 'BIPARA a ** a) ~> UN 'BIPARA a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (UN 'BIPARA a)
a Obj (UN 'BIPARA a)
-> (a ~> Unit) -> (UN 'BIPARA a ** a) ~> (UN 'BIPARA a ** Unit)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` a ~> Unit
f)

  ecomp :: forall (exta :: ()) (a :: BIPARAK k exta) (extb :: ())
       (b :: BIPARAK k extb) (extc :: ()) (c :: BIPARAK k extc).
(EOb a, EOb b, EOb c) =>
O (a %~> b) (b %~> c) ~> (a %~> c)
ecomp = (Day
   (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
   (Bipara (UN 'BIPARA a) (UN 'BIPARA b))
 ~> Bipara (UN 'BIPARA a) (UN 'BIPARA c))
-> Mon2
     ('MK
        (Day
           (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
           (Bipara (UN 'BIPARA a) (UN 'BIPARA b))))
     ('MK (Bipara (UN 'BIPARA a) (UN 'BIPARA c)))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((Day
    (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
    (Bipara (UN 'BIPARA a) (UN 'BIPARA b))
  ~> Bipara (UN 'BIPARA a) (UN 'BIPARA c))
 -> Mon2
      ('MK
         (Day
            (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
            (Bipara (UN 'BIPARA a) (UN 'BIPARA b))))
      ('MK (Bipara (UN 'BIPARA a) (UN 'BIPARA c))))
-> (Day
      (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
      (Bipara (UN 'BIPARA a) (UN 'BIPARA b))
    ~> Bipara (UN 'BIPARA a) (UN 'BIPARA c))
-> Mon2
     ('MK
        (Day
           (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
           (Bipara (UN 'BIPARA a) (UN 'BIPARA b))))
     ('MK (Bipara (UN 'BIPARA a) (UN 'BIPARA c)))
forall a b. (a -> b) -> a -> b
$ (Day
   (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
   (Bipara (UN 'BIPARA a) (UN 'BIPARA b))
 :~> Bipara (UN 'BIPARA a) (UN 'BIPARA c))
-> Prof
     (Day
        (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
        (Bipara (UN 'BIPARA a) (UN 'BIPARA b)))
     (Bipara (UN 'BIPARA a) (UN 'BIPARA c))
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((Day
    (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
    (Bipara (UN 'BIPARA a) (UN 'BIPARA b))
  :~> Bipara (UN 'BIPARA a) (UN 'BIPARA c))
 -> Prof
      (Day
         (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
         (Bipara (UN 'BIPARA a) (UN 'BIPARA b)))
      (Bipara (UN 'BIPARA a) (UN 'BIPARA c)))
-> (Day
      (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
      (Bipara (UN 'BIPARA a) (UN 'BIPARA b))
    :~> Bipara (UN 'BIPARA a) (UN 'BIPARA c))
-> Prof
     (Day
        (Bipara (UN 'BIPARA b) (UN 'BIPARA c))
        (Bipara (UN 'BIPARA a) (UN 'BIPARA b)))
     (Bipara (UN 'BIPARA a) (UN 'BIPARA c))
forall a b. (a -> b) -> a -> b
$ \(Day a ~> (c ** e)
g (Bipara @c @d @bb @cc (UN 'BIPARA b ** c) ~> (d ** UN 'BIPARA c)
p) (Bipara @e @f @aa (UN 'BIPARA a ** e) ~> (f ** UN 'BIPARA b)
q) (d ** f) ~> b
h) -> a ~> (c ** e)
g (a ~> (c ** e))
-> ((Ob a, Ob (c ** e)) =>
    Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b)
-> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (d ** f) ~> b
h ((d ** f) ~> b)
-> ((Ob (d ** f), Ob b) =>
    Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b)
-> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// ((UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA c))
-> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b
forall {k} (p :: k) (q :: k) (a :: k) (b :: k).
(Ob p, Ob q) =>
((a ** p) ~> (q ** b)) -> Bipara a b p q
Bipara (((UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA c))
 -> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b)
-> ((UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA c))
-> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b
forall a b. (a -> b) -> a -> b
$
    let c :: Obj c
c = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c; d :: Obj d
d = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d; e :: Obj e
e = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @e; f :: Obj f
f = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; aa :: Obj (UN 'BIPARA a)
aa = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @aa; bb :: Obj (UN 'BIPARA b)
bb = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @bb; cc :: Obj (UN 'BIPARA c)
cc = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @cc
    in (((d ** f) ~> b
h ((d ** f) ~> b) -> ((f ** d) ~> (d ** f)) -> (f ** d) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj f -> Obj d -> (f ** d) ~> (d ** f)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' Obj f
f Obj d
d) ((f ** d) ~> b)
-> Obj (UN 'BIPARA c)
-> ((f ** d) ** UN 'BIPARA c) ~> (b ** UN 'BIPARA c)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj (UN 'BIPARA c)
cc) (((f ** d) ** UN 'BIPARA c) ~> (b ** UN 'BIPARA c))
-> ((UN 'BIPARA a ** a) ~> ((f ** d) ** UN 'BIPARA c))
-> (UN 'BIPARA a ** a) ~> (b ** UN 'BIPARA c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj f
-> Obj d
-> Obj (UN 'BIPARA c)
-> (f ** (d ** UN 'BIPARA c)) ~> ((f ** d) ** UN 'BIPARA c)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj f
f Obj d
d Obj (UN 'BIPARA c)
cc ((f ** (d ** UN 'BIPARA c)) ~> ((f ** d) ** UN 'BIPARA c))
-> ((UN 'BIPARA a ** a) ~> (f ** (d ** UN 'BIPARA c)))
-> (UN 'BIPARA a ** a) ~> ((f ** d) ** UN 'BIPARA c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj f
f Obj f
-> ((UN 'BIPARA b ** c) ~> (d ** UN 'BIPARA c))
-> (f ** (UN 'BIPARA b ** c)) ~> (f ** (d ** UN 'BIPARA c))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (UN 'BIPARA b ** c) ~> (d ** UN 'BIPARA c)
p) ((f ** (UN 'BIPARA b ** c)) ~> (f ** (d ** UN 'BIPARA c)))
-> ((UN 'BIPARA a ** a) ~> (f ** (UN 'BIPARA b ** c)))
-> (UN 'BIPARA a ** a) ~> (f ** (d ** UN 'BIPARA c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj f
-> Obj (UN 'BIPARA b)
-> Obj c
-> ((f ** UN 'BIPARA b) ** c) ~> (f ** (UN 'BIPARA b ** c))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj f
f Obj (UN 'BIPARA b)
bb Obj c
c (((f ** UN 'BIPARA b) ** c) ~> (f ** (UN 'BIPARA b ** c)))
-> ((UN 'BIPARA a ** a) ~> ((f ** UN 'BIPARA b) ** c))
-> (UN 'BIPARA a ** a) ~> (f ** (UN 'BIPARA b ** c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((UN 'BIPARA a ** e) ~> (f ** UN 'BIPARA b)
q ((UN 'BIPARA a ** e) ~> (f ** UN 'BIPARA b))
-> Obj c
-> ((UN 'BIPARA a ** e) ** c) ~> ((f ** UN 'BIPARA b) ** c)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj c
c) (((UN 'BIPARA a ** e) ** c) ~> ((f ** UN 'BIPARA b) ** c))
-> ((UN 'BIPARA a ** a) ~> ((UN 'BIPARA a ** e) ** c))
-> (UN 'BIPARA a ** a) ~> ((f ** UN 'BIPARA b) ** c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (UN 'BIPARA a)
-> Obj e
-> Obj c
-> (UN 'BIPARA a ** (e ** c)) ~> ((UN 'BIPARA a ** e) ** c)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj (UN 'BIPARA a)
aa Obj e
e Obj c
c ((UN 'BIPARA a ** (e ** c)) ~> ((UN 'BIPARA a ** e) ** c))
-> ((UN 'BIPARA a ** a) ~> (UN 'BIPARA a ** (e ** c)))
-> (UN 'BIPARA a ** a) ~> ((UN 'BIPARA a ** e) ** c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj (UN 'BIPARA a)
aa Obj (UN 'BIPARA a)
-> (a ~> (e ** c))
-> (UN 'BIPARA a ** a) ~> (UN 'BIPARA a ** (e ** c))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (Obj c -> Obj e -> (c ** e) ~> (e ** c)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' Obj c
c Obj e
e ((c ** e) ~> (e ** c)) -> (a ~> (c ** e)) -> a ~> (e ** c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (c ** e)
g))