module Proarrow.Category.Opposite where

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..), Thin)
import Proarrow.Core (CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, lmap, type (+->))
import Proarrow.Functor (Functor (..))

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 :: j +-> k) (c :: k) (a :: k) (b :: j).
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 :: 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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: 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 :: j +-> k) (a :: k) (b :: j) 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 :: 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 :: 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 (ThinProfunctor p) => ThinProfunctor (Op p) where
  type HasArrow (Op p) (OP a) (OP b) = HasArrow p b a
  arr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
(Ob a, Ob b, HasArrow (Op p) a b) =>
Op p a b
arr = p (UN 'OP b) (UN 'OP a) -> Op p ('OP (UN '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) (UN 'OP a)
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
  withArr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
Op p a b -> (HasArrow (Op p) a b => r) -> r
withArr (Op p b a
f) HasArrow (Op p) a b => r
r = p b a -> (HasArrow p b a => 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 b a
f r
HasArrow p b a => r
HasArrow (Op p) a b => r
r

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 :: 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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: 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 :: j +-> k) (a :: k) (b :: j) 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 (Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (UnOp p :: j +-> k) where
  type HasArrow (UnOp p) a b = HasArrow p (OP b) (OP a)
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (UnOp p) a b) =>
UnOp p a b
arr = Op (UnOp p) ('OP b) ('OP a) -> UnOp p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
Op p ('OP a) ('OP b) -> p b a
unOp Op (UnOp p) ('OP b) ('OP a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (a :: OPPOSITE j) (b :: OPPOSITE k).
(Ob a, Ob b, HasArrow (Op (UnOp p)) a b) =>
Op (UnOp p) a b
arr
  withArr :: forall (a :: k) (b :: j) r.
UnOp p a b -> (HasArrow (UnOp p) a b => r) -> r
withArr UnOp p a b
f HasArrow (UnOp p) a b => r
r = Op (UnOp p) ('OP b) ('OP a)
-> (HasArrow (Op (UnOp p)) ('OP b) ('OP a) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
Op (UnOp p) a b -> (HasArrow (Op (UnOp p)) a b => r) -> r
withArr (UnOp p a b -> Op (UnOp p) ('OP b) ('OP a)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Op p ('OP a) ('OP b)
Op UnOp p a b
f) r
HasArrow (UnOp p) a b => r
HasArrow (Op (UnOp p)) ('OP b) ('OP a) => r
r