FiniteCategories-0.1.0.0: Finite categories and usual categorical constructions on them.
CopyrightGuillaume Sabbagh 2021
LicenseGPL-3
Maintainerguillaumesabbagh@protonmail.com
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

YonedaEmbedding.YonedaEmbedding

Description

The Yoneda embedding of a category.

Synopsis

Documentation

type PreSheaf c m o = Diagram (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m) Source #

A presheaf on a category C is a diagram from C^op to Set.

type PreSheavesNatTransfo c m o = NaturalTransformation (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m) Source #

Natural transformation between presheaves.

type PreSheavesCategory c m o = FunctorCategory (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m) Source #

The type of the category of presheaves.

yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (PreSheavesCategory c m o, Diagram c m o (PreSheavesCategory c m o) (PreSheavesNatTransfo c m o) (PreSheaf c m o)) Source #

Returns the presheaf category generated by a Yoneda embedding and an insertion functor full and faithful.