data-category-0.7.1: Category theory

Data.Category.Enriched

Description

Synopsis

# Documentation

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

An enriched category

Associated Types

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

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

type k $ab :: * 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  Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype V PosetTest :: Type -> Type -> Type Source #type PosetTest$ ab :: Type Source # Methodshom :: 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 # Category k => ECategory (InHask k) Source # Any regular category is enriched in (->), aka Hask Instance detailsDefined in Data.Category.Enriched Associated Typestype V (InHask k) :: Type -> Type -> Type Source #type (InHask k) $ab :: Type Source # Methodshom :: 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 detailsDefined in Data.Category.Enriched Associated Typestype V (Self v) :: Type -> Type -> Type Source #type (Self v)$ ab :: Type Source # Methodshom :: 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 k => ECategory (EOp k) Source # The opposite of an enriched category Instance detailsDefined in Data.Category.Enriched Associated Typestype V (EOp k) :: Type -> Type -> Type Source #type (EOp k) $ab :: Type Source # Methodshom :: 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 # (HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) Source # The enriched functor category [a, b] Instance detailsDefined in Data.Category.Enriched Associated Typestype V (FunCat a b) :: Type -> Type -> Type Source #type (FunCat a b)$ ab :: Type Source # Methodshom :: 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 # (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) Source # The enriched product category of enriched categories c1 and c2. Instance detailsDefined in Data.Category.Enriched Associated Typestype V (k1 :<>: k2) :: Type -> Type -> Type Source #type (k1 :<>: k2) $ab :: Type Source # Methodshom :: 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 Elem k = TerminalObject (V k) :*-: V k Source # The elements of k as a functor from V k to (->) type Arr k a b = Elem 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
 ECategory k => Category (Underlying k) Source # The underlying category of an enriched category Instance detailsDefined in Data.Category.Enriched Methodssrc :: Underlying k a b -> Obj (Underlying k) a Source #tgt :: Underlying k a b -> Obj (Underlying k) b Source #(.) :: 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
 ECategory k => ECategory (EOp k) Source # The opposite of an enriched category Instance detailsDefined in Data.Category.Enriched Associated Typestype V (EOp k) :: Type -> Type -> Type Source #type (EOp k) $ab :: Type Source # Methodshom :: 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 detailsDefined in Data.Category.Enriched type V (EOp k) = V k type (EOp k)$ (a, b) Source # Instance detailsDefined in Data.Category.Enriched type (EOp k) $(a, b) = k$ (b, a)

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

Constructors

 (:<>:) :: V k1 ~ V k2 => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
Instances
 (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) Source # The enriched product category of enriched categories c1 and c2. Instance detailsDefined in Data.Category.Enriched Associated Typestype V (k1 :<>: k2) :: Type -> Type -> Type Source #type (k1 :<>: k2) $ab :: Type Source # Methodshom :: 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 detailsDefined in Data.Category.Enriched type V (k1 :<>: k2) = V k1 type (k1 :<>: k2)$ ((a1, a2), (b1, b2)) Source # Instance detailsDefined 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 FieldsgetSelf :: v a b Instances  HasEnds v => HasLimits (Self v) Source # Instance detailsDefined in Data.Category.Enriched MethodslimitObj :: (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => w -> d -> Obj (Self v) (Lim w d) Source #limit :: (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)) Source #limitInv :: (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))) Source # CartesianClosed v => ECategory (Self v) Source # Self enrichment Instance detailsDefined in Data.Category.Enriched Associated Typestype V (Self v) :: Type -> Type -> Type Source #type (Self v)$ ab :: Type Source # Methodshom :: 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 # type V (Self v) Source # Instance detailsDefined in Data.Category.Enriched type V (Self v) = v type WeigtedLimit (Self v) w d Source # Instance detailsDefined in Data.Category.Enriched type WeigtedLimit (Self v) w d = End v (w :->>: d) type (Self v) $(a, b) Source # Instance detailsDefined 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

