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

Data.Category.Enriched

Description

Synopsis

class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where
- type V k :: * -> * -> *
- type k $ ab :: *
- 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 Elem k = TerminalObject (V k) :*-: V k
elem :: CartesianClosed (V k) => Elem k
type Arr k a b = Elem 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 (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * 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)
class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where
- type EDom ftag :: * -> * -> *
- type ECod ftag :: * -> * -> *
- type ftag :%% a :: *
- (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
- map :: EDom ftag ~ k => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)
data Id (k :: * -> * -> *) = Id
data g :.: h where
- (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h
data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
- Const :: Obj c2 x -> Const c1 c2 x
data Opposite f where
- Opposite :: EFunctor f => f -> Opposite f
data f1 :<*>: f2 = f1 :<*>: f2
data DiagProd (k :: * -> * -> *) = DiagProd
newtype UnderlyingF f = UnderlyingF f
data EHom (k :: * -> * -> *) = EHom
data ENat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
- ENat :: (EFunctorOf c d f, EFunctorOf c d g) => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g
data EHomX_ k x = EHomX_ (Obj k x)
data EHom_X k x = EHom_X (Obj (EOp k) x)
type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t
type family End (v :: * -> * -> *) t :: *
class CartesianClosed v => HasEnds v where
- 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)
}
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
data EndFunctor (k :: * -> * -> *) = EndFunctor
type family WeigtedLimit (k :: * -> * -> *) w d :: *
type Lim w d = WeigtedLimit (ECod d) w d
class HasEnds (V k) => HasLimits k where
- limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d)
- limit :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))
- limitInv :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))
type family WeigtedColimit (k :: * -> * -> *) w d :: *
type Colim w d = WeigtedColimit (ECod d) w d
class HasEnds (V k) => HasColimits k where
- colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d)
- colimit :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))
- colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))
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)
yonedaInv :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
data Y (k :: * -> * -> *) = Y
data One
data Two
data Three
data PosetTest a b where
- One :: PosetTest One One
- Two :: PosetTest Two Two
- Three :: PosetTest Three Three
type family Poset3 a b where ...

Documentation

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

An enriched category

Associated Types

type V k :: * -> * -> * #

The tensor product of the category V which k is enriched in

type k $ ab :: * #

The hom object in V from a to b

Methods

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

Instances

Instances details

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

type Elem k = TerminalObject (V k) :*-: V k #

The elements of k as a functor from V k to (->)

elem :: CartesianClosed (V k) => Elem k #

type Arr k a b = Elem k :% (k $ (a, b)) #

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 #

data Underlying k a b #

Constructors

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

Instances

Instances details

ECategory k => Category (Underlying k :: Type -> Type -> Type) #	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 # tgt :: forall (a :: k0) (b :: k0). Underlying k a b -> Obj (Underlying k) b # (.) :: forall (b :: k0) (c :: k0) (a :: k0). Underlying k b c -> Underlying k a b -> Underlying k a c #

newtype EOp k a b #

Constructors

EOp (k b a)

Instances

Instances details

ECategory k => ECategory (EOp k) #	The opposite of an enriched category
Instance details Defined in Data.Category.Enriched Associated Types type V (EOp k) :: Type -> Type -> Type # type (EOp k) $ ab # Methods hom :: Obj (EOp k) a -> Obj (EOp k) b -> Obj (V (EOp k)) (EOp k $ (a, b)) # id :: Obj (EOp k) a -> Arr (EOp k) a a # 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)) #
type V (EOp k) #
Instance details Defined in Data.Category.Enriched type V (EOp k) = V k
type (EOp k) $ (a, b) #
Instance details Defined in Data.Category.Enriched type (EOp k) $ (a, b) = k $ (b, a)

