{-# LANGUAGE MultiParamTypeClasses, MonadComprehensions  #-}

{-| 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. We don't see a diagram as a morphism of categories but as a selection in the target category. See 'FinCat' for a context where 'Diagram's are seen as morphisms of categories.

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

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,
    -- ** Operators
    (->$),
    (->£),
    (<-@<-),
    -- ** Usual diagrams
    selectObject,
    constantDiagram,
    discreteDiagram,
    parallelDiagram,
    -- *** Insertion diagrams for subcategories
    insertionFunctor1,
    insertionFunctor2,
    -- ** Diagram construction helper
    completeDiagram,
    pickRandomDiagram,
    -- * Natural transformation
    NaturalTransformation,
    -- ** Getter
    components,
    -- ** Check structure
    NaturalTransformationError,
    checkNaturalTransformation,
    naturalTransformation,
    unsafeNaturalTransformation,
    -- ** Operators
    (=>$),
    (<=@<=),
    horizontalComposition,
    (<=@<-),
    leftWhiskering,
    (<-@<=),
    rightWhiskering,
    -- * 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              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)
    
    
    -- | 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 constructor 'diagram' which checks the structure of the 'Diagram' at construction.
    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
                                              } deriving (Eq, Show)
    
    instance (  PrettyPrint c1, PrettyPrint m1, PrettyPrint o1, Eq m1, Eq o1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2) => PrettyPrint (Diagram c1 m1 o1 c2 m2 o2) where
        pprint funct = "Diagram(" ++ pprint (src funct) ++ "->" ++ pprint (tgt funct) ++ "," ++ pprint (omap funct) ++ "," ++ pprint (mmap funct) ++ ")"
    
    -- | 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.
    (->£) :: (Eq m1) => Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
    (->£) f x = mmap f |!| x
    
    -- | Compose two 'Diagram's.
    (<-@<-) :: (Eq o2, Eq m2) => 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 = (mmap g) |.| (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)
                               
    -- | Check wether the properties of a 'Diagram' are respected where the target category is 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}
        | domain fm /= arrows s = 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 <- (arrows s), g <- (arFrom s (target f)), fm |!| (g @ f) /= (fm |!| g) @ (fm |!| f)]
            
    -- | Check wether the properties of a 'Diagram' are respected where the 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}
        | domain fm /= arrows s = 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))}
        | 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 <- (arrows s), g <- (arFrom s (target f)), fm |!| (g @ f) /= (fm |!| g) @ (fm |!| f)]
    
    -- | Smart constructor of 'Diagram'.
    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 = checkFiniteDiagram diag
            Just err = check
    
    -- | Complete a partial 'Diagram' by adding the mapping between identities and the mapping between composite morphisms using the decomposition of the indexing category.
    --
    -- Does not check the structure of the resulting 'Diagram', you can use 'checkFiniteDiagram' 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=om, mmap=Map.unions [mm, mapId, mapCompo] }
        where
            mapId = weakMapFromSet [(identity s o, identity t (om |!| o)) | o <- ob s]
            mapCompo = weakMapFromSet [(f, compose $ (mm |!|) <$> decompose s f) | f <- arrows s, isComposite s f]
    
    
    -- | 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)
    
    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 (  PrettyPrint c1, PrettyPrint m1, PrettyPrint o1, Eq m1, Eq o1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2) => PrettyPrint (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        pprint nt = "NaturalTransformation(" ++ pprint (srcNT nt) ++ "->" ++ pprint (tgtNT nt) ++ "," ++ pprint (components nt) ++ ")"
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                       Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
        Morphism (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        source = srcNT
        target = tgtNT
        (@?) nt2 nt1
            | target nt1 == source nt2 && (src.source $ nt1) == (src.target $ nt2) && (tgt.source $ nt1) == (tgt.target $ nt2) = Just NaturalTransformation{srcNT=source nt1, tgtNT=target nt2, components=weakMapFromSet [(o, (nt2 =>$ o) @ (nt1 =>$ o)) | o <- ob (src.source $ nt1)]}
            | otherwise = Nothing
    
    
    -- | 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'.
    (<=@<-) :: (                        Morphism m1 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 -> 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 :: (                          Morphism m1 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 -> 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,
                                         Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                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,
                                                 Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
        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.
                                                      | 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)
    
    
    -- | 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)) 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)
            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}
    
    -- 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)
    
    instance (PrettyPrint c1, PrettyPrint c2) => PrettyPrint (FunctorCategory c1 m1 o1 c2 m2 o2) where
        pprint (FunctorCategory c d) = "FunctorCategory(" ++ pprint c ++ "," ++ pprint d ++ ")"
        
    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)
    
    instance   (PrettyPrint c1, PrettyPrint m1, PrettyPrint o1, Eq m1, Eq o1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2,
                PrettyPrint c3) => PrettyPrint (PrecomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        pprint (PrecomposedFunctorCategory diag d) = "PrecomposedFunctorCategory(" ++ pprint diag ++ "," ++ pprint d ++ ")"
        
    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)
    
    instance   (PrettyPrint c1,
                PrettyPrint c2, PrettyPrint m2, PrettyPrint o2, Eq m2, Eq o2,
                PrettyPrint c3, PrettyPrint m3, PrettyPrint o3, Eq m3, Eq o3) => PrettyPrint (PostcomposedFunctorCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) where
        pprint (PostcomposedFunctorCategory diag d) = "PostcomposedFunctorCategory(" ++ pprint diag ++ "," ++ pprint d ++ ")"
        
    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)}