module Proarrow.Profunctor.Yoneda where

import Data.Kind (Type)
import Data.Function (($))

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), (//), (:~>))


type Yoneda :: (j -> k -> Type) -> PRO j k
data Yoneda p a b where
  Yoneda :: (Ob a, Ob b) => { forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type).
Yoneda p a b -> Yo a b :~> p
getYoneda :: Yo a b :~> p } -> Yoneda p a b

instance (CategoryOf j, CategoryOf k) => Profunctor (Yoneda (p :: PRO j k)) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yoneda p a b -> Yoneda p c d
dimap c ~> a
l b ~> d
r (Yoneda Yo a b :~> p
k) = c ~> a
l (c ~> a) -> ((Ob c, Ob a) => Yoneda p c d) -> Yoneda p c d
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
r (b ~> d) -> ((Ob b, Ob d) => Yoneda p c d) -> Yoneda p c d
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Yo c d :~> p) -> Yoneda p c d
forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type).
(Ob a, Ob b) =>
(Yo a b :~> p) -> Yoneda p a b
Yoneda \(Yo a ~> c
ca d ~> b
bd) -> Yo a b a b -> p a b
Yo a b :~> p
k (Yo a b a b -> p a b) -> Yo a b a b -> p a b
forall a b. (a -> b) -> a -> b
$ (a ~> a) -> (b ~> b) -> Yo a b a b
forall {k} {k} (a :: k) (b :: k) (c :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a b c d
Yo (c ~> a
l (c ~> a) -> (a ~> c) -> a ~> a
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
. a ~> c
ca) (d ~> b
bd (d ~> b) -> (b ~> d) -> b ~> 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
. b ~> d
r)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> Yoneda p a b -> r
\\ Yoneda{} = r
(Ob a, Ob b) => r
r

yoneda :: (CategoryOf j, CategoryOf k) => Yoneda (p :: PRO j k) :~> p
yoneda :: forall j k (p :: PRO j k).
(CategoryOf j, CategoryOf k) =>
Yoneda p :~> p
yoneda (Yoneda Yo a b :~> p
k) = Yo a b a b -> p a b
Yo a b :~> p
k (Yo a b a b -> p a b) -> Yo a b a b -> p a b
forall a b. (a -> b) -> a -> b
$ (a ~> a) -> (b ~> b) -> Yo a b a b
forall {k} {k} (a :: k) (b :: k) (c :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a b c d
Yo 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


-- | Yoneda embedding
data Yo a b c d = Yo (c ~> a) (b ~> d)
instance (CategoryOf j, CategoryOf k) => Profunctor (Yo (a :: j) (b :: k) :: PRO j k) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a b a b -> Yo a b c d
dimap c ~> a
l b ~> d
r (Yo a ~> a
f b ~> b
g) = (c ~> a) -> (b ~> d) -> Yo a b c d
forall {k} {k} (a :: k) (b :: k) (c :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a b c d
Yo (a ~> a
f (a ~> a) -> (c ~> a) -> c ~> a
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) -> (b ~> b) -> b ~> 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
. b ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> Yo a b a b -> r
\\ Yo a ~> a
f b ~> b
g = r
(Ob a, Ob a) => r
(Ob a, Ob b) => r
r ((Ob a, Ob a) => r) -> (a ~> a) -> 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 ~> a
f ((Ob b, Ob b) => r) -> (b ~> 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
\\ b ~> b
g