-- {-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}


{-| Module  : FiniteCategories
Description : The Yoneda embedding of a category.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The Yoneda embedding of a category.
-}

module YonedaEmbedding.YonedaEmbedding where
    import FiniteCategory.FiniteCategory
    import FunctorCategory.FunctorCategory
    import Diagram.Diagram
    import OppositeCategory.OppositeCategory
    import Set.FinSet
    import Utils.AssociationList
    import Subcategories.Subcategory
    import Currying.Currying
    import OppositeCategory.OppositeCategory
    import Limit.Limit
    import ConeCategory.ConeCategory
    import DiagonalFunctor.DiagonalFunctor
    import Utils.Tuple
    
    import IO.PrettyPrint
    
    -- | A presheaf on a category @C@ is a diagram from @C^op@ to __Set__.

    type PreSheaf c m o = Diagram (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
    
    -- | Natural transformation between presheaves.

    type PreSheavesNatTransfo c m o = NaturalTransformation (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
    
    -- | The type of the category of presheaves.

    type PreSheavesCategory c m o = FunctorCategory (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
    
    -- | Returns the presheaf category generated by a Yoneda embedding and an insertion functor full and faithful.

    yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (PreSheavesCategory c m o, Diagram c m o (PreSheavesCategory c m o) (PreSheavesNatTransfo c m o) (PreSheaf c m o))
    yonedaEmbedding :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c
-> (PreSheavesCategory c m o,
    Diagram
      c
      m
      o
      (PreSheavesCategory c m o)
      (PreSheavesNatTransfo c m o)
      (PreSheaf c m o))
yonedaEmbedding c
cat = (FunctorCategory
  (OppositeCategory c m o)
  (OppositeMorphism m o)
  o
  (FinSetCat m)
  (FinMap m)
  (FinSet m)
forall {m} {o} {m1} {o1} {m2} {o2}.
FunctorCategory (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2
presheavesCat, Diagram
  c
  m
  o
  (FunctorCategory
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
  (NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
  (Diagram
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
forall {m} {o} {m1} {o1} {m2} {o2} {m} {o} {m} {o}.
Diagram
  c
  m
  o
  (FunctorCategory
     (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2)
  (NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
  (Diagram
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
functor)
        where
            hom :: a -> FinSet m
hom a
x = [FinSet m] -> FinSet m
forall a. Eq a => [FinSet a] -> FinSet a
fromList ([FinSet m] -> FinSet m) -> [FinSet m] -> FinSet m
forall a b. (a -> b) -> a -> b
$ [FinSet m] -> FinSet m
forall a. Eq a => [FinSet a] -> FinSet a
fromList ([FinSet m] -> FinSet m) -> (a -> [FinSet m]) -> a -> FinSet m
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (\a
s -> m -> FinSet m
forall a. a -> FinSet a
Elem (m -> FinSet m) -> [m] -> [FinSet m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> a -> a -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat a
s a
x) (a -> FinSet m) -> [a] -> [FinSet m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> [a]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat)
            omapPresheaf :: o -> o -> FinSet a
omapPresheaf o
x o
s = [FinSet a] -> FinSet a
forall a. Eq a => [FinSet a] -> FinSet a
fromList ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ a -> FinSet a
forall a. a -> FinSet a
Elem (a -> FinSet a) -> [a] -> [FinSet a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> [a]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
cat o
s o
x
            mmapPresheaf :: o -> OppositeMorphism a o -> FinMap a
mmapPresheaf o
x OppositeMorphism a o
m = FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap{codomain :: FinSet a
codomain = o -> o -> FinSet a
forall {a} {o}.
(Eq a, FiniteCategory c a o, Morphism a o) =>
o -> o -> FinSet a
omapPresheaf o
x (OppositeMorphism a o -> o
forall m o. Morphism m o => m -> o
target OppositeMorphism a o
m)
                                    , finMap :: AssociationList (FinSet a) (FinSet a)
finMap = [FinSet a] -> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. [a] -> [b] -> [(a, b)]
zip (FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList (o -> o -> FinSet a
forall {a} {o}.
(Eq a, FiniteCategory c a o, Morphism a o) =>
o -> o -> FinSet a
omapPresheaf o
x (OppositeMorphism a o -> o
forall m o. Morphism m o => m -> o
source OppositeMorphism a o
m))) ((\FinSet a
f -> (a -> a) -> FinSet a -> FinSet a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> a -> a
forall m o. Morphism m o => m -> m -> m
@ (OppositeMorphism a o -> a
forall m o. OppositeMorphism m o -> m
opOpMorph OppositeMorphism a o
m)) FinSet a
f) (FinSet a -> FinSet a) -> [FinSet a] -> [FinSet a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList (o -> o -> FinSet a
forall {a} {o}.
(Eq a, FiniteCategory c a o, Morphism a o) =>
o -> o -> FinSet a
omapPresheaf o
x (OppositeMorphism a o -> o
forall m o. Morphism m o => m -> o
source OppositeMorphism a o
m))))}
            presheaf :: o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
presheaf o
x = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {    src :: OppositeCategory c m o
src = c -> OppositeCategory c m o
forall c m o. c -> OppositeCategory c m o
Op c
cat
                                    , tgt :: FinSetCat a
tgt = [FinSet a] -> FinSetCat a
forall a. [FinSet a] -> FinSetCat a
FinSetCat ([FinSet a] -> FinSetCat a) -> [FinSet a] -> FinSetCat a
forall a b. (a -> b) -> a -> b
$ FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList (FinSet a -> [FinSet a]) -> FinSet a -> [FinSet a]
forall a b. (a -> b) -> a -> b
$ [FinSet a] -> FinSet a
forall a. Eq a => [FinSet a] -> FinSet a
union ([FinSet a] -> FinSet a) -> [FinSet a] -> FinSet a
forall a b. (a -> b) -> a -> b
$ o -> FinSet a
forall {m} {a}.
(FiniteCategory c m a, Eq m, Morphism m a) =>
a -> FinSet m
hom (o -> FinSet a) -> [o] -> [FinSet a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat
                                    , omap :: AssociationList o (FinSet a)
omap = (o -> FinSet a) -> [o] -> AssociationList o (FinSet a)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (o -> o -> FinSet a
forall {a} {o}.
(Eq a, FiniteCategory c a o, Morphism a o) =>
o -> o -> FinSet a
omapPresheaf o
x) (OppositeCategory c a o -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob (c -> OppositeCategory c a o
forall c m o. c -> OppositeCategory c m o
Op c
cat))
                                    , mmap :: AssociationList (OppositeMorphism a o) (FinMap a)
mmap = (OppositeMorphism a o -> FinMap a)
-> [OppositeMorphism a o]
-> AssociationList (OppositeMorphism a o) (FinMap a)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (o -> OppositeMorphism a o -> FinMap a
forall {a} {o}.
(Morphism a o, Eq a, FiniteCategory c a o) =>
o -> OppositeMorphism a o -> FinMap a
mmapPresheaf o
x) (OppositeCategory c a o -> [OppositeMorphism a o]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (c -> OppositeCategory c a o
forall c m o. c -> OppositeCategory c m o
Op c
cat))}
                                        
            ntFromMorph :: a -> a -> FinMap a
ntFromMorph a
m a
o = FinMap :: forall a.
AssociationList (FinSet a) (FinSet a) -> FinSet a -> FinMap a
FinMap {codomain :: FinSet a
codomain = (Diagram
  (OppositeCategory c Any Any)
  (OppositeMorphism a a)
  a
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
-> AssociationList a (FinSet a)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap (Diagram
   (OppositeCategory c Any Any)
   (OppositeMorphism a a)
   a
   (FinSetCat a)
   (FinMap a)
   (FinSet a)
 -> AssociationList a (FinSet a))
-> Diagram
     (OppositeCategory c Any Any)
     (OppositeMorphism a a)
     a
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
-> AssociationList a (FinSet a)
forall a b. (a -> b) -> a -> b
$ a
-> Diagram
     (OppositeCategory c Any Any)
     (OppositeMorphism a a)
     a
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
forall {a} {o} {m} {o}.
(Eq a, Morphism a o, FiniteCategory c a o) =>
o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
presheaf (a -> a
forall m o. Morphism m o => m -> o
target a
m)) AssociationList a (FinSet a) -> a -> FinSet a
forall a b. Eq a => AssociationList a b -> a -> b
!-! a
o
                                    , finMap :: AssociationList (FinSet a) (FinSet a)
finMap = [FinSet a] -> [FinSet a] -> AssociationList (FinSet a) (FinSet a)
forall a b. [a] -> [b] -> [(a, b)]
zip (FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
domain) (FinSet a -> [FinSet a]
forall a. FinSet a -> [FinSet a]
toList FinSet a
postcom) }
                where
                    domain :: FinSet a
domain = (Diagram
  (OppositeCategory c Any Any)
  (OppositeMorphism a a)
  a
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
-> AssociationList a (FinSet a)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap (Diagram
   (OppositeCategory c Any Any)
   (OppositeMorphism a a)
   a
   (FinSetCat a)
   (FinMap a)
   (FinSet a)
 -> AssociationList a (FinSet a))
-> Diagram
     (OppositeCategory c Any Any)
     (OppositeMorphism a a)
     a
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
-> AssociationList a (FinSet a)
forall a b. (a -> b) -> a -> b
$ a
-> Diagram
     (OppositeCategory c Any Any)
     (OppositeMorphism a a)
     a
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
forall {a} {o} {m} {o}.
(Eq a, Morphism a o, FiniteCategory c a o) =>
o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
presheaf (a -> a
forall m o. Morphism m o => m -> o
source a
m)) AssociationList a (FinSet a) -> a -> FinSet a
forall a b. Eq a => AssociationList a b -> a -> b
!-! a
o
                    postcom :: FinSet a
postcom = (a
m a -> a -> a
forall m o. Morphism m o => m -> m -> m
@) (a -> a) -> FinSet a -> FinSet a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` FinSet a
domain
            mmapFunctor :: a
-> NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
mmapFunctor a
m = NaturalTransformation :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> (o1 -> m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
NaturalTransformation {   srcNT :: Diagram
  (OppositeCategory c m o)
  (OppositeMorphism a o)
  o
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
srcNT = o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
forall {a} {o} {m} {o}.
(Eq a, Morphism a o, FiniteCategory c a o) =>
o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
presheaf (a -> o
forall m o. Morphism m o => m -> o
source a
m)
                                                    , tgtNT :: Diagram
  (OppositeCategory c m o)
  (OppositeMorphism a o)
  o
  (FinSetCat a)
  (FinMap a)
  (FinSet a)
tgtNT = o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
forall {a} {o} {m} {o}.
(Eq a, Morphism a o, FiniteCategory c a o) =>
o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
presheaf (a -> o
forall m o. Morphism m o => m -> o
target a
m)
                                                    , component :: o -> FinMap a
component = a -> o -> FinMap a
forall {a} {a} {o}.
(Eq a, Eq a, FiniteCategory c a a, Morphism a a, Morphism a o) =>
a -> a -> FinMap a
ntFromMorph a
m}
                                                        
            presheavesCat :: FunctorCategory (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2
presheavesCat = FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory { sourceCat :: OppositeCategory c m o
sourceCat = c -> OppositeCategory c m o
forall c m o. c -> OppositeCategory c m o
Op c
cat
                                            , targetCat :: FinSetCat m
targetCat = [FinSet m] -> FinSetCat m
forall a. [FinSet a] -> FinSetCat a
FinSetCat ([FinSet m] -> FinSetCat m) -> [FinSet m] -> FinSetCat m
forall a b. (a -> b) -> a -> b
$ [[FinSet m]] -> [FinSet m]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (FinSet m -> [FinSet m]
forall a. FinSet a -> [FinSet a]
toList (FinSet m -> [FinSet m]) -> [FinSet m] -> [[FinSet m]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (o -> FinSet m
forall {m} {a}.
(FiniteCategory c m a, Eq m, Morphism m a) =>
a -> FinSet m
hom (o -> FinSet m) -> [o] -> [FinSet m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat))}
            functor :: Diagram
  c
  m
  o
  (FunctorCategory
     (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2)
  (NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
  (Diagram
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
functor = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {   src :: c
src = c
cat
                                , tgt :: FunctorCategory (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2
tgt = FunctorCategory (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2
forall {m} {o} {m1} {o1} {m2} {o2}.
FunctorCategory (OppositeCategory c m o) m1 o1 (FinSetCat m) m2 o2
presheavesCat
                                , omap :: AssociationList
  o
  (Diagram
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
omap = (o
 -> Diagram
      (OppositeCategory c m o)
      (OppositeMorphism m o)
      o
      (FinSetCat m)
      (FinMap m)
      (FinSet m))
-> [o]
-> AssociationList
     o
     (Diagram
        (OppositeCategory c m o)
        (OppositeMorphism m o)
        o
        (FinSetCat m)
        (FinMap m)
        (FinSet m))
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m)
forall {a} {o} {m} {o}.
(Eq a, Morphism a o, FiniteCategory c a o) =>
o
-> Diagram
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
presheaf (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
cat)
                                , mmap :: AssociationList
  m
  (NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m))
mmap = (m
 -> NaturalTransformation
      (OppositeCategory c m o)
      (OppositeMorphism m o)
      o
      (FinSetCat m)
      (FinMap m)
      (FinSet m))
-> [m]
-> AssociationList
     m
     (NaturalTransformation
        (OppositeCategory c m o)
        (OppositeMorphism m o)
        o
        (FinSetCat m)
        (FinMap m)
        (FinSet m))
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList m
-> NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism m o)
     o
     (FinSetCat m)
     (FinMap m)
     (FinSet m)
forall {a} {o} {m} {o}.
(Morphism a o, FiniteCategory c a o, Eq a, Eq o) =>
a
-> NaturalTransformation
     (OppositeCategory c m o)
     (OppositeMorphism a o)
     o
     (FinSetCat a)
     (FinMap a)
     (FinSet a)
mmapFunctor (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
cat)
                              }