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

An example of  'yonedaEmbedding' exported with GraphViz.

Export the diagram in the directory "OutputGraphViz\/Examples\/Functors\/YonedaEmbedding".
-}
module Math.Functors.YonedaEmbedding.Example
(
    main
)
where
    import Data.WeakSet         (Set)
    import Data.WeakSet.Safe
    
    import Math.FiniteCategories
    import Math.Categories
    import Math.IO.FiniteCategories.ExportGraphViz
    
    -- | 'yonedaEmbedding' exported with GraphViz.

    main :: IO ()
    main :: IO ()
main = do
        String -> IO ()
putStrLn String
"Start of Math.FiniteCategories.YonedaEmbedding.Example"
        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)
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 (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) String
"OutputGraphViz/Examples/FiniteCategories/YonedaEmbedding/YonedaEmbeddingHat"
        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)
-> String -> IO ()
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Eq o1, Eq m1,
 PrettyPrint m1, PrettyPrint o1, Morphism m2 o2,
 FiniteCategory c2 m2 o2, Eq o2, Eq m2, PrettyPrint m2,
 PrettyPrint o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> String -> IO ()
diagToPdf2 (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) String
"OutputGraphViz/Examples/FiniteCategories/YonedaEmbedding/YonedaEmbeddingSquare"
        String -> IO ()
putStrLn String
"End of Math.FiniteCategories.YonedaEmbedding.Example"