data (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where #

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) #	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 # type (k1 :<>: k2) $ ab # Methods hom :: Obj (k1 :<>: k2) a -> Obj (k1 :<>: k2) b -> Obj (V (k1 :<>: k2)) ((k1 :<>: k2) $ (a, b)) # id :: Obj (k1 :<>: k2) a -> Arr (k1 :<>: k2) a a # 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)) #
type V (k1 :<>: k2) #
Instance details Defined in Data.Category.Enriched type V (k1 :<>: k2) = V k1
type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) #
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 #

Constructors

Self
Fields getSelf :: v a b

Instances

Instances details

HasEnds v => HasLimits (Self v) #
Instance details Defined in Data.Category.Enriched Methods limitObj :: forall (j :: Type -> Type -> Type) d w. (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => w -> d -> Obj (Self v) (Lim w d) # limit :: forall (j :: Type -> Type -> Type) d w e. (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => 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 :: forall (j :: Type -> Type -> Type) d w e. (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => 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))) #
CartesianClosed v => ECategory (Self v) #	Self enrichment
Instance details Defined in Data.Category.Enriched Associated Types type V (Self v) :: Type -> Type -> Type # type (Self v) $ ab # Methods hom :: Obj (Self v) a -> Obj (Self v) b -> Obj (V (Self v)) (Self v $ (a, b)) # id :: Obj (Self v) a -> Arr (Self v) a a # 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)) #
type V (Self v) #
Instance details Defined in Data.Category.Enriched type V (Self v) = v
type WeigtedLimit (Self v) w d #
Instance details Defined in Data.Category.Enriched type WeigtedLimit (Self v) w d = End v (w :->>: d)
type (Self v) $ (a, b) #
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 #

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 #

Constructors

InHask (k a b)

Instances

Instances details

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

class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where #

Enriched functors.

Associated Types

type EDom ftag :: * -> * -> * #

The domain, or source category, of the functor.

type ECod ftag :: * -> * -> * #

The codomain, or target category, of the functor.

type ftag :%% a :: * #

:%% maps objects at the type level

Methods

(%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a) #

%% maps object at the value level

map :: EDom ftag ~ k => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b)) #

map maps arrows.

Instances

Instances details

