{-# 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 f x = apply (hom x x) (getSelf (f %% x)) . (endCounit (EHomX_ x ->> f) x &&& id x . terminate (end (EHomX_ 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 x = endFactorizer (EHomX_ x ->> f) h
  where
    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
    h a = curry fx xa fa (apply fx fa . (map f x a . proj2 fx xa &&& proj1 fx xa))
      where
        xa = hom x a
        Self fx = f %% x
        Self fa = f %% 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 %% EOp x = FArr (EHomX_ x) (EHomX_ x)
  map Y (EOp a) (EOp b) = yonedaInv (EHomX_ b) a