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
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"