(ECategory k, HasEnds (V k)) => EFunctor (Y k) #	Yoneda embedding
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Y k) :: Type -> Type -> Type # type ECod (Y k) :: Type -> Type -> Type # type (Y k) :%% a # Methods (%%) :: Y k -> Obj (EDom (Y k)) a -> Obj (ECod (Y k)) (Y k :%% a) # map :: EDom (Y k) ~ k0 => Y k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (Y k) $ (Y k :%% a, Y k :%% b)) #
(HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EndFunctor k) :: Type -> Type -> Type # type ECod (EndFunctor k) :: Type -> Type -> Type # type (EndFunctor k) :%% a # Methods (%%) :: EndFunctor k -> Obj (EDom (EndFunctor k)) a -> Obj (ECod (EndFunctor k)) (EndFunctor k :%% a) # 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)) #
ECategory k => EFunctor (EHom k) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EHom k) :: Type -> Type -> Type # type ECod (EHom k) :: Type -> Type -> Type # type (EHom k) :%% a # Methods (%%) :: EHom k -> Obj (EDom (EHom k)) a -> Obj (ECod (EHom k)) (EHom k :%% a) # map :: EDom (EHom k) ~ k0 => EHom k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (EHom k) $ (EHom k :%% a, EHom k :%% b)) #
ECategory k => EFunctor (DiagProd k) #	`DiagProd` is the diagonal functor for products.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (DiagProd k) :: Type -> Type -> Type # type ECod (DiagProd k) :: Type -> Type -> Type # type (DiagProd k) :%% a # Methods (%%) :: DiagProd k -> Obj (EDom (DiagProd k)) a -> Obj (ECod (DiagProd k)) (DiagProd k :%% a) # map :: EDom (DiagProd k) ~ k0 => DiagProd k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (DiagProd k) $ (DiagProd k :%% a, DiagProd k :%% b)) #
EFunctor f => EFunctor (Opposite f) #	The dual of a functor
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Opposite f) :: Type -> Type -> Type # type ECod (Opposite f) :: Type -> Type -> Type # type (Opposite f) :%% a # Methods (%%) :: Opposite f -> Obj (EDom (Opposite f)) a -> Obj (ECod (Opposite f)) (Opposite f :%% a) # map :: EDom (Opposite f) ~ k => Opposite f -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (Opposite f) $ (Opposite f :%% a, Opposite f :%% b)) #
ECategory k => EFunctor (Id k) #	The identity functor on k
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Id k) :: Type -> Type -> Type # type ECod (Id k) :: Type -> Type -> Type # type (Id k) :%% a # Methods (%%) :: Id k -> Obj (EDom (Id k)) a -> Obj (ECod (Id k)) (Id k :%% a) # map :: EDom (Id k) ~ k0 => Id k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (Id k) $ (Id k :%% a, Id k :%% b)) #
ECategory k => EFunctor (EHom_X k x) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EHom_X k x) :: Type -> Type -> Type # type ECod (EHom_X k x) :: Type -> Type -> Type # type (EHom_X k x) :%% a # Methods (%%) :: EHom_X k x -> Obj (EDom (EHom_X k x)) a -> Obj (ECod (EHom_X k x)) (EHom_X k x :%% a) # map :: EDom (EHom_X k x) ~ k0 => EHom_X k x -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (EHom_X k x) $ (EHom_X k x :%% a, EHom_X k x :%% b)) #
ECategory k => EFunctor (EHomX_ k x) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EHomX_ k x) :: Type -> Type -> Type # type ECod (EHomX_ k x) :: Type -> Type -> Type # type (EHomX_ k x) :%% a # Methods (%%) :: EHomX_ k x -> Obj (EDom (EHomX_ k x)) a -> Obj (ECod (EHomX_ k x)) (EHomX_ k x :%% a) # map :: EDom (EHomX_ k x) ~ k0 => EHomX_ k x -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (EHomX_ k x) $ (EHomX_ k x :%% a, EHomX_ k x :%% b)) #
(EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) #	`f1 :*: f2` is the product of the functors `f1` and `f2`.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (f1 :<>: f2) :: Type -> Type -> Type # type ECod (f1 :<>: f2) :: Type -> Type -> Type # type (f1 :<>: f2) :%% a # Methods (%%) :: (f1 :<>: f2) -> Obj (EDom (f1 :<>: f2)) a -> Obj (ECod (f1 :<>: f2)) ((f1 :<>: f2) :%% a) # map :: EDom (f1 :<>: f2) ~ k => (f1 :<>: f2) -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (f1 :<>: f2) $ ((f1 :<>: f2) :%% a, (f1 :<>: f2) :%% b)) #
(ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) #	The composition of two functors.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (g :.: h) :: Type -> Type -> Type # type ECod (g :.: h) :: Type -> Type -> Type # type (g :.: h) :%% a # Methods (%%) :: (g :.: h) -> Obj (EDom (g :.: h)) a -> Obj (ECod (g :.: h)) ((g :.: h) :%% a) # map :: EDom (g :.: h) ~ k => (g :.: h) -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (g :.: h) $ ((g :.: h) :%% a, (g :.: h) :%% b)) #
(ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) #	The constant functor.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Const c1 c2 x) :: Type -> Type -> Type # type ECod (Const c1 c2 x) :: Type -> Type -> Type # type (Const c1 c2 x) :%% a # Methods (%%) :: Const c1 c2 x -> Obj (EDom (Const c1 c2 x)) a -> Obj (ECod (Const c1 c2 x)) (Const c1 c2 x :%% a) # map :: EDom (Const c1 c2 x) ~ k => Const c1 c2 x -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (Const c1 c2 x) $ (Const c1 c2 x :%% a, Const c1 c2 x :%% b)) #

