module Proarrow.Category.Opposite where

import Proarrow.Core (PRO, UN, Is, CategoryOf(..), Profunctor(..), Promonad(..), lmap)
import Proarrow.Functor (Functor(..))
import Proarrow.Object.Initial (HasInitialObject(..))
import Proarrow.Object.Terminal (HasTerminalObject(..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..))
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal(..))


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

type Op :: PRO j k -> PRO (OPPOSITE k) (OPPOSITE j)
data Op c a b where
  Op :: { forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
Op c ('OP a) ('OP b) -> c b a
getOp :: c b a } -> Op c (OP a) (OP b)

instance Profunctor p => Functor (Op p a) where
  map :: forall (a :: OPPOSITE j) (b :: OPPOSITE j).
(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} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('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 k) (a :: OPPOSITE k) (b :: OPPOSITE j)
       (d :: OPPOSITE j).
(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} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('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 :: 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 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} (c :: PRO j k) (b :: j) (a :: k).
Op c ('OP a) ('OP b) -> c b a
getOp
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPPOSITE k) (b :: OPPOSITE j) 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 :: 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 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 k). 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} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op c (UN 'OP a) (UN 'OP a)
forall (a :: k). 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 k) (c :: OPPOSITE k) (a :: OPPOSITE k).
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} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (c b a
g c b a -> c b b -> c b a
forall (b :: k) (c :: k) (a :: k). 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). Obj a -> a ~> TerminalObject
terminate' (Op b ~> a
a) = (InitialObject ~> b) -> Op (~>) ('OP b) ('OP InitialObject)
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> InitialObject ~> b
forall (a :: k). Obj a -> InitialObject ~> a
forall k (a :: k).
HasInitialObject k =>
Obj a -> InitialObject ~> a
initiate' Obj b
b ~> a
a)

instance HasTerminalObject k => HasInitialObject (OPPOSITE k) where
  type InitialObject = OP TerminalObject
  initiate' :: forall (a :: OPPOSITE k). Obj a -> InitialObject ~> a
initiate' (Op b ~> a
a) = (b ~> TerminalObject) -> Op (~>) ('OP TerminalObject) ('OP b)
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> b ~> TerminalObject
forall (a :: k). Obj a -> a ~> TerminalObject
forall k (a :: k).
HasTerminalObject k =>
Obj a -> a ~> TerminalObject
terminate' Obj b
b ~> a
a)

instance HasBinaryCoproducts k => HasBinaryProducts (OPPOSITE k) where
  type OP a && OP b = OP (a || b)
  fst' :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
Obj a -> Obj b -> (a && b) ~> a
fst' (Op b ~> a
a) (Op b ~> a
b) = (b ~> (b || b)) -> Op (~>) ('OP (b || b)) ('OP b)
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> Obj b -> b ~> (b || b)
forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b)
forall k (a :: k) (b :: k).
HasBinaryCoproducts k =>
Obj a -> Obj b -> a ~> (a || b)
lft' Obj b
b ~> a
a Obj b
b ~> a
b)
  snd' :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
Obj a -> Obj b -> (a && b) ~> b
snd' (Op b ~> a
a) (Op b ~> a
b) = (b ~> (b || b)) -> Op (~>) ('OP (b || b)) ('OP b)
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> Obj b -> b ~> (b || b)
forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b)
forall k (a :: k) (b :: k).
HasBinaryCoproducts k =>
Obj a -> Obj b -> b ~> (a || b)
rgt' Obj b
b ~> a
a Obj b
b ~> 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} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('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 OP a || OP b = OP (a && b)
  lft' :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
Obj a -> Obj b -> a ~> (a || b)
lft' (Op b ~> a
a) (Op b ~> a
b) = ((b && b) ~> b) -> Op (~>) ('OP b) ('OP (b && b))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> Obj b -> (b && b) ~> b
forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> a
forall k (a :: k) (b :: k).
HasBinaryProducts k =>
Obj a -> Obj b -> (a && b) ~> a
fst' Obj b
b ~> a
a Obj b
b ~> a
b)
  rgt' :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
Obj a -> Obj b -> b ~> (a || b)
rgt' (Op b ~> a
a) (Op b ~> a
b) = ((b && b) ~> b) -> Op (~>) ('OP b) ('OP (b && b))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> Obj b -> (b && b) ~> b
forall (a :: k) (b :: k). Obj a -> Obj b -> (a && b) ~> b
forall k (a :: k) (b :: k).
HasBinaryProducts k =>
Obj a -> Obj b -> (a && b) ~> b
snd' Obj b
b ~> a
a Obj b
b ~> 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} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('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 Monoidal k => Monoidal (OPPOSITE k) where
  type Unit = OP Unit
  type a ** b = OP (UN OP a ** UN OP b)
  Op b ~> a
l par :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k)
       (d :: OPPOSITE k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Op b ~> a
r = ((b ** b) ~> (a ** a)) -> Op (~>) ('OP (a ** a)) ('OP (b ** b))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (b ~> a
l (b ~> a) -> (b ~> a) -> (b ** b) ~> (a ** a)
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` b ~> a
r)
  leftUnitor :: forall (a :: OPPOSITE k). Obj a -> (Unit ** a) ~> a
leftUnitor (Op b ~> a
a) = (b ~> (Unit ** b)) -> Op (~>) ('OP (Unit ** b)) ('OP b)
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> b ~> (Unit ** b)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv Obj b
b ~> a
a)
  leftUnitorInv :: forall (a :: OPPOSITE k). Obj a -> a ~> (Unit ** a)
leftUnitorInv (Op b ~> a
a) = ((Unit ** b) ~> b) -> Op (~>) ('OP b) ('OP (Unit ** b))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> (Unit ** b) ~> b
forall (a :: k). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor Obj b
b ~> a
a)
  rightUnitor :: forall (a :: OPPOSITE k). Obj a -> (a ** Unit) ~> a
rightUnitor (Op b ~> a
a) = (b ~> (b ** Unit)) -> Op (~>) ('OP (b ** Unit)) ('OP b)
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> b ~> (b ** Unit)
forall (a :: k). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
rightUnitorInv Obj b
b ~> a
a)
  rightUnitorInv :: forall (a :: OPPOSITE k). Obj a -> a ~> (a ** Unit)
rightUnitorInv (Op b ~> a
a) = ((b ** Unit) ~> b) -> Op (~>) ('OP b) ('OP (b ** Unit))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> (b ** Unit) ~> b
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor Obj b
b ~> a
a)
  associator :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator (Op b ~> a
a) (Op b ~> a
b) (Op b ~> a
c) = ((b ** (b ** b)) ~> ((b ** b) ** b))
-> Op (~>) ('OP ((b ** b) ** b)) ('OP (b ** (b ** b)))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> Obj b -> Obj b -> (b ** (b ** b)) ~> ((b ** b) ** b)
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 b
b ~> a
a Obj b
b ~> a
b Obj b
b ~> a
c)
  associatorInv :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv (Op b ~> a
a) (Op b ~> a
b) (Op b ~> a
c) = (((b ** b) ** b) ~> (b ** (b ** b)))
-> Op (~>) ('OP (b ** (b ** b))) ('OP ((b ** b) ** b))
forall {j} {k} (c :: PRO j k) (b :: j) (a :: k).
c b a -> Op c ('OP a) ('OP b)
Op (Obj b -> Obj b -> Obj b -> ((b ** b) ** b) ~> (b ** (b ** b))
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 b
b ~> a
a Obj b
b ~> a
b Obj b
b ~> a
c)

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