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

An example of adjunction.
-}
module ExampleAdjunction.ExampleAdjunction
(
    main
)
where
    import              ExportGraphViz.ExportGraphViz          (catToPdf,genToPdf, diagToPdf, diagToPdf2, natToPdf)
    import              Diagram.Diagram
    import              Limit.Limit
    import              UsualCategories.DiscreteCategory
    import              Utils.AssociationList
    import              CompositionGraph.CompositionGraph
    import              IO.Parsers.Lexer
    import              IO.Parsers.SafeCompositionGraph
    import              IO.Parsers.SafeCompositionGraphFunctor
    import              FunctorCategory.FunctorCategory
    import              FiniteCategory.FiniteCategory
    import              ConeCategory.ConeCategory
    
    -- | Export the categories defined above as pdf with GraphViz.
    main = do
        putStrLn "Start of ExampleAdjunction"
        cg <- readSCGFile "test/ExampleAdjunction/ExampleAdjunction.scg"
        catToPdf cg "OutputGraphViz/Examples/Adjunction/category"
        diag1 <- readFSCGFile "test/ExampleAdjunction/ExampleAdjunctionDiag1.fscg"
        diagToPdf2 diag1 "OutputGraphViz/Examples/Adjunction/diag1"
        diag2 <- readFSCGFile "test/ExampleAdjunction/ExampleAdjunctionDiag2.fscg"
        diagToPdf2 diag2 "OutputGraphViz/Examples/Adjunction/diag2"
        catToPdf (mkConeCategory diag1) "OutputGraphViz/Examples/Adjunction/coneCat1"
        catToPdf (mkConeCategory diag2) "OutputGraphViz/Examples/Adjunction/coneCat2"
        putStrLn $ show $ (omap (limitFunctor (src diag1) (tgt diag1))) !-! diag1
        putStrLn $ show $ (omap (limitFunctor (src diag2) (tgt diag2))) !-! diag2
        putStrLn $ show $ (mmap (limitFunctor (src diag1) (tgt diag1))) !-! (head (ar FunctorCategory{sourceCat = src diag1, targetCat = tgt diag1} diag1 diag2))
        putStrLn "End of ExampleAdjunction"