type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b) #

data Id (k :: * -> * -> *) #

Constructors

Id

Instances

Instances details

ECategory k => EFunctor (Id k) #	The identity functor on k
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Id k) :: Type -> Type -> Type # type ECod (Id k) :: Type -> Type -> Type # type (Id k) :%% a # Methods (%%) :: Id k -> Obj (EDom (Id k)) a -> Obj (ECod (Id k)) (Id k :%% a) # map :: EDom (Id k) ~ k0 => Id k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (Id k) $ (Id k :%% a, Id k :%% b)) #
type EDom (Id k) #
Instance details Defined in Data.Category.Enriched type EDom (Id k) = k
type ECod (Id k) #
Instance details Defined in Data.Category.Enriched type ECod (Id k) = k
type (Id k) :%% a #
Instance details Defined in Data.Category.Enriched type (Id k) :%% a = a

data g :.: h where #

Constructors

(:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h

Instances

Instances details

(ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) #	The composition of two functors.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (g :.: h) :: Type -> Type -> Type # type ECod (g :.: h) :: Type -> Type -> Type # type (g :.: h) :%% a # Methods (%%) :: (g :.: h) -> Obj (EDom (g :.: h)) a -> Obj (ECod (g :.: h)) ((g :.: h) :%% a) # map :: EDom (g :.: h) ~ k => (g :.: h) -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (g :.: h) $ ((g :.: h) :%% a, (g :.: h) :%% b)) #
type EDom (g :.: h) #
Instance details Defined in Data.Category.Enriched type EDom (g :.: h) = EDom h
type ECod (g :.: h) #
Instance details Defined in Data.Category.Enriched type ECod (g :.: h) = ECod g
type (g :.: h) :%% a #
Instance details Defined in Data.Category.Enriched type (g :.: h) :%% a = g :%% (h :%% a)

data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where #

Constructors

Const :: Obj c2 x -> Const c1 c2 x

Instances

Instances details

(ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) #	The constant functor.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Const c1 c2 x) :: Type -> Type -> Type # type ECod (Const c1 c2 x) :: Type -> Type -> Type # type (Const c1 c2 x) :%% a # Methods (%%) :: Const c1 c2 x -> Obj (EDom (Const c1 c2 x)) a -> Obj (ECod (Const c1 c2 x)) (Const c1 c2 x :%% a) # map :: EDom (Const c1 c2 x) ~ k => Const c1 c2 x -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (Const c1 c2 x) $ (Const c1 c2 x :%% a, Const c1 c2 x :%% b)) #
type EDom (Const c1 c2 x) #
Instance details Defined in Data.Category.Enriched type EDom (Const c1 c2 x) = c1
type ECod (Const c1 c2 x) #
Instance details Defined in Data.Category.Enriched type ECod (Const c1 c2 x) = c2
type (Const c1 c2 x) :%% a #
Instance details Defined in Data.Category.Enriched type (Const c1 c2 x) :%% a = x

data Opposite f where #

Constructors

Opposite :: EFunctor f => f -> Opposite f

Instances

Instances details

EFunctor f => EFunctor (Opposite f) #	The dual of a functor
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Opposite f) :: Type -> Type -> Type # type ECod (Opposite f) :: Type -> Type -> Type # type (Opposite f) :%% a # Methods (%%) :: Opposite f -> Obj (EDom (Opposite f)) a -> Obj (ECod (Opposite f)) (Opposite f :%% a) # map :: EDom (Opposite f) ~ k => Opposite f -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (Opposite f) $ (Opposite f :%% a, Opposite f :%% b)) #
type EDom (Opposite f) #
Instance details Defined in Data.Category.Enriched type EDom (Opposite f) = EOp (EDom f)
type ECod (Opposite f) #
Instance details Defined in Data.Category.Enriched type ECod (Opposite f) = EOp (ECod f)
type (Opposite f) :%% a #
Instance details Defined in Data.Category.Enriched type (Opposite f) :%% a = f :%% a

