{-# 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 { forall t.
HaskEnd t
-> forall (k :: * -> * -> *) a.
   VProfunctor k k t =>
   t -> Obj k a -> t :%% (a, a)
getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }
instance HasEnds (->) where
  type End (->) t = HaskEnd t
  end :: forall (k :: * -> * -> *) t.
(VProfunctor k k t, V k ~ (->)) =>
t -> Obj (->) (End (->) t)
end t
_ End (->) t
e = End (->) t
e
  endCounit :: forall (k :: * -> * -> *) t a.
(VProfunctor k k t, V k ~ (->)) =>
t -> Obj k a -> End (->) t -> (t :%% (a, a))
endCounit t
t Obj k a
a (HaskEnd forall (k :: * -> * -> *) a.
VProfunctor k k t =>
t -> Obj k a -> t :%% (a, a)
e) = forall (k :: * -> * -> *) a.
VProfunctor k k t =>
t -> Obj k a -> t :%% (a, a)
e t
t Obj k a
a
  endFactorizer :: forall (k :: * -> * -> *) t x.
(VProfunctor k k t, V k ~ (->)) =>
t -> (forall a. Obj k a -> x -> (t :%% (a, a))) -> x -> End (->) t
endFactorizer t
_ forall a. Obj k a -> x -> (t :%% (a, a))
e x
x = forall t.
(forall (k :: * -> * -> *) a.
 VProfunctor k k t =>
 t -> Obj k a -> t :%% (a, a))
-> HaskEnd t
HaskEnd (\t
_ Obj k a
a -> forall a. Obj k a -> x -> (t :%% (a, a))
e Obj k a
a x
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
t ->> :: forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> s
s = forall (k :: * -> * -> *). EHom k
EHom forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: (forall f. EFunctor f => f -> Opposite f
Opposite t
t forall f1 f2. f1 -> f2 -> f1 :<*>: f2
:<*>: s
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 :: forall a b.
Obj (FunCat a b) a
-> Obj (FunCat a b) b -> Obj (V (FunCat a b)) (FunCat a b $ (a, b))
hom (FArr a
t a
_) (FArr b
s b
_) = forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (a
t forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
s)
  id :: forall a. Obj (FunCat a b) a -> Arr (FunCat a b) a a
id (FArr a
t a
_) = 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 (a
t forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> a
t) (\Obj a a
a -> forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id (a
t forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
a))
  comp :: forall a b c.
Obj (FunCat a b) a
-> Obj (FunCat a b) b
-> Obj (FunCat a b) c
-> V (FunCat a b)
     (BinaryProduct
        (V (FunCat a b)) (FunCat a b $ (b, c)) (FunCat a b $ (a, b)))
     (FunCat a b $ (a, c))
comp (FArr a
t a
_) (FArr b
s b
_) (FArr c
r c
_) = 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 (a
t forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> c
r)
    (\Obj a a
a -> forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b
-> Obj k c
-> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
comp (a
t forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
a) (b
s forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
a) (c
r forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a 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 (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 (b
s forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> c
r) Obj a a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** 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 (a
t forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
s) Obj a a
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 k
EndFunctor %% :: forall a.
EndFunctor k
-> Obj (EDom (EndFunctor k)) a
-> Obj (ECod (EndFunctor k)) (EndFunctor k :%% a)
%% (FArr a
t a
_) = forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end a
t)
  map :: forall (k :: * -> * -> *) a b.
(EDom (EndFunctor k) ~ k) =>
EndFunctor k
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (EndFunctor k) $ (EndFunctor k :%% a, EndFunctor k :%% b))
map EndFunctor k
EndFunctor (FArr a
f a
_) (FArr b
g b
_) = 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 (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (a
f forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
g)) (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end a
f) (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end b
g) (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 b
g (\Obj k a
a ->
    let aa :: (:<>:) (EOp k) k (a, a) (a, a)
aa = forall (k :: * -> * -> *) a b. k b a -> EOp k a b
EOp Obj k a
a forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: Obj k a
a in 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 (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (a
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% (:<>:) (EOp k) k (a, a) (a, a)
aa)) (forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (b
g forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% (:<>:) (EOp k) k (a, a) (a, a)
aa)) 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 (a
f forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
g) (:<>:) (EOp k) k (a, a) (a, a)
aa forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** 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 a
f Obj k a
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 :: forall d.
EFunctorOf (EDom w) (Self v) d =>
w -> d -> Obj (Self v) (Lim w d)
limitObj w
w d
d = forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d))
  limit :: forall d e.
EFunctorOf (EDom w) (Self v) d =>
w
-> d
-> Obj (Self v) e
-> V (Self v)
     (Self v $ (e, Lim w d))
     (End (V (Self v)) (w :->>: (EHomX_ (Self v) e :.: d)))
limit    w
w d
d (Self v e e
e) = let wed :: w :->>: (EHomX_ (Self v) e :.: d)
wed = w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ (forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self v e e
e) forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: d
d) in 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 w :->>: (EHomX_ (Self v) e :.: d)
wed
    (\Obj (EDom w) a
a -> let { Self V (EDom w) (w :%% a) (w :%% a)
wa = w
w forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom w) a
a; Self V (EDom w) (d :%% a) (d :%% a)
da = d
d forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom w) a
a } in forall {k1} (k2 :: k1 -> k1 -> *) (a :: k1) (b :: k1) (c :: k1).
CartesianClosed k2 =>
Obj k2 a
-> Obj k2 b
-> Obj k2 c
-> k2
     (Exponential k2 a (Exponential k2 b c))
     (Exponential k2 b (Exponential k2 a c))
flip v e e
e V (EDom w) (w :%% a) (w :%% a)
wa V (EDom w) (d :%% a) (d :%% a)
da 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 (w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d) Obj (EDom w) a
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ v e e
e))
  limitInv :: forall d e.
