{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : The category of presheaves on a 'Category' /C/ has functors from /C/^op to __FinSet__ as objects and natural transformations as morphisms. It is a 'FunctorCategory'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The category of presheaves on a 'Category' /C/ has functors from /C/^op to __FinSet__ as objects and natural transformations as morphisms. It is a 'FunctorCategory'.

The 'yonedaEmbedding' goes to a category of presheaves, it allows to cocomplete a 'FiniteCategory'.
-}

module Math.Categories.PresheafCategory
(
    -- * Presheaves
    Presheaf(..),
    PresheafMorphism(..),
    PresheafCategory(..),
    -- * Yoneda embedding
    yonedaEmbedding
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.Opposite
    import              Math.Categories.FinSet
    
    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
    
    -- | A 'Presheaf' on a 'Category' /C/ is a diagram from @/C/^op@ to __FinSet__.
    type Presheaf c m o = Diagram (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
    
    -- | A 'PresheafMorphism' is a 'NaturalTransformation' between presheaves.
    type PresheafMorphism c m o = NaturalTransformation (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
    
    -- | The type of the category of presheaves.
    type PresheafCategory c m o = FunctorCategory (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
    
    -- | Given a 'FiniteCategory' /C/, return its Yoneda embedding in the 'FunctorCategory' [/C/^op, __FinSet__].
    --
    -- It allows to cocomplete a 'FiniteCategory'. The insertion functor from the category to [/C/^op, __FinSet__] is full and faithful.
    yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Diagram c m o (PresheafCategory c m o) (PresheafMorphism c m o) (Presheaf c m o)
    yonedaEmbedding cat = functor
        where
            hom x = (\s -> ar cat s x) <$> (ob cat)
            omapPresheaf x s = ar cat s x
            mmapPresheaf x m = Function{codomain = omapPresheaf x (target m)
                                      , function = weakMap $ zip (Set.toList (omapPresheaf x (source m))) ((\f -> (f @ (opOpMorphism m))) <$> (Set.toList (omapPresheaf x (source m))))}
            presheaf x = Diagram {    src = Op cat
                                    , tgt = FinSet
                                    , omap = memorizeFunction (omapPresheaf x) (ob (Op cat))
                                    , mmap = memorizeFunction (mmapPresheaf x) (arrows (Op cat))}
                                        
            ntFromMorph m o = Function {codomain = (presheaf (target m)) ->$ o
                                      , function = weakMap $ zip domain postcom }
                where
                    domain = Set.toList $ (presheaf (source m)) ->$ o
                    postcom = (m @) <$> domain
            mmapFunctor m = unsafeNaturalTransformation (presheaf (source m)) (presheaf (target m)) (memorizeFunction (ntFromMorph m) (ob cat))
                                                        
            presheavesCat = FunctorCategory (Op cat) FinSet
            functor = Diagram {   src = cat
                                , tgt = presheavesCat
                                , omap = memorizeFunction presheaf (ob cat)
                                , mmap = memorizeFunction mmapFunctor (arrows cat)
                              }