data f1 :<*>: f2 #

Constructors

f1 :<*>: f2

Instances

Instances details

(EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) #	`f1 :*: f2` is the product of the functors `f1` and `f2`.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (f1 :<>: f2) :: Type -> Type -> Type # type ECod (f1 :<>: f2) :: Type -> Type -> Type # type (f1 :<>: f2) :%% a # Methods (%%) :: (f1 :<>: f2) -> Obj (EDom (f1 :<>: f2)) a -> Obj (ECod (f1 :<>: f2)) ((f1 :<>: f2) :%% a) # map :: EDom (f1 :<>: f2) ~ k => (f1 :<>: f2) -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (f1 :<>: f2) $ ((f1 :<>: f2) :%% a, (f1 :<>: f2) :%% b)) #
type EDom (f1 :<*>: f2) #
Instance details Defined in Data.Category.Enriched type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2
type ECod (f1 :<*>: f2) #
Instance details Defined in Data.Category.Enriched type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2
type (f1 :<*>: f2) :%% (a1, a2) #
Instance details Defined in Data.Category.Enriched type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)

data DiagProd (k :: * -> * -> *) #

Constructors

DiagProd

Instances

Instances details

ECategory k => EFunctor (DiagProd k) #	`DiagProd` is the diagonal functor for products.
Instance details Defined in Data.Category.Enriched Associated Types type EDom (DiagProd k) :: Type -> Type -> Type # type ECod (DiagProd k) :: Type -> Type -> Type # type (DiagProd k) :%% a # Methods (%%) :: DiagProd k -> Obj (EDom (DiagProd k)) a -> Obj (ECod (DiagProd k)) (DiagProd k :%% a) # map :: EDom (DiagProd k) ~ k0 => DiagProd k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (DiagProd k) $ (DiagProd k :%% a, DiagProd k :%% b)) #
type EDom (DiagProd k) #
Instance details Defined in Data.Category.Enriched type EDom (DiagProd k) = k
type ECod (DiagProd k) #
Instance details Defined in Data.Category.Enriched type ECod (DiagProd k) = k :<>: k
type (DiagProd k) :%% a #
Instance details Defined in Data.Category.Enriched type (DiagProd k) :%% a = (a, a)

newtype UnderlyingF f #

Constructors

UnderlyingF f

Instances

Instances details

EFunctor f => Functor (UnderlyingF f) #	The underlying functor of an enriched functor `f`
Instance details Defined in Data.Category.Enriched Associated Types type Dom (UnderlyingF f) :: Type -> Type -> Type # type Cod (UnderlyingF f) :: Type -> Type -> Type # type (UnderlyingF f) :% a # Methods (%) :: UnderlyingF f -> Dom (UnderlyingF f) a b -> Cod (UnderlyingF f) (UnderlyingF f :% a) (UnderlyingF f :% b) #
type Dom (UnderlyingF f) #
Instance details Defined in Data.Category.Enriched type Dom (UnderlyingF f) = Underlying (EDom f)
type Cod (UnderlyingF f) #
Instance details Defined in Data.Category.Enriched type Cod (UnderlyingF f) = Underlying (ECod f)
type (UnderlyingF f) :% a #
Instance details Defined in Data.Category.Enriched type (UnderlyingF f) :% a = f :%% a

data EHom (k :: * -> * -> *) #

Constructors

EHom

Instances

Instances details

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

data ENat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where #

Enriched natural transformations.

Constructors

ENat :: (EFunctorOf c d f, EFunctorOf c d g) => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g

data EHomX_ k x #

The enriched functor k(x, -)

Constructors

EHomX_ (Obj k x)

Instances

Instances details

