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

An example of  'yonedaEmbedding' pretty printed.


-}
module Math.Functors.YonedaEmbedding.Example
(
    main
)
where
    import Data.WeakSet         (Set)
    import Data.WeakSet.Safe
    
    import Math.FiniteCategories
    import Math.Categories
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint
    
    -- | 'yonedaEmbedding' pretty printed.

    main :: IO ()
    main :: IO ()
main = do
        String -> IO ()
putStrLn String
"Start of Math.FiniteCategories.YonedaEmbedding.Example"
        String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ 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
forall a. PrettyPrint a => a -> String
pprint (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 -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ 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
forall a. PrettyPrint a => a -> String
pprint (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 -> IO ()
putStrLn String
"End of Math.FiniteCategories.YonedaEmbedding.Example"