{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Profunctor.Corepresentable where

import Data.Kind (Constraint)

import Proarrow.Core (PRO, CategoryOf(..), Profunctor(..), Promonad(..))
import Proarrow.Object (obj)

infixl 8 %%

type Corepresentable :: forall {j} {k}. PRO j k -> Constraint
class Profunctor p => Corepresentable (p :: PRO j k) where
  type p %% (a :: j) :: k
  coindex :: p a b -> p %% a ~> b
  cotabulate :: Ob a => (p %% a ~> b) -> p a b
  corepMap :: (a ~> b) -> p %% a ~> p %% b

withCorepCod :: forall p a r. (Corepresentable p, Ob a) => (Ob (p %% a) => r) -> r
withCorepCod :: forall {j} {k} (p :: PRO j k) (a :: j) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withCorepCod Ob (p %% a) => r
r = r
Ob (p %% a) => r
(Ob (p %% a), Ob (p %% a)) => r
r ((Ob (p %% a), Ob (p %% a)) => r) -> ((p %% a) ~> (p %% a)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

dimapCorep :: forall p a b c d. Corepresentable p => (c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep :: forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (c :: j) (d :: k).
Corepresentable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapCorep c ~> a
l b ~> d
r = forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (p :: PRO j k) (a :: j) (b :: k).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate @p (((p %% c) ~> d) -> p c d)
-> (p a b -> (p %% c) ~> d) -> p a b -> p c d
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
. ((p %% c) ~> (p %% a))
-> (b ~> d) -> ((p %% a) ~> b) -> (p %% c) ~> d
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> 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 (forall {j} {k} (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: PRO j k) (a :: j) (b :: j).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p c ~> a
l) b ~> d
r (((p %% a) ~> b) -> (p %% c) ~> d)
-> (p a b -> (p %% a) ~> b) -> p a b -> (p %% c) ~> d
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
. p a b -> (p %% a) ~> b
forall (a :: j) (b :: k). p a b -> (p %% a) ~> b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((Ob c, Ob a) => p a b -> p c d) -> (c ~> a) -> p a b -> p c d
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
l