{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-| Module  : FiniteCategories
Description : Diagonal functor.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The diagonal functor sends each object to the constant functor on this object.
-}

module Math.Functors.DiagonalFunctor 
(
    diagonalFunctor,
)
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
    
    -- | Given two categories /J/ and /C/, return the diagonal functor /C/ -> /C/^/J/.

    --

    -- Let /J/ and /C/ be two categories, we consider the functor category /C/^/J/.

    -- The diagonal functor /D/ : /C/ -> /C/^/J/ maps each object /x/ of /C/ to the constant diagram /D_x/ from /J/ to /C/.

    -- It maps each morphism to the natural transformation between the two constant diagrams associated to the source and the target of the morphism.

    diagonalFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                        FiniteCategory c2 m2 o2, Morphism m2 o2) =>
                        c1 -- ^ /J/

                     -> c2 -- ^ /C/

                     -> Diagram c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) -- ^ /D/ : /C/ -> /C/^/J/

    diagonalFunctor :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunctor c1
j c2
c = Diagram{src :: c2
src=c2
c
                                , tgt :: FunctorCategory c1 m1 o1 c2 m2 o2
tgt=c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory c1
j c2
c
                                , omap :: Map o2 (Diagram c1 m1 o1 c2 m2 o2)
omap=(o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Set o2 -> Map o2 (Diagram c1 m1 o1 c2 m2 o2)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
j c2
c) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob c2
c)
                                , mmap :: Map m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
mmap=(m2 -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Set m2 -> Map m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\m2
f -> Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
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 (c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
j c2
c (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
f)) (c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
j c2
c (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
f)) ((o1 -> m2) -> Set o1 -> Map o1 m2
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\o1
x->m2
f) (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
j))) (c2 -> Set m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c2
c)}