{-# LANGUAGE MonadComprehensions, MultiParamTypeClasses  #-}
{-| Module  : FiniteCategories
Description : Data migration functors as defined by David Spivak in FQL.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Data migration functors as defined by David Spivak in FQL.
-}

module Math.Functors.DataMigration 
(
    deltaFunctor,
    piFunctor,
    sigmaFunctor
)
where
    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

    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    import              Math.Functors.Adjunction
    
    -- | Precomposition functor.
    deltaFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                     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 c diag = Diagram{src = s, tgt = t,
                                  omap = memorizeFunction (<-@<- diag) (ob s),
                                  mmap = memorizeFunction (<=@<- diag) (arrows s)}
        where
            s = FunctorCategory (tgt diag) c
            t = FunctorCategory (src diag) c
    
    -- | Right adjoint of the precomposition functor.
    piFunctor c = rightAdjoint.(deltaFunctor c)
    
    -- | Left adjoint of the precomposition functor.
    sigmaFunctor c = leftAdjoint.(deltaFunctor c)