module Proarrow.Profunctor.Product where

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core (Profunctor (..), (:~>), type (+->))
import Proarrow.Category.Monoidal.Action (Strong (..))
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..))

type (:*:) :: (j +-> k) -> (j +-> k) -> (j +-> k)
data (p :*: q) a b where
  (:*:) :: {forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
(:*:) p q a b -> p a b
fstP :: p a b, forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: 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 {k} {j} (r :: k -> j -> Type) (p :: k -> j -> Type)
       (q :: k -> j -> 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 :: j +-> k) (a :: k) (b :: j) (q :: 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 :: k) (a :: k) (b :: j) (d :: j).
(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 :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: (c ~> a) -> (b ~> d) -> q a b -> q c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> q a b -> q c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: k) (b :: j) 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 :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) (q :: 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 :: j +-> k) (a :: k) (b :: j) (q :: 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 :: k) (b :: k). (:*:) 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 :: k) (b :: k). p a b -> p b a
forall k (p :: k +-> k) (a :: k) (b :: k).
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 :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: q a b -> q b a
forall (a :: k) (b :: k). q a b -> q b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger q a b
q

instance (ThinProfunctor p, ThinProfunctor q) => ThinProfunctor (p :*: q) where
  type HasArrow (p :*: q) a b = (HasArrow p a b, HasArrow q a b)
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (p :*: q) a b) =>
(:*:) p q a b
arr = p a b
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr p a b -> q a b -> (:*:) p q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: q a b
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow q a b) => q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
  withArr :: forall (a :: k) (b :: j) r.
(:*:) p q a b -> (HasArrow (p :*: q) a b => r) -> r
withArr (p a b
p :*: q a b
q) HasArrow (p :*: q) a b => r
r = p a b -> (HasArrow p a b => r) -> r
forall (a :: k) (b :: j) r. p a b -> (HasArrow p a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr p a b
p (q a b -> (HasArrow q a b => r) -> r
forall (a :: k) (b :: j) r. q a b -> (HasArrow q a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr q a b
q r
HasArrow q a b => r
HasArrow (p :*: q) a b => r
r)

instance (Strong m p, Strong m q) => Strong m (p :*: q) where
  act :: forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> (:*:) p q x y -> (:*:) p q (Act a x) (Act b y)
act a ~> b
f (p x y
p :*: q x y
q) = (a ~> b) -> p x y -> p (Act a x) (Act b y)
forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f p x y
p p (Act a x) (Act b y)
-> q (Act a x) (Act b y) -> (:*:) p q (Act a x) (Act b y)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: (a ~> b) -> q x y -> q (Act a x) (Act b y)
forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> q x y -> q (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
f q x y
q