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

An example of Yoneda embedding.
-}
module ExampleYonedaEmbedding.ExampleYonedaEmbedding
(
    main
)
where
    import              CompositionGraph.CompositionGraph
    import              ExportGraphViz.ExportGraphViz           (catToPdf, diagToPdf, diagToPdf2)
    import              FiniteCategory.FiniteCategory hiding    (f,g,h,i)
    import              Data.Text                               (Text, pack)
    import              YonedaEmbedding.YonedaEmbedding
    import              IO.PrettyPrint
    import              Subcategories.Subcategory
    import              Subcategories.FullSubcategory
    import              Diagram.Diagram
    import              Utils.AssociationList
    
    import              Set.FinSet
    
    import              OppositeCategory.OppositeCategory 

    f = (pack "A", pack "B", 1) :: Arrow Text Int
    g = (pack "A", pack "C", 2) :: Arrow Text Int
    h = (pack "B", pack "D", 3) :: Arrow Text Int
    i = (pack "C", pack "D", 4) :: Arrow Text Int
    
    -- | A composition law defined by hand. 
    myLaw = []
            
    myGraph = (pack.pure <$> ['A'..'D'], [f,g,h,i])
    -- | An example of a composition graph
    Right square = mkCompositionGraph myGraph myLaw
    
    (yoneda, funct) = yonedaEmbedding square
    
    type YC = (CompositionGraph Text Int)
    type YM = (CGMorphism Text Int)
    type YO = Text
    
    emptySheaf = Diagram {src = Op square, tgt = tgt ((ob yoneda) !! 0), omap = functToAssocList (const emptyFinSet) (ob square), mmap = functToAssocList (const FinMap{codomain = emptyFinSet, finMap = []}) (arrows (Op square))}
    
    subTarget = (FullSubcategory (tgt funct) (emptySheaf:(((omap funct) !-!) <$> (ob (src funct))))) :: FullSubcategory (PreSheavesCategory YC YM YO) (PreSheavesNatTransfo YC YM YO) (PreSheaf YC YM YO)
    
    -- | Exports the composition graphs and its Yoneda embedding as pdf files with GraphViz.
    main = do
            putStrLn "Start of ExampleYonedaEmbedding"
            catToPdf square "OutputGraphViz/Examples/YonedaEmbedding/square"
            -- diagToPdf (minimalDiagram funct) "OutputGraphViz/Examples/YonedaEmbedding/yonedaEmbeddingAsFunct"
            diagToPdf2 (fullDiagram funct) "OutputGraphViz/Examples/YonedaEmbedding/yonedaEmbedding"
            catToPdf subTarget "OutputGraphViz/Examples/YonedaEmbedding/fullYonedaEmbedding"
            putStrLn "End of ExampleYonedaEmbedding"