module Proarrow.Profunctor.Identity where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Category.Dagger (DaggerProfunctor (..), Dagger)

type Id :: CAT k
newtype Id a b = Id {forall k (a :: k) (b :: k). Id a b -> a ~> b
unId :: 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
unId
  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
unId
  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

instance (Monoidal k) => MonoidalProfunctor (Id :: CAT k) where
  par0 :: Id Unit Unit
par0 = (Unit ~> Unit) -> Id Unit Unit
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Id x1 ~> x2
f par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Id x1 x2 -> Id y1 y2 -> Id (x1 ** y1) (x2 ** y2)
`par` Id y1 ~> y2
g = ((x1 ** y1) ~> (x2 ** y2)) -> Id (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (x1 ~> x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` y1 ~> y2
g)

instance (Dagger k) => DaggerProfunctor (Id :: CAT k) where
  dagger :: forall (a :: k) (b :: k). Id a b -> Id b a
dagger (Id a ~> b
p) = (b ~> a) -> Id b a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> b ~> a
forall (a :: k) (b :: k). (a ~> b) -> b ~> a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger a ~> b
p)