| Copyright | Guillaume Sabbagh 2021 |
|---|---|
| License | GPL-3 |
| Maintainer | guillaumesabbagh@protonmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
YonedaEmbedding.YonedaEmbedding
Description
The Yoneda embedding of a category.
Synopsis
- type PreSheaf c m o = Diagram (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
- type PreSheavesNatTransfo c m o = NaturalTransformation (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
- type PreSheavesCategory c m o = FunctorCategory (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
- 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))
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.