FiniteCategories 0.6.0.0 → 0.6.0.1
raw patch · 8 files changed
+147/−5 lines, 8 filesPVP: minor bump suggested
API additions: PVP suggests at least a minor version bump
API changes (from Hackage documentation)
+ Math.FiniteCategories.FinSketch.Examples: exampleSketchSAT1 :: Sketch Text Text
+ Math.FiniteCategories.FinSketch.Examples: exampleSketchSAT2 :: Sketch Text Text
+ Math.FiniteCategories.FinSketch.Examples: exampleSketchSAT3 :: Sketch Text Text
+ Math.FiniteCategories.FinSketch.Examples: exampleSketchSAT4 :: Sketch Text Text
+ Math.FiniteCategories.FinSketch.Examples: exampleSketchSAT5 :: Sketch Text Text
+ Math.FiniteCategories.FinSketch.Examples: exampleSketchSAT6 :: Sketch Text Text
Files
- CHANGELOG.md +5/−1
- FiniteCategories.cabal +1/−1
- src/Math/Categories/FunctorCategory.hs +1/−1
- src/Math/FiniteCategories/DiscreteTwo.hs +1/−0
- src/Math/FiniteCategories/ExponentialCategory.hs +5/−1
- src/Math/FiniteCategories/FinSketch/Examples.hs +132/−1
- src/Math/FiniteCategories/LimitCategory/Examples.hs +1/−0
- src/Math/IO/PrettyPrint.hs +1/−0
CHANGELOG.md view
@@ -26,4 +26,8 @@ ## 0.6.0.0 -- 2024-01-11 -* Sketches, (co)complete categories and cartesian closed categories.+* Sketches, (co)complete categories and cartesian closed categories. + +## 0.6.0.1 -- 2024-01-14 + +* Correct bug in completeDiagram.
FiniteCategories.cabal view
@@ -14,7 +14,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change -version: 0.6.0.0 +version: 0.6.0.1 -- A short (one-line) description of the package. synopsis: Finite categories and usual categorical constructions on them.
src/Math/Categories/FunctorCategory.hs view
@@ -269,7 +269,7 @@ Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 completeDiagram Diagram{src=s,tgt=t,omap=om,mmap=mm} = Diagram{src=s,tgt=t,omap=newMapObj, mmap=Map.unions [mm, mapId] } where - mapId = weakMapFromSet [(identity s o, identity t (newMapObj |!| o)) | o <- ob s] + mapId = weakMapFromSet [(identity s o, identity t (newMapObj |!| o)) | o <- ob s, o `isIn` (keys' newMapObj)] mapSrc = weakMap [(source f1, source f2) | (f1,f2) <- (Map.mapToList mm)] mapTgt= weakMap [(target f1, target f2) | (f1,f2) <- (Map.mapToList mm)] newMapObj = Map.unions [om, mapSrc, mapTgt]
src/Math/FiniteCategories/DiscreteTwo.hs view
@@ -40,6 +40,7 @@ -- It has two constructors 'A' and 'B'. data DiscreteTwoOb = A | B deriving (Eq, Show, Generic, PrettyPrint, Simplifiable) + -- | There are two identities corresponding to 'A' and 'B'. type DiscreteTwoAr = DiscreteTwoOb instance Morphism DiscreteTwoOb DiscreteTwoOb where
src/Math/FiniteCategories/ExponentialCategory.hs view
@@ -102,13 +102,17 @@ ob (ExprojectedCategory cat) = ExprojectedObject <$> ob cat ob (ExponentialCategory functCat) = ExponentialElementObject <$> ob functCat - type TwoProductOfCategories c m o = FinCat (LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o) (Limit DiscreteTwoOb m) (Limit DiscreteTwoOb o) type TwoProductOfCategoriesMorphism c m o = FinFunctor (LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o) (Limit DiscreteTwoOb m) (Limit DiscreteTwoOb o) type TwoProductOfCategoriesObject c m o = LimitCategory DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o + -- | The type of the category containing categories and their exponential objects. type CartesianCategory c m o = TwoProductOfCategories (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) + + -- | A morphism in 'CartesianCategory'. type CartesianMorphism c m o = TwoProductOfCategoriesMorphism (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) + + -- | An object in 'CartesianCategory'. type CartesianObject c m o = TwoProductOfCategoriesObject (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => CartesianClosedCategory (FinCat c m o) (FinFunctor c m o) c (TwoProductOfCategories c m o) (TwoProductOfCategoriesMorphism c m o) (TwoProductOfCategoriesObject c m o) (CartesianCategory c m o) (CartesianMorphism c m o) (CartesianObject c m o) where
src/Math/FiniteCategories/FinSketch/Examples.hs view
@@ -27,6 +27,13 @@ exampleCocrescentMoon, exampleNoCrescentMoon, exampleSketchToRealize, + exampleSketchSAT1, + exampleSketchSAT2, + exampleSketchSAT3, + exampleSketchSAT4, + exampleSketchSAT5, + exampleSketchSAT6, + ) where import qualified Data.WeakSet as Set @@ -222,4 +229,128 @@ result = unsafeSketch cg (set [c1]) (set []) (set []) - + exampleSketchSAT1 :: Sketch Text Text + exampleSketchSAT1 = simplify result + where + cg = unsafeReadCGString "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 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<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 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCocone (pack "B") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "V")),(pack "B", unsafeGetMorphismFromLabel cg (pack "F"))])) + indx3 = unsafeReadCGString "A\nB\n" + base3 = unsafeReadCGDString "<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 = unsafeCone (pack "BxB") (unsafeNaturalTransformation (constantDiagram indx3 cg (pack "BxB")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))])) + result = unsafeSketch cg (set [c1,c3]) (set [cc2]) (set []) + + exampleSketchSAT2 :: Sketch Text Text + exampleSketchSAT2 = simplify result + where + cg = unsafeReadCGString "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 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<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 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCocone (pack "B") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "V")),(pack "B", unsafeGetMorphismFromLabel cg (pack "F"))])) + indx3 = unsafeReadCGString "A\nB\n" + base3 = unsafeReadCGDString "<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 = unsafeCone (pack "BxB") (unsafeNaturalTransformation (constantDiagram indx3 cg (pack "BxB")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))])) + result = unsafeSketch cg (set [c1,c3]) (set [cc2]) (set []) + + exampleSketchSAT3 :: Sketch Text Text + exampleSketchSAT3 = simplify result + where + cg = unsafeReadCGString "P&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n" + indx1 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\nP&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n</TGT>\n" + c1 = unsafeCone (pack "P&Q") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "P&Q")) base1 (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCone (pack "P&Q") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "P&Q")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))])) + result = unsafeSketch cg (set [c1,c2]) (set []) (set []) + + exampleSketchSAT4 :: Sketch Text Text + exampleSketchSAT4 = simplify result + where + cg = unsafeReadCGString "P -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n" + indx1 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\nP -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n</TGT>\n" + cc1 = unsafeCocone (pack "P|Q") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "P|Q")) (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCocone (pack "P|Q") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "P|Q")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))])) + result = unsafeSketch cg (set []) (set [cc1,cc2]) (set []) + + exampleSketchSAT5 :: Sketch Text Text + exampleSketchSAT5 = simplify result + where + cg = unsafeReadCGString "A&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n" + indx1 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<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 = unsafeCocone (pack "A&-A") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "A&-A")) (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCone (pack "A&-A") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "A&-A")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p3")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p4"))])) + result = unsafeSketch cg (set [c3]) (set [cc1]) (set []) + + exampleSketchSAT6 :: Sketch Text Text + exampleSketchSAT6 = simplify result + where + cg = unsafeReadCGString "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 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<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 = unsafeCocone (pack "0") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "0")) (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2A"))])) + base3 = unsafeReadCGDString "<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 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2B"))])) + base4 = unsafeReadCGDString "<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 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base4 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2C"))])) + base5 = unsafeReadCGDString "<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 = unsafeCocone (pack "-A|B") (unsafeNaturalTransformation base5 (constantDiagram indx2 cg (pack "-A|B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))])) + base6 = unsafeReadCGDString "<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 = unsafeCocone (pack "-B|C") (unsafeNaturalTransformation base6 (constantDiagram indx2 cg (pack "-B|C")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q3")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q4"))])) + indx7 = unsafeReadCGString "A\nB\nC\nD\n" + base7 = unsafeReadCGDString "<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 = unsafeCone (pack "(-A|B)&(-B|C)&A&-C") (unsafeNaturalTransformation (constantDiagram indx7 cg (pack "(-A|B)&(-B|C)&A&-C")) base7 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2")),(pack "C", unsafeGetMorphismFromLabel cg (pack "p3")),(pack "D", unsafeGetMorphismFromLabel cg (pack "p4"))])) + base8 = unsafeReadCGDString "<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 = unsafeCocone (pack "1") (unsafeNaturalTransformation base8 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2A"))])) + base9 = unsafeReadCGDString "<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 = unsafeCocone (pack "1") (unsafeNaturalTransformation base9 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2B"))])) + base10 = unsafeReadCGDString "<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 = unsafeCocone (pack "1") (unsafeNaturalTransformation base10 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2C"))])) + c11 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap [])) + result = unsafeSketch cg (set [c2,c3,c4,c7,c11]) (set [cc1,cc5,cc6,cc8,cc9,cc10]) (set []) + + exampleSketchSAT7 :: Sketch Text Text + exampleSketchSAT7 = simplify result + where + cg = unsafeReadCGString "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 = unsafeReadCGString "" + base1 = unsafeReadCGDString "<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 = unsafeCocone (pack "0") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "0")) (weakMap [])) + indx2 = unsafeReadCGString "A\nB\n" + base2 = unsafeReadCGDString "<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 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2A"))])) + base3 = unsafeReadCGDString "<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 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2B"))])) + base4 = unsafeReadCGDString "<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 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base4 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2C"))])) + base5 = unsafeReadCGDString "<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 = unsafeCocone (pack "-A|B") (unsafeNaturalTransformation base5 (constantDiagram indx2 cg (pack "-A|B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))])) + base6 = unsafeReadCGDString "<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 = unsafeCocone (pack "-B|C") (unsafeNaturalTransformation base6 (constantDiagram indx2 cg (pack "-B|C")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q3")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q4"))])) + indx7 = unsafeReadCGString "A\nB\nC\nD\n" + base7 = unsafeReadCGDString "<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 = unsafeCone (pack "(-A|B)&(-B|C)&A&-C") (unsafeNaturalTransformation (constantDiagram indx7 cg (pack "(-A|B)&(-B|C)&A&-C")) base7 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2")),(pack "C", unsafeGetMorphismFromLabel cg (pack "p3")),(pack "D", unsafeGetMorphismFromLabel cg (pack "p4"))])) + base8 = unsafeReadCGDString "<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 = unsafeCocone (pack "1") (unsafeNaturalTransformation base8 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2A"))])) + base9 = unsafeReadCGDString "<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 = unsafeCocone (pack "1") (unsafeNaturalTransformation base9 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2B"))])) + base10 = unsafeReadCGDString "<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 = unsafeCocone (pack "1") (unsafeNaturalTransformation base10 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2C"))])) + c11 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap [])) + result = unsafeSketch cg (set [c2,c3,c4,c7,c11]) (set [cc1,cc5,cc6,cc8,cc9,cc10]) (set [])
src/Math/FiniteCategories/LimitCategory/Examples.hs view
@@ -27,6 +27,7 @@ import Math.FiniteCategories.V import Math.FiniteCategories.CompositionGraph + -- | An example of 'Diagram' from 'V' to 'FinCat'. exampleDiagramVToFinCat :: Diagram V VAr VOb (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text) (FinFunctor (CompositionGraph Text Text) (CGMorphism Text Text) Text) (CompositionGraph Text Text) exampleDiagramVToFinCat = completeDiagram diag where
src/Math/IO/PrettyPrint.hs view
@@ -72,6 +72,7 @@ ppi :: (PrettyPrint a) => Int -> a -> IO () ppi v a = putStrLn $ pprintIndent v a + -- | Add indentation at the begining of a string. indentation :: Int -> String -> String indentation i s = concat $ replicate i s