module Proarrow.Profunctor.Coyoneda where import Data.Kind (Type) import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..)) type Coyoneda :: (j -> k -> Type) -> PRO j k data Coyoneda p a b where Coyoneda :: (a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b instance (CategoryOf j, CategoryOf k) => Profunctor (Coyoneda (p :: j -> k -> Type)) where dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> Coyoneda p a b -> Coyoneda p c d dimap c ~> a l b ~> d r (Coyoneda a ~> c f d ~> b g p c d p) = (c ~> c) -> (d ~> d) -> p c d -> Coyoneda p c d forall {k} {k} (a :: k) (c :: k) (d :: k) (b :: k) (p :: k -> k -> Type). (a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b Coyoneda (a ~> c f (a ~> c) -> (c ~> a) -> c ~> c forall (b :: j) (c :: j) (a :: j). (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 . c ~> a l) (b ~> d r (b ~> d) -> (d ~> b) -> d ~> d forall (b :: k) (c :: k) (a :: k). (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 . d ~> b g) p c d p (Ob a, Ob b) => r r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> Coyoneda p a b -> r \\ Coyoneda a ~> c f d ~> b g p c d _ = r (Ob a, Ob c) => r (Ob a, Ob b) => r r ((Ob a, Ob c) => r) -> (a ~> c) -> r 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 \\ a ~> c f ((Ob d, Ob b) => r) -> (d ~> b) -> 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 \\ d ~> b g coyoneda :: (CategoryOf j, CategoryOf k, Ob a, Ob b) => p a b -> Coyoneda (p :: j -> k -> Type) a b coyoneda :: forall j k (a :: j) (b :: k) (p :: j -> k -> Type). (CategoryOf j, CategoryOf k, Ob a, Ob b) => p a b -> Coyoneda p a b coyoneda = (a ~> a) -> (b ~> b) -> p a b -> Coyoneda p a b forall {k} {k} (a :: k) (c :: k) (d :: k) (b :: k) (p :: k -> k -> Type). (a ~> c) -> (d ~> b) -> p c d -> Coyoneda p a b Coyoneda a ~> a forall (a :: j). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id b ~> b forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id