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

Examples of data migration.
-}
module Math.Functors.DataMigration.Examples
(
    exampleDeltaFunctor,
    examplePiFunctor,
    exampleSigmaFunctor,
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategories
    import              Math.Categories
    import              Math.Functors.DataMigration

    
    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 example of 'deltaFunctor', you can see it as a cast operation on models of a given linear sketch.
    --
    -- Here we consider a sketch morphism from the sketch of graphs ('Parellel') to the sketch of sets ('One').
    exampleDeltaFunctor :: Diagram (FunctorCategory One One One (Ens Int) (Function Int) (Set Int)) (NaturalTransformation One One One (Ens Int) (Function Int) (Set Int)) (Diagram One One One (Ens Int) (Function Int) (Set Int)) (FunctorCategory Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (NaturalTransformation Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (Diagram Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int))
    exampleDeltaFunctor = deltaFunctor universe functor
        where
            universe = ens $ set [set[], set [1], set [1,2]]
            functor = anElement.ob $ FunctorCategory Parallel One
    
    
    -- | An example of 'piFunctor', it is the right adjoint of 'exampleDeltaFunctor'.
    examplePiFunctor :: Diagram (FunctorCategory Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (NaturalTransformation Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (Diagram Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (FunctorCategory One One One (Ens Int) (Function Int) (Set Int)) (NaturalTransformation One One One (Ens Int) (Function Int) (Set Int)) (Diagram One One One (Ens Int) (Function Int) (Set Int)) 
    examplePiFunctor = piFunctor universe functor
        where
            universe = ens $ set [set[], set [1], set [1,2]]
            functor = anElement.ob $ FunctorCategory Parallel One
    
    -- | An example of 'piFunctor', it is the left adjoint of 'exampleDeltaFunctor'.
    exampleSigmaFunctor :: Diagram (FunctorCategory Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (NaturalTransformation Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (Diagram Parallel ParallelAr ParallelOb (Ens Int) (Function Int) (Set Int)) (FunctorCategory One One One (Ens Int) (Function Int) (Set Int)) (NaturalTransformation One One One (Ens Int) (Function Int) (Set Int)) (Diagram One One One (Ens Int) (Function Int) (Set Int)) 
    exampleSigmaFunctor = sigmaFunctor universe functor
        where
            universe = ens $ set [set[], set [1], set [1,2]]
            functor = anElement.ob $ FunctorCategory Parallel One