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

Data.Category.Yoneda

Description

Synopsis

type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))
pattern YonedaEmbedding :: Category k => YonedaEmbedding k
data Yoneda (k :: * -> * -> *) f = Yoneda
fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f
toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f)
haskUnit :: Obj (->) ()
data M1 = M1
haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->))

Documentation

The Yoneda embedding functor, C -> Set^(C^op).

data Yoneda (k :: * -> * -> *) f Source #

Constructors

Instances

(Category k, Functor f, Dom f ~ Op k, Cod f ~ ((->) :: Type -> Type -> Type)) => Functor (Yoneda k f) Source #	`Yoneda` converts a functor `f` into a natural transformation from the hom functor to f.
Instance details Defined in Data.Category.Yoneda Associated Types type Dom (Yoneda k f) :: Type -> Type -> Type Source # type Cod (Yoneda k f) :: Type -> Type -> Type Source # type (Yoneda k f) :% a :: Type Source # Methods (%) :: Yoneda k f -> Dom (Yoneda k f) a b -> Cod (Yoneda k f) (Yoneda k f :% a) (Yoneda k f :% b) Source #
type Dom (Yoneda k f) Source #
Instance details Defined in Data.Category.Yoneda type Dom (Yoneda k f) = Op k
type Cod (Yoneda k f) Source #
Instance details Defined in Data.Category.Yoneda type Cod (Yoneda k f) = ((->) :: Type -> Type -> Type)
type (Yoneda k f) :% a Source #
Instance details Defined in Data.Category.Yoneda type (Yoneda k f) :% a = Nat (Op k) ((->) :: Type -> Type -> Type) (k :-*: a) f

fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f Source #

fromYoneda and toYoneda are together the isomophism from the Yoneda lemma.

toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f) Source #

Constructors

Instances

Functor M1 Source #
Instance details Defined in Data.Category.Yoneda Associated Types type Dom M1 :: Type -> Type -> Type Source # type Cod M1 :: Type -> Type -> Type Source # type M1 :% a :: Type Source # Methods (%) :: M1 -> Dom M1 a b -> Cod M1 (M1 :% a) (M1 :% b) Source #
type Dom M1 Source #
Instance details Defined in Data.Category.Yoneda type Dom M1 = Nat (Op ((->) :: Type -> Type -> Type)) ((->) :: Type -> Type -> Type)
type Cod M1 Source #
Instance details Defined in Data.Category.Yoneda type Cod M1 = ((->) :: Type -> Type -> Type)
type M1 :% f Source #
Instance details Defined in Data.Category.Yoneda type M1 :% f = f :% ()