module Proarrow.Profunctor.Product where

import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core (PRO, Profunctor (..), (:~>))
import Proarrow.Category.Dagger (DaggerProfunctor (..))

type (:*:) :: PRO j k -> PRO j k -> PRO j k
data (p :*: q) a b where
  (:*:) :: {forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
(:*:) p q a b -> p a b
fstP :: p a b, forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
(:*:) p q a b -> q a b
sndP :: q a b} -> (p :*: q) a b

prod :: (r :~> p) -> (r :~> q) -> r :~> p :*: q
prod :: forall {j} {k} (r :: j -> k -> Type) (p :: j -> k -> Type)
       (q :: j -> k -> Type).
(r :~> p) -> (r :~> q) -> r :~> (p :*: q)
prod r :~> p
l r :~> q
r r a b
p = r a b -> p a b
r :~> p
l r a b
p p a b -> q a b -> (:*:) p q a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: r a b -> q a b
r :~> q
r r a b
p

instance (Profunctor p, Profunctor q) => Profunctor (p :*: q) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (:*:) p q a b -> (:*:) p q c d
dimap c ~> a
l b ~> d
r (p a b
p :*: q a b
q) = (c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> d
r p a b
p p c d -> q c d -> (:*:) p q c d
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: (c ~> a) -> (b ~> d) -> q a b -> q c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> q a b -> q c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> d
r q a b
q
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> (:*:) p q a b -> r
\\ (p a b
p :*: q a b
_) = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

instance (MonoidalProfunctor p, MonoidalProfunctor q) => MonoidalProfunctor (p :*: q) where
  par0 :: (:*:) p q Unit Unit
par0 = p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 p Unit Unit -> q Unit Unit -> (:*:) p q Unit Unit
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: q Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  par :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
(:*:) p q x1 x2
-> (:*:) p q y1 y2 -> (:*:) p q (x1 ** y1) (x2 ** y2)
par (p x1 x2
p1 :*: q x1 x2
p2) (p y1 y2
q1 :*: q y1 y2
q2) = p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (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 p x1 x2
p1 p y1 y2
q1 p (x1 ** y1) (x2 ** y2)
-> q (x1 ** y1) (x2 ** y2) -> (:*:) p q (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: q x1 x2 -> q y1 y2 -> q (x1 ** y1) (x2 ** y2)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
q x1 x2 -> q y1 y2 -> q (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 q x1 x2
p2 q y1 y2
q2

instance (DaggerProfunctor p, DaggerProfunctor q) => DaggerProfunctor (p :*: q) where
  dagger :: forall (a :: j) (b :: j). (:*:) p q a b -> (:*:) p q b a
dagger (p a b
p :*: q a b
q) = p a b -> p b a
forall (a :: j) (b :: j). p a b -> p b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
p p b a -> q b a -> (:*:) p q b a
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: q a b -> q b a
forall (a :: j) (b :: j). q a b -> q b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger q a b
q