-- | @'Direp' f g@ is the profunctor of arrows @f \@ a ~> g \@ b@ between the images of two functors
-- (given as 'Proarrow.Functor.FunctorForRep's).
module Proarrow.Profunctor.Instance.Direp where

import Prelude (($))

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

-- | An arrow @f \@ a '~>' g \@ b@ between the images of the functors @f@ and @g@, as a profunctor.
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 :: CAT 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 :: CAT 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, Ob a, Ob b) => r) -> r
withArr (Direp (f @ a) ~> (g @ b)
f) (HasArrow (Direp f g) a b, Ob a, Ob b) => r
r = ((f @ a) ~> (g @ b))
-> ((HasArrow (Hom k) (f @ a) (g @ b), Ob (f @ a), Ob (g @ b)) =>
    r)
-> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr (f @ a) ~> (g @ b)
f r
(HasArrow (Hom k) (f @ a) (g @ b), Ob (f @ a), Ob (g @ b)) => r
(HasArrow (Direp f g) a b, Ob a, Ob b) => r
r

instance
  (DecidableProfunctor (Hom k), FunctorForRep f, FunctorForRep g)
  => DecidableProfunctor (Direp (f :: j +-> k) (g :: i +-> k))
  where
  type Holds (Direp (f :: j +-> k) g) a b = Holds (Hom k) (f @ a) (g @ b)
  decide :: forall (a :: j) (b :: i).
(Ob a, Ob b) =>
Decision (Direp f g) a b (Holds (Direp f g) a b)
decide @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 (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 ((((f @ a) ~> (g @ b)) -> Direp f g a b)
-> Decision (Hom k) (f @ a) (g @ b) (Holds (Hom k) (f @ a) (g @ b))
-> Decision (Direp f g) a b (Holds (Hom k) (f @ a) (g @ b))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision ((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).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: k +-> k) (a :: k) (b :: k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom k) @(f @ a) @(g @ b))))
  toHolds :: forall (a :: j) (b :: i) r.
Direp f g a b
-> ((Holds (Direp f g) a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (Direp (f @ a) ~> (g @ b)
f) (Holds (Direp f g) a b ~ 'TRU, Ob a, Ob b) => r
r = ((f @ a) ~> (g @ b))
-> ((Holds (Hom k) (f @ a) (g @ b) ~ 'TRU, Ob (f @ a),
     Ob (g @ b)) =>
    r)
-> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (f @ a) ~> (g @ b)
f r
(Holds (Hom k) (f @ a) (g @ b) ~ 'TRU, Ob (f @ a), Ob (g @ b)) => r
(Holds (Direp f g) a b ~ 'TRU, Ob a, Ob b) => r
r