{-# 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