{-# 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.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction

type YonedaEmbedding k =
  Postcompose (Hom k) (Op k) :.:
  (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))

-- | The Yoneda embedding functor, @C -> Set^(C^op)@.
pattern YonedaEmbedding :: Category k => YonedaEmbedding k
pattern $bYonedaEmbedding :: YonedaEmbedding k
$mYonedaEmbedding :: forall r (k :: * -> * -> *).
Category k =>
YonedaEmbedding k -> (Void# -> r) -> (Void# -> r) -> r
YonedaEmbedding = Postcompose Hom :.: (Postcompose Swap :.: Tuple)


data Yoneda (k :: * -> * -> *) 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 % :: Yoneda k f
-> Dom (Yoneda k f) a b
-> Cod (Yoneda k f) (Yoneda k f :% a) (Yoneda k f :% b)
% Op ab = \Nat (Op k) (->) (k :-*: a) f
n -> Nat (Op k) (->) (k :-*: a) f
n Nat (Op k) (->) (k :-*: a) f
-> Nat (Op k) (->) (k :-*: b) (k :-*: a)
-> Nat (Op k) (->) (k :-*: b) f
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (FunctorCompose (Op k) (Op k :**: k) (->)
 :.: ((Const
         (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
       :***: Id (Nat (Op k) (Op k :**: k)))
      :.: DiagProd (Nat (Op k) (Op k :**: k))))
:.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
      :.: ((Const
              (Nat (Op k) (k :**: Op k))
              (Nat (k :**: Op k) (Op k :**: k))
              ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
            :***: Id (Nat (Op k) (k :**: Op k)))
           :.: DiagProd (Nat (Op k) (k :**: Op k))))
     :.: Tuple k (Op k))
forall (k :: * -> * -> *). Category k => YonedaEmbedding k
YonedaEmbedding ((FunctorCompose (Op k) (Op k :**: k) (->)
  :.: ((Const
          (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
        :***: Id (Nat (Op k) (Op k :**: k)))
       :.: DiagProd (Nat (Op k) (Op k :**: k))))
 :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
       :.: ((Const
               (Nat (Op k) (k :**: Op k))
               (Nat (k :**: Op k) (Op k :**: k))
               ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
             :***: Id (Nat (Op k) (k :**: Op k)))
            :.: DiagProd (Nat (Op k) (k :**: Op k))))
      :.: Tuple k (Op k)))
-> Dom
     ((FunctorCompose (Op k) (Op k :**: k) (->)
       :.: ((Const
               (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
             :***: Id (Nat (Op k) (Op k :**: k)))
            :.: DiagProd (Nat (Op k) (Op k :**: k))))
      :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
            :.: ((Const
                    (Nat (Op k) (k :**: Op k))
                    (Nat (k :**: Op k) (Op k :**: k))
                    ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
                  :***: Id (Nat (Op k) (k :**: Op k)))
                 :.: DiagProd (Nat (Op k) (k :**: Op k))))
           :.: Tuple k (Op k)))
     b
     a
-> Cod
     ((FunctorCompose (Op k) (Op k :**: k) (->)
       :.: ((Const
               (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
             :***: Id (Nat (Op k) (Op k :**: k)))
            :.: DiagProd (Nat (Op k) (Op k :**: k))))
      :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
            :.: ((Const
                    (Nat (Op k) (k :**: Op k))
                    (Nat (k :**: Op k) (Op k :**: k))
                    ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
                  :***: Id (Nat (Op k) (k :**: Op k)))
                 :.: DiagProd (Nat (Op k) (k :**: Op k))))
           :.: Tuple k (Op k)))
     (((FunctorCompose (Op k) (Op k :**: k) (->)
        :.: ((Const
                (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
              :***: Id (Nat (Op k) (Op k :**: k)))
             :.: DiagProd (Nat (Op k) (Op k :**: k))))
       :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
             :.: ((Const
                     (Nat (Op k) (k :**: Op k))
                     (Nat (k :**: Op k) (Op k :**: k))
                     ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
                   :***: Id (Nat (Op k) (k :**: Op k)))
                  :.: DiagProd (Nat (Op k) (k :**: Op k))))
            :.: Tuple k (Op k)))
      :% b)
     (((FunctorCompose (Op k) (Op k :**: k) (->)
        :.: ((Const
                (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
              :***: Id (Nat (Op k) (Op k :**: k)))
             :.: DiagProd (Nat (Op k) (Op k :**: k))))
       :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
             :.: ((Const
                     (Nat (Op k) (k :**: Op k))
                     (Nat (k :**: Op k) (Op k :**: k))
                     ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
                   :***: Id (Nat (Op k) (k :**: Op k)))
                  :.: DiagProd (Nat (Op k) (k :**: Op k))))
            :.: Tuple k (Op k)))
      :% a)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k b a
