{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : A 'FunctorCategory' has 'Diagram's as objects and 'NaturalTransformation's between them as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'FunctorCategory' /D/^/C/ (also written [/C/,/D/]) where /C/ is a 'FiniteCategory' and /D/ is a 'Category' has 'Diagram's @F : C -> D@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category. See the operator ('<=@<=') for horizontal composition.

A 'Diagram' is a heterogeneous functor, meaning that the source category might be different from the target category. See 'FinCat' for a homogeneous ones.

'Diagram's are objects in a 'FunctorCategory', they therefore can not be composed with the usual operator ('@'). See ('<-@<-') for composing 'Diagram's.

Beware that 'source' and 'target' are not defined on 'Diagram' because it is not a 'Morphism', use 'src' and 'tgt' instead. Also note that a 'Diagram' does not need to contain the mapping of all morphisms from the source category, it may only contain a mapping for the generating morphisms of the source category. 

You can also do left and right whiskering with the operators ('<=@<-') and ('<-@<=').

A `FunctorCategory` is a 'FiniteCategory' if the source and target category are finite, but it is only a 'Category' if the target category is not finite. 

All operators defined in this module respect the following convention: a "->" arrow represent a functor and a "=>" represent a natural transformation. For example ('<-@<=') allows to compose a natural transformation (the "<=" arrow) with a functor (the "<-" arrow), note that composition is always read from right to left.

-}

