module Math.Functors.SetValued.Examples
(
exampleSetValuedLeftKanExtension,
exampleSetValuedRightKanExtension,
)
where
import Math.FiniteCategory
import Math.IO.PrettyPrint
import Math.FiniteCategories
import Math.Categories.FinSet
import Math.Functors.SetValued
import Data.WeakSet (Set)
import qualified Data.WeakSet as Set
import Data.WeakSet.Safe
import Data.WeakMap (Map)
import qualified Data.WeakMap as Map
import Data.WeakMap.Safe
import Data.Text (Text, pack)
exampleSetValuedLeftKanExtension :: (Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (FinSet (ColimitObject Text (CGMorphism Text Text) Int)) (Function (ColimitObject Text (CGMorphism Text Text) Int)) (Set (ColimitObject Text (CGMorphism Text Text) Int)), NaturalTransformation (CompositionGraph Text Text) (CGMorphism Text Text) Text (FinSet (ColimitObject Text (CGMorphism Text Text) Int)) (Function (ColimitObject Text (CGMorphism Text Text) Int)) (Set (ColimitObject Text (CGMorphism Text Text) Int)))
exampleSetValuedLeftKanExtension :: (Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int)),
NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int)))
exampleSetValuedLeftKanExtension = (Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int))
lan,NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int))
eta)
where
Right CompositionGraph Text Text
a = String
-> Either
(FiniteCategoryError (CGMorphism Text Text) Text)
(CompositionGraph Text Text)
readCGString String
"A -f-> B\n"
Right CompositionGraph Text Text
b = String
-> Either
(FiniteCategoryError (CGMorphism Text Text) Text)
(CompositionGraph Text Text)
readCGString String
"A -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
Right CGD
f = String
-> Either
(DiagramError
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text)
CGD
readCGDString String
"<SRC>\nA -f-> B\n</SRC>\n<TGT>\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n</TGT>\nA -f-> B => A -f-> B\n"
x :: Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
x = Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
-> Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph Text Text
src = CompositionGraph Text Text
a, tgt :: FinSet Int
tgt = FinSet Int
forall a. FinSet a
FinSet, omap :: Map Text (Set Int)
omap = AssociationList Text (Set Int) -> Map Text (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map (CGMorphism Text Text) (Function Int)
mmap = AssociationList (CGMorphism Text Text) (Function Int)
-> Map (CGMorphism Text Text) (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap [(Set (CGMorphism Text Text) -> CGMorphism Text Text
forall a. Set a -> a
anElement (CompositionGraph Text Text
-> Text -> Text -> Set (CGMorphism Text Text)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar CompositionGraph Text Text
a (String -> Text
pack String
"A") (String -> Text
pack String
"B")),Function{function :: Map Int Int
function=AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
1,Int
3),(Int
2,Int
3)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
3,Int
4]})]}
(Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int))
lan,NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int))
eta) = CGD
-> Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
-> (Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int)),
NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (ColimitObject Text (CGMorphism Text Text) Int))
(Function (ColimitObject Text (CGMorphism Text Text) Int))
(Set (ColimitObject Text (CGMorphism Text Text) Int)))
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> (Diagram
c2
m2
o2
(FinSet (ColimitObject o1 m2 a))
(Function (ColimitObject o1 m2 a))
(Set (ColimitObject o1 m2 a)),
NaturalTransformation
c1
m1
o1
(FinSet (ColimitObject o1 m2 a))
(Function (ColimitObject o1 m2 a))
(Set (ColimitObject o1 m2 a)))
leftKanSetValued CGD
f Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
x
exampleSetValuedRightKanExtension :: (Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (FinSet (LimitObject Text (CGMorphism Text Text) Int)) (Function (LimitObject Text (CGMorphism Text Text) Int)) (Set (LimitObject Text (CGMorphism Text Text) Int)), NaturalTransformation (CompositionGraph Text Text) (CGMorphism Text Text) Text (FinSet (LimitObject Text (CGMorphism Text Text) Int)) (Function (LimitObject Text (CGMorphism Text Text) Int)) (Set (LimitObject Text (CGMorphism Text Text) Int)))
exampleSetValuedRightKanExtension :: (Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int)),
NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int)))
exampleSetValuedRightKanExtension = (Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int))
ran,NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int))
epsilon)
where
Right CompositionGraph Text Text
a = String
-> Either
(FiniteCategoryError (CGMorphism Text Text) Text)
(CompositionGraph Text Text)
readCGString String
"A -f-> B\n"
Right CompositionGraph Text Text
b = String
-> Either
(FiniteCategoryError (CGMorphism Text Text) Text)
(CompositionGraph Text Text)
readCGString String
"A -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
Right CGD
f = String
-> Either
(DiagramError
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text)
CGD
readCGDString String
"<SRC>\nA -f-> B\n</SRC>\n<TGT>\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n</TGT>\nA -f-> B => A -f-> B\n"
x :: Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
x = Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
-> Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph Text Text
src = CompositionGraph Text Text
a, tgt :: FinSet Int
tgt = FinSet Int
forall a. FinSet a
FinSet, omap :: Map Text (Set Int)
omap = AssociationList Text (Set Int) -> Map Text (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map (CGMorphism Text Text) (Function Int)
mmap = AssociationList (CGMorphism Text Text) (Function Int)
-> Map (CGMorphism Text Text) (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap [(Set (CGMorphism Text Text) -> CGMorphism Text Text
forall a. Set a -> a
anElement (CompositionGraph Text Text
-> Text -> Text -> Set (CGMorphism Text Text)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar CompositionGraph Text Text
a (String -> Text
pack String
"A") (String -> Text
pack String
"B")),Function{function :: Map Int Int
function=AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
1,Int
3),(Int
2,Int
3)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
3,Int
4]})]}
(Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int))
ran,NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int))
epsilon) = CGD
-> Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
-> (Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int)),
NaturalTransformation
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet (LimitObject Text (CGMorphism Text Text) Int))
(Function (LimitObject Text (CGMorphism Text Text) Int))
(Set (LimitObject Text (CGMorphism Text Text) Int)))
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> (Diagram
c2
m2
o2
(FinSet (LimitObject o1 m2 a))
(Function (LimitObject o1 m2 a))
(Set (LimitObject o1 m2 a)),
NaturalTransformation
c1
m1
o1
(FinSet (LimitObject o1 m2 a))
(Function (LimitObject o1 m2 a))
(Set (LimitObject o1 m2 a)))
rightKanSetValued CGD
f Diagram
(CompositionGraph Text Text)
(CGMorphism Text Text)
Text
(FinSet Int)
(Function Int)
(Set Int)
x