{-| Module  : FiniteCategories
Description : Diagonal functor of an index category.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

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.
-}

module DiagonalFunctor.DiagonalFunctor
(
mkDiagonalFunctor
)
where
    import Diagram.Diagram
    import FiniteCategory.FiniteCategory
    import FunctorCategory.FunctorCategory
    import Data.Maybe                              (fromJust)
    import Utils.AssociationList
    
    -- | Given two categories /J/ and /C/, returns the diagonal functor /C/ -> /C/^/J/.

    mkDiagonalFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                         FiniteCategory c2 m2 o2, Morphism m2 o2, Eq 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/

    mkDiagonalFunctor :: forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq 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)
mkDiagonalFunctor c1
j c2
c = 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 :: c2
src=c2
c
                                  , tgt :: FunctorCategory c1 m1 o1 c2 m2 o2
tgt=FunctorCategory :: forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory{sourceCat :: c1
sourceCat=c1
j, targetCat :: c2
targetCat=c2
c}
                                  , omap :: AssociationList o2 (Diagram c1 m1 o1 c2 m2 o2)
omap=(o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> [o2] -> AssociationList o2 (Diagram c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (\o2
o ->  o2 -> Diagram c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}.
(FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
 Morphism m2 o2, Eq o2) =>
o2 -> Diagram c1 m1 o1 c2 m2 o2
constDiag o2
o) (c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [o]
ob c2
c)
                                  , mmap :: AssociationList m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
mmap=(m2 -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> [m2]
-> AssociationList m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> [a] -> AssociationList a b
functToAssocList (\m2
f -> 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 c1 m1 o1 c2 m2 o2
srcNT=o2 -> Diagram c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}.
(FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
 Morphism m2 o2, Eq o2) =>
o2 -> Diagram c1 m1 o1 c2 m2 o2
constDiag (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
f),tgtNT :: Diagram c1 m1 o1 c2 m2 o2
tgtNT=o2 -> Diagram c1 m1 o1 c2 m2 o2
forall {m1} {o1} {m2} {o2}.
(FiniteCategory c1 m1 o1, FiniteCategory c2 m2 o2, Morphism m1 o1,
 Morphism m2 o2, Eq o2) =>
o2 -> Diagram c1 m1 o1 c2 m2 o2
constDiag (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
f),component :: o1 -> m2
component=(\o1
x->m2
f)}) (c2 -> [m2]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c2
c)}
                            where
                                constDiag :: o2 -> Diagram c1 m1 o1 c2 m2 o2
constDiag o2
obj = Maybe (Diagram c1 m1 o1 c2 m2 o2) -> Diagram c1 m1 o1 c2 m2 o2
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Diagram c1 m1 o1 c2 m2 o2) -> Diagram c1 m1 o1 c2 m2 o2)
-> Maybe (Diagram c1 m1 o1 c2 m2 o2) -> Diagram c1 m1 o1 c2 m2 o2
forall a b. (a -> b) -> a -> b
$ c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq o2) =>
c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkConstantDiagram c1
j c2
c o2
obj