| Copyright | Guillaume Sabbagh 2022 |
|---|---|
| License | GPL-3 |
| Maintainer | guillaumesabbagh@protonmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Math.Categories.PresheafCategory
Contents
Description
The category of presheaves on a Category C has functors from C^op to FinSet as objects and natural transformations as morphisms. It is a FunctorCategory.
The yonedaEmbedding goes to a category of presheaves, it allows to cocomplete a FiniteCategory.
Synopsis
- type Presheaf c m o = Diagram (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
- type PresheafMorphism c m o = NaturalTransformation (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
- type PresheafCategory c m o = FunctorCategory (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
- yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Diagram c m o (PresheafCategory c m o) (PresheafMorphism c m o) (Presheaf c m o)
Presheaves
type PresheafMorphism c m o = NaturalTransformation (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m) Source #
A PresheafMorphism is a NaturalTransformation between presheaves.
type PresheafCategory c m o = FunctorCategory (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m) Source #
The type of the category of presheaves.
Yoneda embedding
yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Diagram c m o (PresheafCategory c m o) (PresheafMorphism c m o) (Presheaf c m o) Source #
Given a FiniteCategory C, return its Yoneda embedding in the FunctorCategory [C^op, FinSet].
It allows to cocomplete a FiniteCategory. The insertion functor from the category to [C^op, FinSet] is full and faithful.