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

Examples of Kan extensions of set-valued functors pretty printed.


-}
module Math.Functors.SetValued.Example
(
    main
)
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                (pack)
    

    
    -- | Examples of Kan extensions of set-valued functors pretty printed.
    main :: IO ()
    main = do
        putStrLn "Start of Math.Functors.SetValued.Example"
        let Right c1 = readSCGString "2\nA -f-> B\nC -g-> B\n"
        putStrLn $ pprintFiniteCategory c1 
        let Right c2 = readSCGString "2\nA -f-> B\nC -g-> B\nB -h-> C\nA -i-> C\nC -g-> B -h-> C = <ID>\nB -h-> C -g-> B = <ID>\nA -i-> C -g-> B = A -f-> B\nA -f-> B -h-> C = A -i-> C\n"
        putStrLn $ pprintFiniteCategory c2 
        let Right f = readSCGDString "<SRC>\n2\nA -f-> B\nC -g-> B\n</SRC>\n<TGT>\n2\nA -f-> B\nC -g-> B\nB -h-> C\nA -i-> C\nC -g-> B -h-> C = <ID>\nB -h-> C -g-> B = <ID>\nA -i-> C -g-> B = A -f-> B\nA -f-> B -h-> C = A -i-> C\n</TGT>\nA -f-> B => A -f-> B\nC -g-> B => C -g-> B\n"
        putStrLn $ pprint f 
        let x = completeDiagram Diagram{src=c1,tgt=FinSet,omap=weakMap [(pack "A",set [1 :: Int]),(pack "B",set [2,3]),(pack "C",set [4,5])], mmap= weakMap [(anElement (genAr c1 (pack "A") (pack "B")),Function{function=weakMap [(1,2)], codomain = set [2,3]}),(anElement (genAr c1 (pack "C") (pack "B")),Function{function=weakMap [(4,2),(5,3)], codomain = set [2,3]})]}
        putStrLn $ pprint (fullDiagram2 x) 
        let (ran, epsilon) = rightKanSetValued f x
        putStrLn $ pprint (fullDiagram2 ran) 
        putStrLn $ pprint (fullDiagram2 ran)
        putStrLn $ pprint (fullNaturalTransformation2 epsilon)
        let (lan, eta) = leftKanSetValued f x
        putStrLn $ pprint (fullDiagram2 lan) 
        putStrLn $ pprint (fullDiagram2 lan)
        putStrLn $ pprint (fullNaturalTransformation2 eta) 
        putStrLn "End of Math.Functors.SetValued.Example"