{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Prof where

import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, (:~>), type (+->))

type Prof :: CAT (j +-> k)
data Prof p q where
  Prof
    :: (Profunctor p, Profunctor q)
    => {forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf :: p :~> q}
    -> Prof p q

-- | The category of profunctors and natural transformations between them.
instance CategoryOf (j +-> k) where
  type (~>) = Prof
  type Ob p = Profunctor p

instance Promonad Prof where
  id :: forall (a :: j +-> k). Ob a => Prof a a
id = (a :~> a) -> Prof a a
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> a a b
a :~> a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Prof b :~> c
f . :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. Prof a :~> b
g = (a :~> c) -> Prof a c
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (b a b -> c a b
b :~> c
f (b a b -> c a b) -> (a a b -> b a b) -> a a b -> c a 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
. a a b -> b a b
a :~> b
g)

instance Profunctor Prof where
  dimap :: forall (c :: j +-> k) (a :: j +-> k) (b :: j +-> k) (d :: j +-> k).
(c ~> a) -> (b ~> d) -> Prof a b -> Prof c d
dimap = (c ~> a) -> (b ~> d) -> Prof a b -> Prof c d
Prof c a -> Prof b d -> Prof a b -> Prof c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: j +-> k) (b :: j +-> k) r.
((Ob a, Ob b) => r) -> Prof a b -> r
\\ Prof{} = r
(Ob a, Ob b) => r
r