License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category.Enriched.Limit

Description

Documentation

type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t Source #

class CartesianClosed v => HasEnds v where Source #

Associated Types

type End (v :: Type -> Type -> Type) t :: Type Source #

Methods

end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t) Source #

endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a)) Source #

endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t) Source #

Instances

Instances details

HasEnds (->) Source #

Instance details

Defined in Data.Category.Enriched.Limit

Associated Types

type End (->) t Source #

Methods

end :: forall (k :: Type -> Type -> Type) t. (VProfunctor k k t, V k ~ (->)) => t -> Obj (->) (End (->) t) Source #

endCounit :: (VProfunctor k k t, V k ~ (->)) => t -> Obj k a -> End (->) t -> (t :%% (a, a)) Source #

endFactorizer :: (VProfunctor k k t, V k ~ (->)) => t -> (forall a. Obj k a -> x -> (t :%% (a, a))) -> x -> End (->) t Source #

newtype HaskEnd t Source #

Constructors

HaskEnd
Fields getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a)

data FunCat a b t s where Source #

Constructors

FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s

Instances

Instances details

(HasEnds (V a), CartesianClosed (V a), V a ~ V b) => ECategory (FunCat a b) Source #	The enriched functor category `[a, b]`
Instance details Defined in Data.Category.Enriched.Limit Associated Types type V (FunCat a b) :: Type -> Type -> Type Source # type (FunCat a b) $ ab Source # Methods hom :: Obj (FunCat a b) a0 -> Obj (FunCat a b) b0 -> Obj (V (FunCat a b)) (FunCat a b $ (a0, b0)) Source # id :: Obj (FunCat a b) a0 -> Arr (FunCat a b) a0 a0 Source # comp :: Obj (FunCat a b) a0 -> Obj (FunCat a b) b0 -> Obj (FunCat a b) c -> V (FunCat a b) (BinaryProduct (V (FunCat a b)) (FunCat a b $ (b0, c)) (FunCat a b $ (a0, b0))) (FunCat a b $ (a0, c)) Source #
type V (FunCat a b) Source #
Instance details Defined in Data.Category.Enriched.Limit type V (FunCat a b) = V a
type (FunCat a b) $ (t, s) Source #
Instance details Defined in Data.Category.Enriched.Limit type (FunCat a b) $ (t, s) = End (V a) (t :->>: s)

type (:->>:) t s = EHom (ECod t) :.: (Opposite t :<*>: s) Source #

(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s Source #

data EndFunctor (k :: Type -> Type -> Type) Source #

Constructors

EndFunctor

Instances

Instances details

(HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) Source #
Instance details Defined in Data.Category.Enriched.Limit Associated Types type EDom (EndFunctor k) :: Type -> Type -> Type Source # type ECod (EndFunctor k) :: Type -> Type -> Type Source # type (EndFunctor k) :%% a Source # Methods (%%) :: EndFunctor k -> Obj (EDom (EndFunctor k)) a -> Obj (ECod (EndFunctor k)) (EndFunctor k :%% a) Source # map :: EDom (EndFunctor k) ~ k0 => EndFunctor k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (EndFunctor k) $ (EndFunctor k :%% a, EndFunctor k :%% b)) Source #
type ECod (EndFunctor k) Source #
Instance details Defined in Data.Category.Enriched.Limit type ECod (EndFunctor k) = Self (V k)
type EDom (EndFunctor k) Source #
Instance details Defined in Data.Category.Enriched.Limit type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))
type (EndFunctor k) :%% t Source #
Instance details Defined in Data.Category.Enriched.Limit type (EndFunctor k) :%% t = End (V k) t

type family WeigtedLimit (k :: Type -> Type -> Type) w d :: Type Source #

Instances

Instances details

type WeigtedLimit (Self v) w d Source #
Instance details Defined in Data.Category.Enriched.Limit type WeigtedLimit (Self v) w d = End v (w :->>: d)
type WeigtedLimit (InHask k) (InHaskToHask w) d Source #
Instance details Defined in Data.Category.Enriched.Limit type WeigtedLimit (InHask k) (InHaskToHask w) d = WeightedLimit k w (UnderlyingHask (Dom w) k d)

type Lim w d = WeigtedLimit (ECod d) w d Source #

class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasLimits k w where Source #

Methods

limitObj :: EFunctorOf (EDom w) k d => w -> d -> Obj k (Lim w d) Source #

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))) Source #

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)) Source #

Instances

Instances details

(HasEnds v, EFunctor w, ECod w ~ Self v) => HasLimits (Self v) w Source #
Instance details Defined in Data.Category.Enriched.Limit Methods limitObj :: EFunctorOf (EDom w) (Self v) d => w -> d -> Obj (Self v) (Lim w d) Source # limit :: 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))) Source # limitInv :: 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)) Source #
HasWLimits k w => HasLimits (InHask k) (InHaskToHask w) Source #
Instance details Defined in Data.Category.Enriched.Limit Methods limitObj :: EFunctorOf (EDom (InHaskToHask w)) (InHask k) d => InHaskToHask w -> d -> Obj (InHask k) (Lim (InHaskToHask w) d) Source # limit :: 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))) Source # limitInv :: 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)) Source #

type family WeigtedColimit (k :: Type -> Type -> Type) w d :: Type Source #

type Colim w d = WeigtedColimit (ECod d) w d Source #

class (HasEnds (V k), EFunctor w, ECod w ~ Self (V k)) => HasColimits k w where Source #

Methods

colimitObj :: (EFunctorOf j k d, EOp j ~ EDom w) => w -> d -> Obj k (Colim w d) Source #

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))) Source #

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)) Source #