module Proarrow.Profunctor.Product where

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

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

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
  lift0 :: (:*:) p q Unit Unit
lift0 = p Unit Unit
forall j k (p :: PRO j k). MonoidalProfunctor p => p Unit Unit
lift0 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 :: PRO j k). MonoidalProfunctor p => p Unit Unit
lift0
  lift2 :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
(:*:) p q x1 x2
-> (:*:) p q y1 y2 -> (:*:) p q (x1 ** y1) (x2 ** y2)
lift2 (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 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall j k (p :: PRO j k) (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
lift2 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 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
q x1 x2 -> q y1 y2 -> q (x1 ** y1) (x2 ** y2)
forall j k (p :: PRO j k) (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
lift2 q x1 x2
p2 q y1 y2
q2

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