module Math.FiniteCategories.FinSketch.Examples
(
exampleSketchMagma,
exampleSketchUnitalMagma,
exampleSketchMorphismMagmaToUnitalMagma,
exampleSketchGraph,
exampleSketchPointedSet,
exampleSketchAtomic,
exampleDiagramOfSketches,
exampleSketchLoop,
exampleDiagramOfSketches2,
exampleLantern,
exampleSpotlight,
exampleCrescentMoon,
exampleColantern,
exampleCospotlight,
exampleCocrescentMoon,
exampleNoCrescentMoon,
exampleSketchToRealize,
exampleSketchSAT1,
exampleSketchSAT2,
exampleSketchSAT3,
exampleSketchSAT4,
exampleSketchSAT5,
exampleSketchSAT6,
)
where
import qualified Data.WeakSet as Set
import Data.WeakSet.Safe
import Data.WeakMap.Safe
import Data.Simplifiable
import Math.FiniteCategory
import Math.Categories
import Math.CocompleteCategory
import Math.FiniteCategories
import Math.FiniteCategories.FunctorCategory
import Math.Categories.FinCat
import Math.Categories.FinSketch
import Data.Text (pack , Text)
import System.Random
import Numeric.Natural
exampleSketchMagma :: Sketch Text Text
exampleSketchMagma :: Sketch Text Text
exampleSketchMagma = Sketch Text Text
result
where
Right CG
cg = String
-> Either (FiniteCategoryError (CGMorphism Text Text) Text) CG
readCGString String
"ExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\n"
Right CG
indx = String
-> Either (FiniteCategoryError (CGMorphism Text Text) Text) CG
readCGString String
"A\nB\n"
Right CGD
base = String
-> Either
(DiagramError
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
CGD
readCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\n</TGT>\nA => E\nB => E\n"
Just Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Maybe
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall m1 o1 c1 m2 o2 c2.
(Morphism m1 o1, FiniteCategory c1 m1 o1, Morphism m2 o2,
FiniteCategory c2 m2 o2, Eq c1, Eq m1, Eq o1, Eq c2, Eq m2,
Eq o2) =>
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Maybe (Cone c1 m1 o1 c2 m2 o2)
cone (String -> Text
pack String
"ExE") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx CG
cg (String -> Text
pack String
"ExE")) CGD
base (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p_1")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p_2"))]))
Right Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Either (SketchError Text Text) (Sketch Text Text)
sketchText CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchUnitalMagma :: Sketch Text Text
exampleSketchUnitalMagma :: Sketch Text Text
exampleSketchUnitalMagma = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"ExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n</TGT>\nA => E\nB => E\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"ExE") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"ExE")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p_1")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p_2"))]))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
""
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n</TGT>"
c2 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base2 CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchMorphismMagmaToUnitalMagma :: SketchMorphism Text Text
exampleSketchMorphismMagmaToUnitalMagma :: SketchMorphism Text Text
exampleSketchMorphismMagmaToUnitalMagma = SketchMorphism Text Text -> SketchMorphism Text Text
forall a. Simplifiable a => a -> a
simplify SketchMorphism Text Text
result
where
f :: CGD
f = String -> CGD
unsafeReadCGDString String
"<SRC>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n</TGT>\nExE -p_1-> E => ExE -p_1-> E\nExE -p_2-> E => ExE -p_2-> E\nExE -+-> E => ExE -+-> E\n"
Right SketchMorphism Text Text
result = Sketch Text Text
-> Sketch Text Text
-> CGD
-> Either
(SketchMorphismError Text Text) (SketchMorphism Text Text)
forall n e.
(Eq n, Eq e) =>
Sketch n e
-> Sketch n e
-> FunctorSketch n e
-> Either (SketchMorphismError n e) (SketchMorphism n e)
sketchMorphism Sketch Text Text
exampleSketchMagma Sketch Text Text
exampleSketchUnitalMagma CGD
f
exampleSketchGraph :: Sketch Text Text
exampleSketchGraph :: Sketch Text Text
exampleSketchGraph = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"E -s-> V\nE -t-> V\n"
Right Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Either (SketchError Text Text) (Sketch Text Text)
sketchText CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchPointedSet :: Sketch Text Text
exampleSketchPointedSet :: Sketch Text Text
exampleSketchPointedSet = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"1 -p-> E\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\n1 -p-> E\n</TGT>\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"1")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
Right Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Either (SketchError Text Text) (Sketch Text Text)
sketchText CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchAtomic :: Sketch Text Text
exampleSketchAtomic :: Sketch Text Text
exampleSketchAtomic = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"E\n"
Right Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Either (SketchError Text Text) (Sketch Text Text)
sketchText CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleDiagramOfSketches :: Diagram Hat HatAr HatOb (FinSketch Text Text) (SketchMorphism Text Text) (Sketch Text Text)
exampleDiagramOfSketches :: Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
exampleDiagramOfSketches = Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
-> Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
forall a. Simplifiable a => a -> a
simplify Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
result
where
Right CGD
f = String
-> Either
(DiagramError
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
CGD
readCGDString String
"<SRC>\nE\n</SRC>\n<TGT>\n1 -p-> E\n</TGT>\nE => E\n"
Right SketchMorphism Text Text
sm1 = Sketch Text Text
-> Sketch Text Text
-> CGD
-> Either
(SketchMorphismError Text Text) (SketchMorphism Text Text)
forall n e.
(Eq n, Eq e) =>
Sketch n e
-> Sketch n e
-> FunctorSketch n e
-> Either (SketchMorphismError n e) (SketchMorphism n e)
sketchMorphism Sketch Text Text
exampleSketchAtomic Sketch Text Text
exampleSketchPointedSet CGD
f
Right CGD
g = String
-> Either
(DiagramError
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
CGD
readCGDString String
"<SRC>\nE\n</SRC>\n<TGT>\nE -s-> V\nE -t-> V\n</TGT>\nE => E\n"
Right SketchMorphism Text Text
sm2 = Sketch Text Text
-> Sketch Text Text
-> CGD
-> Either
(SketchMorphismError Text Text) (SketchMorphism Text Text)
forall n e.
(Eq n, Eq e) =>
Sketch n e
-> Sketch n e
-> FunctorSketch n e
-> Either (SketchMorphismError n e) (SketchMorphism n e)
sketchMorphism Sketch Text Text
exampleSketchAtomic Sketch Text Text
exampleSketchGraph CGD
g
result :: Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
result = Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
-> Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
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 :: Hat
src = Hat
Hat, tgt :: FinSketch Text Text
tgt = FinSketch Text Text
forall n e. FinSketch n e
FinSketch, omap :: Map HatOb (Sketch Text Text)
omap = AssociationList HatOb (Sketch Text Text)
-> Map HatOb (Sketch Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map HatAr (SketchMorphism Text Text)
mmap = AssociationList HatAr (SketchMorphism Text Text)
-> Map HatAr (SketchMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(HatAr
HatF,SketchMorphism Text Text
sm1), (HatAr
HatG, SketchMorphism Text Text
sm2)]}
exampleSketchLoop :: Sketch Text Text
exampleSketchLoop :: Sketch Text Text
exampleSketchLoop = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"N -s-> N\n"
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleDiagramOfSketches2 :: Diagram Hat HatAr HatOb (FinSketch Text Text) (SketchMorphism Text Text) (Sketch Text Text)
exampleDiagramOfSketches2 :: Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
exampleDiagramOfSketches2 = Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
-> Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
forall a. Simplifiable a => a -> a
simplify Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
result
where
Right CGD
f = String
-> Either
(DiagramError
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
CGD
readCGDString String
"<SRC>\nE\n</SRC>\n<TGT>\n1 -p-> E\n</TGT>\nE => E\n"
Right SketchMorphism Text Text
sm1 = Sketch Text Text
-> Sketch Text Text
-> CGD
-> Either
(SketchMorphismError Text Text) (SketchMorphism Text Text)
forall n e.
(Eq n, Eq e) =>
Sketch n e
-> Sketch n e
-> FunctorSketch n e
-> Either (SketchMorphismError n e) (SketchMorphism n e)
sketchMorphism Sketch Text Text
exampleSketchAtomic Sketch Text Text
exampleSketchPointedSet CGD
f
g :: CGD
g = CGD -> CGD
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 :: CG
src = Sketch Text Text -> CG
forall n e. Sketch n e -> CategorySketch n e
underlyingCategory Sketch Text Text
exampleSketchAtomic, tgt :: CG
tgt = Sketch Text Text -> CG
forall n e. Sketch n e -> CategorySketch n e
underlyingCategory Sketch Text Text
exampleSketchLoop, omap :: Map Text Text
omap = AssociationList Text Text -> Map Text Text
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"E",String -> Text
pack String
"N")],mmap :: Map (CGMorphism Text Text) (CGMorphism Text Text)
mmap = AssociationList (CGMorphism Text Text) (CGMorphism Text Text)
-> Map (CGMorphism Text Text) (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []}
Right SketchMorphism Text Text
sm2 = Sketch Text Text
-> Sketch Text Text
-> CGD
-> Either
(SketchMorphismError Text Text) (SketchMorphism Text Text)
forall n e.
(Eq n, Eq e) =>
Sketch n e
-> Sketch n e
-> FunctorSketch n e
-> Either (SketchMorphismError n e) (SketchMorphism n e)
sketchMorphism Sketch Text Text
exampleSketchAtomic Sketch Text Text
exampleSketchLoop CGD
g
result :: Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
result = Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
-> Diagram
Hat
HatAr
HatOb
(FinSketch Text Text)
(SketchMorphism Text Text)
(Sketch Text Text)
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 :: Hat
src = Hat
Hat, tgt :: FinSketch Text Text
tgt = FinSketch Text Text
forall n e. FinSketch n e
FinSketch, omap :: Map HatOb (Sketch Text Text)
omap = AssociationList HatOb (Sketch Text Text)
-> Map HatOb (Sketch Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(HatOb
HatA, SketchMorphism Text Text -> Sketch Text Text
forall m o. Morphism m o => m -> o
source SketchMorphism Text Text
sm1),(HatOb
HatB, SketchMorphism Text Text -> Sketch Text Text
forall m o. Morphism m o => m -> o
target SketchMorphism Text Text
sm1),(HatOb
HatC, SketchMorphism Text Text -> Sketch Text Text
forall m o. Morphism m o => m -> o
target SketchMorphism Text Text
sm2)], mmap :: Map HatAr (SketchMorphism Text Text)
mmap = AssociationList HatAr (SketchMorphism Text Text)
-> Map HatAr (SketchMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(HatAr
HatF,SketchMorphism Text Text
sm1), (HatAr
HatG, SketchMorphism Text Text
sm2)]}
exampleLantern :: Sketch Text Text
exampleLantern :: Sketch Text Text
exampleLantern = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"C -f-> A x B -p1-> A = C -g-> A x B -p1-> A\nC -f-> A x B -p2-> B = C -g-> A x B -p2-> B\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nC -f-> A x B -p1-> A = C -g-> A x B -p1-> A\nC -f-> A x B -p2-> B = C -g-> A x B -p2-> B\n</TGT>\nA => A\nB => B\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"A x B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A x B")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSpotlight :: Sketch Text Text
exampleSpotlight :: Sketch Text Text
exampleSpotlight = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"A -f-> B\nA -g-> B\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> B\n</TGT>\nA => B\nB => B\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleCrescentMoon :: Sketch Text Text
exampleCrescentMoon :: Sketch Text Text
exampleCrescentMoon = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"A -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\nX -j-> C\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\nX -j-> C\n</TGT>\nA => B\nB => C\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"g"))]))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"*\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\n*\n</SRC>\n<TGT>\nA -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\nX -j-> C\n</TGT>\n* => B\n"
c2 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"A")) CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"*", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleNoCrescentMoon :: Sketch Text Text
exampleNoCrescentMoon :: Sketch Text Text
exampleNoCrescentMoon = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"D -p1-> A -f-> C = D -p3-> C\nD -p2-> B\nX -c-> A\nX -a-> C\nX -b-> C\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A -f-> C\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA -f-> C\nB\n</SRC>\n<TGT>\nD -p1-> A -f-> C = D -p3-> C\nD -p2-> B\nX -c-> A\nX -a-> C\nX -b-> C\n</TGT>\nA -f-> C => A -f-> C\nB => B\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"D") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"D")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2")), (String -> Text
pack String
"C", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p3"))]))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"*\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\n*\n</SRC>\n<TGT>\nD -p1-> A -f-> C = D -p3-> C\nD -p2-> B\nX -c-> A\nX -a-> C\nX -b-> C\n</TGT>\n* => A\n"
c2 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"D") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"D")) CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"*", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleColantern :: Sketch Text Text
exampleColantern :: Sketch Text Text
exampleColantern = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"A -q1-> A + B -f-> C = A -q1-> A + B -g-> C\nB -q2-> A + B -f-> C = B -q2-> A + B -g-> C\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA -q1-> A + B -f-> C = A -q1-> A + B -g-> C\nB -q2-> A + B -f-> C = B -q2-> A + B -g-> C\n</TGT>\nA => A\nB => B\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"A + B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A + B")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleCospotlight :: Sketch Text Text
exampleCospotlight :: Sketch Text Text
exampleCospotlight = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"A -f-> B\nA -g-> B\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> B\n</TGT>\nA => A\nB => A\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"B")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleCocrescentMoon :: Sketch Text Text
exampleCocrescentMoon :: Sketch Text Text
exampleCocrescentMoon = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"B -f-> A\nC -g-> A\nB -h-> X\nC -i-> X\nC -j-> X\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nB -f-> A\nC -g-> A\nB -h-> X\nC -i-> X\nC -j-> X\n</TGT>\nA => B\nB => C\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"g"))]))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"*\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\n*\n</SRC>\n<TGT>\nB -f-> A\nC -g-> A\nB -h-> X\nC -i-> X\nC -j-> X\n</TGT>\n* => B\n"
cc2 :: CoconeSketch Text Text
cc2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base2 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"A")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"*", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1,CoconeSketch Text Text
cc2]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchToRealize :: Sketch Text Text
exampleSketchToRealize :: Sketch Text Text
exampleSketchToRealize = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"A -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
"A\nB\n"
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\n</TGT>\nA => B\nB => C\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"f")), (String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"g"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT1 :: Sketch Text Text
exampleSketchSAT1 :: Sketch Text Text
exampleSketchSAT1 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n</TGT>\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"1")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n</TGT>\nA => 1\nB => 1\n"
cc2 :: CoconeSketch Text Text
cc2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base2 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"B")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"V")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"F"))]))
indx3 :: CG
indx3 = String -> CG
unsafeReadCGString String
"A\nB\n"
base3 :: CGD
base3 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n</TGT>\nA => B\nB => B\n"
c3 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"BxB") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx3 CG
cg (String -> Text
pack String
"BxB")) CGD
base3 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc2]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT2 :: Sketch Text Text
exampleSketchSAT2 :: Sketch Text Text
exampleSketchSAT2 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n</TGT>\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"1")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n</TGT>\nA => 1\nB => 1\n"
cc2 :: CoconeSketch Text Text
cc2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base2 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"B")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"V")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"F"))]))
indx3 :: CG
indx3 = String -> CG
unsafeReadCGString String
"A\nB\n"
base3 :: CGD
base3 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n</TGT>\nA => B\nB => B\n"
c3 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"BxB") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx3 CG
cg (String -> Text
pack String
"BxB")) CGD
base3 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc2]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT3 :: Sketch Text Text
exampleSketchSAT3 :: Sketch Text Text
exampleSketchSAT3 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"P&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\nP&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n</TGT>\n"
c1 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"P&Q") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"P&Q")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nP&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n</TGT>\nA => P\nB => Q\n"
c2 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"P&Q") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"P&Q")) CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c1,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set []) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT4 :: Sketch Text Text
exampleSketchSAT4 :: Sketch Text Text
exampleSketchSAT4 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"P -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\nP -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n</TGT>\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"P|Q") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"P|Q")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nP -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n</TGT>\nA => P\nB => Q\n"
cc2 :: CoconeSketch Text Text
cc2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"P|Q") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base2 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"P|Q")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set []) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1,CoconeSketch Text Text
cc2]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT5 :: Sketch Text Text
exampleSketchSAT5 :: Sketch Text Text
exampleSketchSAT5 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"A&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\nA&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n</TGT>\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"A&-A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"A&-A")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\nA&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n</TGT>\nA => A\nB => -A\n"
c3 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"A&-A") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"A&-A")) CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p3")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p4"))]))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT6 :: Sketch Text Text
exampleSketchSAT6 :: Sketch Text Text
exampleSketchSAT6 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"0")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
c2 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"0")) CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1A")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2A"))]))
base3 :: CGD
base3 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
c3 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"0")) CGD
base3 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1B")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2B"))]))
base4 :: CGD
base4 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
c4 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c4 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"0")) CGD
base4 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1C")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2C"))]))
base5 :: CGD
base5 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A\nB => B\n"
cc5 :: CoconeSketch Text Text
cc5 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"-A|B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base5 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"-A|B")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2"))]))
base6 :: CGD
base6 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -B\nB => C\n"
cc6 :: CoconeSketch Text Text
cc6 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"-B|C") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base6 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"-B|C")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q3")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q4"))]))
indx7 :: CG
indx7 = String -> CG
unsafeReadCGString String
"A\nB\nC\nD\n"
base7 :: CGD
base7 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\nC\nD\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A|B\nB => -B|C\nC => A\nD => -C\n"
c7 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c7 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"(-A|B)&(-B|C)&A&-C") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx7 CG
cg (String -> Text
pack String
"(-A|B)&(-B|C)&A&-C")) CGD
base7 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2")),(String -> Text
pack String
"C", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p3")),(String -> Text
pack String
"D", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p4"))]))
base8 :: CGD
base8 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
cc8 :: CoconeSketch Text Text
cc8 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base8 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"1")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1A")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2A"))]))
base9 :: CGD
base9 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
cc9 :: CoconeSketch Text Text
cc9 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base9 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"1")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1B")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2B"))]))
base10 :: CGD
base10 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
cc10 :: CoconeSketch Text Text
cc10 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base10 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"1")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1C")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2C"))]))
c11 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c11 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"1")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c4,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c7,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c11]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1,CoconeSketch Text Text
cc5,CoconeSketch Text Text
cc6,CoconeSketch Text Text
cc8,CoconeSketch Text Text
cc9,CoconeSketch Text Text
cc10]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])
exampleSketchSAT7 :: Sketch Text Text
exampleSketchSAT7 :: Sketch Text Text
exampleSketchSAT7 = Sketch Text Text -> Sketch Text Text
forall a. Simplifiable a => a -> a
simplify Sketch Text Text
result
where
cg :: CG
cg = String -> CG
unsafeReadCGString String
"0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n"
indx1 :: CG
indx1 = String -> CG
unsafeReadCGString String
""
base1 :: CGD
base1 = String -> CGD
unsafeReadCGDString String
"<SRC>\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\n"
cc1 :: CoconeSketch Text Text
cc1 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base1 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"0")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
indx2 :: CG
indx2 = String -> CG
unsafeReadCGString String
"A\nB\n"
base2 :: CGD
base2 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
c2 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"0")) CGD
base2 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1A")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2A"))]))
base3 :: CGD
base3 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
c3 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"0")) CGD
base3 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1B")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2B"))]))
base4 :: CGD
base4 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
c4 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c4 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"0") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"0")) CGD
base4 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1C")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2C"))]))
base5 :: CGD
base5 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A\nB => B\n"
cc5 :: CoconeSketch Text Text
cc5 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"-A|B") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base5 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"-A|B")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2"))]))
base6 :: CGD
base6 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -B\nB => C\n"
cc6 :: CoconeSketch Text Text
cc6 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"-B|C") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base6 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"-B|C")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q3")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q4"))]))
indx7 :: CG
indx7 = String -> CG
unsafeReadCGString String
"A\nB\nC\nD\n"
base7 :: CGD
base7 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\nC\nD\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A|B\nB => -B|C\nC => A\nD => -C\n"
c7 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c7 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"(-A|B)&(-B|C)&A&-C") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx7 CG
cg (String -> Text
pack String
"(-A|B)&(-B|C)&A&-C")) CGD
base7 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p1")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p2")),(String -> Text
pack String
"C", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p3")),(String -> Text
pack String
"D", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"p4"))]))
base8 :: CGD
base8 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
cc8 :: CoconeSketch Text Text
cc8 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base8 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"1")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1A")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2A"))]))
base9 :: CGD
base9 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
cc9 :: CoconeSketch Text Text
cc9 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base9 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"1")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1B")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2B"))]))
base10 :: CGD
base10 = String -> CGD
unsafeReadCGDString String
"<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
cc10 :: CoconeSketch Text Text
cc10 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> CoconeSketch Text Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation CGD
base10 (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx2 CG
cg (String -> Text
pack String
"1")) (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(String -> Text
pack String
"A", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q1C")),(String -> Text
pack String
"B", CG -> Text -> CGMorphism Text Text
forall b a. Eq b => CompositionGraph a b -> b -> CGMorphism a b
unsafeGetMorphismFromLabel CG
cg (String -> Text
pack String
"q2C"))]))
c11 :: Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c11 = Text
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
-> Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone (String -> Text
pack String
"1") (CGD
-> CGD
-> Map Text (CGMorphism Text Text)
-> NaturalTransformation
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (CG -> CG -> Text -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram CG
indx1 CG
cg (String -> Text
pack String
"1")) CGD
base1 (AssociationList Text (CGMorphism Text Text)
-> Map Text (CGMorphism Text Text)
forall k v. AssociationList k v -> Map k v
weakMap []))
result :: Sketch Text Text
result = CG
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
-> Set (CoconeSketch Text Text)
-> Set (TripodSketch Text Text)
-> Sketch Text Text
forall n e.
CategorySketch n e
-> Set (ConeSketch n e)
-> Set (CoconeSketch n e)
-> Set (TripodSketch n e)
-> Sketch n e
unsafeSketch CG
cg ([Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text]
-> Set
(Cone
CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text)
forall a. [a] -> Set a
set [Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c2,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c3,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c4,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c7,Cone CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text
c11]) ([CoconeSketch Text Text] -> Set (CoconeSketch Text Text)
forall a. [a] -> Set a
set [CoconeSketch Text Text
cc1,CoconeSketch Text Text
cc5,CoconeSketch Text Text
cc6,CoconeSketch Text Text
cc8,CoconeSketch Text Text
cc9,CoconeSketch Text Text
cc10]) ([TripodSketch Text Text] -> Set (TripodSketch Text Text)
forall a. [a] -> Set a
set [])