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

Data.Category.Enriched.Functor

Description

Synopsis

class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where
- type EDom ftag :: Type -> Type -> Type
- type ECod ftag :: Type -> Type -> Type
- type ftag :%% a :: Type
- (%%) :: 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 :: Type -> Type -> Type) = Id
data g :.: h where
- (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h
data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) 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 :: Type -> Type -> Type) = DiagProd
newtype UnderlyingF f = UnderlyingF f
newtype InHaskF f = InHaskF f
newtype InHaskToHask f = InHaskToHask f
newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f = UnderlyingHask f
data EHom (k :: Type -> Type -> Type) = EHom
data EHomX_ k x = EHomX_ (Obj k x)
data EHom_X k x = EHom_X (Obj (EOp k) x)
strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% BinaryProduct v a b)
data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type 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

Documentation

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

Enriched functors.

Associated Types

type EDom ftag :: Type -> Type -> Type Source #

The domain, or source category, of the functor.

type ECod ftag :: Type -> Type -> Type Source #

The codomain, or target category, of the functor.

type ftag :%% a :: Type 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

Instances details

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

Constructors

Id

Instances

Instances details

ECategory k => EFunctor (Id k) Source #	The identity functor on k
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (Id k) :: Type -> Type -> Type Source # type ECod (Id k) :: Type -> Type -> Type Source # type (Id k) :%% a 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 ECod (Id k) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (Id k) = k
type EDom (Id k) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (Id k) = k
type (Id k) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (Id k) :%% a = a

data g :.: h where Source #

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) Source #	The composition of two functors.
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (g :.: h) :: Type -> Type -> Type Source # type ECod (g :.: h) :: Type -> Type -> Type Source # type (g :.: h) :%% a 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 ECod (g :.: h) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (g :.: h) = ECod g
type EDom (g :.: h) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (g :.: h) = EDom h
type (g :.: h) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (g :.: h) :%% a = g :%% (h :%% a)

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

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) Source #	The constant functor.
Instance details Defined in Data.Category.Enriched.Functor 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 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 ECod (Const c1 c2 x) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (Const c1 c2 x) = c2
type EDom (Const c1 c2 x) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (Const c1 c2 x) = c1
type (Const c1 c2 x) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (Const c1 c2 x) :%% a = x

data Opposite f where Source #

Constructors

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

Instances

Instances details

EFunctor f => EFunctor (Opposite f) Source #	The dual of a functor
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (Opposite f) :: Type -> Type -> Type Source # type ECod (Opposite f) :: Type -> Type -> Type Source # type (Opposite f) :%% a 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 ECod (Opposite f) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (Opposite f) = EOp (ECod f)
type EDom (Opposite f) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (Opposite f) = EOp (EDom f)
type (Opposite f) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (Opposite f) :%% a = f :%% a

data f1 :<*>: f2 Source #

Constructors

f1 :<*>: f2

Instances

Instances details

(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.Functor Associated Types type EDom (f1 :<>: f2) :: Type -> Type -> Type Source # type ECod (f1 :<>: f2) :: Type -> Type -> Type Source # type (f1 :<>: f2) :%% a 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 ECod (f1 :<*>: f2) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2
type EDom (f1 :<*>: f2) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2
type (f1 :<*>: f2) :%% (a1, a2) Source #
Instance details Defined in Data.Category.Enriched.Functor type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)

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

Constructors

DiagProd

Instances

Instances details

ECategory k => EFunctor (DiagProd k) Source #	`DiagProd` is the diagonal functor for products.
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (DiagProd k) :: Type -> Type -> Type Source # type ECod (DiagProd k) :: Type -> Type -> Type Source # type (DiagProd k) :%% a 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 ECod (DiagProd k) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (DiagProd k) = k :<>: k
type EDom (DiagProd k) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (DiagProd k) = k
type (DiagProd k) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (DiagProd k) :%% a = (a, a)

newtype UnderlyingF f Source #

Constructors

UnderlyingF f

Instances

Instances details

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

newtype InHaskF f Source #

Constructors

InHaskF f

Instances

Instances details

Functor f => EFunctor (InHaskF f) Source #	A regular functor is a functor enriched in Hask.
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (InHaskF f) :: Type -> Type -> Type Source # type ECod (InHaskF f) :: Type -> Type -> Type Source # type (InHaskF f) :%% a Source # Methods (%%) :: InHaskF f -> Obj (EDom (InHaskF f)) a -> Obj (ECod (InHaskF f)) (InHaskF f :%% a) Source # map :: EDom (InHaskF f) ~ k => InHaskF f -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (InHaskF f) $ (InHaskF f :%% a, InHaskF f :%% b)) Source #
type ECod (InHaskF f) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (InHaskF f) = InHask (Cod f)
type EDom (InHaskF f) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (InHaskF f) = InHask (Dom f)
type (InHaskF f) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (InHaskF f) :%% a = f :% a

newtype InHaskToHask f Source #

Constructors

InHaskToHask f

Instances

Instances details

