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.Yoneda

Description

Documentation

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), EFunctor f, EDom f ~ k, ECod f ~ Self (V k)) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f)) Source #

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

Constructors

Instances details

(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 #
type ECod (Y k) Source #
Instance details Defined in Data.Category.Enriched.Yoneda type ECod (Y k) = FunCat k (Self (V k))
type EDom (Y k) Source #
Instance details Defined in Data.Category.Enriched.Yoneda type EDom (Y k) = EOp k
type (Y k) :%% x Source #
Instance details Defined in Data.Category.Enriched.Yoneda type (Y k) :%% x = EHomX_ k x