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

Examples of 'LimitCategory'.
-}
module Math.FiniteCategories.LimitCategory.Examples
(
    exampleDiagramVToFinCat,
    exampleLimitCategoryOfCompositionGraphs,
    exampleLimitOfCompositionGraphs,
)
where
    import Data.WeakSet.Safe
    import Data.WeakMap.Safe
    import Data.Text (pack, Text)
    
    import Math.CompleteCategory
    import Math.Categories.FunctorCategory
    import Math.Categories.ConeCategory
    import Math.Categories.FinCat
    import Math.FiniteCategories.LimitCategory
    import Math.FiniteCategories.V
    import Math.FiniteCategories.CompositionGraph
    
    -- | An example of 'Diagram' from 'V' to 'FinCat'.

    exampleDiagramVToFinCat :: Diagram V VAr VOb (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text) (FinFunctor (CompositionGraph Text Text) (CGMorphism Text Text) Text) (CompositionGraph Text Text)
    exampleDiagramVToFinCat :: Diagram
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
exampleDiagramVToFinCat = Diagram
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> Diagram
     V
     VAr
     VOb
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph 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
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
forall {c} {m} {o}.
Diagram V VAr VOb (FinCat c m o) CGD (CompositionGraph Text Text)
diag
        where
            Right CompositionGraph Text Text
cg1 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"A -f-> B\nB -i-> D\nA -g-> C\nC -h-> D"
            Right CompositionGraph Text Text
cg2 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"F -j-> G"
            Right CompositionGraph Text Text
cg3 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"H -k-> I\nH -l-> I"
            Right CGD
diag1 = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nA -f-> B\nB -i-> D\nA -g-> C\nC -h-> D\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nB => H\nC => H\nA -f-> B => <ID>\nA -g-> C => <ID>\nB -i-> D => H -k-> I\nC -h-> D => H -l-> I\nA => H\n"
            Right CGD
diag2 = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nF -j-> G\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nF -j-> G => H -k-> I\n"
            diag :: Diagram V VAr VOb (FinCat c m o) CGD (CompositionGraph Text Text)
diag = Diagram {src :: V
src = V
V, tgt :: FinCat c m o
tgt = FinCat c m o
forall c m o. FinCat c m o
FinCat, omap :: Map VOb (CompositionGraph Text Text)
omap = AssociationList VOb (CompositionGraph Text Text)
-> Map VOb (CompositionGraph Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(VOb
VA,CompositionGraph Text Text
cg3),(VOb
VB,CompositionGraph Text Text
cg1),(VOb
VC,CompositionGraph Text Text
cg2)], mmap :: Map VAr CGD
mmap = AssociationList VAr CGD -> Map VAr CGD
forall k v. AssociationList k v -> Map k v
weakMap [(VAr
VF, CGD
diag1),(VAr
VG, CGD
diag2)]}
    
    -- | An example of 'LimitCategory' of 'CompositionGraph's.

    exampleLimitCategoryOfCompositionGraphs :: LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text
    exampleLimitCategoryOfCompositionGraphs :: LimitCategory
  V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text
exampleLimitCategoryOfCompositionGraphs = Diagram
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> LimitCategory
     V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text
