{-| Module  : FiniteCategories
Description : Examples of 'Sketch'es.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of 'Sketch'es.
-}
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
    
    -- | The 'Sketch' of the magma structure.

    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 [])
            
    -- | The 'Sketch' of the unital magma structure. A unital magma is a magma with an identity.

    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 [])
            
    -- | The inclusion sketch morphism from the sketch of magmas to the sketch of unital magmas.

    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
            
    -- | The sketch of graphs.

    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 [])
            
    -- | The sketch of pointed sets.

    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 [])
   
    -- |  A sketch with just one object and no (co)cone.     

    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 [])
            
    -- | A diagram selecting 'exampleSketchAtomic', 'exampleSketchPointedSet' and 'exampleSketchGraph' so that its colimit is the sketch of graphs with a distinguished edge.

    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)]}
    
    
    -- | A sketch with a single object and a loop. This sketch is infinite because of the loop.

    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 [])
            
    -- | A diagram selecting 'exampleSketchAtomic', 'exampleSketchPointedSet' and 'exampleSketchLoop' so that its colimit is the sketch of discrete systems.

    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)]}
            
            
    -- | An example of 'Sketch' containing a 'Lantern'.        

    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 [])
    
    -- | An example of 'Sketch' containing a 'Spotlight'.     

    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 [])
            
    -- | An example of 'Sketch' containing a 'CrescentMoon'. 

    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 [])
            
    -- | An example of 'Sketch' containing no 'CrescentMoon' but in a tricky way. 

    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 [])
    

    -- | An example of 'Sketch' containing a 'Colantern'. 

    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 [])
    
    -- | An example of 'Sketch' containing a 'Cospotlight'. 

    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 [])
        
    -- | An example of 'Sketch' containing a 'CocrescentMoon'. 

    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 [])
            
    
    -- | An example of 'Sketch' to realize.

    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 [])