ExampleColimit.hs

{-| Module  : FiniteCategories
Description : An example of colimits of a diagram.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An example of colimits of a diagram.
-}
module ExampleConeCategory.ExampleColimit
(
    main
)
where
    import              RandomCompositionGraph.RandomCompositionGraph
    import              System.Random                                   
    import              ExportGraphViz.ExportGraphViz
    import              FiniteCategory.FiniteCategory
    import              FunctorCategory.FunctorCategory
    import              Diagram.Diagram
    import              UsualCategories.Three
    import              Utils.Sample
    import              ConeCategory.ConeCategory

    (rcg,newGen) = (mkRandomCompositionGraph 20 25 5 (mkStdGen 878))
    
    (diag,newGen1) = (pickOne (ob FunctorCategory{sourceCat=Three, targetCat=rcg}) newGen)
    
    colimit = colimits diag
    
    recuNatToPdf [] = putStrLn "End of natural transformation export"
    recuNatToPdf (x:xs) = do
                            natToPdf (coconeToNaturalTransformation x) ("OutputGraphViz/Examples/ConeCategory/Colimit/nat"++show (length xs))
                            putStrLn $ show $ (naturalTransformationToCocone (coconeToNaturalTransformation x)) == x
                            recuNatToPdf xs

    -- | Export the colimits as a pdf with GraphViz.
    main = do 
        putStrLn "Start of ExampleColimit"
        catToPdf rcg "OutputGraphViz/Examples/ConeCategory/Colimit/rcg"
        diagToPdf diag "OutputGraphViz/Examples/ConeCategory/Colimit/funct"
        diagToPdf2 diag "OutputGraphViz/Examples/ConeCategory/Colimit/diag"
        recuNatToPdf colimit
        putStrLn "End of ExampleColimit"