module Proarrow.Category.Enriched.Bipara where

import Data.Kind (Type)
import Prelude (($), type (~))

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

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) => b ** p ~> q ** a -> 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 (b ** a) ~> (b ** a)
h) = ((b ** c) ~> (d ** a)) -> Bipara a b c d
forall {k} (p :: k) (q :: k) (b :: k) (a :: k).
(Ob p, Ob q) =>
((b ** p) ~> (q ** a)) -> 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 @a b ~> d
g ((b ** a) ~> (d ** a))
-> ((b ** c) ~> (b ** a)) -> (b ** c) ~> (d ** 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
. (b ** a) ~> (b ** a)
h ((b ** a) ~> (b ** a))
-> ((b ** c) ~> (b ** a)) -> (b ** c) ~> (b ** 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
. 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 @b 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 (Monoidal k) => ECategory (BIPARAK k) where
  type EOb a = (Is BIPARA a, Ob (UN BIPARA a))

  eid :: forall {exta} (a :: k) (a' :: BIPARAK k exta). (a' ~ BIPARA a, EOb a') => I ~> (a' %~> a')
  eid :: forall {exta :: ()} (a :: k) (a' :: BIPARAK k exta).
(a' ~ 'BIPARA a, EOb a') =>
I ~> (a' %~> a')
eid = (DayUnit ~> Bipara a a) -> Mon2 ('MK DayUnit) ('MK (Bipara a a))
forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k).
(a1 ~> b1) -> Mon2 ('MK a1) ('MK b1)
Mon2 ((DayUnit ~> Bipara a a) -> Mon2 ('MK DayUnit) ('MK (Bipara a a)))
-> (DayUnit ~> Bipara a a) -> Mon2 ('MK DayUnit) ('MK (Bipara a a))
forall a b. (a -> b) -> a -> b
$ (DayUnit :~> Bipara a a) -> Prof DayUnit (Bipara a a)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((DayUnit :~> Bipara a a) -> Prof DayUnit (Bipara a a))
-> (DayUnit :~> Bipara a a) -> Prof DayUnit (Bipara a 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 a a a b) -> Bipara a 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 a a a b) -> Bipara a 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
// ((a ** a) ~> (b ** a)) -> Bipara a a a b
forall {k} (p :: k) (q :: k) (b :: k) (a :: k).
(Ob p, Ob q) =>
((b ** p) ~> (q ** a)) -> Bipara a b p q
Bipara (((a ** a) ~> (b ** a)) -> Bipara a a a b)
-> ((a ** a) ~> (b ** a)) -> Bipara a a a b
forall a b. (a -> b) -> a -> b
$
      let a :: Obj a
a = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a
      in (Unit ~> b
g (Unit ~> b) -> Obj a -> (Unit ** a) ~> (b ** 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)
`par` Obj a
a) ((Unit ** a) ~> (b ** a))
-> ((a ** a) ~> (Unit ** a)) -> (a ** a) ~> (b ** 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 a -> a ~> (Unit ** a)
forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> a ~> (Unit ** b)
leftUnitorInv' Obj a
a (a ~> (Unit ** a)) -> ((a ** a) ~> a) -> (a ** a) ~> (Unit ** 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 a -> (a ** Unit) ~> a
forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> (a ** Unit) ~> b
rightUnitor' Obj a
a ((a ** Unit) ~> a) -> ((a ** a) ~> (a ** Unit)) -> (a ** a) ~> 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 a
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)
`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 (b %~> c) (a %~> b) ~> (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 {k} {j} (p :: j +-> k) (q :: 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 @aa (UN 'BIPARA c ** c) ~> (d ** UN 'BIPARA b)
p) (Bipara @e @f @bb @cc (UN 'BIPARA b ** e) ~> (f ** UN 'BIPARA a)
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 c ** a) ~> (b ** UN 'BIPARA a))
-> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b
forall {k} (p :: k) (q :: k) (b :: k) (a :: k).
(Ob p, Ob q) =>
((b ** p) ~> (q ** a)) -> Bipara a b p q
Bipara (((UN 'BIPARA c ** a) ~> (b ** UN 'BIPARA a))
 -> Bipara (UN 'BIPARA a) (UN 'BIPARA c) a b)
-> ((UN 'BIPARA c ** a) ~> (b ** UN 'BIPARA a))
-> 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 c)
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 a)
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)
-> Obj (UN 'BIPARA a)
-> ((d ** f) ** UN 'BIPARA a) ~> (b ** UN 'BIPARA 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)
`par` Obj (UN 'BIPARA a)
cc)
          (((d ** f) ** UN 'BIPARA a) ~> (b ** UN 'BIPARA a))
-> ((UN 'BIPARA c ** a) ~> ((d ** f) ** UN 'BIPARA a))
-> (UN 'BIPARA c ** 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 d
-> Obj f
-> Obj (UN 'BIPARA a)
-> (d ** (f ** UN 'BIPARA a)) ~> ((d ** f) ** UN 'BIPARA a)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' Obj d
d Obj f
f Obj (UN 'BIPARA a)
cc
          ((d ** (f ** UN 'BIPARA a)) ~> ((d ** f) ** UN 'BIPARA a))
-> ((UN 'BIPARA c ** a) ~> (d ** (f ** UN 'BIPARA a)))
-> (UN 'BIPARA c ** a) ~> ((d ** f) ** 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 d
d Obj d
-> ((UN 'BIPARA b ** e) ~> (f ** UN 'BIPARA a))
-> (d ** (UN 'BIPARA b ** e)) ~> (d ** (f ** UN 'BIPARA 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)
`par` (UN 'BIPARA b ** e) ~> (f ** UN 'BIPARA a)
q)
          ((d ** (UN 'BIPARA b ** e)) ~> (d ** (f ** UN 'BIPARA a)))
-> ((UN 'BIPARA c ** a) ~> (d ** (UN 'BIPARA b ** e)))
-> (UN 'BIPARA c ** a) ~> (d ** (f ** 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 d
-> Obj (UN 'BIPARA b)
-> Obj e
-> ((d ** UN 'BIPARA b) ** e) ~> (d ** (UN 'BIPARA b ** e))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' Obj d
d Obj (UN 'BIPARA b)
bb Obj e
e
          (((d ** UN 'BIPARA b) ** e) ~> (d ** (UN 'BIPARA b ** e)))
-> ((UN 'BIPARA c ** a) ~> ((d ** UN 'BIPARA b) ** e))
-> (UN 'BIPARA c ** a) ~> (d ** (UN 'BIPARA b ** e))
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 c ** c) ~> (d ** UN 'BIPARA b)
p ((UN 'BIPARA c ** c) ~> (d ** UN 'BIPARA b))
-> Obj e
-> ((UN 'BIPARA c ** c) ** e) ~> ((d ** UN 'BIPARA b) ** e)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` Obj e
e)
          (((UN 'BIPARA c ** c) ** e) ~> ((d ** UN 'BIPARA b) ** e))
-> ((UN 'BIPARA c ** a) ~> ((UN 'BIPARA c ** c) ** e))
-> (UN 'BIPARA c ** a) ~> ((d ** UN 'BIPARA b) ** e)
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 c)
-> Obj c
-> Obj e
-> (UN 'BIPARA c ** (c ** e)) ~> ((UN 'BIPARA c ** c) ** e)
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 c)
aa Obj c
c Obj e
e
          ((UN 'BIPARA c ** (c ** e)) ~> ((UN 'BIPARA c ** c) ** e))
-> ((UN 'BIPARA c ** a) ~> (UN 'BIPARA c ** (c ** e)))
-> (UN 'BIPARA c ** a) ~> ((UN 'BIPARA c ** c) ** e)
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 c)
aa Obj (UN 'BIPARA c)
-> (a ~> (c ** e))
-> (UN 'BIPARA c ** a) ~> (UN 'BIPARA c ** (c ** e))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` a ~> (c ** e)
g)