FiniteCategories-0.3.0.0: src/Math/Functors/SetValued/Example.hs
{-| 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"