module Proarrow.Profunctor.Direpresentable where

import Prelude (($))

import Proarrow.Category.Enriched.Thin (Thin, ThinProfunctor (..))
import Proarrow.Core (CategoryOf (..), Hom, Profunctor (..), Promonad (..), type (+->))
import Proarrow.Functor (FunctorForRep (..), withMappedOb)

type Direp :: (j +-> k) -> (i +-> k) -> i +-> j
data Direp f g a b where
  Direp :: (Ob a, Ob b) => (f @ a) ~> (g @ b) -> Direp f g a b

instance (FunctorForRep f, FunctorForRep g) => Profunctor (Direp f g) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Direp f g a b -> Direp f g c d
dimap c ~> a
l b ~> d
r (Direp (f @ a) ~> (g @ b)
f) = ((f @ c) ~> (g @ d)) -> Direp f g c d
forall {j} {j} {k} (a :: j) (b :: j) (f :: j +-> k) (g :: j +-> k).
(Ob a, Ob b) =>
((f @ a) ~> (g @ b)) -> Direp f g a b
Direp (forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @g b ~> d
r ((g @ b) ~> (g @ d)) -> ((f @ c) ~> (g @ b)) -> (f @ c) ~> (g @ d)
forall (b :: k) (c :: k) (a :: k). (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
. (f @ a) ~> (g @ b)
f ((f @ a) ~> (g @ b)) -> ((f @ c) ~> (f @ a)) -> (f @ c) ~> (g @ b)
forall (b :: k) (c :: k) (a :: k). (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
. forall {j} {k} (f :: j +-> k) (a :: j) (b :: j).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
forall (f :: k +-> k) (a :: k) (b :: k).
FunctorForRep f =>
(a ~> b) -> (f @ a) ~> (f @ b)
fmap @f c ~> a
l) ((Ob b, Ob d) => Direp f g c d) -> (b ~> d) -> Direp f g c d
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> d
r ((Ob c, Ob a) => Direp f g c d) -> (c ~> a) -> Direp f g c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
l
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Direp f g a b -> r
\\ Direp{} = r
(Ob a, Ob b) => r
r

instance (Thin k, FunctorForRep f, FunctorForRep g) => ThinProfunctor (Direp (f :: j +-> k) (g :: i +-> k)) where
  type HasArrow (Direp (f :: j +-> k) g) a b = HasArrow (Hom k) (f @ a) (g @ b)
  arr :: forall (a :: j) (b :: i).
(Ob a, Ob b, HasArrow (Direp f g) a b) =>
Direp f g a b
arr @a @b = forall {j} {k} (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
forall (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
withMappedOb @f @a ((Ob (f @ a) => Direp f g a b) -> Direp f g a b)
-> (Ob (f @ a) => Direp f g a b) -> Direp f g a b
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (f :: j +-> k) (a :: j) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
forall (f :: i +-> k) (a :: i) r.
(FunctorForRep f, Ob a) =>
(Ob (f @ a) => r) -> r
withMappedOb @g @b ((Ob (g @ b) => Direp f g a b) -> Direp f g a b)
-> (Ob (g @ b) => Direp f g a b) -> Direp f g a b
forall a b. (a -> b) -> a -> b
$ ((f @ a) ~> (g @ b)) -> Direp f g a b
forall {j} {j} {k} (a :: j) (b :: j) (f :: j +-> k) (g :: j +-> k).
(Ob a, Ob b) =>
((f @ a) ~> (g @ b)) -> Direp f g a b
Direp (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(Hom k) @(f @ a) @(g @ b))
  withArr :: forall (a :: j) (b :: i) r.
Direp f g a b -> (HasArrow (Direp f g) a b => r) -> r
withArr (Direp (f @ a) ~> (g @ b)
f) HasArrow (Direp f g) a b => r
r = ((f @ a) ~> (g @ b))
-> (HasArrow (Hom k) (f @ a) (g @ b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> (HasArrow (Hom k) 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 (f @ a) ~> (g @ b)
f r
HasArrow (Hom k) (f @ a) (g @ b) => r
HasArrow (Direp f g) a b => r
r