{-# LANGUAGE TypeOperators, RankNTypes, TypeFamilies, PatternSynonyms, UndecidableInstances, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Yoneda
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Yoneda where

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction

type YonedaEmbedding k = Curry2 (Op k) k (Hom k)
-- | The Yoneda embedding functor, @C -> Set^(C^op)@.
pattern YonedaEmbedding :: Category k => YonedaEmbedding k
pattern $bYonedaEmbedding :: forall (k :: * -> * -> *). Category k => YonedaEmbedding k
$mYonedaEmbedding :: forall {r} {k :: * -> * -> *}.
Category k =>
YonedaEmbedding k -> ((# #) -> r) -> ((# #) -> r) -> r
YonedaEmbedding = Curry2 Hom


data Yoneda (k :: Type -> Type -> Type) f = Yoneda
-- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.
instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where
  type Dom (Yoneda k f) = Op k
  type Cod (Yoneda k f) = (->)
  type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
  Yoneda k f
Yoneda % :: forall a b.
Yoneda k f
-> Dom (Yoneda k f) a b
-> Cod (Yoneda k f) (Yoneda k f :% a) (Yoneda k f :% b)
% Op k b a
ab = \Cod
  ((FunctorCompose (Op k) (Op k :**: k) (->)
    :.: Tuple1
          (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
   :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
         :.: Tuple1
               (Nat (k :**: Op k) (Op k :**: k))
               (Nat (Op k) (k :**: Op k))
               (Swap k (Op k)))
        :.: Tuple k (Op k)))
  (((FunctorCompose (Op k) (Op k :**: k) (->)
     :.: Tuple1
           (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
    :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
          :.: Tuple1
                (Nat (k :**: Op k) (Op k :**: k))
                (Nat (Op k) (k :**: Op k))
                (Swap k (Op k)))
         :.: Tuple k (Op k)))
   :% a)
  f
n -> Cod
  ((FunctorCompose (Op k) (Op k :**: k) (->)
    :.: Tuple1
          (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
   :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
         :.: Tuple1
               (Nat (k :**: Op k) (Op k :**: k))
               (Nat (Op k) (k :**: Op k))
               (Swap k (Op k)))
        :.: Tuple k (Op k)))
  (((FunctorCompose (Op k) (Op k :**: k) (->)
     :.: Tuple1
           (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
    :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
          :.: Tuple1
                (Nat (k :**: Op k) (Op k :**: k))
                (Nat (Op k) (k :**: Op k))
                (Swap k (Op k)))
         :.: Tuple k (Op k)))
   :% a)
  f
n forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *). Category k => YonedaEmbedding k
YonedaEmbedding forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k b a
ab


-- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.
fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f
fromYoneda :: forall (k :: * -> * -> *) f.
(Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) =>
f -> Nat (Op k) (->) (Yoneda k f) f
fromYoneda f
f = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall (k :: * -> * -> *) f. Yoneda k f
Yoneda f
f (\(Op k z z
a) Nat (Op k) (->) (k :-*: z) f
n -> (Nat (Op k) (->) (k :-*: z) f
n forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k z z
a) k z z
a)

toYoneda   :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f)
toYoneda :: forall (k :: * -> * -> *) f.
(Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) =>
f -> Nat (Op k) (->) f (Yoneda k f)
toYoneda   f
f = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f forall (k :: * -> * -> *) f. Yoneda k f
Yoneda (\(Op k z z
a) f :% z
fa -> forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X k z z
a) f
f (\Obj (Op k) z
_ k z z
h -> (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k z z
h) f :% z
fa))


haskUnit :: Obj (->) ()
haskUnit :: Obj (->) ()
haskUnit = forall a. Obj (->) a
obj

data M1 = M1
instance Functor M1 where
  type Dom M1 = Nat (Op (->)) (->)
  type Cod M1 = (->)
  type M1 :% f = f :% ()
  M1
M1 % :: forall a b. M1 -> Dom M1 a b -> Cod M1 (M1 :% a) (M1 :% b)
% Dom M1 a b
n = Dom M1 a b
n forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj (->) ()
haskUnit

haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))
haskIsTotal = forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> d a (g :% (f :% a)))
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionInit M1
M1 forall (k :: * -> * -> *). Category k => YonedaEmbedding k
YonedaEmbedding
  (\(Nat a
f a
_ forall z. Obj (Op (->)) z -> Component a a z
_) -> forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
f (forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X (a
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj (->) ()
haskUnit)) (\Obj (Op (->)) z
_ a :% z
fz z
z -> (a
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (\() -> z
z)) a :% z
fz))
  (\Obj (->) b
_ Nat
  (Op (->))
  (->)
  a
  (((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
     :.: Tuple1
           (Nat (Op (->) :**: (->)) (->))
           (Nat (Op (->)) (Op (->) :**: (->)))
           (Hom (->)))
    :.: ((FunctorCompose
            (Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
          :.: Tuple1
                (Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
                (Nat (Op (->)) ((->) :**: Op (->)))
                (Swap (->) (Op (->))))
         :.: Tuple (->) (Op (->))))
   :% b)
n a :% ()
fu -> (Nat
  (Op (->))
  (->)
  a
  (((FunctorCompose (Op (->)) (Op (->) :**: (->)) (->)
     :.: Tuple1
           (Nat (Op (->) :**: (->)) (->))
           (Nat (Op (->)) (Op (->) :**: (->)))
           (Hom (->)))
    :.: ((FunctorCompose
            (Op (->)) ((->) :**: Op (->)) (Op (->) :**: (->))
          :.: Tuple1
                (Nat ((->) :**: Op (->)) (Op (->) :**: (->)))
                (Nat (Op (->)) ((->) :**: Op (->)))
                (Swap (->) (Op (->))))
         :.: Tuple (->) (Op (->))))
   :% b)
n forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op Obj (->) ()
haskUnit) a :% ()
fu ())