module Proarrow.Profunctor.Identity where import Proarrow.Core (CAT, CategoryOf(..), Promonad(..), Profunctor(..)) import Proarrow.Profunctor.Representable (Representable(..)) import Proarrow.Profunctor.Corepresentable (Corepresentable(..)) type Id :: CAT k newtype Id a b = Id { forall k (a :: k) (b :: k). Id a b -> a ~> b getId :: a ~> b } instance CategoryOf k => Profunctor (Id :: CAT k) where dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> Id a b -> Id c d dimap c ~> a l b ~> d r (Id a ~> b f) = (c ~> d) -> Id c d forall k (a :: k) (b :: k). (a ~> b) -> Id a b Id (b ~> d r (b ~> d) -> (c ~> b) -> c ~> 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 . a ~> b f (a ~> b) -> (c ~> a) -> c ~> b 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 . c ~> a l) (Ob a, Ob b) => r r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Id a b -> r \\ Id a ~> b f = r (Ob a, Ob b) => r r ((Ob a, Ob b) => r) -> (a ~> 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 \\ a ~> b f instance CategoryOf k => Promonad (Id :: CAT k) where id :: forall (a :: k). Ob a => Id a a id = (a ~> a) -> Id a a forall k (a :: k) (b :: k). (a ~> b) -> Id a b Id a ~> a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Id b ~> c f . :: forall (b :: k) (c :: k) (a :: k). Id b c -> Id a b -> Id a c . Id a ~> b g = (a ~> c) -> Id a c forall k (a :: k) (b :: k). (a ~> b) -> Id a b Id (b ~> c f (b ~> c) -> (a ~> b) -> a ~> c 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 . a ~> b g) instance CategoryOf k => Representable (Id :: CAT k) where type Id % a = a index :: forall (a :: k) (b :: k). Id a b -> a ~> (Id % b) index = Id a b -> a ~> b Id a b -> a ~> (Id % b) forall k (a :: k) (b :: k). Id a b -> a ~> b getId tabulate :: forall (b :: k) (a :: k). Ob b => (a ~> (Id % b)) -> Id a b tabulate = (a ~> b) -> Id a b (a ~> (Id % b)) -> Id a b forall k (a :: k) (b :: k). (a ~> b) -> Id a b Id repMap :: forall (a :: k) (b :: k). (a ~> b) -> (Id % a) ~> (Id % b) repMap = (a ~> b) -> a ~> b (a ~> b) -> (Id % a) ~> (Id % b) forall a. Ob a => a -> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id instance CategoryOf k => Corepresentable (Id :: CAT k) where type Id %% a = a coindex :: forall (a :: k) (b :: k). Id a b -> (Id %% a) ~> b coindex = Id a b -> a ~> b Id a b -> (Id %% a) ~> b forall k (a :: k) (b :: k). Id a b -> a ~> b getId cotabulate :: forall (a :: k) (b :: k). Ob a => ((Id %% a) ~> b) -> Id a b cotabulate = (a ~> b) -> Id a b ((Id %% a) ~> b) -> Id a b forall k (a :: k) (b :: k). (a ~> b) -> Id a b Id corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Id %% a) ~> (Id %% b) corepMap = (a ~> b) -> a ~> b (a ~> b) -> (Id %% a) ~> (Id %% b) forall a. Ob a => a -> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id