module Proarrow.Category.Monoidal.Rev where

import Proarrow.Core (CAT, Profunctor(..), Promonad(..), CategoryOf(..), dimapDefault, UN, Is)
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal(..))

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

type Rev :: CAT k
data Rev a b where
  Rev :: a ~> b -> Rev (R a) (R b)

instance CategoryOf k => Profunctor (Rev :: CAT (REV k)) where
  dimap :: forall (c :: REV k) (a :: REV k) (b :: REV k) (d :: REV k).
(c ~> a) -> (b ~> d) -> Rev a b -> Rev c d
dimap = (c ~> a) -> (b ~> d) -> Rev a b -> Rev c d
Rev c a -> Rev b d -> Rev a b -> Rev c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: REV k) (b :: REV k) r.
((Ob a, Ob b) => r) -> Rev a b -> r
\\ Rev a ~> b
t = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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
\\ a ~> b
a ~> b
t

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

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

instance Monoidal k => Monoidal (REV k) where
  type Unit = R Unit
  type (R a) ** (R b) = R (b ** a)
  Rev a ~> b
f par :: forall (a :: REV k) (b :: REV k) (c :: REV k) (d :: REV k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Rev a ~> b
g = ((a ** a) ~> (b ** b)) -> Rev (R (a ** a)) (R (b ** b))
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (a ~> b
a ~> b
g (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` a ~> b
a ~> b
f)
  leftUnitor :: forall (a :: REV k). Obj a -> (Unit ** a) ~> a
leftUnitor (Rev a ~> b
a) = ((a ** Unit) ~> a) -> Rev (R (a ** Unit)) (R a)
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (Obj a -> (a ** Unit) ~> a
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor Obj a
a ~> b
a)
  leftUnitorInv :: forall (a :: REV k). Obj a -> a ~> (Unit ** a)
leftUnitorInv (Rev a ~> b
a) = (a ~> (a ** Unit)) -> Rev (R a) (R (a ** Unit))
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (Obj a -> a ~> (a ** Unit)
forall (a :: k). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
rightUnitorInv Obj a
a ~> b
a)
  rightUnitor :: forall (a :: REV k). Obj a -> (a ** Unit) ~> a
rightUnitor (Rev a ~> b
a) = ((Unit ** a) ~> a) -> Rev (R (Unit ** a)) (R a)
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (Obj a -> (Unit ** a) ~> a
forall (a :: k). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor Obj a
a ~> b
a)
  rightUnitorInv :: forall (a :: REV k). Obj a -> a ~> (a ** Unit)
rightUnitorInv (Rev a ~> b
a) = (a ~> (Unit ** a)) -> Rev (R a) (R (Unit ** a))
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (Obj a -> a ~> (Unit ** a)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv Obj a
a ~> b
a)
  associator :: forall (a :: REV k) (b :: REV k) (c :: REV k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator (Rev a ~> b
a) (Rev a ~> b
b) (Rev a ~> b
c) = ((a ** (a ** a)) ~> ((a ** a) ** a))
-> Rev (R (a ** (a ** a))) (R ((a ** a) ** a))
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (Obj a -> Obj a -> Obj a -> (a ** (a ** a)) ~> ((a ** a) ** a)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj a
a ~> b
c Obj a
a ~> b
b Obj a
a ~> b
a)
  associatorInv :: forall (a :: REV k) (b :: REV k) (c :: REV k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv (Rev a ~> b
a) (Rev a ~> b
b) (Rev a ~> b
c) = (((a ** a) ** a) ~> (a ** (a ** a)))
-> Rev (R ((a ** a) ** a)) (R (a ** (a ** a)))
forall {k} (a :: k) (b :: k). (a ~> b) -> Rev (R a) (R b)
Rev (Obj a -> Obj a -> Obj a -> ((a ** a) ** a) ~> (a ** (a ** a))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj a
a ~> b
c Obj a
a ~> b
b Obj a
a ~> b
a)

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