{-# 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
    import              Data.Simplifiable
    
    -- | 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 :: forall c m o.
(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 c
cat = Diagram
  c
  m
  o
  (FunctorCategory
     (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m))
  (NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m))
  (Diagram (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m))
forall {m1} {o1} {a} {m2} {o2} {a} {a}.
Diagram
  c
  m
  o
  (FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2)
  (NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
  (Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
functor
        where
            hom :: o -> Set (Set m)
hom o
x = (\o
s -> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
cat o
s o
x) (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat)
            omapPresheaf :: o -> o -> Set m
omapPresheaf o
x o
s = c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
cat o
s o
x
            mmapPresheaf :: o -> OpMorphism m -> Function m
mmapPresheaf o
x OpMorphism m
m = Function{codomain :: Set m
codomain = o -> o -> Set m
omapPresheaf o
x (OpMorphism m -> o
forall m o. Morphism m o => m -> o
target OpMorphism m
m)
                                      , function :: Map m m
function = AssociationList m m -> Map m m
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList m m -> Map m m) -> AssociationList m m -> Map m m
forall a b. (a -> b) -> a -> b
$ [m] -> [m] -> AssociationList m m
forall a b. [a] -> [b] -> [(a, b)]
zip (Set m -> [m]
forall a. Eq a => Set a -> [a]
Set.toList (o -> o -> Set m
omapPresheaf o
x (OpMorphism m -> o
forall m o. Morphism m o => m -> o
source OpMorphism m
m))) ((\m
f -> (m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (OpMorphism m -> m
forall m. OpMorphism m -> m
opOpMorphism OpMorphism m
m))) (m -> m) -> [m] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set m -> [m]
forall a. Eq a => Set a -> [a]
Set.toList (o -> o -> Set m
omapPresheaf o
x (OpMorphism m -> o
forall m o. Morphism m o => m -> o
source OpMorphism m
m))))}
            presheaf :: o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf o
x = Diagram {    src :: Op c
src = c -> Op c
forall c. c -> Op c
Op c
cat
                                    , tgt :: FinSet a
tgt = FinSet a
forall a. FinSet a
FinSet
                                    , omap :: Map o (Set m)
omap = (o -> Set m) -> Set o -> Map o (Set m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (o -> o -> Set m
omapPresheaf o
x) (Op c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob (c -> Op c
forall c. c -> Op c
Op c
cat))
                                    , mmap :: Map (OpMorphism m) (Function m)
mmap = (OpMorphism m -> Function m)
-> Set (OpMorphism m) -> Map (OpMorphism m) (Function m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (o -> OpMorphism m -> Function m
mmapPresheaf o
x) (Op c -> Set (OpMorphism m)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (c -> Op c
forall c. c -> Op c
Op c
cat))}
                                        
            ntFromMorph :: m -> o -> Function m
ntFromMorph m
m o
o = Function {codomain :: Set m
codomain = (o
-> Diagram
     (Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
target m
m)) Diagram (Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
-> o -> Set m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o
o
                                      , function :: Map m m
function = AssociationList m m -> Map m m
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList m m -> Map m m) -> AssociationList m m -> Map m m
forall a b. (a -> b) -> a -> b
$ [m] -> [m] -> AssociationList m m
forall a b. [a] -> [b] -> [(a, b)]
zip [m]
domain [m]
postcom }
                where
                    domain :: [m]
domain = Set m -> [m]
forall a. Eq a => Set a -> [a]
Set.toList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ (o
-> Diagram
     (Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
source m
m)) Diagram (Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
-> o -> Set m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o
o
                    postcom :: [m]
postcom = (m
m m -> m -> m
forall m o. Morphism m o => m -> m -> m
@) (m -> m) -> [m] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m]
domain
            mmapFunctor :: m
-> NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
mmapFunctor m
m = Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
-> Map o (Function m)
-> NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
source m
m)) (o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
target m
m)) ((o -> Function m) -> Set o -> Map o (Function m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (m -> o -> Function m
ntFromMorph m
m) (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat))
                                                        
            presheavesCat :: FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
presheavesCat = Op c -> FinSet a -> FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (c -> Op c
forall c. c -> Op c
Op c
cat) FinSet a
forall a. FinSet a
FinSet
            functor :: Diagram
  c
  m
  o
  (FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2)
  (NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
  (Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
functor = Diagram {   src :: c
src = c
cat
                                , tgt :: FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
tgt = FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
forall {m1} {o1} {a} {m2} {o2}.
FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
presheavesCat
                                , omap :: Map
  o (Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
omap = (o
 -> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
-> Set o
-> Map
     o (Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat)
                                , mmap :: Map
  m
  (NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
mmap = (m
 -> NaturalTransformation
      (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
-> Set m
-> Map
     m
     (NaturalTransformation
        (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction m
-> NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
m
-> NaturalTransformation
     (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
mmapFunctor (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
cat)
                              }