module Math.Categories.FunctorCategory
(
    -- * Diagram
    Diagram(..),
    -- ** Check diagram structure
    DiagramError,
    checkFiniteDiagram,
    checkDiagram,
    diagram,
    finiteDiagram,
    -- ** Operators
    (->$),
    (->£),
    (<-@<-),
    -- ** Usual diagrams
    selectObject,
    constantDiagram,
    discreteDiagram,
    parallelDiagram,
    -- *** Insertion diagrams for subcategories
    insertionFunctor1,
    insertionFunctor2,
    -- ** Diagram construction helper
    completeDiagram,
    pickRandomDiagram,
    -- ** Other diagram functions
    inverseDiagram,
    unsafeInverseDiagram,
    -- * Natural transformation
    NaturalTransformation,
    -- ** Getter
    components,
    -- ** Check structure
    NaturalTransformationError,
    checkNaturalTransformation,
    naturalTransformation,
    unsafeNaturalTransformation,
    -- ** Operators
    (=>$),
    (<=@<=),
    horizontalComposition,
    (<=@<-),
    leftWhiskering,
    (<-@<=),
    rightWhiskering,
    -- ** Misc
    indexingCategory,
    -- * Functor categories
    FunctorCategory(..),
    PrecomposedFunctorCategory(..),
    PostcomposedFunctorCategory(..),
)
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              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategories.One
    import              Math.Categories.Galaxy
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.FiniteCategories.Parallel
    import              Math.FiniteCategories.FullSubcategory
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint
    
    import              System.Random            (RandomGen, uniformR)
    
    import              GHC.Generics
    
    
    -- | A 'Diagram' is a functor from a 'FiniteCategory' to a 'Category'.
    --    
    -- A 'Diagram' can have a source category and a target category with different types. It must obey the following rules :
    --
    -- prop> funct ->$ (source f) == source (funct ->£ f)
    -- prop> funct ->$ (target f) == target (funct ->£ f)
    -- prop> funct ->£ (f @ g) = (funct ->£ f) @ (funct ->£ g)
    -- prop> funct ->£ (identity a) = identity (funct ->$ a)
    --
    -- 'Diagram' is not private because we can't always check functoriality if the target category is infinite.
    -- However it is recommanded to use the smart constructors 'diagram' or 'finiteDiagram' which check the structure of the 'Diagram' at construction. See also the useful function 'completeDiagram'.
    --
    -- You can omit the mapping of generated morphisms of the source category.
    data Diagram c1 m1 o1 c2 m2 o2 = Diagram { 
                                                src :: c1, -- ^ The source category
                                                tgt :: c2, -- ^ The target category
                                                omap :: Map o1 o2, -- ^ The object map
                                                mmap :: Map m1 m2 -- ^ The morphism map, generated morphisms can be omitted.
                                              } deriving (Show, Generic, PrettyPrint, Simplifiable)
    
    instance (Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2, FiniteCategory c1 m1 o1, Morphism m1 o1) => Eq (Diagram c1 m1 o1 c2 m2 o2) where
        d1 == d2 = src d1 == src d2 && tgt d1 == tgt d2 && omap d1 == omap d2 && Map.restrictKeys (mmap d1) (genArrows (src d1)) == Map.restrictKeys (mmap d2) (genArrows (src d2))     
    
    -- | Apply a 'Diagram' on an object of the source category.
    (->$) :: (Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
    (->$) f x = omap f |!| x
    
    -- | Apply a 'Diagram' on a morphism of the source category.
    (->£) :: (Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) => Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
    (->£) f x
        | null mapped = compose $ (mmap f |!|) <$> decompose (src f) x
        | otherwise = y
        where
            mapped = mmap f |?| x
            Just y = mapped
    
    -- | Compose two 'Diagram's.
    (<-@<-) :: (Category c1 m1 o1, Morphism m1 o1, Eq m1,
                Category c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2,
                Morphism m3 o3) => Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
    (<-@<-) g f = Diagram{src = src f, tgt = tgt g, omap = (omap g) |.| (omap f), mmap = mm}
        where
            mm = weakMapFromSet [(x, g ->£ (f ->£ x)) | x <- keys' (mmap f)]
    
    -- | Construct a 'Diagram' selecting an object in a category.
    --
    -- There is no check that the object belongs in the category.
    selectObject :: (Category c m o, Morphism m o, Eq o) => c -> o -> Diagram One One One c m o
    selectObject c o = Diagram{src=One, tgt=c, omap=weakMap [(One,o)], mmap=weakMap [(One, identity c o)]}
    
    -- | Construct a constant 'Diagram' on an object of the target 'Category' given an indexing 'FiniteCategory'.
    --
    -- There is no check that the object belongs in the category.
    constantDiagram :: (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 index targ o = Diagram{src=index, tgt=targ, omap=memorizeFunction (const o) (ob index), mmap=memorizeFunction (const (identity targ o)) (arrows index)}
    
    -- | Construct a discrete 'Diagram' on a list of objects of the target 'Category'.
    --
    -- We consider list of objects because a single object can be selected several times.
    --
    -- There is no check that the objects belongs in the category.
    discreteDiagram :: (Category c m o, Morphism m o, Eq o) => 
            c -> [o] -> Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int c m o
    discreteDiagram targ os = Diagram{src=discreteCategory indices, tgt=targ, omap=memorizeFunction (os !!) indices, mmap=memorizeFunction (\(StarIdentity x) -> identity targ (os !! x)) (arrows (discreteCategory indices))}
        where
            indices = set [0..((length os)-1)]
    
    -- | Construct a parallel 'Diagram' on two parallel morphisms of the target 'Category'.
    --
    -- There is no check that the morphisms belongs in the category and no check that the two morphisms are parallel.
    parallelDiagram :: (Category c m o, Morphism m o, Eq o) => 
            c -> m -> m -> Diagram Parallel ParallelAr ParallelOb c m o
    parallelDiagram targ f g = completeDiagram Diagram{src=Parallel, tgt=targ, omap=weakMap [(ParallelA,source f),(ParallelB,target f)], mmap=weakMap [(ParallelF, f), (ParallelG, g)]}
        
    
    -- Diagram structure check
    
    -- | A datatype to represent a malformation of a 'Diagram'.
    data DiagramError c1 m1 o1 c2 m2 o2 = WrongDomainObjects{srcObjs :: Set o1, domainObjs :: Set o1} -- ^ The objects in the domain of the object mapping are not the same as the objects of the source category.
                                        | WrongDomainMorphisms{srcMorphs :: Set m1, domainMorphs :: Set m1} -- ^ The morphisms in the domain of the morphism mapping are not the same as the morphisms of the source category.
                                        | WrongImageObjects{imageObjs :: Set o2, codomainObjs :: Set o2} -- ^ The objects in the image of the object mapping are not included in the objects of the codomain category.
                                        | WrongImageMorphisms{imageMorphs :: Set m2, codomainMorphs :: Set m2} -- ^ The morphisms in the image of the morphism mapping are not included in the morphisms of the codomain category.
                                        | TornMorphism{f :: m1, fImage :: m2} -- ^ A morphism /f/ is torn apart.
                                        | IdentityNotPreserved{originalId :: m1, imageId :: m2} -- ^ The image of an identity is not an identity.
                                        | CompositionNotPreserved{f :: m1, g :: m1, imageFG :: m2} -- ^ Composition is not preserved by the functor.
                               deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)
                               
    -- | Check wether the properties of a 'Diagram' are respected where the source and target category are finite.
    checkFiniteDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                           FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                      Diagram c1 m1 o1 c2 m2 o2 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
    checkFiniteDiagram d@Diagram{src=s,tgt=t,omap=om,mmap=fm}
        | domain om /= ob s = Just WrongDomainObjects{srcObjs = ob s, domainObjs = domain om}
        | not $ (genArrows s) `isIncludedIn` (domain fm) = Just WrongDomainMorphisms{srcMorphs = arrows s, domainMorphs = domain fm}
        | not $ image om `isIncludedIn` ob t = Just WrongImageObjects{imageObjs = image om, codomainObjs = ob t}
        | not $ image fm `isIncludedIn` arrows t = Just WrongImageMorphisms{imageMorphs = image fm, codomainMorphs = arrows t}
        | not.(Set.null) $ tear = Just TornMorphism{f = anElement tear, fImage = d ->£ (anElement tear)}
        | not.(Set.null) $ imId = Just IdentityNotPreserved{originalId = identity s (anElement imId), imageId = d ->£ (identity s (anElement imId))}
        | not.(Set.null) $ errCompo = Just CompositionNotPreserved{f = fst (anElement errCompo), g = snd (anElement errCompo), imageFG = d ->£ ((snd (anElement errCompo)) @ (fst (anElement errCompo)))}
        | otherwise = Nothing
        where
            tear = [arr | arr <- domain fm, om |!| (source arr) /= source (fm |!| arr) || om |!| (target arr) /= target (fm |!| arr)]
            imId = [a | a <- ob s, fm |!| (identity s a) /= identity t (om |!| a)]
            errCompo = [(f,g) | f <- (genArrows s), g <- (genArFrom s (target f)), not (null $ fm |?| (g @ f)) && fm |!| (g @ f) /= (fm |!| g) @ (fm |!| f)]
            
    -- | Check wether the properties of a 'Diagram' are respected where the source or target category is infinite.
    checkDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                           Category c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                      Diagram c1 m1 o1 c2 m2 o2 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
    checkDiagram d@Diagram{src=s,tgt=t,omap=om,mmap=fm}
        | domain om /= ob s = Just WrongDomainObjects{srcObjs = ob s, domainObjs = domain om}
        | not $ (genArrows s) `isIncludedIn` (domain fm) = Just WrongDomainMorphisms{srcMorphs = arrows s, domainMorphs = domain fm}
        | not.(Set.null) $ tear = Just TornMorphism{f = anElement tear, fImage = d ->£ (anElement tear)}
        | not.(Set.null) $ imId = Just IdentityNotPreserved{originalId = identity s (anElement imId), imageId = d ->£ (identity s (anElement imId))}
        | otherwise = Nothing
        where
            tear = [arr | arr <- domain fm, om |!| (source arr) /= source (fm |!| arr) || om |!| (target arr) /= target (fm |!| arr)]
            imId = [a | a <- ob s, fm |!| (identity s a) /= identity t (om |!| a)]
    
    -- | Return the inverse of a finite 'Diagram' if possible, return a 'DiagramError' otherwise. Note that this function fails almost all the time if the mapping of morphisms contains generators only (it would only work if all the generators are in the image of the diagram).
    inverseDiagram :: (FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
                       FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => 
        Diagram c1 m1 o1 c2 m2 o2 -> Either (DiagramError c2 m2 o2 c1 m1 o1) (Diagram c2 m2 o2 c1 m1 o1)
    inverseDiagram diag
        | null err = Right pseudoInverseDiag
        | otherwise = Left $ fromJust err
        where
            pseudoInverseDiag = Diagram{src = tgt diag, tgt = src diag, omap = pseudoInverse (omap diag), mmap = pseudoInverse (mmap diag)}
            err = checkFiniteDiagram pseudoInverseDiag
            fromJust (Just x) = x
    
    -- | Return the inverse of a 'Diagram' without checking the structure of the returned 'Diagram'. See 'inverseDiagram' for the safe version. Note that this function fails almost all the time if the mapping of morphisms contains generators only (it would only work if all the generators are in the image of the diagram).
    unsafeInverseDiagram :: Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
    unsafeInverseDiagram diag = Diagram{src = tgt diag, tgt = src diag, omap = pseudoInverse (omap diag), mmap = pseudoInverse (mmap diag)}
    
    -- | Smart constructor of a finite 'Diagram'.
    finiteDiagram :: ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                 c1 -> c2 -> Map o1 o2 -> Map m1 m2 -> Either (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
    finiteDiagram c1 c2 om mm 
        | null check = Right diag
        | otherwise = Left err
        where
            diag = Diagram{src = c1, tgt = c2, omap = om, mmap = mm}
            check = checkFiniteDiagram diag
            Just err = check
       
    -- | Smart constructor of a 'Diagram'. See 'finiteDiagram' for constructing finite 'Diagram's.
    diagram :: ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                 c1 -> c2 -> Map o1 o2 -> Map m1 m2 -> Either (DiagramError c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
    diagram c1 c2 om mm 
        | null check = Right diag
        | otherwise = Left err
        where
            diag = Diagram{src = c1, tgt = c2, omap = om, mmap = mm}
            check = checkDiagram diag
            Just err = check
    
    -- | Complete a partial 'Diagram' by adding mapping on objects from mapping of arrows and mapping on identities.
    --
    -- Does not check the structure of the resulting 'Diagram', you can use 'checkFiniteDiagram' or 'checkDiagram' to check afterwards.
    completeDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                              Category c2 m2 o2, Morphism m2 o2) => 
        Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
    completeDiagram Diagram{src=s,tgt=t,omap=om,mmap=mm} = Diagram{src=s,tgt=t,omap=newMapObj, mmap=Map.unions [mm, mapId] }
        where
            mapId = weakMapFromSet [(identity s o, identity t (newMapObj |!| o)) | o <- ob s, o `isIn` (keys' newMapObj)]
            mapSrc = weakMap [(source f1, source f2) | (f1,f2) <- (Map.mapToList mm)]
            mapTgt= weakMap [(target f1, target f2) | (f1,f2) <- (Map.mapToList mm)]
            newMapObj = Map.unions [om, mapSrc, mapTgt]
    
    
    -- | Pick one element of a list randomly.
    pickOne :: (RandomGen g) => [a] -> g -> (a,g)
    pickOne [] g = error "pickOne in an empty list."
    pickOne l g = ((l !! index),newGen) where
        (index,newGen) = (uniformR (0,(length l)-1) g)
    
    -- | Choose a random diagram in the functor category of an index category and an image category.
    pickRandomDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                        FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                        RandomGen g) => c1 -> c2 -> g -> (Diagram c1 m1 o1 c2 m2 o2, g)
    pickRandomDiagram index cat gen = pickOne (setToList.ob $ FunctorCategory index cat) gen
    
    
    
    
    -- NaturalTransformation
    
    -- | A `NaturalTransformation` between two 'Diagram's from /C/ to /D/ is a mapping from objects of /C/ to morphisms of /D/ such that naturality is respected. /C/ must be a 'FiniteCategory' because we need its objects in the mapping of a 'NaturalTransformation'.
    --
    -- Formally, let /F/ and /G/ be functors, and eta : Ob(/C/) -> Ar(/D/). The following properties should be respected :
    --
    -- prop> source F = source G
    -- prop> target F = target G
    -- prop> (eta =>$ target f) @ (F ->£ f) = (G ->£ f) @ (eta =>$ source f)
    --
    -- 'NaturalTransformation' is private, use the smart constructor 'naturalTransformation' to instantiate it.
    data NaturalTransformation c1 m1 o1 c2 m2 o2 = NaturalTransformation 
                                                        {
                                                            srcNT :: Diagram c1 m1 o1 c2 m2 o2, -- ^ The source functor (private, use 'source' instead).
                                                            tgtNT :: Diagram c1 m1 o1 c2 m2 o2, -- ^ The target functor (private, use 'target' instead).
                                                            components :: Map o1 m2 -- ^ The components
                                                        } deriving (Eq, Generic, PrettyPrint, Simplifiable)
    
    instance (Show c1, Show m1, Show o1, Show c2, Show m2, Show o2) => Show (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        show nt = "(unsafeNaturalTransformation "++ (show.srcNT $ nt) ++ " " ++ (show.tgtNT $ nt) ++ " " ++ (show.components $ nt) ++ ")"
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                       Morphism m2 o2) => 
        Morphism (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        source = srcNT
        target = tgtNT
        (@) nt2 nt1 = NaturalTransformation{srcNT=source nt1, tgtNT=target nt2, components=weakMapFromSet [(o, (nt2 =>$ o) @ (nt1 =>$ o)) | o <- ob (src.source $ nt1)]}
    
    
    -- | Apply a 'NaturalTransformation' on an object of the source 'Diagram'.
    (=>$) :: (Eq o1) => NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
    (=>$) nt x = (components nt) |!| x
    
    -- | Compose horizontally 'NaturalTransformation's.
    (<=@<=) :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                         Morphism m3 o3, Eq c3, Eq m3, Eq o3) => 
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    (<=@<=) nt2 nt1 = NaturalTransformation{srcNT=source nt2 <-@<- source nt1, tgtNT=target nt2 <-@<- target nt1, components = weakMapFromSet [(o, ((nt2 <=@<- target nt1) =>$ o) @ ((source nt2 <-@<= nt1) =>$ o)) | o <- ob (src.source $ nt1)]}
    
    -- | Alias of ('<=@<=').
    horizontalComposition :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                                       Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>  
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    horizontalComposition = (<=@<=)
    
    -- | Left whiskering allows to compose a 'Diagram' with a 'NaturalTransformation'.
    (<=@<-) :: (     Category c1 m1 o1, Morphism m1 o1, Eq m1,
               FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                        Morphism m3 o3, Eq c3, Eq m3, Eq o3) => 
                NaturalTransformation c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    (<=@<-) nt funct = NaturalTransformation{   
                                                srcNT = (source nt) <-@<- funct,
                                                tgtNT = (target nt) <-@<- funct,
                                                components = (components nt) |.| (omap funct)
                                            }
    
    -- | Alias of ('<=@<-').
    leftWhiskering :: (       Category c1 m1 o1, Morphism m1 o1, Eq m1,
                        FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                                 Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    leftWhiskering = (<=@<-)
    
    -- | Right whiskering allows to compose a 'NaturalTransformation' with a 'Diagram'.
    (<-@<=) :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                      Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                         Morphism m3 o3) => 
                Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    (<-@<=) funct nt = NaturalTransformation {  
                                                srcNT = funct <-@<- (source nt),
                                                tgtNT = funct <-@<- (target nt),
                                                components = (mmap funct) |.| (components nt)
                                             }
    
    -- | Alias of ('<-@<=').
    rightWhiskering :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                              Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                                                 Morphism m3 o3) => 
        Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    rightWhiskering = (<-@<=)
    
    -- | A datatype to represent a malformation of a 'NaturalTransformation'.
    data NaturalTransformationError c1 m1 o1 c2 m2 o2 = IncompatibleFunctorsSource{sourceCat :: c1, targetCat :: c1} -- ^ The source and target functors don't have the same source category.
                                                      | IncompatibleFunctorsTarget{sourceCat2 :: c2, targetCat2 :: c2} -- ^ The source and target functors don't have the same target category.
                                                      | WrongComponentSource{faultyComponent1 :: m2, correctSource :: o1} -- ^ The source of a component is not the image of the indexing object by the source functor. 
                                                      | WrongComponentTarget{faultyComponent2 :: m2, correctTarget :: o1} -- ^ The target of a component is not the image of the indexing object by the target functor. 
                                                      | NotTotal{domainNat :: Set o1, objectsCat :: Set o1} -- ^ The mapping from objects to morphisms is not total.
                                                      | NaturalityFail{originalMorphism :: m1} -- ^ A morphism does not close a commutative square.
                                                      deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    
    -- | Check wether the structure of a 'NaturalTransformation' is respected.
    checkNaturalTransformation :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                            Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                        NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (NaturalTransformationError c1 m1 o1 c2 m2 o2)
    checkNaturalTransformation nt
        | incompatibleFunctorsSource = Just IncompatibleFunctorsSource{sourceCat=(src.source $ nt), targetCat=(src.target $ nt)}
        | incompatibleFunctorsTarget = Just IncompatibleFunctorsTarget{sourceCat2=(tgt.source $ nt), targetCat2=(tgt.target $ nt)}
        | notTotal = Just NotTotal{domainNat = (domain.components $ nt), objectsCat = (ob.src.source $ nt)}
        | (not.(Set.null)) wrongSource = Just WrongComponentSource{faultyComponent1 = fst $ anElement wrongSource, correctSource = snd $ anElement wrongSource}
        | (not.(Set.null)) wrongTarget = Just WrongComponentTarget{faultyComponent2 = fst $ anElement wrongTarget, correctTarget = snd $ anElement wrongTarget}
        | (not.(Set.null)) naturalityFail = Just NaturalityFail{originalMorphism = anElement naturalityFail}
        | otherwise = Nothing
        where
            incompatibleFunctorsSource = (src.source $ nt) /= (src.target $ nt)
            incompatibleFunctorsTarget = (tgt.source $ nt) /= (tgt.target $ nt)  
            notTotal = (domain.components $ nt) /= (ob.src.source $ nt)
            wrongSource = [((nt =>$ i),i) | i <- (ob.src.source $ nt), (source nt) ->$ i /= source (nt =>$ i)]
            wrongTarget = [((nt =>$ i),i) | i <- (ob.src.source $ nt), (target nt) ->$ i /= target (nt =>$ i)]
            naturalityFail = [f | f <- (arrows.src.source $ nt), (target nt ->£ f) @ (nt =>$ (source f)) /= (nt =>$ (target f)) @ (source nt ->£ f)]
    
    -- | The smart constructor of 'NaturalTransformation'. Checks wether the structure is correct.
    naturalTransformation :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                       Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
                            Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Map o1 m2 -> Either (NaturalTransformationError c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2)
    naturalTransformation s t c
        | null check = Right nt
        | otherwise = Left err
        where
            nt = NaturalTransformation{srcNT=s,tgtNT=t,components=c}
            check = checkNaturalTransformation nt
            Just err = check
    
    -- | Unsafe constructor of 'NaturalTransformation' for performance purposes. It does not check the structure of the 'NaturalTransformation'.
    --
    -- Use this constructor only if the 'NaturalTransformation' is necessarily well formed.
    unsafeNaturalTransformation :: 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 s t c = NaturalTransformation{srcNT = s, tgtNT = t, components = c}
    
    indexingCategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
    indexingCategory = src.source
    
    -- Functor Category
    
    
    -- | A 'FunctorCategory' /D/^/C/ where /C/ is a 'FiniteCategory' and /D/ is a 'Category' has 'Diagram's @F : C -> D@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category.
    data FunctorCategory c1 m1 o1 c2 m2 o2 = FunctorCategory c1 c2 deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                    Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
        Category (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        identity (FunctorCategory c d) funct
            | src funct == c && tgt funct == d = NaturalTransformation{srcNT=funct, tgtNT=funct, components=weakMapFromSet [(o, identity d (funct ->$ o))| o <- (ob.src $ funct)]}
            | otherwise = error "Math.Categories.FunctorCategory.identity: functor not in the functor category."
        ar (FunctorCategory c d) s t
            | src s == src t && tgt s == tgt t = snd.(Set.catEither) $ [naturalTransformation s t mapCompo | mapCompo <- mapComponent]
            | otherwise = error "Math.Categories.FunctorCategory.ar: incompatible functors"
            where
                mapComponent = weakMap <$> cartesianProductOfSets [(\x -> (o,x)) <$> (ar (tgt s) (omap s |!| o) (omap t |!| o)) | o <- (setToList (ob.src $ s))]
                transformToFunction ((o,f):xs) x = if o == x then f else transformToFunction xs x
                
                
    
    -- | A  'FunctorCategory' where the target category is finite allows to enumerate all 'Diagram's thus making it a 'FiniteCategory'.
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
        FiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        ob (FunctorCategory s t) = snd.(Set.catEither) $ [diagram s t appO appF | appO <- appObj, appF <- ((fmap $ (Map.unions)).cartesianProductOfSets) [twoObjToMaps a b appO| a <- (setToList $ ob s), b <- (setToList $ ob s)]]
            where
                appObj = Map.enumerateMaps (ob s) (ob t)
                twoObjToMaps a b appO = Map.enumerateMaps (ar s a b) (ar t (appO |!| a) (appO |!| b))

    
    -- | A 'FunctorCategory' /D/^/C/ precomposed by a functor @F : B -> C@ where /B/ and /C/ are 'FiniteCategory' and /D/ is a 'Category'.
    --
    -- It has 'Diagram's @G o F : B -> D@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category.
    data PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = PrecomposedFunctorCategory (Diagram c1 m1 o1 c2 m2 o2) c3 deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        identity (PrecomposedFunctorCategory diag c3) = identity (FunctorCategory (src diag) c3)
        ar (PrecomposedFunctorCategory diag c3) = ar (FunctorCategory (src diag) c3)
                
                
    
    -- | A 'PrecomposedFunctorCategory' where the target category is finite allows to enumerate all 'Diagram's thus making it a 'FiniteCategory'.
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        FiniteCategory (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        ob (PrecomposedFunctorCategory diag c3) = (<-@<- diag) <$> (ob (FunctorCategory (tgt diag) c3))
        
        
    -- | A 'FunctorCategory' /D/^/C/ postcomposed by a functor @F : D -> E@ where /C/ is a 'FiniteCategory' and /D/  and /E/ are 'Category'. 
    --
    -- It has 'Diagram's @ F o G : C -> E@ as objects and 'NaturalTransformation's between them as morphisms. 'NaturalTransformation's compose vertically in this category.
    data PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = PostcomposedFunctorCategory (Diagram c2 m2 o2 c3 m3 o3) c1 deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                    Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
                    Category c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        Category (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        identity (PostcomposedFunctorCategory diag c1) = identity (FunctorCategory c1 (tgt diag))
        ar (PostcomposedFunctorCategory diag c1) = ar (FunctorCategory c1 (tgt diag))
                
                
    
    -- | A 'PostcomposedFunctorCategory' where the target category is finite allows to enumerate all 'Diagram's thus making it a 'FiniteCategory'.
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
              FiniteCategory c3 m3 o3, Morphism m3 o3, Eq c3, Eq m3, Eq o3) =>
        FiniteCategory (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (NaturalTransformation c1 m1 o1 c3 m3 o3) (Diagram c1 m1 o1 c3 m3 o3) where
        ob (PostcomposedFunctorCategory diag c1) = (diag <-@<-) <$> (ob (FunctorCategory c1 (src diag))) 
              
    -- | The insertion functor from the 'FullSubcategory' to the original category.
    insertionFunctor1 :: (Category c m o, Morphism m o, Eq o) => FullSubcategory c m o -> Diagram (FullSubcategory c m o) m o c m o
    insertionFunctor1 sc@(FullSubcategory c s) = Diagram{src=sc,tgt=c,omap=memorizeFunction id s, mmap=memorizeFunction id (arrows sc)}
    
    -- | The insertion functor from the 'InheritedFullSubcategory' to the original category.
    insertionFunctor2 :: (Category c m o, Morphism m o, Eq o) => InheritedFullSubcategory c m o -> Diagram (InheritedFullSubcategory c m o) m o c m o
    insertionFunctor2 sc@(InheritedFullSubcategory c s) = Diagram{src=sc,tgt=c,omap=memorizeFunction id s, mmap=memorizeFunction id (arrows sc)}