data-category-0.7.2: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

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
ECategory PosetTest Source # 
Instance details

Defined in Data.Category.Enriched

Associated Types

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

type PosetTest $ ab :: Type 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 :: Type 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 :: Type 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 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 :: Type 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 #

(HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) Source #

The enriched functor category [a, b]

Instance details

Defined in Data.Category.Enriched

Associated Types

type V (FunCat a b) :: Type -> Type -> Type Source #

type (FunCat a b) $ ab :: Type 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 #

(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 :: Type 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 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 details

Defined in Data.Category.Enriched

Methods

src :: 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 details

Defined in Data.Category.Enriched

Associated Types

type V (EOp k) :: Type -> Type -> Type Source #

type (EOp k) $ ab :: Type 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 (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * 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 details

Defined in Data.Category.Enriched

Associated Types

type V (k1 :<>: k2) :: Type -> Type -> Type Source #

type (k1 :<>: k2) $ ab :: Type 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

Instances
HasEnds v => HasLimits (Self v) Source # 
Instance details

Defined in Data.Category.Enriched

Methods

limitObj :: (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 details

Defined in Data.Category.Enriched

Associated Types

type V (Self v) :: Type -> Type -> Type Source #

type (Self v) $ ab :: Type 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 #

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

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
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 :: Type 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 #

type V (InHask k) Source # 
Instance details

Defined in Data.Category.Enriched

type V (InHask k) = ((->) :: Type -> Type -> Type)
type (InHask k) $ (a, b) Source # 
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 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (Id k) = k
type ECod (Id k) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (Id k) = k
type (Id k) :%% a Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (g :.: h) = EDom h
type ECod (g :.: h) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (g :.: h) = ECod g
type (g :.: h) :%% a Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (Const c1 c2 x) = c1
type ECod (Const c1 c2 x) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (Const c1 c2 x) = c2
type (Const c1 c2 x) :%% a Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (Opposite f) = EOp (EDom f)
type ECod (Opposite f) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (Opposite f) = EOp (ECod f)
type (Opposite f) :%% a Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2
type ECod (f1 :<*>: f2) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2
type (f1 :<*>: f2) :%% (a1, a2) Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (DiagProd k) = k
type ECod (DiagProd k) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (DiagProd k) = k :<>: k
type (DiagProd k) :%% a Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type Cod (UnderlyingF f) Source # 
Instance details

Defined in Data.Category.Enriched

type (UnderlyingF f) :% a Source # 
Instance details

Defined in Data.Category.Enriched

type (UnderlyingF f) :% a = f :%% a

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

Constructors

EHom 
Instances
ECategory k => EFunctor (EHom k) Source # 
Instance details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (EHom k) = EOp k :<>: k
type ECod (EHom k) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (EHom k) = Self (V k)
type (EHom k) :%% (a, b) Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (EHomX_ k x) = k
type ECod (EHomX_ k x) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (EHomX_ k x) = Self (V k)
type (EHomX_ k x) :%% y Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (EHom_X k x) = EOp k
type ECod (EHom_X k x) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (EHom_X k x) = Self (V k)
type (EHom_X k x) :%% y Source # 
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 Source #

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

Instances
type End ((->) :: Type -> Type -> Type) t Source # 
Instance details

Defined 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 details

Defined in Data.Category.Enriched

Methods

end :: (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

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 details

Defined in Data.Category.Enriched

Associated Types

type V (FunCat a b) :: Type -> Type -> Type Source #

type (FunCat a b) $ ab :: Type 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

type V (FunCat a b) = V a
type (FunCat a b) $ (t, s) Source # 
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) 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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))
type ECod (EndFunctor k) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (EndFunctor k) = Self (V k)
type (EndFunctor k) :%% t Source # 
Instance details

Defined 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 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 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 details

Defined in Data.Category.Enriched

Methods

limitObj :: (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 details

Defined in Data.Category.Enriched

Associated Types

type 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 details

Defined in Data.Category.Enriched

type EDom (Y k) = EOp k
type ECod (Y k) Source # 
Instance details

Defined in Data.Category.Enriched

type ECod (Y k) = FunCat k (Self (V k))
type (Y k) :%% x Source # 
Instance details

Defined in Data.Category.Enriched

type (Y k) :%% x = EHomX_ k x

data One Source #

data Two Source #

data PosetTest a b where Source #

Instances
ECategory PosetTest Source # 
Instance details

Defined in Data.Category.Enriched

Associated Types

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

type PosetTest $ ab :: Type Source #

type V PosetTest Source # 
Instance details

Defined in Data.Category.Enriched

type PosetTest $ (a, b) Source # 
Instance details

Defined 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