EFunctorOf (EDom w) (Self v) d =>
w
-> d
-> Obj (Self v) e
-> V (Self v)
     (End (V (Self v)) (w :->>: (EHomX_ (Self v) e :.: d)))
     (Self v $ (e, Lim w d))
limitInv w
w d
d (Self v e e
e) = let wed :: w :->>: (EHomX_ (Self v) e :.: d)
wed = w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ (forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self v e e
e) forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: d
d) in 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 (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end w :->>: (EHomX_ (Self v) e :.: d)
wed) v e e
e (forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d))
    (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 (w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d) (\Obj (EDom w) a
a -> let { Self v (w :%% a) (w :%% a)
wa = w
w forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom w) a
a; Self v (d :%% a) (d :%% a)
da = d
d forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom w) a
a } in 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 e e
e (v (d :%% a) (d :%% a)
da forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ v (w :%% a) (w :%% a)
wa) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall {k1} (k2 :: k1 -> k1 -> *) (a :: k1) (b :: k1) (c :: k1).
CartesianClosed k2 =>
Obj k2 a
-> Obj k2 b
-> Obj k2 c
-> k2
     (Exponential k2 a (Exponential k2 b c))
     (Exponential k2 b (Exponential k2 a c))
flip v (w :%% a) (w :%% a)
wa v e e
e v (d :%% a) (d :%% a)
da 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 w :->>: (EHomX_ (Self v) e :.: d)
wed Obj (EDom w) a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** v e e
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 :: forall d.
EFunctorOf (EDom (InHaskToHask w)) (InHask k) d =>
InHaskToHask w -> d -> Obj (InHask k) (Lim (InHaskToHask w) d)
limitObj (InHaskToHask w
w) d
d = forall (k :: * -> * -> *) a b. k a b -> InHask k a b
InHask (forall (k :: * -> * -> *) w d.
(HasWLimits k w, FunctorOf (Dom w) k d) =>
w -> d -> Obj k (WLimit w d)
Hask.limitObj w
w (forall (c :: * -> * -> *) (d :: * -> * -> *) f.
f -> UnderlyingHask c d f
UnderlyingHask d
d))
  limit :: forall d e.
