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

import Data.Kind (Type)

import Data.Category (Category(..), Obj)
import Data.Category.CartesianClosed (CartesianClosed(..), curry)
import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
import Data.Category.Enriched
import Data.Category.Enriched.Functor
import Data.Category.Enriched.Limit


yoneda    :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)
yoneda :: forall f (k :: * -> * -> *) x.
(HasEnds (V k), EFunctorOf k (Self (V k)) f) =>
f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)
yoneda f
f Obj k x
x = forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k x
x Obj k x
x) (forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k x
x)) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k x
x forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> f
f) Obj k x
x forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k x
x forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k x
x forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> f
f)))

yonedaInv :: forall f k x. (HasEnds (V k), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
yonedaInv :: forall f (k :: * -> * -> *) x.
(HasEnds (V k), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) =>
f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
yonedaInv f
f Obj k x
x = forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k x
x forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> f
f) forall a.
Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
h
  where
    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
    h :: forall a.
Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
h Obj k a
a = forall {k1} (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, Kind k2 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry V k (f :%% x) (f :%% x)
fx Obj (V k) (k $ (x, a))
xa V k (f :%% a) (f :%% a)
fa (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply V k (f :%% x) (f :%% x)
fx V k (f :%% a) (f :%% a)
fa forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f
f Obj k x
x Obj k a
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 V k (f :%% x) (f :%% x)
fx Obj (V k) (k $ (x, a))
xa forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 V k (f :%% x) (f :%% x)
fx Obj (V k) (k $ (x, a))
xa))
      where
        xa :: Obj (V k) (k $ (x, a))
xa = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k x
x Obj k a
a
        Self V k (f :%% x) (f :%% x)
fx = f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k x
x
        Self V k (f :%% a) (f :%% a)
fa = f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k a
a

data Y (k :: Type -> Type -> Type) = Y
-- | Yoneda embedding
instance (ECategory k, HasEnds (V k)) => EFunctor (Y k) where
  type EDom (Y k) = EOp k
  type ECod (Y k) = FunCat k (Self (V k))
  type Y k :%% x = EHomX_ k x
  Y k
Y %% :: forall a. Y k -> Obj (EDom (Y k)) a -> Obj (ECod (Y k)) (Y k :%% a)
%% EOp k a a
x = forall (a :: * -> * -> *) (b :: * -> * -> *) t s.
(EFunctorOf a b t, EFunctorOf a b s) =>
t -> s -> FunCat a b t s
FArr (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ k a a
x) (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ k a a
x)
  map :: forall (k :: * -> * -> *) a b.
(EDom (Y k) ~ k) =>
Y k
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod (Y k) $ (Y k :%% a, Y k :%% b))
map Y k
Y (EOp k a a
a) (EOp k b b
b) = forall f (k :: * -> * -> *) x.
(HasEnds (V k), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) =>
f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
yonedaInv (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ k b b
b) k a a
a