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

Math.Categories.PresheafCategory

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

Presheaves

type Presheaf c m o = Diagram (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m) Source #

A Presheaf on a Category C is a diagram from C^op to FinSet.

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.