Instances
 Category k => ECategory (InHask k) Source # Any regular category is enriched in (->), aka Hask Instance detailsDefined in Data.Category.Enriched Associated Typestype V (InHask k) :: Type -> Type -> Type Source #type (InHask k) $ab :: Type Source # Methodshom :: 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 # type V (InHask k) Source # Instance detailsDefined in Data.Category.Enriched type V (InHask k) = ((->) :: Type -> Type -> Type) type (InHask k)$ (a, b) Source # Instance detailsDefined 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 Source # Enriched functors. Associated Types type EDom ftag :: * -> * -> * Source # The domain, or source category, of the functor. type ECod ftag :: * -> * -> * Source # The codomain, or target category, of the functor. type ftag :%% a :: * Source # :%% maps objects at the type level Methods (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a) Source # %% 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)) Source # map maps arrows. Instances  (ECategory k, HasEnds (V k)) => EFunctor (Y k) Source # Yoneda embedding Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Y k) :: Type -> Type -> Type Source #type ECod (Y k) :: Type -> Type -> Type Source #type (Y k) :%% a :: Type Source # Methods(%%) :: Y k -> Obj (EDom (Y k)) a -> Obj (ECod (Y k)) (Y k :%% a) Source #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)) Source # (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EndFunctor k) :: Type -> Type -> Type Source #type ECod (EndFunctor k) :: Type -> Type -> Type Source #type (EndFunctor k) :%% a :: Type 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 # ECategory k => EFunctor (EHom k) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EHom k) :: Type -> Type -> Type Source #type ECod (EHom k) :: Type -> Type -> Type Source #type (EHom k) :%% a :: Type Source # Methods(%%) :: EHom k -> Obj (EDom (EHom k)) a -> Obj (ECod (EHom k)) (EHom k :%% a) Source #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)) Source # ECategory k => EFunctor (DiagProd k) Source # DiagProd is the diagonal functor for products. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (DiagProd k) :: Type -> Type -> Type Source #type ECod (DiagProd k) :: Type -> Type -> Type Source #type (DiagProd k) :%% a :: Type Source # Methods(%%) :: DiagProd k -> Obj (EDom (DiagProd k)) a -> Obj (ECod (DiagProd k)) (DiagProd k :%% a) Source #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)) Source # EFunctor f => EFunctor (Opposite f) Source # The dual of a functor Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Opposite f) :: Type -> Type -> Type Source #type ECod (Opposite f) :: Type -> Type -> Type Source #type (Opposite f) :%% a :: Type Source # Methods(%%) :: Opposite f -> Obj (EDom (Opposite f)) a -> Obj (ECod (Opposite f)) (Opposite f :%% a) Source #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)) Source # ECategory k => EFunctor (Id k) Source # The identity functor on k Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Id k) :: Type -> Type -> Type Source #type ECod (Id k) :: Type -> Type -> Type Source #type (Id k) :%% a :: Type Source # Methods(%%) :: Id k -> Obj (EDom (Id k)) a -> Obj (ECod (Id k)) (Id k :%% a) Source #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)) Source # ECategory k => EFunctor (EHom_X k x) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EHom_X k x) :: Type -> Type -> Type Source #type ECod (EHom_X k x) :: Type -> Type -> Type Source #type (EHom_X k x) :%% a :: Type Source # Methods(%%) :: EHom_X k x -> Obj (EDom (EHom_X k x)) a -> Obj (ECod (EHom_X k x)) (EHom_X k x :%% a) Source #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)) Source # ECategory k => EFunctor (EHomX_ k x) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EHomX_ k x) :: Type -> Type -> Type Source #type ECod (EHomX_ k x) :: Type -> Type -> Type Source #type (EHomX_ k x) :%% a :: Type Source # Methods(%%) :: EHomX_ k x -> Obj (EDom (EHomX_ k x)) a -> Obj (ECod (EHomX_ k x)) (EHomX_ k x :%% a) Source #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)) Source # (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) Source # f1 :*: f2 is the product of the functors f1 and f2. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (f1 :<*>: f2) :: Type -> Type -> Type Source #type ECod (f1 :<*>: f2) :: Type -> Type -> Type Source #type (f1 :<*>: f2) :%% a :: Type Source # Methods(%%) :: (f1 :<*>: f2) -> Obj (EDom (f1 :<*>: f2)) a -> Obj (ECod (f1 :<*>: f2)) ((f1 :<*>: f2) :%% a) Source #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)) Source # (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) Source # The composition of two functors. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (g :.: h) :: Type -> Type -> Type Source #type ECod (g :.: h) :: Type -> Type -> Type Source #type (g :.: h) :%% a :: Type Source # Methods(%%) :: (g :.: h) -> Obj (EDom (g :.: h)) a -> Obj (ECod (g :.: h)) ((g :.: h) :%% a) Source #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)) Source # (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) Source # The constant functor. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Const c1 c2 x) :: Type -> Type -> Type Source #type ECod (Const c1 c2 x) :: Type -> Type -> Type Source #type (Const c1 c2 x) :%% a :: Type Source # Methods(%%) :: Const c1 c2 x -> Obj (EDom (Const c1 c2 x)) a -> Obj (ECod (Const c1 c2 x)) (Const c1 c2 x :%% a) Source #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)) Source # type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b) Source # data Id (k :: * -> * -> *) Source # Constructors  Id Instances  ECategory k => EFunctor (Id k) Source # The identity functor on k Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Id k) :: Type -> Type -> Type Source #type ECod (Id k) :: Type -> Type -> Type Source #type (Id k) :%% a :: Type Source # Methods(%%) :: Id k -> Obj (EDom (Id k)) a -> Obj (ECod (Id k)) (Id k :%% a) Source #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)) Source # type EDom (Id k) Source # Instance detailsDefined in Data.Category.Enriched type EDom (Id k) = k type ECod (Id k) Source # Instance detailsDefined in Data.Category.Enriched type ECod (Id k) = k type (Id k) :%% a Source # Instance detailsDefined in Data.Category.Enriched type (Id k) :%% a = a data g :.: h where Source # Constructors  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h Instances  (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) Source # The composition of two functors. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (g :.: h) :: Type -> Type -> Type Source #type ECod (g :.: h) :: Type -> Type -> Type Source #type (g :.: h) :%% a :: Type Source # Methods(%%) :: (g :.: h) -> Obj (EDom (g :.: h)) a -> Obj (ECod (g :.: h)) ((g :.: h) :%% a) Source #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)) Source # type EDom (g :.: h) Source # Instance detailsDefined in Data.Category.Enriched type EDom (g :.: h) = EDom h type ECod (g :.: h) Source # Instance detailsDefined in Data.Category.Enriched type ECod (g :.: h) = ECod g type (g :.: h) :%% a Source # Instance detailsDefined in Data.Category.Enriched type (g :.: h) :%% a = g :%% (h :%% a) data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where Source # Constructors  Const :: Obj c2 x -> Const c1 c2 x Instances  (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) Source # The constant functor. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Const c1 c2 x) :: Type -> Type -> Type Source #type ECod (Const c1 c2 x) :: Type -> Type -> Type Source #type (Const c1 c2 x) :%% a :: Type Source # Methods(%%) :: Const c1 c2 x -> Obj (EDom (Const c1 c2 x)) a -> Obj (ECod (Const c1 c2 x)) (Const c1 c2 x :%% a) Source #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)) Source # type EDom (Const c1 c2 x) Source # Instance detailsDefined in Data.Category.Enriched type EDom (Const c1 c2 x) = c1 type ECod (Const c1 c2 x) Source # Instance detailsDefined in Data.Category.Enriched type ECod (Const c1 c2 x) = c2 type (Const c1 c2 x) :%% a Source # Instance detailsDefined in Data.Category.Enriched type (Const c1 c2 x) :%% a = x data Opposite f where Source # Constructors  Opposite :: EFunctor f => f -> Opposite f Instances  EFunctor f => EFunctor (Opposite f) Source # The dual of a functor Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Opposite f) :: Type -> Type -> Type Source #type ECod (Opposite f) :: Type -> Type -> Type Source #type (Opposite f) :%% a :: Type Source # Methods(%%) :: Opposite f -> Obj (EDom (Opposite f)) a -> Obj (ECod (Opposite f)) (Opposite f :%% a) Source #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)) Source # type EDom (Opposite f) Source # Instance detailsDefined in Data.Category.Enriched type EDom (Opposite f) = EOp (EDom f) type ECod (Opposite f) Source # Instance detailsDefined in Data.Category.Enriched type ECod (Opposite f) = EOp (ECod f) type (Opposite f) :%% a Source # Instance detailsDefined in Data.Category.Enriched type (Opposite f) :%% a = f :%% a data f1 :<*>: f2 Source # Constructors  f1 :<*>: f2 Instances  (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) Source # f1 :*: f2 is the product of the functors f1 and f2. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (f1 :<*>: f2) :: Type -> Type -> Type Source #type ECod (f1 :<*>: f2) :: Type -> Type -> Type Source #type (f1 :<*>: f2) :%% a :: Type Source # Methods(%%) :: (f1 :<*>: f2) -> Obj (EDom (f1 :<*>: f2)) a -> Obj (ECod (f1 :<*>: f2)) ((f1 :<*>: f2) :%% a) Source #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)) Source # type EDom (f1 :<*>: f2) Source # Instance detailsDefined in Data.Category.Enriched type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2 type ECod (f1 :<*>: f2) Source # Instance detailsDefined in Data.Category.Enriched type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2 type (f1 :<*>: f2) :%% (a1, a2) Source # Instance detailsDefined in Data.Category.Enriched type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2) data DiagProd (k :: * -> * -> *) Source # Constructors  DiagProd Instances  ECategory k => EFunctor (DiagProd k) Source # DiagProd is the diagonal functor for products. Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (DiagProd k) :: Type -> Type -> Type Source #type ECod (DiagProd k) :: Type -> Type -> Type Source #type (DiagProd k) :%% a :: Type Source # Methods(%%) :: DiagProd k -> Obj (EDom (DiagProd k)) a -> Obj (ECod (DiagProd k)) (DiagProd k :%% a) Source #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)) Source # type EDom (DiagProd k) Source # Instance detailsDefined in Data.Category.Enriched type EDom (DiagProd k) = k type ECod (DiagProd k) Source # Instance detailsDefined in Data.Category.Enriched type ECod (DiagProd k) = k :<>: k type (DiagProd k) :%% a Source # Instance detailsDefined in Data.Category.Enriched type (DiagProd k) :%% a = (a, a) newtype UnderlyingF f Source # Constructors  UnderlyingF f Instances  EFunctor f => Functor (UnderlyingF f) Source # The underlying functor of an enriched functor f Instance detailsDefined in Data.Category.Enriched Associated Typestype Dom (UnderlyingF f) :: Type -> Type -> Type Source #type Cod (UnderlyingF f) :: Type -> Type -> Type Source #type (UnderlyingF f) :% a :: Type Source # Methods(%) :: UnderlyingF f -> Dom (UnderlyingF f) a b -> Cod (UnderlyingF f) (UnderlyingF f :% a) (UnderlyingF f :% b) Source # type Dom (UnderlyingF f) Source # Instance detailsDefined in Data.Category.Enriched type Dom (UnderlyingF f) = Underlying (EDom f) type Cod (UnderlyingF f) Source # Instance detailsDefined in Data.Category.Enriched type Cod (UnderlyingF f) = Underlying (ECod f) type (UnderlyingF f) :% a Source # Instance detailsDefined in Data.Category.Enriched type (UnderlyingF f) :% a = f :%% a data EHom (k :: * -> * -> *) Source # Constructors  EHom Instances  ECategory k => EFunctor (EHom k) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EHom k) :: Type -> Type -> Type Source #type ECod (EHom k) :: Type -> Type -> Type Source #type (EHom k) :%% a :: Type Source # Methods(%%) :: EHom k -> Obj (EDom (EHom k)) a -> Obj (ECod (EHom k)) (EHom k :%% a) Source #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)) Source # type EDom (EHom k) Source # Instance detailsDefined in Data.Category.Enriched type EDom (EHom k) = EOp k :<>: k type ECod (EHom k) Source # Instance detailsDefined in Data.Category.Enriched type ECod (EHom k) = Self (V k) type (EHom k) :%% (a, b) Source # Instance detailsDefined in Data.Category.Enriched type (EHom k) :%% (a, b) = k$ (a, b)

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

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

