module Proarrow.Category.Opposite where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, lmap, type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))

newtype OPPOSITE k = OP k
type instance UN OP (OP k) = k

type Op :: j +-> k -> OPPOSITE k +-> OPPOSITE j
data Op p a b where
  Op :: {forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp :: p b a} -> Op p (OP a) (OP b)

instance (Profunctor p) => Functor (Op p a) where
  map :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(a ~> b) -> Op p a a ~> Op p a b
map (Op b ~> a
f) (Op p b a
p) = p b a -> Op p ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op ((b ~> b) -> p b a -> p b a
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap b ~> a
b ~> b
f p b a
p)

instance (Profunctor p) => Profunctor (Op p) where
  dimap :: forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k)
       (d :: OPPOSITE k).
(c ~> a) -> (b ~> d) -> Op p a b -> Op p c d
dimap (Op b ~> a
l) (Op b ~> a
r) = p b a -> Op p ('OP a) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (p b a -> Op p ('OP a) ('OP b))
-> (Op p ('OP b) ('OP a) -> p b a)
-> Op p ('OP b) ('OP a)
-> Op p ('OP a) ('OP b)
forall b c a. (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
. (b ~> a) -> (b ~> a) -> p a b -> p b a
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 b ~> a
r b ~> a
l (p a b -> p b a)
-> (Op p ('OP b) ('OP a) -> p a b) -> Op p ('OP b) ('OP a) -> p b a
forall b c a. (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
. Op p ('OP b) ('OP a) -> p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
((Ob a, Ob b) => r) -> Op p a b -> r
\\ Op p b a
f = r
(Ob b, Ob a) => r
(Ob a, Ob b) => r
r ((Ob b, Ob a) => r) -> p b a -> 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 b a
f

-- | The opposite category of the category of `k`.
instance (CategoryOf k) => CategoryOf (OPPOSITE k) where
  type (~>) = Op (~>)
  type Ob a = (Is OP a, Ob (UN OP a))

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

instance (HasInitialObject k) => HasTerminalObject (OPPOSITE k) where
  type TerminalObject = OP InitialObject
  terminate :: forall (a :: OPPOSITE k). Ob a => a ~> TerminalObject
terminate = (InitialObject ~> UN 'OP a)
-> Op (~>) ('OP (UN 'OP a)) ('OP InitialObject)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op InitialObject ~> UN 'OP a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (HasTerminalObject k) => HasInitialObject (OPPOSITE k) where
  type InitialObject = OP TerminalObject
  initiate :: forall (a :: OPPOSITE k). Ob a => InitialObject ~> a
initiate = (UN 'OP a ~> TerminalObject)
-> Op (~>) ('OP TerminalObject) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op UN 'OP a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

instance (HasBinaryCoproducts k) => HasBinaryProducts (OPPOSITE k) where
  type a && b = OP (UN OP a || UN OP b)
  fst :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(OP a) @(OP b) = (UN 'OP a ~> (UN 'OP a || UN 'OP b))
-> Op (~>) ('OP (UN 'OP a || UN 'OP b)) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  snd :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(OP a) @(OP b) = (UN 'OP b ~> (UN 'OP a || UN 'OP b))
-> Op (~>) ('OP (UN 'OP a || UN 'OP b)) ('OP (UN 'OP b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Op b ~> a
a &&& :: forall (a :: OPPOSITE k) (x :: OPPOSITE k) (y :: OPPOSITE k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Op b ~> a
b = ((b || b) ~> a) -> Op (~>) ('OP a) ('OP (b || b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (b ~> a
a (b ~> a) -> (b ~> a) -> (b || b) ~> a
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> a
b ~> a
b)

instance (HasBinaryProducts k) => HasBinaryCoproducts (OPPOSITE k) where
  type a || b = OP (UN OP a && UN OP b)
  lft :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(OP a) @(OP b) = ((UN 'OP a && UN 'OP b) ~> UN 'OP a)
-> Op (~>) ('OP (UN 'OP a)) ('OP (UN 'OP a && UN 'OP b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b)
  rgt :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(OP a) @(OP b) = ((UN 'OP a && UN 'OP b) ~> UN 'OP b)
-> Op (~>) ('OP (UN 'OP b)) ('OP (UN 'OP a && UN 'OP b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b)
  Op b ~> a
a ||| :: forall (x :: OPPOSITE k) (a :: OPPOSITE k) (y :: OPPOSITE k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Op b ~> a
b = (b ~> (a && a)) -> Op (~>) ('OP (a && a)) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (b ~> a
a (b ~> a) -> (b ~> a) -> b ~> (a && a)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& b ~> a
b ~> a
b)

instance (MonoidalProfunctor p) => MonoidalProfunctor (Op p) where
  par0 :: Op p Unit Unit
par0 = p Unit Unit -> Op p ('OP Unit) ('OP Unit)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Op p b a
l par :: forall (x1 :: OPPOSITE j) (x2 :: OPPOSITE k) (y1 :: OPPOSITE j)
       (y2 :: OPPOSITE k).
Op p x1 x2 -> Op p y1 y2 -> Op p (x1 ** y1) (x2 ** y2)
`par` Op p b a
r = p (b ** b) (a ** a) -> Op p ('OP (a ** a)) ('OP (b ** b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (p b a
l p b a -> p b a -> p (b ** b) (a ** a)
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 b a
r)

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

instance (SymMonoidal k) => SymMonoidal (OPPOSITE k) where
  swap' :: forall (a :: OPPOSITE k) (a' :: OPPOSITE k) (b :: OPPOSITE k)
       (b' :: OPPOSITE k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Op b ~> a
a) (Op b ~> a
b) = ((b ** b) ~> (a ** a)) -> Op (~>) ('OP (a ** a)) ('OP (b ** b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op ((b ~> a) -> (b ~> a) -> (b ** b) ~> (a ** a)
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' b ~> a
b b ~> a
a)

instance (Comonoid c) => Monoid (OP c) where
  mempty :: Unit ~> 'OP c
mempty = (c ~> Unit) -> Op (~>) ('OP Unit) ('OP c)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  mappend :: ('OP c ** 'OP c) ~> 'OP c
mappend = (c ~> (c ** c)) -> Op (~>) ('OP (c ** c)) ('OP c)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

instance (Monoid c) => Comonoid (OP c) where
  counit :: 'OP c ~> Unit
counit = (Unit ~> c) -> Op (~>) ('OP c) ('OP Unit)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op Unit ~> c
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  comult :: 'OP c ~> ('OP c ** 'OP c)
comult = ((c ** c) ~> c) -> Op (~>) ('OP c) ('OP (c ** c))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (c ** c) ~> c
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend

instance (Representable p) => Corepresentable (Op p) where
  type Op p %% OP a = OP (p % a)
  coindex :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
Op p a b -> (Op p %% a) ~> b
coindex (Op p b a
f) = (b ~> (p % a)) -> Op (~>) ('OP (p % a)) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (p b a -> b ~> (p % a)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p b a
f)
  cotabulate :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
Ob a =>
((Op p %% a) ~> b) -> Op p a b
cotabulate (Op b ~> a
f) = p b (UN 'OP a) -> Op p ('OP (UN 'OP a)) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op ((b ~> (p % UN 'OP a)) -> p b (UN 'OP a)
forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate b ~> a
b ~> (p % UN 'OP a)
f)
  corepMap :: forall (a :: OPPOSITE j) (b :: OPPOSITE j).
(a ~> b) -> (Op p %% a) ~> (Op p %% b)
corepMap (Op b ~> a
f) = ((p % b) ~> (p % a)) -> Op (~>) ('OP (p % a)) ('OP (p % b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p b ~> a
f)

instance (Corepresentable p) => Representable (Op p) where
  type Op p % OP a = OP (p %% a)
  index :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
Op p a b -> a ~> (Op p % b)
index (Op p b a
f) = ((p %% b) ~> a) -> Op (~>) ('OP a) ('OP (p %% b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (p b a -> (p %% b) ~> a
forall (a :: k) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p b a
f)
  tabulate :: forall (b :: OPPOSITE k) (a :: OPPOSITE j).
Ob b =>
(a ~> (Op p % b)) -> Op p a b
tabulate (Op b ~> a
f) = p (UN 'OP b) a -> Op p ('OP a) ('OP (UN 'OP b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (((p %% UN 'OP b) ~> a) -> p (UN 'OP b) a
forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate b ~> a
(p %% UN 'OP b) ~> a
f)
  repMap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(a ~> b) -> (Op p % a) ~> (Op p % b)
repMap (Op b ~> a
f) = ((p %% b) ~> (p %% a)) -> Op (~>) ('OP (p %% a)) ('OP (p %% b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p b ~> a
f)

type UnOp :: OPPOSITE k +-> OPPOSITE j -> j +-> k
data UnOp p a b where
  UnOp :: {forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
UnOp p a b -> p ('OP b) ('OP a)
unUnOp :: p (OP b) (OP a)} -> UnOp p a b
instance (CategoryOf j, CategoryOf k, Profunctor p) => Profunctor (UnOp p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> UnOp p a b -> UnOp p c d
dimap c ~> a
l b ~> d
r = p ('OP d) ('OP c) -> UnOp p c d
forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
p ('OP b) ('OP a) -> UnOp p a b
UnOp (p ('OP d) ('OP c) -> UnOp p c d)
-> (UnOp p a b -> p ('OP d) ('OP c)) -> UnOp p a b -> UnOp p c d
forall b c a. (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
. ('OP d ~> 'OP b)
-> ('OP a ~> 'OP c) -> p ('OP b) ('OP a) -> p ('OP d) ('OP c)
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
forall (c :: OPPOSITE j) (a :: OPPOSITE j) (b :: OPPOSITE k)
       (d :: OPPOSITE k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap ((b ~> d) -> Op (~>) ('OP d) ('OP b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op b ~> d
r) ((c ~> a) -> Op (~>) ('OP a) ('OP c)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op c ~> a
l) (p ('OP b) ('OP a) -> p ('OP d) ('OP c))
-> (UnOp p a b -> p ('OP b) ('OP a))
-> UnOp p a b
-> p ('OP d) ('OP c)
forall b c a. (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
. UnOp p a b -> p ('OP b) ('OP a)
forall {k} {k} (p :: OPPOSITE k +-> OPPOSITE k) (b :: k) (a :: k).
UnOp p a b -> p ('OP b) ('OP a)
unUnOp
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> UnOp p a b -> r
\\ UnOp p ('OP b) ('OP a)
f = r
(Ob a, Ob b) => r
(Ob ('OP b), Ob ('OP a)) => r
r ((Ob ('OP b), Ob ('OP a)) => r) -> p ('OP b) ('OP a) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
((Ob a, Ob b) => r) -> p a b -> r
\\ p ('OP b) ('OP a)
f

instance Strong k p => Strong (OPPOSITE k) (Op p) where
  act :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (x :: OPPOSITE j)
       (y :: OPPOSITE k).
(a ~> b) -> Op p x y -> Op p (Act a x) (Act b y)
act (Op b ~> a
w) (Op p b a
p) = p (Act b b) (Act a a) -> Op p ('OP (Act a a)) ('OP (Act b b))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op ((b ~> a) -> p b a -> p (Act b b) (Act a a)
forall (a :: k) (b :: k) (x :: k) (y :: j).
(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 b ~> a
w p b a
p)
instance MonoidalAction m k => MonoidalAction (OPPOSITE m) (OPPOSITE k) where
  type Act (OP a) (OP b) = OP (Act a b)
  unitor :: forall (x :: OPPOSITE k). Ob x => Act Unit x ~> x
unitor = (UN 'OP x ~> Act Unit (UN 'OP x))
-> Op (~>) ('OP (Act Unit (UN 'OP x))) ('OP (UN 'OP x))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m)
  unitorInv :: forall (x :: OPPOSITE k). Ob x => x ~> Act Unit x
unitorInv = (Act Unit (UN 'OP x) ~> UN 'OP x)
-> Op (~>) ('OP (UN 'OP x)) ('OP (Act Unit (UN 'OP x)))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m)
  multiplicator :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @(OP a) @(OP b) @(OP x) = (Act (UN 'OP a ** UN 'OP b) (UN 'OP x)
 ~> Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x)))
-> Op
     (~>)
     ('OP (Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x))))
     ('OP (Act (UN 'OP a ** UN 'OP b) (UN 'OP x)))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @a @b @x)
  multiplicatorInv :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @(OP a) @(OP b) @(OP x) = (Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x))
 ~> Act (UN 'OP a ** UN 'OP b) (UN 'OP x))
-> Op
     (~>)
     ('OP (Act (UN 'OP a ** UN 'OP b) (UN 'OP x)))
     ('OP (Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x))))
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @a @b @x)