{-| Module : FiniteCategories Description : An exemple of 'leftAdjoint' and 'rightAdjoint' use exported with GraphViz. Copyright : Guillaume Sabbagh 2022 License : GPL-3 Maintainer : guillaumesabbagh@protonmail.com Stability : experimental Portability : portable An exemple of 'leftAdjoint' and 'rightAdjoint' use exported with GraphViz. Export the lim functor of a discrete 'Diagram' in 'Ens' in the directory "OutputGraphViz\/Examples\/Functor\/Adjunction". -} module Math.Functors.Adjunction.Example ( main ) where import Math.FiniteCategory import Math.FiniteCategories.Ens import Math.FiniteCategories.DiscreteCategory import Math.Categories.FunctorCategory import Math.Functors.Adjunction import Math.Functors.DiagonalFunctor import Math.IO.FiniteCategories.ExportGraphViz 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 -- | An exemple of 'leftAdjoint' and 'rightAdjoint' use exported with GraphViz. main :: IO () main = do putStrLn "Start of Math.Functors.Adjunction.Example" let universe = ens $ set [set [1 :: Int], set [3,4]] let indexing = discreteCategory $ set [0 :: Int,1] let diagFunct = diagonalFunctor indexing universe let leftAdj = leftAdjoint diagFunct let rightAdj = rightAdjoint diagFunct catToPdf universe "OutputGraphViz/Examples/Functors/Adjunction/ens" catToPdf indexing "OutputGraphViz/Examples/Functors/Adjunction/indexing" diagToPdf2 (fst.anElement.(Map.mapToSet).omap $ leftAdj) "OutputGraphViz/Examples/Functors/Adjunction/diag" diagToPdf2 (selectObject universe (snd.anElement.(Map.mapToSet).omap $ leftAdj)) "OutputGraphViz/Examples/Functors/Adjunction/limit" putStrLn "End of Math.Functors.Adjunction.Example"