{-| 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 = (lan,eta)
        where
            Right a = readCGString "A -f-> B\n"
            Right b = readCGString "A -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
            Right f = readCGDString "<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 = completeDiagram Diagram{src = a, tgt = FinSet, omap = weakMap [], mmap = weakMap [(anElement (ar a (pack "A") (pack "B")),Function{function=weakMap [(1,3),(2,3)], codomain = set [3,4]})]}
            (lan,eta) = leftKanSetValued f 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 = (ran,epsilon)
        where
            Right a = readCGString "A -f-> B\n"
            Right b = readCGString "A -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
            Right f = readCGDString "<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 = completeDiagram Diagram{src = a, tgt = FinSet, omap = weakMap [], mmap = weakMap [(anElement (ar a (pack "A") (pack "B")),Function{function=weakMap [(1,3),(2,3)], codomain = set [3,4]})]}
            (ran,epsilon) = rightKanSetValued f x