content: {-# LANGUAGE
      TypeOperators
    , TypeFamilies
    , GADTs
    , RankNTypes
    , PatternSynonyms
    , FlexibleContexts
    , FlexibleInstances
    , NoImplicitPrelude
    , UndecidableInstances
    , ScopedTypeVariables
    , ConstraintKinds
    , MultiParamTypeClasses
    #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Data.Category.Enriched.Limit
  -- License     :  BSD-style (see the file LICENSE)
  --
  -- Maintainer  :  sjoerd@w3future.com
  -- Stability   :  experimental
  -- Portability :  non-portable
  -----------------------------------------------------------------------------
  module Data.Category.Enriched.Limit where
  
  import Data.Kind (Type)
  
  import Data.Category (Category(..), Obj)
  import Data.Category.Functor (Functor(..))
  import Data.Category.Limit (HasBinaryProducts(..))
  import Data.Category.CartesianClosed (CartesianClosed(..), curry, flip)
  import qualified Data.Category.WeightedLimit as Hask
  import Data.Category.Enriched
  import Data.Category.Enriched.Functor
  
  type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t
  
  class CartesianClosed v => HasEnds v where
    type End (v :: Type -> Type -> Type) t :: Type
    end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)
    endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))
    endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
  
  
  newtype HaskEnd t = HaskEnd { getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }
  instance HasEnds (->) where
    type End (->) t = HaskEnd t
    end _ e = e
    endCounit t a (HaskEnd e) = e t a
    endFactorizer _ e x = HaskEnd (\_ a -> e a x)
  
  
  data FunCat a b t s where
    FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s
  
  type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)
  (->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s
  t ->> s = EHom :.: (Opposite t :<*>: s)
  -- | The enriched functor category @[a, b]@
  instance (HasEnds (V a), CartesianClosed (V a), V a ~ V b) => ECategory (FunCat a b) where
    type V (FunCat a b) = V a
    type FunCat a b $ (t, s) = End (V a) (t :->>: s)
    hom (FArr t _) (FArr s _) = end (t ->> s)
    id (FArr t _) = endFactorizer (t ->> t) (\a -> id (t %% a))
    comp (FArr t _) (FArr s _) (FArr r _) = endFactorizer (t ->> r)
      (\a -> comp (t %% a) (s %% a) (r %% a) . (endCounit (s ->> r) a *** endCounit (t ->> s) a))
  
  
  data EndFunctor (k :: Type -> Type -> Type) = EndFunctor
  instance (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) where
    type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))
    type ECod (EndFunctor k) = Self (V k)
    type EndFunctor k :%% t = End (V k) t
    EndFunctor %% (FArr t _) = Self (end t)
    map EndFunctor (FArr f _) (FArr g _) = curry (end (f ->> g)) (end f) (end g) (endFactorizer g (\a ->
      let aa = EOp a :<>: a in apply (getSelf (f %% aa)) (getSelf (g %% aa)) . (endCounit (f ->> g) aa *** endCounit f a)))
  
  
  -- d :: j -> k, w :: j -> Self (V k)
  type family WeigtedLimit (k :: Type -> Type -> Type) w d :: Type
  type Lim w d = WeigtedLimit (ECod d) w d
  
  class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasLimits k w where
    limitObj :: EFunctorOf (EDom w) k d => w -> d -> Obj k (Lim w d)
    limit    :: EFunctorOf (EDom w) k d => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))
    limitInv :: EFunctorOf (EDom w) k d => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))
  
  -- d :: j -> k, w :: EOp j -> Self (V k)
  type family WeigtedColimit (k :: Type -> Type -> Type) w d :: Type
  type Colim w d = WeigtedColimit (ECod d) w d
  
  class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasColimits k w where
    colimitObj :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k (Colim w d)
    colimit    :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))
    colimitInv :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))
  
  
  type instance WeigtedLimit (Self v) w d = End v (w :->>: d)
  instance (HasEnds v, EFunctor w, ECod w ~ Self v) => HasLimits (Self v) w where
    limitObj w d = Self (end (w ->> d))
    limit    w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in endFactorizer wed
      (\a -> let { Self wa = w %% a; Self da = d %% a } in flip e wa da . (endCounit (w ->> d) a ^^^ e))
    limitInv w d (Self e) = let wed = w ->> (EHomX_ (Self e) :.: d) in curry (end wed) e (end (w ->> d))
      (endFactorizer (w ->> d) (\a -> let { Self wa = w %% a; Self da = d %% a } in apply e (da ^^^ wa) . (flip wa e da . endCounit wed a *** e)))
  
  type instance WeigtedLimit (InHask k) (InHaskToHask w) d = Hask.WeightedLimit k w (UnderlyingHask (Dom w) k d)
  instance Hask.HasWLimits k w => HasLimits (InHask k) (InHaskToHask w) where
    limitObj (InHaskToHask w) d = InHask (Hask.limitObj w (UnderlyingHask d))
    limit    (InHaskToHask w) d _ el = HaskEnd (\_ (InHask a) wa -> Hask.limit w (UnderlyingHask d) a wa . el)
    limitInv (InHaskToHask w) d (InHask e) (HaskEnd n) =
      Hask.limitFactorizer w (UnderlyingHask d) e (n (InHaskToHask w ->> (EHomX_ (InHask e) :.: d)) . InHask)
  