Dom
  ((FunctorCompose (Op k) (Op k :**: k) (->)
    :.: ((Const
            (Nat (Op k) (Op k :**: k)) (Nat (Op k :**: k) (->)) (Hom k)
          :***: Id (Nat (Op k) (Op k :**: k)))
         :.: DiagProd (Nat (Op k) (Op k :**: k))))
   :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
         :.: ((Const
                 (Nat (Op k) (k :**: Op k))
                 (Nat (k :**: Op k) (Op k :**: k))
                 ((Proj2 k (Op k) :***: Proj1 k (Op k)) :.: DiagProd (k :**: Op k))
               :***: Id (Nat (Op k) (k :**: Op k)))
              :.: DiagProd (Nat (Op k) (k :**: Op k))))
        :.: Tuple k (Op 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 :: f -> Nat (Op k) (->) (Yoneda k f) f
fromYoneda f
f = Yoneda k f
-> f
-> (forall z. Obj (Op k) z -> Component (Yoneda k f) f z)
-> Nat (Op k) (->) (Yoneda k 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 Yoneda k f
forall (k :: * -> * -> *) f. Yoneda k f
Yoneda f
f (\(Op a) Nat (Op k) (->) (k :-*: z) f
n -> (Nat (Op k) (->) (k :-*: z) f
n Nat (Op k) (->) (k :-*: z) f
-> Obj (Op k) z -> ((k :-*: z) :% z) -> f :% z
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! k z z -> Obj (Op k) z
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 :: f -> Nat (Op k) (->) f (Yoneda k f)
toYoneda   f
f = f
-> Yoneda k f
-> (forall z. Obj (Op k) z -> Component f (Yoneda k f) z)
-> Nat (Op k) (->) f (Yoneda k 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 Yoneda k f
forall (k :: * -> * -> *) f. Yoneda k f
Yoneda (\(Op a) f :% z
fa -> (k :-*: z)
-> f
-> (forall z. Obj (Op k) z -> Component (k :-*: z) f z)
-> Nat (Op k) (->) (k :-*: z) 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 (Obj k z -> k :-*: z
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k z
a) f
f (\Obj (Op k) z
_ k z z
h -> (f
f f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k z z -> Op k z z
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 () = ()

data M1 = M1
instance Functor M1 where
  type Dom M1 = Nat (Op (->)) (->)
  type Cod M1 = (->)
  type M1 :% f = f :% ()
  M1
M1 % :: M1 -> Dom M1 a b -> Cod M1 (M1 :% a) (M1 :% b)
% Dom M1 a b
n = Dom M1 a b
Nat (Op (->)) (->) a b
n Nat (Op (->)) (->) a b -> Op (->) () () -> (a :% ()) -> b :% ()
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (->) () -> Op (->) () ()
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 = M1
-> ((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 (->))))
-> (forall a.
    Obj (Nat (Op (->)) (->)) a
    -> Component
         (Id (Nat (Op (->)) (->)))
         (((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 (->))))
          :.: M1)
         a)
-> (forall a b.
    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)
    -> (M1 :% a)
    -> b)
-> Adjunction
     (->)
     (Nat (Op (->)) (->))
     M1
     ((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 (->))))
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 -> Component (Id d) (g :.: f) a)
-> (forall a b. Obj c b -> d a (g :% b) -> c (f :% a) b)
-> Adjunction c d f g
mkAdjunctionUnit M1
M1 (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 (->)))
forall (k :: * -> * -> *). Category k => YonedaEmbedding k
YonedaEmbedding
  (\(Nat f _ _) -> a
-> ((->) :-*: (a :% ()))
-> (forall z.
    Obj (Op (->)) z -> Component a ((->) :-*: (a :% ())) z)
-> Nat (Op (->)) (->) a ((->) :-*: (a :% ()))
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 (Obj (->) (a :% ()) -> (->) :-*: (a :% ())
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X (a
f a -> Dom a () () -> Cod a (a :% ()) (a :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (->) () -> Op (->) () ()
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 a -> Dom a z () -> Cod a (a :% z) (a :% ())
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (() -> z) -> Op (->) z ()
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
_ n :: 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@(Nat f _ _) a :% ()
fu -> (Nat
  (Op (->))
  (->)
  a
  (Hom (->)
   :.: (Swap (->) (Op (->))
        :.: ((Const (Op (->)) (->) b :***: Id (Op (->)))
             :.: DiagProd (Op (->)))))
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 Nat
  (Op (->))
  (->)
  a
  (Hom (->)
   :.: (Swap (->) (Op (->))
        :.: ((Const (Op (->)) (->) b :***: Id (Op (->)))
             :.: DiagProd (Op (->)))))
-> Op (->) () ()
-> (a :% ())
-> (Hom (->)
    :.: (Swap (->) (Op (->))
         :.: ((Const (Op (->)) (->) b :***: Id (Op (->)))
              :.: DiagProd (Op (->)))))
   :% ()
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj (->) () -> Op (->) () ()
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj (->) ()
haskUnit) a :% ()
fu ())