data-category-0.10: Category theory

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 detailsDefined in Data.Category.Yoneda Associated Typestype 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 detailsDefined in Data.Category.Yoneda type Dom (Yoneda k f) = Op k type Cod (Yoneda k f) Source # Instance detailsDefined in Data.Category.Yoneda type Cod (Yoneda k f) = ((->) :: Type -> Type -> Type) type (Yoneda k f) :% a Source # Instance detailsDefined 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
 Source # Instance detailsDefined in Data.Category.Yoneda Associated Typestype 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 detailsDefined in Data.Category.Yoneda type Dom M1 = Nat (Op ((->) :: Type -> Type -> Type)) ((->) :: Type -> Type -> Type) type Cod M1 Source # Instance detailsDefined in Data.Category.Yoneda type Cod M1 = ((->) :: Type -> Type -> Type) type M1 :% f Source # Instance detailsDefined in Data.Category.Yoneda type M1 :% f = f :% ()

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