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

Description

Synopsis

class CartesianClosed (V k) => ECategory (k :: Type -> Type -> Type) where
- type V k :: Type -> Type -> Type
- type k $ ab :: Type
- hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
- id :: Obj k a -> Arr k a a
- comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
type Arr k a b = V k (TerminalObject (V k)) (k $ (a, b))
compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
data Underlying k a b = Underlying (Obj k a) (Arr k a b) (Obj k b)
newtype EOp k a b = EOp (k b a)
data (:<>:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
- (:<>:) :: V k1 ~ V k2 => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
newtype Self v a b = Self {
- getSelf :: v a b
}
toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b
fromSelf :: forall v a b. CartesianClosed v => Obj v a -> Obj v b -> Arr (Self v) a b -> v a b
newtype InHask k a b = InHask (k a b)

Documentation

class CartesianClosed (V k) => ECategory (k :: Type -> Type -> Type) where Source #

An enriched category

Associated Types

type V k :: Type -> Type -> Type Source #

The category V which k is enriched in

type k $ ab :: Type Source #

The hom object in V from a to b

Methods

hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b)) Source #

id :: Obj k a -> Arr k a a Source #

comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c)) Source #

Instances

Instances details

ECategory PosetTest Source #
Instance details Defined in Data.Category.Enriched.Poset3 Associated Types type V PosetTest :: Type -> Type -> Type Source # type PosetTest $ ab Source # Methods hom :: Obj PosetTest a -> Obj PosetTest b -> Obj (V PosetTest) (PosetTest $ (a, b)) Source # id :: Obj PosetTest a -> Arr PosetTest a a Source # comp :: Obj PosetTest a -> Obj PosetTest b -> Obj PosetTest c -> V PosetTest (BinaryProduct (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b))) (PosetTest $ (a, c)) Source #
ECategory k => ECategory (EOp k) Source #	The opposite of an enriched category
Instance details Defined in Data.Category.Enriched Associated Types type V (EOp k) :: Type -> Type -> Type Source # type (EOp k) $ ab Source # Methods hom :: Obj (EOp k) a -> Obj (EOp k) b -> Obj (V (EOp k)) (EOp k $ (a, b)) Source # id :: Obj (EOp k) a -> Arr (EOp k) a a Source # comp :: Obj (EOp k) a -> Obj (EOp k) b -> Obj (EOp k) c -> V (EOp k) (BinaryProduct (V (EOp k)) (EOp k $ (b, c)) (EOp k $ (a, b))) (EOp k $ (a, c)) Source #
Category k => ECategory (InHask k) Source #	Any regular category is enriched in (->), aka Hask
Instance details Defined in Data.Category.Enriched Associated Types type V (InHask k) :: Type -> Type -> Type Source # type (InHask k) $ ab Source # Methods hom :: Obj (InHask k) a -> Obj (InHask k) b -> Obj (V (InHask k)) (InHask k $ (a, b)) Source # id :: Obj (InHask k) a -> Arr (InHask k) a a Source # comp :: Obj (InHask k) a -> Obj (InHask k) b -> Obj (InHask k) c -> V (InHask k) (BinaryProduct (V (InHask k)) (InHask k $ (b, c)) (InHask k $ (a, b))) (InHask k $ (a, c)) Source #
CartesianClosed v => ECategory (Self v) Source #	Self enrichment
Instance details Defined in Data.Category.Enriched Associated Types type V (Self v) :: Type -> Type -> Type Source # type (Self v) $ ab Source # Methods hom :: Obj (Self v) a -> Obj (Self v) b -> Obj (V (Self v)) (Self v $ (a, b)) Source # id :: Obj (Self v) a -> Arr (Self v) a a Source # comp :: Obj (Self v) a -> Obj (Self v) b -> Obj (Self v) c -> V (Self v) (BinaryProduct (V (Self v)) (Self v $ (b, c)) (Self v $ (a, b))) (Self v $ (a, c)) Source #
(ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) Source #	The enriched product category of enriched categories `c1` and `c2`.
Instance details Defined in Data.Category.Enriched Associated Types type V (k1 :<>: k2) :: Type -> Type -> Type Source # type (k1 :<>: k2) $ ab Source # Methods hom :: Obj (k1 :<>: k2) a -> Obj (k1 :<>: k2) b -> Obj (V (k1 :<>: k2)) ((k1 :<>: k2) $ (a, b)) Source # id :: Obj (k1 :<>: k2) a -> Arr (k1 :<>: k2) a a Source # comp :: Obj (k1 :<>: k2) a -> Obj (k1 :<>: k2) b -> Obj (k1 :<>: k2) c -> V (k1 :<>: k2) (BinaryProduct (V (k1 :<>: k2)) ((k1 :<>: k2) $ (b, c)) ((k1 :<>: k2) $ (a, b))) ((k1 :<>: k2) $ (a, c)) Source #
(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 Arr k a b = V k (TerminalObject (V k)) (k $ (a, b)) Source #

Arrows as elements of k

compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c Source #

data Underlying k a b Source #

Constructors

Underlying (Obj k a) (Arr k a b) (Obj k b)

Instances

Instances details

ECategory k => Category (Underlying k :: Type -> Type -> Type) Source #	The underlying category of an enriched category
Instance details Defined in Data.Category.Enriched Methods src :: forall (a :: k0) (b :: k0). Underlying k a b -> Obj (Underlying k) a Source # tgt :: forall (a :: k0) (b :: k0). Underlying k a b -> Obj (Underlying k) b Source # (.) :: forall (b :: k0) (c :: k0) (a :: k0). Underlying k b c -> Underlying k a b -> Underlying k a c Source #

newtype EOp k a b Source #

Constructors

EOp (k b a)

Instances

Instances details

ECategory k => ECategory (EOp k) Source #	The opposite of an enriched category
Instance details Defined in Data.Category.Enriched Associated Types type V (EOp k) :: Type -> Type -> Type Source # type (EOp k) $ ab Source # Methods hom :: Obj (EOp k) a -> Obj (EOp k) b -> Obj (V (EOp k)) (EOp k $ (a, b)) Source # id :: Obj (EOp k) a -> Arr (EOp k) a a Source # comp :: Obj (EOp k) a -> Obj (EOp k) b -> Obj (EOp k) c -> V (EOp k) (BinaryProduct (V (EOp k)) (EOp k $ (b, c)) (EOp k $ (a, b))) (EOp k $ (a, c)) Source #
type V (EOp k) Source #
Instance details Defined in Data.Category.Enriched type V (EOp k) = V k
type (EOp k) $ (a, b) Source #
Instance details Defined in Data.Category.Enriched type (EOp k) $ (a, b) = k $ (b, a)

data (:<>:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where Source #

Constructors

(:<>:) :: V k1 ~ V k2 => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)

Instances

Instances details

(ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) Source #	The enriched product category of enriched categories `c1` and `c2`.
Instance details Defined in Data.Category.Enriched Associated Types type V (k1 :<>: k2) :: Type -> Type -> Type Source # type (k1 :<>: k2) $ ab Source # Methods hom :: Obj (k1 :<>: k2) a -> Obj (k1 :<>: k2) b -> Obj (V (k1 :<>: k2)) ((k1 :<>: k2) $ (a, b)) Source # id :: Obj (k1 :<>: k2) a -> Arr (k1 :<>: k2) a a Source # comp :: Obj (k1 :<>: k2) a -> Obj (k1 :<>: k2) b -> Obj (k1 :<>: k2) c -> V (k1 :<>: k2) (BinaryProduct (V (k1 :<>: k2)) ((k1 :<>: k2) $ (b, c)) ((k1 :<>: k2) $ (a, b))) ((k1 :<>: k2) $ (a, c)) Source #
type V (k1 :<>: k2) Source #
Instance details Defined in Data.Category.Enriched type V (k1 :<>: k2) = V k1
type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) Source #
Instance details Defined in Data.Category.Enriched type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) = BinaryProduct (V k1) (k1 $ (a1, b1)) (k2 $ (a2, b2))