forall cIndex mIndex oIndex c m o.
Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> LimitCategory cIndex mIndex oIndex c m o
LimitCategory (Diagram
   V
   VAr
   VOb
   (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
   CGD
   (CompositionGraph Text Text)
 -> LimitCategory
      V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
-> Diagram
     V
     VAr
     VOb
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph Text Text)
-> LimitCategory
     V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text
forall a b. (a -> b) -> a -> b
$ Diagram
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> Diagram
     V
     VAr
     VOb
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph 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
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
forall {c} {m} {o}.
Diagram V VAr VOb (FinCat c m o) CGD (CompositionGraph Text Text)
diag
        where
            Right CompositionGraph Text Text
cg1 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"A -f-> B\nB -i-> D\nA -g-> C\nC -h-> D"
            Right CompositionGraph Text Text
cg2 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"F -j-> G"
            Right CompositionGraph Text Text
cg3 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"H -k-> I\nH -l-> I"
            Right CGD
diag1 = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nA -f-> B\nB -i-> D\nA -g-> C\nC -h-> D\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nB => H\nC => H\nA -f-> B => <ID>\nA -g-> C => <ID>\nB -i-> D => H -k-> I\nC -h-> D => H -l-> I\nA => H\n"
            Right CGD
diag2 = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nF -j-> G\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nF -j-> G => H -k-> I\n"
            diag :: Diagram V VAr VOb (FinCat c m o) CGD (CompositionGraph Text Text)
diag = Diagram {src :: V
src = V
V, tgt :: FinCat c m o
tgt = FinCat c m o
forall c m o. FinCat c m o
FinCat, omap :: Map VOb (CompositionGraph Text Text)
omap = AssociationList VOb (CompositionGraph Text Text)
-> Map VOb (CompositionGraph Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(VOb
VA,CompositionGraph Text Text
cg3),(VOb
VB,CompositionGraph Text Text
cg1),(VOb
VC,CompositionGraph Text Text
cg2)], mmap :: Map VAr CGD
mmap = AssociationList VAr CGD -> Map VAr CGD
forall k v. AssociationList k v -> Map k v
weakMap [(VAr
VF, CGD
diag1),(VAr
VG, CGD
diag2)]}
            
    -- | Same example as 'exampleLimitCategoryOfCompositionGraphs' but the complete 'Cone'.

    exampleLimitOfCompositionGraphs :: Cone V VAr VOb (FinCat (LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text) (Limit VOb (CGMorphism Text Text)) (Limit VOb Text)) (FinFunctor (LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text) (Limit VOb (CGMorphism Text Text)) (Limit VOb Text)) (LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
    exampleLimitOfCompositionGraphs :: Cone
  V
  VAr
  VOb
  (FinCat
     (LimitCategory
        V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     (Limit VOb (CGMorphism Text Text))
     (Limit VOb Text))
  (FinFunctor
     (LimitCategory
        V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     (Limit VOb (CGMorphism Text Text))
     (Limit VOb Text))
  (LimitCategory
     V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
exampleLimitOfCompositionGraphs = Diagram
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> Cone
     V
     VAr
     VOb
     (FinCat
        (LimitCategory
           V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
        (Limit VOb (CGMorphism Text Text))
        (Limit VOb Text))
     (FinFunctor
        (LimitCategory
           V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
        (Limit VOb (CGMorphism Text Text))
        (Limit VOb Text))
     (LimitCategory
        V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
forall c m o cLim mLim oLim cIndex mIndex oIndex.
(CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex c m o
-> Cone cIndex mIndex oIndex cLim mLim oLim
limit (Diagram
   V
   VAr
   VOb
   (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
   CGD
   (CompositionGraph Text Text)
 -> Cone
      V
      VAr
      VOb
      (FinCat
         (LimitCategory
            V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
         (Limit VOb (CGMorphism Text Text))
         (Limit VOb Text))
      (FinFunctor
         (LimitCategory
            V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
         (Limit VOb (CGMorphism Text Text))
         (Limit VOb Text))
      (LimitCategory
         V
         VAr
         VOb
         (CompositionGraph Text Text)
         (CGMorphism Text Text)
         Text))
-> Diagram
     V
     VAr
     VOb
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph Text Text)
-> Cone
     V
     VAr
     VOb
     (FinCat
        (LimitCategory
           V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
        (Limit VOb (CGMorphism Text Text))
        (Limit VOb Text))
     (FinFunctor
        (LimitCategory
           V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
        (Limit VOb (CGMorphism Text Text))
        (Limit VOb Text))
     (LimitCategory
        V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
forall a b. (a -> b) -> a -> b
$ Diagram
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> Diagram
     V
     VAr
     VOb
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph 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
  V
  VAr
  VOb
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
forall {c} {m} {o}.
Diagram V VAr VOb (FinCat c m o) CGD (CompositionGraph Text Text)
diag
        where
            Right CompositionGraph Text Text
cg1 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"A -f-> B\nB -i-> D\nA -g-> C\nC -h-> D"
            Right CompositionGraph Text Text
cg2 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"F -j-> G"
            Right CompositionGraph Text Text
cg3 = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"H -k-> I\nH -l-> I"
            Right CGD
diag1 = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nA -f-> B\nB -i-> D\nA -g-> C\nC -h-> D\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nB => H\nC => H\nA -f-> B => <ID>\nA -g-> C => <ID>\nB -i-> D => H -k-> I\nC -h-> D => H -l-> I\nA => H\n"
            Right CGD
diag2 = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nF -j-> G\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nF -j-> G => H -k-> I\n"
            diag :: Diagram V VAr VOb (FinCat c m o) CGD (CompositionGraph Text Text)
diag = Diagram {src :: V
src = V
V, tgt :: FinCat c m o
tgt = FinCat c m o
forall c m o. FinCat c m o
FinCat, omap :: Map VOb (CompositionGraph Text Text)
omap = AssociationList VOb (CompositionGraph Text Text)
-> Map VOb (CompositionGraph Text Text)
forall k v. AssociationList k v -> Map k v
weakMap [(VOb
VA,CompositionGraph Text Text
cg3),(VOb
VB,CompositionGraph Text Text
cg1),(VOb
VC,CompositionGraph Text Text
cg2)], mmap :: Map VAr CGD
mmap = AssociationList VAr CGD -> Map VAr CGD
forall k v. AssociationList k v -> Map k v
weakMap [(VAr
VF, CGD
diag1),(VAr
VG, CGD
diag2)]}