{-| 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 :: 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 = Ens Int
-> Diagram Parallel ParallelAr ParallelOb One One One
-> 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))
forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
     (FunctorCategory c1 m1 o1 c3 m3 o3)
     (NaturalTransformation c1 m1 o1 c3 m3 o3)
     (Diagram c1 m1 o1 c3 m3 o3)
deltaFunctor Ens Int
universe Diagram Parallel ParallelAr ParallelOb One One One
functor
        where
            universe :: Ens Int
universe = Set (Set Int) -> Ens Int
forall a. Set (Set a) -> Ens a
ens (Set (Set Int) -> Ens Int) -> Set (Set Int) -> Ens Int
forall a b. (a -> b) -> a -> b
$ [Set Int] -> Set (Set Int)
forall a. [a] -> Set a
set [[Int] -> Set Int
forall a. [a] -> Set a
set[], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1,Int
2]]
            functor :: Diagram Parallel ParallelAr ParallelOb One One One
functor = Set (Diagram Parallel ParallelAr ParallelOb One One One)
-> Diagram Parallel ParallelAr ParallelOb One One One
forall a. Set a -> a
anElement(Set (Diagram Parallel ParallelAr ParallelOb One One One)
 -> Diagram Parallel ParallelAr ParallelOb One One One)
-> (FunctorCategory Parallel ParallelAr ParallelOb One One One
    -> Set (Diagram Parallel ParallelAr ParallelOb One One One))
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Diagram Parallel ParallelAr ParallelOb One One One
forall b c a. (b -> c) -> (a -> b) -> a -> c
.FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Set (Diagram Parallel ParallelAr ParallelOb One One One)
forall c m o. FiniteCategory c m o => c -> Set o
ob (FunctorCategory Parallel ParallelAr ParallelOb One One One
 -> Diagram Parallel ParallelAr ParallelOb One One One)
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Diagram Parallel ParallelAr ParallelOb One One One
forall a b. (a -> b) -> a -> b
$ Parallel
-> One
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory Parallel
Parallel One
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 :: 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 = Ens Int
-> Diagram Parallel ParallelAr ParallelOb One One One
-> 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))
forall {c1} {m1} {o1} {c3} {m3} {o3} {c2} {m2} {o2}.
(FiniteCategory c1 m1 o1, FiniteCategory c3 m3 o3,
 FiniteCategory c2 m2 o2, Morphism m1 o1, Morphism m3 o3,
 Morphism m2 o2, Eq c1, Eq m1, Eq o1, Eq c3, Eq m3, Eq o3, Eq c2,
 Eq m2, Eq o2) =>
c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     (FunctorCategory c1 m1 o1 c3 m3 o3)
     (NaturalTransformation c1 m1 o1 c3 m3 o3)
     (Diagram c1 m1 o1 c3 m3 o3)
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
piFunctor Ens Int
universe Diagram Parallel ParallelAr ParallelOb One One One
functor
        where
            universe :: Ens Int
universe = Set (Set Int) -> Ens Int
forall a. Set (Set a) -> Ens a
ens (Set (Set Int) -> Ens Int) -> Set (Set Int) -> Ens Int
forall a b. (a -> b) -> a -> b
$ [Set Int] -> Set (Set Int)
forall a. [a] -> Set a
set [[Int] -> Set Int
forall a. [a] -> Set a
set[], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1,Int
2]]
            functor :: Diagram Parallel ParallelAr ParallelOb One One One
functor = Set (Diagram Parallel ParallelAr ParallelOb One One One)
-> Diagram Parallel ParallelAr ParallelOb One One One
forall a. Set a -> a
anElement(Set (Diagram Parallel ParallelAr ParallelOb One One One)
 -> Diagram Parallel ParallelAr ParallelOb One One One)
-> (FunctorCategory Parallel ParallelAr ParallelOb One One One
    -> Set (Diagram Parallel ParallelAr ParallelOb One One One))
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Diagram Parallel ParallelAr ParallelOb One One One
forall b c a. (b -> c) -> (a -> b) -> a -> c
.FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Set (Diagram Parallel ParallelAr ParallelOb One One One)
forall c m o. FiniteCategory c m o => c -> Set o
ob (FunctorCategory Parallel ParallelAr ParallelOb One One One
 -> Diagram Parallel ParallelAr ParallelOb One One One)
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Diagram Parallel ParallelAr ParallelOb One One One
forall a b. (a -> b) -> a -> b
$ Parallel
-> One
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory Parallel
Parallel One
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 :: 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 = Ens Int
-> Diagram Parallel ParallelAr ParallelOb One One One
-> 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))
forall {c2} {m2} {o2} {c3} {m3} {o3} {c1} {m1} {o1}.
(FiniteCategory c2 m2 o2, FiniteCategory c3 m3 o3,
 FiniteCategory c1 m1 o1, Morphism m2 o2, Morphism m3 o3,
 Morphism m1 o1, Eq c2, Eq m2, Eq o2, Eq c3, Eq m3, Eq o3, Eq c1,
 Eq m1, Eq o1) =>
c3
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     (FunctorCategory c1 m1 o1 c3 m3 o3)
     (NaturalTransformation c1 m1 o1 c3 m3 o3)
     (Diagram c1 m1 o1 c3 m3 o3)
     (FunctorCategory c2 m2 o2 c3 m3 o3)
     (NaturalTransformation c2 m2 o2 c3 m3 o3)
     (Diagram c2 m2 o2 c3 m3 o3)
sigmaFunctor Ens Int
universe Diagram Parallel ParallelAr ParallelOb One One One
functor
        where
            universe :: Ens Int
universe = Set (Set Int) -> Ens Int
forall a. Set (Set a) -> Ens a
ens (Set (Set Int) -> Ens Int) -> Set (Set Int) -> Ens Int
forall a b. (a -> b) -> a -> b
$ [Set Int] -> Set (Set Int)
forall a. [a] -> Set a
set [[Int] -> Set Int
forall a. [a] -> Set a
set[], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1], [Int] -> Set Int
forall a. [a] -> Set a
set [Int
1,Int
2]]
            functor :: Diagram Parallel ParallelAr ParallelOb One One One
functor = Set (Diagram Parallel ParallelAr ParallelOb One One One)
-> Diagram Parallel ParallelAr ParallelOb One One One
forall a. Set a -> a
anElement(Set (Diagram Parallel ParallelAr ParallelOb One One One)
 -> Diagram Parallel ParallelAr ParallelOb One One One)
-> (FunctorCategory Parallel ParallelAr ParallelOb One One One
    -> Set (Diagram Parallel ParallelAr ParallelOb One One One))
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Diagram Parallel ParallelAr ParallelOb One One One
forall b c a. (b -> c) -> (a -> b) -> a -> c
.FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Set (Diagram Parallel ParallelAr ParallelOb One One One)
forall c m o. FiniteCategory c m o => c -> Set o
ob (FunctorCategory Parallel ParallelAr ParallelOb One One One
 -> Diagram Parallel ParallelAr ParallelOb One One One)
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
-> Diagram Parallel ParallelAr ParallelOb One One One
forall a b. (a -> b) -> a -> b
$ Parallel
-> One
-> FunctorCategory Parallel ParallelAr ParallelOb One One One
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory Parallel
Parallel One
One