data-category-0.7.2: Category theory

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

Data.Category.Yoneda

Description

 
Synopsis

Documentation

type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k)) Source #

pattern YonedaEmbedding :: Category k => YonedaEmbedding k Source #

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

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

Constructors

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

haskUnit :: Obj (->) () Source #

data M1 Source #

Constructors

M1 
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 :% ()

haskIsTotal :: Adjunction (->) (Nat (Op (->)) (->)) M1 (YonedaEmbedding (->)) Source #