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

Data.Category.Yoneda

Description

Synopsis

type YonedaEmbedding k = Curry2 (Op k) k (Hom k)
pattern YonedaEmbedding :: Category k => YonedaEmbedding k
data Yoneda (k :: Type -> Type -> Type) 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).

Constructors

Instances details

(Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => 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 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 Cod (Yoneda k f) Source #
Instance details Defined in Data.Category.Yoneda type Cod (Yoneda k f) = (->)
type Dom (Yoneda k f) Source #
Instance details Defined in Data.Category.Yoneda type Dom (Yoneda k f) = Op k
type (Yoneda k f) :% a Source #
Instance details Defined in Data.Category.Yoneda type (Yoneda k f) :% a = Nat (Op k) (->) (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 details

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 Source # Methods (%) :: M1 -> Dom M1 a b -> Cod M1 (M1 :% a) (M1 :% b) Source #
type Cod M1 Source #
Instance details Defined in Data.Category.Yoneda type Cod M1 = (->)
type Dom M1 Source #
Instance details Defined in Data.Category.Yoneda type Dom M1 = Nat (Op (->)) (->)
type M1 :% f Source #
Instance details Defined in Data.Category.Yoneda type M1 :% f = f :% ()