ECategory k => EFunctor (EHomX_ k x) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EHomX_ k x) :: Type -> Type -> Type # type ECod (EHomX_ k x) :: Type -> Type -> Type # type (EHomX_ k x) :%% a # Methods (%%) :: EHomX_ k x -> Obj (EDom (EHomX_ k x)) a -> Obj (ECod (EHomX_ k x)) (EHomX_ k x :%% a) # map :: EDom (EHomX_ k x) ~ k0 => EHomX_ k x -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (EHomX_ k x) $ (EHomX_ k x :%% a, EHomX_ k x :%% b)) #
type EDom (EHomX_ k x) #
Instance details Defined in Data.Category.Enriched type EDom (EHomX_ k x) = k
type ECod (EHomX_ k x) #
Instance details Defined in Data.Category.Enriched type ECod (EHomX_ k x) = Self (V k)
type (EHomX_ k x) :%% y #
Instance details Defined in Data.Category.Enriched type (EHomX_ k x) :%% y = k $ (x, y)

data EHom_X k x #

The enriched functor k(-, x)

Constructors

EHom_X (Obj (EOp k) x)

Instances

Instances details

ECategory k => EFunctor (EHom_X k x) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EHom_X k x) :: Type -> Type -> Type # type ECod (EHom_X k x) :: Type -> Type -> Type # type (EHom_X k x) :%% a # Methods (%%) :: EHom_X k x -> Obj (EDom (EHom_X k x)) a -> Obj (ECod (EHom_X k x)) (EHom_X k x :%% a) # map :: EDom (EHom_X k x) ~ k0 => EHom_X k x -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (EHom_X k x) $ (EHom_X k x :%% a, EHom_X k x :%% b)) #
type EDom (EHom_X k x) #
Instance details Defined in Data.Category.Enriched type EDom (EHom_X k x) = EOp k
type ECod (EHom_X k x) #
Instance details Defined in Data.Category.Enriched type ECod (EHom_X k x) = Self (V k)
type (EHom_X k x) :%% y #
Instance details Defined in Data.Category.Enriched type (EHom_X k x) :%% y = k $ (y, x)

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

type family End (v :: * -> * -> *) t :: * #

Instances

Instances details

type End ((->) :: Type -> Type -> Type) t #
Instance details Defined in Data.Category.Enriched type End ((->) :: Type -> Type -> Type) t = HaskEnd t

class CartesianClosed v => HasEnds v where #

Methods

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

Instances

Instances details

HasEnds ((->) :: Type -> Type -> Type) #
Instance details Defined in Data.Category.Enriched Methods end :: forall (k :: Type -> Type -> Type) t. (VProfunctor k k t, V k ~ (->)) => t -> Obj (->) (End (->) t) # endCounit :: (VProfunctor k k t, V k ~ (->)) => t -> Obj k a -> End (->) t -> (t :%% (a, a)) # endFactorizer :: (VProfunctor k k t, V k ~ (->)) => t -> (forall a. Obj k a -> x -> (t :%% (a, a))) -> x -> End (->) t #

newtype HaskEnd t #

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 #

Constructors

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

Instances

Instances details

(HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) #	The enriched functor category `[a, b]`
Instance details Defined in Data.Category.Enriched Associated Types type V (FunCat a b) :: Type -> Type -> Type # type (FunCat a b) $ ab # Methods hom :: Obj (FunCat a b) a0 -> Obj (FunCat a b) b0 -> Obj (V (FunCat a b)) (FunCat a b $ (a0, b0)) # id :: Obj (FunCat a b) a0 -> Arr (FunCat a b) a0 a0 # 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)) #
type V (FunCat a b) #
Instance details Defined in Data.Category.Enriched type V (FunCat a b) = V a
type (FunCat a b) $ (t, s) #
Instance details Defined in Data.Category.Enriched type (FunCat a b) $ (t, s) = End (V a) (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 #

data EndFunctor (k :: * -> * -> *) #

Constructors

EndFunctor

Instances

Instances details

(HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) #
Instance details Defined in Data.Category.Enriched Associated Types type EDom (EndFunctor k) :: Type -> Type -> Type # type ECod (EndFunctor k) :: Type -> Type -> Type # type (EndFunctor k) :%% a # Methods (%%) :: EndFunctor k -> Obj (EDom (EndFunctor k)) a -> Obj (ECod (EndFunctor k)) (EndFunctor k :%% a) # 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)) #
type EDom (EndFunctor k) #
Instance details Defined in Data.Category.Enriched type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))
type ECod (EndFunctor k) #
Instance details Defined in Data.Category.Enriched type ECod (EndFunctor k) = Self (V k)
type (EndFunctor k) :%% t #
Instance details Defined in Data.Category.Enriched type (EndFunctor k) :%% t = End (V k) t

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

