{-| 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 :: 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 = Diagram
  Hat
  HatAr
  HatOb
  (PresheafCategory Hat HatAr HatOb)
  (PresheafMorphism Hat HatAr HatOb)
  (Presheaf Hat HatAr HatOb)
-> 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)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
fullDiagram(Diagram
   Hat
   HatAr
   HatOb
   (PresheafCategory Hat HatAr HatOb)
   (PresheafMorphism Hat HatAr HatOb)
   (Presheaf Hat HatAr HatOb)
 -> 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))
-> (Hat
    -> Diagram
         Hat
         HatAr
         HatOb
         (PresheafCategory Hat HatAr HatOb)
         (PresheafMorphism Hat HatAr HatOb)
         (Presheaf Hat HatAr HatOb))
-> Hat
-> 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)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Hat
-> Diagram
     Hat
     HatAr
     HatOb
     (PresheafCategory Hat HatAr HatOb)
     (PresheafMorphism Hat HatAr HatOb)
     (Presheaf Hat HatAr HatOb)
forall c m o.
(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)
yonedaEmbedding (Hat
 -> 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))
-> Hat
-> 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)
forall a b. (a -> b) -> a -> b
$ Hat
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 :: 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 = Diagram
  Square
  SquareAr
  SquareOb
  (PresheafCategory Square SquareAr SquareOb)
  (PresheafMorphism Square SquareAr SquareOb)
  (Presheaf Square SquareAr SquareOb)
-> 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)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
fullDiagram(Diagram
   Square
   SquareAr
   SquareOb
   (PresheafCategory Square SquareAr SquareOb)
   (PresheafMorphism Square SquareAr SquareOb)
   (Presheaf Square SquareAr SquareOb)
 -> 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))
-> (Square
    -> Diagram
         Square
         SquareAr
         SquareOb
         (PresheafCategory Square SquareAr SquareOb)
         (PresheafMorphism Square SquareAr SquareOb)
         (Presheaf Square SquareAr SquareOb))
-> Square
-> 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)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Square
-> Diagram
     Square
     SquareAr
     SquareOb
     (PresheafCategory Square SquareAr SquareOb)
     (PresheafMorphism Square SquareAr SquareOb)
     (Presheaf Square SquareAr SquareOb)
forall c m o.
(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)
yonedaEmbedding (Square
 -> 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))
-> Square
-> 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)
forall a b. (a -> b) -> a -> b
$ Square
Square