{-| Module  : FiniteCategories
Description : Examples of  __'Ens'__.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of  __'Ens'__.
-}
module Math.FiniteCategories.Ens.Examples
(
    exampleEns,
    exampleEns2,
    exampleDiscreteDiagToSet,
    exampleProductSet,
    exampleCoproductSet,
    exampleParallelDiagramToSet,
    exampleEqualizerSet,
    exampleCoequalizerSet,
    exampleDiagramVToFinSet,
    exampleLimitSet,
    exampleColimitSet,
    exampleExponentialObjectInSet,
)
where
    import Data.WeakSet         (powerSet, Set)
    import Data.WeakSet.Safe
    import Data.WeakMap
    
    import Math.FiniteCategories
    import Math.Categories
    import Math.IO.PrettyPrint
    import Math.FiniteCategory
    import Math.CompleteCategory
    import Math.CocompleteCategory
    import Math.CartesianClosedCategory
    
    -- | An example of 'Ens' containing all subsets of {'A', 'B', 'C'}.
    exampleEns :: Ens Char
    exampleEns = ens.powerSet.set $ "ABC"
    
    -- | An example of 'Ens' containing sets {{},{'A'},{'A','B'},{'A','B','C'}}.
    exampleEns2 :: Ens Char
    exampleEns2 = ens.set $ [set "", set "A", set "AB", set "ABC"]
    
    -- | An example of 'discreteDiagram' to 'FinSet'.
    exampleDiscreteDiagToSet :: Diagram (DiscreteCategory Char) (DiscreteMorphism Char) Char (FinSet Int) (Function Int) (Set Int)
    exampleDiscreteDiagToSet = completeDiagram Diagram{src=discreteCategory (set ['a','b']), tgt=FinSet, omap= (weakMap [('a',set [1,2]),('b',set [3,4,5])]), mmap = weakMap []}

    -- | An example of product computed in 'FinSet' thanks to the fact that 'FinSet' is complete. Computes {1,2} x {3,4,5}.
    exampleProductSet :: Cone (DiscreteCategory Char) (DiscreteMorphism Char) Char (FinSet (Limit Char Int)) (Function (Limit Char Int)) (Set (Limit Char Int))
    exampleProductSet = Math.CompleteCategory.product exampleDiscreteDiagToSet
    
    -- | An example of coproduct computed in 'FinSet' thanks to the fact that 'FinSet' is cocomplete. Computes {1,2} + {3,4,5}.
    exampleCoproductSet :: Cocone (DiscreteCategory Char) (DiscreteMorphism Char) Char (FinSet (Colimit Char Int)) (Function (Colimit Char Int)) (Set (Colimit Char Int))
    exampleCoproductSet = coproduct exampleDiscreteDiagToSet
            
    -- | An example of 'parallelDiagram' to 'FinSet', the first function selected is x%2 on {0,1,2,3,4} and the second is (const 0).
    exampleParallelDiagramToSet :: Diagram Parallel ParallelAr ParallelOb (FinSet Int) (Function Int) (Set Int)
    exampleParallelDiagramToSet = completeDiagram Diagram{src = Parallel, tgt = FinSet, omap = weakMap [], mmap = weakMap [(ParallelF,Function{function = weakMap [(0,0),(1,1),(2,0),(3,1),(4,0)], codomain = set [0,1]}),(ParallelG,Function{function = weakMap [(0,0),(1,0),(2,0),(3,0),(4,0)], codomain = set [0,1]})]}
    
    -- | An example of equalizer of a 'parallelDiagram' to 'FinSet' thanks to the fact that 'FinSet' is complete.
    --
    -- It equalizes 'exampleParallelDiagramToSet', therefore the apex of the equalizer is {0,2,4}.
    exampleEqualizerSet :: Cone Parallel ParallelAr ParallelOb (FinSet Int) (Function Int) (Set Int)
    exampleEqualizerSet = equalize exampleParallelDiagramToSet
    
    -- | An example of coequalizer of a 'parallelDiagram' to 'FinSet' thanks to the fact that 'FinSet' is cocomplete.
    --
    -- It equalizes 'exampleParallelDiagramToSet', therefore the nadir of the coequalizer is {0}.
    exampleCoequalizerSet :: Cocone Parallel ParallelAr ParallelOb (FinSet Int) (Function Int) (Set Int)
    exampleCoequalizerSet = coequalize exampleParallelDiagramToSet
    
    
    -- | An example of a diagram from 'V' to 'FinSet'. The two functions selected are identities, the first from {1,2,3,4} to {1,2,3,4,5,6,7,8,9,10} and the second from {3,4,5,6} to {1,2,3,4,5,6,7,8,9,10}.
    exampleDiagramVToFinSet :: Diagram V VAr VOb (FinSet Int) (Function Int) (Set Int)
    exampleDiagramVToFinSet = completeDiagram Diagram{src = V, tgt = FinSet, omap = weakMap [], mmap = weakMap [(VF,Function{function = weakMap [(1,1),(2,2),(3,3),(4,4)], codomain = set [1..10]}),(VG,Function{function = weakMap [(3,3),(4,4),(5,5),(6,6)], codomain = set [1..10]})]}
    
    -- | An example of limit computation of a 'Diagram' to 'FinSet' thanks to the fact that 'FinSet' is complete.
    exampleLimitSet :: Cone V VAr VOb (FinSet (Limit VOb Int)) (Function (Limit VOb Int)) (Set (Limit VOb Int))
    exampleLimitSet = limit exampleDiagramVToFinSet
    
    
    
    -- | An example of a diagram from 'Hat' to 'FinSet'. The two functions selected are identities, the first from {3,4} to {1,2,3,4} and the second from {3,4} to {3,4,5,6}.
    exampleDiagramHatToFinSet :: Diagram Hat HatAr HatOb (FinSet Int) (Function Int) (Set Int)
    exampleDiagramHatToFinSet = completeDiagram Diagram{src = Hat, tgt = FinSet, omap = weakMap [], mmap = weakMap [(HatF,Function{function = weakMap [(3,3),(4,4)], codomain = set [1..4]}),(HatG,Function{function = weakMap [(3,3),(4,4)], codomain = set [3..6]})]}
    
    -- | An example of colimit computation of a 'Diagram' to 'FinSet' thanks to the fact that 'FinSet' is cocomplete.
    --
    -- It is the colimit of 'exampleDiagramHatToFinSet' which computes the union of {1,2,3,4} and {3,4,5,6} where 3 and 4 are identified.
    exampleColimitSet :: Cocone Hat HatAr HatOb (FinSet (Colimit HatOb Int)) (Function (Colimit HatOb Int)) (Set (Colimit HatOb Int))
    exampleColimitSet = colimit exampleDiagramHatToFinSet
    
    -- | An example of exponential object. Computes the internal hom of 'exampleDiscreteDiagToSet', meaning all functions from {1,2} to {3,4,5}.
    exampleExponentialObjectInSet :: Tripod (FinSet (Cartesian Int)) (Function (Cartesian Int)) (Set (Cartesian Int))
    exampleExponentialObjectInSet = internalHom $ exampleDiscreteDiagToSet <-@<- (insertionDiscreteTwoInDiscreteCategory (src exampleDiscreteDiagToSet) 'a' 'b')