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