{-| Module  : FiniteCategories
Description : Examples of Kan extensions of set-valued functors.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of Kan extensions of set-valued functors.

Kan extensions of set-valued functors are useful for the study of models of linear sketches.
-}
module Math.Functors.SetValued.Examples
(
    exampleSetValuedLeftKanExtension,
    exampleSetValuedRightKanExtension,
)
where
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint
    import              Math.FiniteCategories
    import              Math.Categories.FinSet
    import              Math.Functors.SetValued

    
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap             (Map)
    import qualified    Data.WeakMap           as Map
    import              Data.WeakMap.Safe
    
    import              Data.Text                (Text, pack)
    

    -- | Computes the left Kan extension of a set-valued model to compute the pseudo-inverse of a function.

    exampleSetValuedLeftKanExtension :: (Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (FinSet (ColimitObject Text (CGMorphism Text Text) Int)) (Function (ColimitObject Text (CGMorphism Text Text) Int)) (Set (ColimitObject Text (CGMorphism Text Text) Int)), NaturalTransformation (CompositionGraph Text Text) (CGMorphism Text Text) Text (FinSet (ColimitObject Text (CGMorphism Text Text) Int)) (Function (ColimitObject Text (CGMorphism Text Text) Int)) (Set (ColimitObject Text (CGMorphism Text Text) Int))) 
    exampleSetValuedLeftKanExtension :: (Diagram
   (CompositionGraph Text Text)
   (CGMorphism Text Text)
   Text
   (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
   (Function (ColimitObject Text (CGMorphism Text Text) Int))
   (Set (ColimitObject Text (CGMorphism Text Text) Int)),
 NaturalTransformation
   (CompositionGraph Text Text)
   (CGMorphism Text Text)
   Text
   (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
   (Function (ColimitObject Text (CGMorphism Text Text) Int))
   (Set (ColimitObject Text (CGMorphism Text Text) Int)))
exampleSetValuedLeftKanExtension = (Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
  (Function (ColimitObject Text (CGMorphism Text Text) Int))
  (Set (ColimitObject Text (CGMorphism Text Text) Int))
lan,NaturalTransformation
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
  (Function (ColimitObject Text (CGMorphism Text Text) Int))
  (Set (ColimitObject Text (CGMorphism Text Text) Int))
eta)
        where
            Right CompositionGraph Text Text
a = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"A -f-> B\n"
            Right CompositionGraph Text Text
b = String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
"A -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
            Right CGD
f = String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
"<SRC>\nA -f-> B\n</SRC>\n<TGT>\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n</TGT>\nA -f-> B => A -f-> B\n"
            x :: Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet Int)
  (Function Int)
  (Set Int)
x = Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet Int)
  (Function Int)
  (Set Int)
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (FinSet Int)
     (Function Int)
     (Set Int)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph Text Text
src = CompositionGraph Text Text
a, tgt :: FinSet Int
tgt = FinSet Int
forall a. FinSet a
FinSet, omap :: Map Text (Set Int)
omap = AssociationList Text (Set Int) -> Map Text (Set Int)
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map (CGMorphism Text Text) (Function Int)
mmap = AssociationList (CGMorphism Text Text) (Function Int)
-> Map (CGMorphism Text Text) (Function Int)
forall k v. AssociationList k v -> Map k v
weakMap [(Set (CGMorphism Text Text) -> CGMorphism Text Text
forall a. Set a -> a
anElement (CompositionGraph Text Text
-> Text -> Text -> Set (CGMorphism Text Text)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar CompositionGraph Text Text
a (String -> Text
pack String
"A") (String -> Text
pack String
"B")),Function{function :: Map Int Int
function=AssociationList Int Int -> Map Int Int
forall k v. AssociationList k v -> Map k v
weakMap [(Int
1,Int
3),(Int
2,Int
3)], codomain :: Set Int
codomain = [Int] -> Set Int
forall a. [a] -> Set a
set [Int
3,Int
4]})]}
            (Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
  (Function (ColimitObject Text (CGMorphism Text Text) Int))
  (Set (ColimitObject Text (CGMorphism Text Text) Int))
lan,NaturalTransformation
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
  (Function (ColimitObject Text (CGMorphism Text Text) Int))
  (Set (ColimitObject Text (CGMorphism Text Text) Int))
eta) = CGD
-> Diagram
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (FinSet Int)
     (Function Int)
     (Set Int)
-> (Diagram
      (CompositionGraph Text Text)
      (CGMorphism Text Text)
      Text
      (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
      (Function (ColimitObject Text (CGMorphism Text Text) Int))
      (Set (ColimitObject Text (CGMorphism Text Text) Int)),
    NaturalTransformation
      (CompositionGraph Text Text)
      (CGMorphism Text Text)
      Text
      (FinSet (ColimitObject Text (CGMorphism Text Text) Int))
      (Function (ColimitObject Text (CGMorphism Text Text) Int))
      (Set (ColimitObject Text (CGMorphism Text Text) Int)))
forall c1 m1 o1 c2 m2 o2 a.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a)
-> (Diagram
      c2
      m2
      o2
      (FinSet (ColimitObject o1 m2 a))
      (Function (ColimitObject o1 m2 a))
      (Set (ColimitObject o1 m2 a)),
    NaturalTransformation
      c1
      m1
      o1
      (FinSet (ColimitObject o1 m2 a))
      (Function (ColimitObject o1 m2 a))
      (Set (ColimitObject o1 m2 a)))
leftKanSetValued CGD
f Diagram
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (FinSet Int)
  (Function Int)
  (Set Int)
x
    
    -- | Computes the right Kan extension of a set-valued model to compute the pseudo-inverse of a function.

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