module Proarrow.Category.Monoidal.Rev where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, type (+->))

type data REV k = R k
type instance UN R (R a) = a

type Rev :: j +-> k -> REV j +-> REV k
data Rev p a b where
  Rev :: p a b -> Rev p (R a) (R b)

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

instance (Promonad p) => Promonad (Rev p) where
  id :: forall (a :: REV j). Ob a => Rev p a a
id = p (UN R a) (UN R a) -> Rev p (R (UN R a)) (R (UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev p (UN R a) (UN R a)
forall (a :: j). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Rev p a b
f . :: forall (b :: REV j) (c :: REV j) (a :: REV j).
Rev p b c -> Rev p a b -> Rev p a c
. Rev p a b
g = p a b -> Rev p (R a) (R b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (p a b
f p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p 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
. p a a
p a b
g)

instance (CategoryOf k) => CategoryOf (REV k) where
  type (~>) = Rev (~>)
  type Ob a = (Is R a, Ob (UN R a))

instance (MonoidalProfunctor p) => MonoidalProfunctor (Rev p) where
  par0 :: Rev p Unit Unit
par0 = p Unit Unit -> Rev p (R Unit) (R Unit)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Rev p a b
f par :: forall (x1 :: REV k) (x2 :: REV j) (y1 :: REV k) (y2 :: REV j).
Rev p x1 x2 -> Rev p y1 y2 -> Rev p (x1 ** y1) (x2 ** y2)
`par` Rev p a b
g = p (a ** a) (b ** b) -> Rev p (R (a ** a)) (R (b ** b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (p a b
g p a b -> p a b -> p (a ** a) (b ** b)
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 a b
f)

instance (Monoidal k) => Monoidal (REV k) where
  type Unit = R Unit
  type (R a) ** (R b) = R (b ** a)
  leftUnitor :: forall (a :: REV k). Ob a => (Unit ** a) ~> a
leftUnitor = ((UN R a ** Unit) ~> UN R a)
-> Rev (~>) (R (UN R a ** Unit)) (R (UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (UN R a ** Unit) ~> UN R a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  leftUnitorInv :: forall (a :: REV k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN R a ~> (UN R a ** Unit))
-> Rev (~>) (R (UN R a)) (R (UN R a ** Unit))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev UN R a ~> (UN R a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  rightUnitor :: forall (a :: REV k). Ob a => (a ** Unit) ~> a
rightUnitor = ((Unit ** UN R a) ~> UN R a)
-> Rev (~>) (R (Unit ** UN R a)) (R (UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (Unit ** UN R a) ~> UN R a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  rightUnitorInv :: forall (a :: REV k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN R a ~> (Unit ** UN R a))
-> Rev (~>) (R (UN R a)) (R (Unit ** UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev UN R a ~> (Unit ** UN R a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  associator :: forall (a :: REV k) (b :: REV k) (c :: REV k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(R a) @(R b) @(R c) = ((UN R c ** (UN R b ** UN R a)) ~> ((UN R c ** UN R b) ** UN R a))
-> Rev
     (~>)
     (R (UN R c ** (UN R b ** UN R a)))
     (R ((UN R c ** UN R b) ** UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @c @b @a)
  associatorInv :: forall (a :: REV k) (b :: REV k) (c :: REV k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(R a) @(R b) @(R c) = (((UN R c ** UN R b) ** UN R a) ~> (UN R c ** (UN R b ** UN R a)))
-> Rev
     (~>)
     (R ((UN R c ** UN R b) ** UN R a))
     (R (UN R c ** (UN R b ** UN R a)))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @c @b @a)

instance (SymMonoidal k) => SymMonoidal (REV k) where
  swap' :: forall (a :: REV k) (a' :: REV k) (b :: REV k) (b' :: REV k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Rev a ~> b
a) (Rev a ~> b
b) = ((a ** a) ~> (b ** b)) -> Rev (~>) (R (a ** a)) (R (b ** b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev ((a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' a ~> b
b a ~> b
a)