Instances

Instances details

type WeigtedLimit (Self v) w d #
Instance details Defined in Data.Category.Enriched type WeigtedLimit (Self v) w d = End v (w :->>: d)

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

class HasEnds (V k) => HasLimits k where #

Methods

limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d) #

limit :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d)) #

limitInv :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d))) #

Instances

Instances details

HasEnds v => HasLimits (Self v) #

Instance details

Defined in Data.Category.Enriched

Methods

limitObj :: forall (j :: Type -> Type -> Type) d w. (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => w -> d -> Obj (Self v) (Lim w d) #

limit :: forall (j :: Type -> Type -> Type) d w e. (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => 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 :: forall (j :: Type -> Type -> Type) d w e. (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => 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))) #

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

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

class HasEnds (V k) => HasColimits k where #

Methods

colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d) #

colimit :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e)) #

colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) #

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

yonedaInv :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f)) #

data Y (k :: * -> * -> *) #

Constructors

Y

Instances

Instances details

(ECategory k, HasEnds (V k)) => EFunctor (Y k) #	Yoneda embedding
Instance details Defined in Data.Category.Enriched Associated Types type EDom (Y k) :: Type -> Type -> Type # type ECod (Y k) :: Type -> Type -> Type # type (Y k) :%% a # Methods (%%) :: Y k -> Obj (EDom (Y k)) a -> Obj (ECod (Y k)) (Y k :%% a) # map :: EDom (Y k) ~ k0 => Y k -> Obj k0 a -> Obj k0 b -> V k0 (k0 $ (a, b)) (ECod (Y k) $ (Y k :%% a, Y k :%% b)) #
type EDom (Y k) #
Instance details Defined in Data.Category.Enriched type EDom (Y k) = EOp k
type ECod (Y k) #
Instance details Defined in Data.Category.Enriched type ECod (Y k) = FunCat k (Self (V k))
type (Y k) :%% x #
Instance details Defined in Data.Category.Enriched type (Y k) :%% x = EHomX_ k x

data One #

data Two #

data Three #

data PosetTest a b where #

Constructors

One :: PosetTest One One
Two :: PosetTest Two Two
Three :: PosetTest Three Three

Instances

Instances details

ECategory PosetTest #
Instance details Defined in Data.Category.Enriched Associated Types type V PosetTest :: Type -> Type -> Type # type PosetTest $ ab # Methods hom :: Obj PosetTest a -> Obj PosetTest b -> Obj (V PosetTest) (PosetTest $ (a, b)) # id :: Obj PosetTest a -> Arr PosetTest a a # comp :: Obj PosetTest a -> Obj PosetTest b -> Obj PosetTest c -> V PosetTest (BinaryProduct (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b))) (PosetTest $ (a, c)) #
type V PosetTest #
Instance details Defined in Data.Category.Enriched type V PosetTest = Boolean
type PosetTest $ (a, b) #
Instance details Defined in Data.Category.Enriched type PosetTest $ (a, b) = Poset3 a b

type family Poset3 a b where ... #

Equations

Poset3 Two One = Fls
Poset3 Three One = Fls
Poset3 Three Two = Fls
Poset3 a b = Tru