newtype Self v a b Source #

Constructors

Self
Fields getSelf :: v a b

Instances

Instances details

CartesianClosed v => ECategory (Self v) Source #	Self enrichment
Instance details Defined in Data.Category.Enriched Associated Types type V (Self v) :: Type -> Type -> Type Source # type (Self v) $ ab Source # Methods hom :: Obj (Self v) a -> Obj (Self v) b -> Obj (V (Self v)) (Self v $ (a, b)) Source # id :: Obj (Self v) a -> Arr (Self v) a a Source # comp :: Obj (Self v) a -> Obj (Self v) b -> Obj (Self v) c -> V (Self v) (BinaryProduct (V (Self v)) (Self v $ (b, c)) (Self v $ (a, b))) (Self v $ (a, c)) Source #
(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 #
type V (Self v) Source #
Instance details Defined in Data.Category.Enriched type V (Self v) = v
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 (Self v) $ (a, b) Source #
Instance details Defined in Data.Category.Enriched type (Self v) $ (a, b) = Exponential v a b

toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b Source #

fromSelf :: forall v a b. CartesianClosed v => Obj v a -> Obj v b -> Arr (Self v) a b -> v a b Source #

newtype InHask k a b Source #

Constructors

InHask (k a b)

Instances

Instances details

Category k => ECategory (InHask k) Source #	Any regular category is enriched in (->), aka Hask
Instance details Defined in Data.Category.Enriched Associated Types type V (InHask k) :: Type -> Type -> Type Source # type (InHask k) $ ab Source # Methods hom :: Obj (InHask k) a -> Obj (InHask k) b -> Obj (V (InHask k)) (InHask k $ (a, b)) Source # id :: Obj (InHask k) a -> Arr (InHask k) a a Source # comp :: Obj (InHask k) a -> Obj (InHask k) b -> Obj (InHask k) c -> V (InHask k) (BinaryProduct (V (InHask k)) (InHask k $ (b, c)) (InHask k $ (a, b))) (InHask k $ (a, c)) 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 V (InHask k) Source #
Instance details Defined in Data.Category.Enriched type V (InHask k) = (->)
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 (InHask k) $ (a, b) Source #
Instance details Defined in Data.Category.Enriched type (InHask k) $ (a, b) = k a b