{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Yoneda where

import Data.Function (($))

import Proarrow.Category.Instance.Prof (Prof (Prof))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Cofree (HasCofree (..))
import Proarrow.Profunctor.Star (Star (..))
import Proarrow.Category.Opposite (OPPOSITE(..), Op(..))
import Proarrow.Category.Instance.Nat (Nat(..))

type Yoneda :: (j +-> k) -> j +-> k
data Yoneda p a b where
  Yoneda :: (Ob a, Ob b) => {forall {k} {k1} (a :: k) (b :: k1) (p :: k1 +-> k).
Yoneda p a b -> Yo a ('OP b) :~> p
unYoneda :: Yo a (OP b) :~> p} -> Yoneda p a b

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

instance Functor Yoneda where
  map :: forall (a :: k -> j -> Type) (b :: k -> j -> Type).
(a ~> b) -> Yoneda a ~> Yoneda b
map (Prof a :~> b
n) = (Yoneda a :~> Yoneda b) -> Prof (Yoneda a) (Yoneda b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Yoneda Yo a ('OP b) :~> a
k) -> (Yo a ('OP b) :~> b) -> Yoneda b a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k1 +-> k).
(Ob a, Ob b) =>
(Yo a ('OP b) :~> p) -> Yoneda p a b
Yoneda (a a b -> b a b
a :~> b
n (a a b -> b a b)
-> (Yo a ('OP b) a b -> a a b) -> Yo a ('OP b) a b -> b a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Yo a ('OP b) a b -> a a b
Yo a ('OP b) :~> a
k)

instance HasCofree Profunctor where
  type Cofree Profunctor = Star Yoneda
  lower' :: forall (a :: j +-> k) (b :: j +-> k).
Cofree Profunctor a b -> a ~> b
lower' (Star (Prof a :~> Yoneda b
n)) = (a :~> b) -> Prof a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (Yoneda b a b -> b a b
Yoneda b :~> b
forall j k (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
Yoneda p :~> p
yoneda (Yoneda b a b -> b a b)
-> (a a b -> Yoneda b a b) -> a a b -> b a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a a b -> Yoneda b a b
a :~> Yoneda b
n)
  section' :: forall (a :: j +-> k) (b :: j +-> k).
Profunctor a =>
(a ~> b) -> Cofree Profunctor a b
section' (Prof a :~> b
n) = (a ~> Yoneda b) -> Star Yoneda a b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Yoneda b) -> Prof a (Yoneda b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (b a b -> Yoneda b a b
b :~> Yoneda b
forall {j} {k} (p :: j +-> k). Profunctor p => p :~> Yoneda p
mkYoneda (b a b -> Yoneda b a b)
-> (a a b -> b a b) -> a a b -> Yoneda b a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a a b -> b a b
a :~> b
n))

yoneda :: (CategoryOf j, CategoryOf k) => Yoneda (p :: j +-> k) :~> p
yoneda :: forall j k (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
Yoneda p :~> p
yoneda (Yoneda Yo a ('OP b) :~> p
k) = Yo a ('OP b) a b -> p a b
Yo a ('OP b) :~> p
k (Yo a ('OP b) a b -> p a b) -> Yo a ('OP b) a b -> p a b
forall a b. (a -> b) -> a -> b
$ (a ~> a) -> (b ~> b) -> Yo a ('OP b) a b
forall {k} {k} (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a ('OP b) c d
Yo a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

mkYoneda :: (Profunctor p) => p :~> Yoneda p
mkYoneda :: forall {j} {k} (p :: j +-> k). Profunctor p => p :~> Yoneda p
mkYoneda p a b
p = p a b
p p a b -> ((Ob a, Ob b) => Yoneda p a b) -> Yoneda p a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Yo a ('OP b) :~> p) -> Yoneda p a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k1 +-> k).
(Ob a, Ob b) =>
(Yo a ('OP b) :~> p) -> Yoneda p a b
Yoneda \(Yo a ~> a
ca b ~> b
bd) -> (a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> a
ca b ~> b
b ~> b
bd p a b
p

-- | Yoneda embedding
type Yo :: k -> OPPOSITE j -> j +-> k
data Yo a b c d where
  Yo :: c ~> a -> b ~> d -> Yo a (OP b) c d

instance (CategoryOf j, CategoryOf k) => Profunctor (Yo (a :: k) (OP b :: OPPOSITE j) :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Yo a ('OP b) a b -> Yo a ('OP b) c d
dimap c ~> a
l b ~> d
r (Yo a ~> a
f b ~> b
g) = (c ~> a) -> (b ~> d) -> Yo a ('OP b) c d
forall {k} {k} (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a ('OP b) c d
Yo (a ~> a
f (a ~> a) -> (c ~> a) -> c ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: 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 :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> b
b ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Yo a ('OP b) a b -> r
\\ Yo a ~> a
f b ~> b
g = r
(Ob a, Ob b) => r
(Ob a, Ob a) => r
r ((Ob a, Ob a) => r) -> (a ~> a) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) 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 :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> b
b ~> b
g
instance (CategoryOf j, CategoryOf k) => Functor (Yo (a :: k) :: OPPOSITE j -> j +-> k) where
  map :: forall (a :: OPPOSITE j) (b :: OPPOSITE j).
(a ~> b) -> Yo a a ~> Yo a b
map (Op b1 ~> a1
f) = (Yo a ('OP a1) :~> Yo a ('OP b1))
-> Prof (Yo a ('OP a1)) (Yo a ('OP b1))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Yo a ~> a
ca b ~> b
bd) -> (a ~> a) -> (b1 ~> b) -> Yo a ('OP b1) a b
forall {k} {k} (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a ('OP b) c d
Yo a ~> a
ca (a1 ~> b
b ~> b
bd (a1 ~> b) -> (b1 ~> a1) -> b1 ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b1 ~> a1
f)
instance (CategoryOf j, CategoryOf k) => Functor (Yo :: k -> OPPOSITE j -> j +-> k) where
  map :: forall (a :: k) (b :: k). (a ~> b) -> Yo a ~> Yo b
map a ~> b
f = (Yo a .~> Yo b) -> Nat (Yo a) (Yo b)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Yo a ('OP (UN 'OP a)) :~> Yo b ('OP (UN 'OP a)))
-> Prof (Yo a ('OP (UN 'OP a))) (Yo b ('OP (UN 'OP a)))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Yo a ~> a
ca b ~> b
bd) -> (a ~> b) -> (UN 'OP a ~> b) -> Yo b ('OP (UN 'OP a)) a b
forall {k} {k} (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Yo a ('OP b) c d
Yo (a ~> b
f (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
ca) b ~> b
UN 'OP a ~> b
bd)