The enriched functor k(x, -)

Constructors

 EHomX_ (Obj k x)
Instances
 ECategory k => EFunctor (EHomX_ k x) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EHomX_ k x) :: Type -> Type -> Type Source #type ECod (EHomX_ k x) :: Type -> Type -> Type Source #type (EHomX_ k x) :%% a :: Type Source # Methods(%%) :: EHomX_ k x -> Obj (EDom (EHomX_ k x)) a -> Obj (ECod (EHomX_ k x)) (EHomX_ k x :%% a) Source #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)) Source # type EDom (EHomX_ k x) Source # Instance detailsDefined in Data.Category.Enriched type EDom (EHomX_ k x) = k type ECod (EHomX_ k x) Source # Instance detailsDefined in Data.Category.Enriched type ECod (EHomX_ k x) = Self (V k) type (EHomX_ k x) :%% y Source # Instance detailsDefined in Data.Category.Enriched type (EHomX_ k x) :%% y = k $(x, y) data EHom_X k x Source # The enriched functor k(-, x) Constructors  EHom_X (Obj (EOp k) x) Instances  ECategory k => EFunctor (EHom_X k x) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EHom_X k x) :: Type -> Type -> Type Source #type ECod (EHom_X k x) :: Type -> Type -> Type Source #type (EHom_X k x) :%% a :: Type Source # Methods(%%) :: EHom_X k x -> Obj (EDom (EHom_X k x)) a -> Obj (ECod (EHom_X k x)) (EHom_X k x :%% a) Source #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)) Source # type EDom (EHom_X k x) Source # Instance detailsDefined in Data.Category.Enriched type EDom (EHom_X k x) = EOp k type ECod (EHom_X k x) Source # Instance detailsDefined in Data.Category.Enriched type ECod (EHom_X k x) = Self (V k) type (EHom_X k x) :%% y Source # Instance detailsDefined 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 Source #

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

