module Math.Functors.YonedaEmbedding.Examples
(
exampleYonedaEmbeddingOfHat,
exampleYonedaEmbeddingOfSquare,
)
where
import Math.FiniteCategories
import Math.Categories
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
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