EFunctorOf (EDom (InHaskToHask w)) (InHask k) d =>
InHaskToHask w
-> d
-> Obj (InHask k) e
-> V (InHask k)
     (InHask k $ (e, Lim (InHaskToHask w) d))
     (End
        (V (InHask k)) (InHaskToHask w :->>: (EHomX_ (InHask k) e :.: d)))
limit    (InHaskToHask w
w) d
d Obj (InHask k) e
_ k e (WeightedLimit k w (UnderlyingHask (Dom w) k d))
el = forall t.
(forall (k :: * -> * -> *) a.
 VProfunctor k k t =>
 t -> Obj k a -> t :%% (a, a))
-> HaskEnd t
HaskEnd (\EHom (Self (->))
:.: (Opposite (InHaskToHask w) :<*>: (EHomX_ (InHask k) e :.: d))
_ (InHask Dom w a a
a) w :% a
wa -> forall (k :: * -> * -> *) w d.
(HasWLimits k w, FunctorOf (Dom w) k d) =>
w -> d -> WeightedCone w d (WLimit w d)
Hask.limit w
w (forall (c :: * -> * -> *) (d :: * -> * -> *) f.
f -> UnderlyingHask c d f
UnderlyingHask d
d) Dom w a a
a w :% a
wa forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k e (WeightedLimit k w (UnderlyingHask (Dom w) k d))
el)
  limitInv :: forall d e.
EFunctorOf (EDom (InHaskToHask w)) (InHask k) d =>
InHaskToHask w
-> d
-> Obj (InHask k) e
-> V (InHask k)
     (End
        (V (InHask k)) (InHaskToHask w :->>: (EHomX_ (InHask k) e :.: d)))
     (InHask k $ (e, Lim (InHaskToHask w) d))
limitInv (InHaskToHask w
w) d
d (InHask k e e
e) (HaskEnd forall (k :: * -> * -> *) a.
VProfunctor
  k
  k
  (EHom (Self (->))
   :.: (Opposite (InHaskToHask w)
        :<*>: (EHomX_ (InHask k) e :.: d))) =>
(EHom (Self (->))
 :.: (Opposite (InHaskToHask w) :<*>: (EHomX_ (InHask k) e :.: d)))
-> Obj k a
-> (EHom (Self (->))
    :.: (Opposite (InHaskToHask w) :<*>: (EHomX_ (InHask k) e :.: d)))
   :%% (a, a)
n) =
    forall (k :: * -> * -> *) w d e.
(HasWLimits k w, FunctorOf (Dom w) k d) =>
w -> d -> Obj k e -> WeightedCone w d e -> k e (WLimit w d)
Hask.limitFactorizer w
w (forall (c :: * -> * -> *) (d :: * -> * -> *) f.
f -> UnderlyingHask c d f
UnderlyingHask d
d) k e e
e (forall (k :: * -> * -> *) a.
VProfunctor
  k
  k
  (EHom (Self (->))
   :.: (Opposite (InHaskToHask w)
        :<*>: (EHomX_ (InHask k) e :.: d))) =>
(EHom (Self (->))
 :.: (Opposite (InHaskToHask w) :<*>: (EHomX_ (InHask k) e :.: d)))
-> Obj k a
-> (EHom (Self (->))
    :.: (Opposite (InHaskToHask w) :<*>: (EHomX_ (InHask k) e :.: d)))
   :%% (a, a)
n (forall f. f -> InHaskToHask f
InHaskToHask w
w forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> (forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ (forall (k :: * -> * -> *) a b. k a b -> InHask k a b
InHask k e e
e) forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: d
d)) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b. k a b -> InHask k a b
InHask)