Instances
 type End ((->) :: Type -> Type -> Type) t Source # Instance detailsDefined in Data.Category.Enriched type End ((->) :: Type -> Type -> Type) t = HaskEnd t

class CartesianClosed v => HasEnds v where 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
 HasEnds ((->) :: Type -> Type -> Type) Source # Instance detailsDefined in Data.Category.Enriched Methodsend :: (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 #

Constructors

 HaskEnd FieldsgetHaskEnd :: 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
 (HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) Source # The enriched functor category [a, b] Instance detailsDefined in Data.Category.Enriched Associated Typestype V (FunCat a b) :: Type -> Type -> Type Source #type (FunCat a b) $ab :: Type Source # Methodshom :: 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 detailsDefined in Data.Category.Enriched type V (FunCat a b) = V a type (FunCat a b)$ (t, s) Source # Instance detailsDefined in Data.Category.Enriched 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 :: * -> * -> *) Source # Constructors  EndFunctor Instances  (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (EndFunctor k) :: Type -> Type -> Type Source #type ECod (EndFunctor k) :: Type -> Type -> Type Source #type (EndFunctor k) :%% a :: Type 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 EDom (EndFunctor k) Source # Instance detailsDefined in Data.Category.Enriched type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k)) type ECod (EndFunctor k) Source # Instance detailsDefined in Data.Category.Enriched type ECod (EndFunctor k) = Self (V k) type (EndFunctor k) :%% t Source # Instance detailsDefined in Data.Category.Enriched type (EndFunctor k) :%% t = End (V k) t type family WeigtedLimit (k :: * -> * -> *) w d :: * Source # Instances  type WeigtedLimit (Self v) w d Source # Instance detailsDefined in Data.Category.Enriched type WeigtedLimit (Self v) w d = End v (w :->>: d) type Lim w d = WeigtedLimit (ECod d) w d Source # class HasEnds (V k) => HasLimits k where Source # Methods limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d) Source # 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)) Source #

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))) Source # Instances  HasEnds v => HasLimits (Self v) Source # Instance detailsDefined in Data.Category.Enriched MethodslimitObj :: (EFunctorOf j (Self v) d, EFunctorOf j (Self (V (Self v))) w) => w -> d -> Obj (Self v) (Lim w d) Source #limit :: (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)) Source #limitInv :: (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))) Source # type family WeigtedColimit (k :: * -> * -> *) w d :: * Source # type Colim w d = WeigtedColimit (ECod d) w d Source # class HasEnds (V k) => HasColimits k where Source # Methods colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d) Source # 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)) Source #

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))) Source # 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) Source # 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)) Source # data Y (k :: * -> * -> *) Source # Constructors  Y Instances  (ECategory k, HasEnds (V k)) => EFunctor (Y k) Source # Yoneda embedding Instance detailsDefined in Data.Category.Enriched Associated Typestype EDom (Y k) :: Type -> Type -> Type Source #type ECod (Y k) :: Type -> Type -> Type Source #type (Y k) :%% a :: Type Source # Methods(%%) :: Y k -> Obj (EDom (Y k)) a -> Obj (ECod (Y k)) (Y k :%% a) Source #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)) Source # type EDom (Y k) Source # Instance detailsDefined in Data.Category.Enriched type EDom (Y k) = EOp k type ECod (Y k) Source # Instance detailsDefined in Data.Category.Enriched type ECod (Y k) = FunCat k (Self (V k)) type (Y k) :%% x Source # Instance detailsDefined in Data.Category.Enriched type (Y k) :%% x = EHomX_ k x data One Source # data Two Source # data PosetTest a b where Source # Constructors  One :: PosetTest One One Two :: PosetTest Two Two Three :: PosetTest Three Three Instances  Source # Instance detailsDefined in Data.Category.Enriched Associated Typestype V PosetTest :: Type -> Type -> Type Source #type PosetTest$ ab :: Type Source # Methodshom :: 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 # type V PosetTest Source # Instance detailsDefined in Data.Category.Enriched type V PosetTest = Boolean type PosetTest $(a, b) Source # Instance detailsDefined in Data.Category.Enriched type PosetTest$ (a, b) = Poset3 a b

type family Poset3 a b where ... Source #

Equations

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