FiniteCategories-0.6.5.1: src/Math/Functors/YonedaEmbedding/Examples.hs

{-| Module  : FiniteCategories
Description : Examples of 'yonedaEmbedding'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of  'yonedaEmbedding'.


-}
module Math.Functors.YonedaEmbedding.Examples
(
    exampleYonedaEmbeddingOfHat,
    exampleYonedaEmbeddingOfSquare,
)
where
    import              Math.FiniteCategories
    import              Math.Categories
    
    
    -- | The full and faithfull part of the 'yonedaEmbedding' of 'Hat'.
    exampleYonedaEmbeddingOfHat :: Diagram Hat HatAr HatOb (Subcategory (PresheafCategory Hat HatAr HatOb) (PresheafMorphism Hat HatAr HatOb) (Presheaf Hat HatAr HatOb)) (PresheafMorphism Hat HatAr HatOb) (Presheaf Hat HatAr HatOb)
    exampleYonedaEmbeddingOfHat = fullDiagram.yonedaEmbedding $ Hat
    
    -- | The full and faithfull part of the 'yonedaEmbedding' of 'Square'.
    exampleYonedaEmbeddingOfSquare :: Diagram Square SquareAr SquareOb (Subcategory (PresheafCategory Square SquareAr SquareOb) (PresheafMorphism Square SquareAr SquareOb) (Presheaf Square SquareAr SquareOb)) (PresheafMorphism Square SquareAr SquareOb) (Presheaf Square SquareAr SquareOb)
    exampleYonedaEmbeddingOfSquare = fullDiagram.yonedaEmbedding $ Square