(Functor f, Cod f ~ (->)) => EFunctor (InHaskToHask f) Source #
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (InHaskToHask f) :: Type -> Type -> Type Source # type ECod (InHaskToHask f) :: Type -> Type -> Type Source # type (InHaskToHask f) :%% a Source # Methods (%%) :: InHaskToHask f -> Obj (EDom (InHaskToHask f)) a -> Obj (ECod (InHaskToHask f)) (InHaskToHask f :%% a) Source # map :: EDom (InHaskToHask f) ~ k => InHaskToHask f -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod (InHaskToHask f) $ (InHaskToHask f :%% a, InHaskToHask f :%% b)) Source #
HasWLimits k w => HasLimits (InHask k) (InHaskToHask w) Source #
Instance details Defined in Data.Category.Enriched.Limit Methods limitObj :: EFunctorOf (EDom (InHaskToHask w)) (InHask k) d => InHaskToHask w -> d -> Obj (InHask k) (Lim (InHaskToHask w) d) Source # limit :: EFunctorOf (EDom (InHaskToHask w)) (InHask k) d => InHaskToHask w -> d -> Obj (InHask k) e -> V (InHask k) (InHask k $ (e, Lim (InHaskToHask w) d)) (End (V (InHask k)) (InHaskToHask w :->>: (EHomX_ (InHask k) e :.: d))) Source # limitInv :: EFunctorOf (EDom (InHaskToHask w)) (InHask k) d => InHaskToHask w -> d -> Obj (InHask k) e -> V (InHask k) (End (V (InHask k)) (InHaskToHask w :->>: (EHomX_ (InHask k) e :.: d))) (InHask k $ (e, Lim (InHaskToHask w) d)) Source #
type ECod (InHaskToHask f) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (InHaskToHask f) = Self (->)
type EDom (InHaskToHask f) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (InHaskToHask f) = InHask (Dom f)
type (InHaskToHask f) :%% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (InHaskToHask f) :%% a = f :% a
type WeigtedLimit (InHask k) (InHaskToHask w) d Source #
Instance details Defined in Data.Category.Enriched.Limit type WeigtedLimit (InHask k) (InHaskToHask w) d = WeightedLimit k w (UnderlyingHask (Dom w) k d)

newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f Source #

Constructors

UnderlyingHask f

Instances

Instances details

(EFunctor f, EDom f ~ InHask c, ECod f ~ InHask d, Category c, Category d) => Functor (UnderlyingHask c d f) Source #	The underlying functor of an enriched functor `f` enriched in Hask.
Instance details Defined in Data.Category.Enriched.Functor Associated Types type Dom (UnderlyingHask c d f) :: Type -> Type -> Type Source # type Cod (UnderlyingHask c d f) :: Type -> Type -> Type Source # type (UnderlyingHask c d f) :% a Source # Methods (%) :: UnderlyingHask c d f -> Dom (UnderlyingHask c d f) a b -> Cod (UnderlyingHask c d f) (UnderlyingHask c d f :% a) (UnderlyingHask c d f :% b) Source #
type Cod (UnderlyingHask c d f) Source #
Instance details Defined in Data.Category.Enriched.Functor type Cod (UnderlyingHask c d f) = d
type Dom (UnderlyingHask c d f) Source #
Instance details Defined in Data.Category.Enriched.Functor type Dom (UnderlyingHask c d f) = c
type (UnderlyingHask c d f) :% a Source #
Instance details Defined in Data.Category.Enriched.Functor type (UnderlyingHask c d f) :% a = f :%% a

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

Constructors

EHom

Instances

Instances details

ECategory k => EFunctor (EHom k) Source #
Instance details Defined in Data.Category.Enriched.Functor Associated Types type EDom (EHom k) :: Type -> Type -> Type Source # type ECod (EHom k) :: Type -> Type -> Type Source # type (EHom k) :%% a 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 ECod (EHom k) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (EHom k) = Self (V k)
type EDom (EHom k) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (EHom k) = EOp k :<>: k
type (EHom k) :%% (a, b) Source #
Instance details Defined in Data.Category.Enriched.Functor type (EHom k) :%% (a, b) = k $ (a, b)

data EHomX_ k x Source #

The enriched functor k(x, -)

Constructors

EHomX_ (Obj k x)

Instances

Instances details

ECategory k => EFunctor (EHomX_ k x) Source #
Instance details Defined in Data.Category.Enriched.Functor 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 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 ECod (EHomX_ k x) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (EHomX_ k x) = Self (V k)
type EDom (EHomX_ k x) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (EHomX_ k x) = k
type (EHomX_ k x) :%% y Source #
Instance details Defined in Data.Category.Enriched.Functor 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

Instances details

ECategory k => EFunctor (EHom_X k x) Source #
Instance details Defined in Data.Category.Enriched.Functor 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 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 ECod (EHom_X k x) Source #
Instance details Defined in Data.Category.Enriched.Functor type ECod (EHom_X k x) = Self (V k)
type EDom (EHom_X k x) Source #
Instance details Defined in Data.Category.Enriched.Functor type EDom (EHom_X k x) = EOp k
type (EHom_X k x) :%% y Source #
Instance details Defined in Data.Category.Enriched.Functor type (EHom_X k x) :%% y = k $ (y, x)

strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% BinaryProduct v a b) Source #

A V-enrichment on a functor F: V -> V is the same thing as tensorial strength (a, f b) -> f (a, b).

data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type 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