{-| Module  : FiniteCategories
Description : Category of 'Cone's of a 'Diagram'.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Category of 'Cone's of a 'Diagram'.

This module allows to find the (co)'limit' of a 'Diagram'.
-}

module Math.Categories.ConeCategory
(
    -- * Cone
    Cone,
    -- ** Helper functions
    apex,
    baseCone,
    legsCone,
    naturalTransformationToCone,
    -- * Cone Morphism
    ConeMorphism,
    -- ** Helper function
    bindingMorphismCone,
    -- * Cone Category
    ConeCategory,
    -- ** Helper functions
    coneCategory,
    limits,
    -- * Cocone
    Cocone,
    -- ** Helper functions
    nadir,
    baseCocone,
    legsCocone,
    naturalTransformationToCocone,
    -- * Cocone Morphism
    CoconeMorphism,
    -- ** Helper function
    bindingMorphismCocone,
    -- * Cocone Category
    CoconeCategory,
    -- ** Helper functions
    coconeCategory,
    colimits,
)
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.FiniteCategory
    import              Math.Categories.CommaCategory
    import              Math.Categories.FunctorCategory
    import              Math.Functors.DiagonalFunctor
    import              Math.FiniteCategories.One
    

    -- --------------------------------
    -- Cone related functions and types.
    -- --------------------------------
        
    -- | A `Cone` is a `CommaObject` in the `CommaCategory` (/D/|1_/F/) where /D/ is the 'diagonalFunctor' and /F/ is the 'Diagram' of interest.
    --
    -- Intuitively, a 'Cone' is an 'apex', a base and a set of legs indexed by the indexing objects of /F/ such that the legs commute with every arrow in the base of the 'Cone'.
    --
    -- See "Categories for the working mathematician", Saunders Mac Lane, P.67.
    type Cone c1 m1 o1 c2 m2 o2 = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | Return the apex of a `Cone`.
    apex :: Cone c1 m1 o1 c2 m2 o2 -> o2
    apex = indexSource

    -- | Return the base of a 'Cone'.
    baseCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                      Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
            Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
    baseCone = target.selectedArrow
    
    -- | Return the legs of a 'Cone' as a 'NaturalTransformation'.
    legsCone :: Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
    legsCone = selectedArrow

    -- | Transform a `NaturalTransformation` from a 'constantDiagram' to a 'Diagram' /D/ into a `Cone` on /D/.
    naturalTransformationToCone :: (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) =>
                                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
    naturalTransformationToCone nt
        | Set.null (ob (src.source $ nt)) = Nothing
        | source nt /= constDiag = Nothing
        | otherwise = Just $ unsafeCommaObject apexCandidate One nt
        where
            apexCandidate = (source nt) ->$ (anElement.ob.src.source $ nt)
            constDiag = constantDiagram (src.source $ nt) (tgt.source $ nt) apexCandidate
        
    -- | A `ConeMorphism` is a morphism binding two 'Cone's. Formally, it is a 'CommaMorphism' in the 'CommaCategory' (/D/|1_/F/) where /D/ is the 'diagonalFunctor' and /F/ is the 'Diagram' of interest.
    type ConeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | Return the binding morphism between the two 'Cone's of a 'ConeMorphism.
    bindingMorphismCone :: ConeMorphism c1 m1 o1 c2 m2 o2 -> m2
    bindingMorphismCone = indexFirstArrow
    
    -- | A `ConeCategory` is the category of 'Cone's of a given 'Diagram', it is a `CommaCategory` (/D/|1_/F/) where /D/ is the 'diagonalFunctor' and /F/ is the 'Diagram' of interest.
    type ConeCategory c1 m1 o1 c2 m2 o2 = CommaCategory c2 m2 o2 One One One (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)
    

    -- | Construct the category of cones of a 'Diagram'.
    coneCategory :: (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) =>
                       Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
    coneCategory diag@Diagram{src=s,tgt=t,omap=om,mmap=fm} =  CommaCategory {leftDiagram = diagonalFunct
                                                                           , rightDiagram = selectObject (tgt diagonalFunct) diag}
                                                                where
                                                                    diagonalFunct = diagonalFunctor s t
            
    -- | Returns limits of a diagram (terminal cones).
    limits :: (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) =>
               Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
    limits = terminalObjects.coneCategory
    
                                
    -- -- --------------------------------
    -- -- Cocone related functions and types.
    -- -- --------------------------------
    
    -- | A `Cocone` is a `CommaObject` in the `CommaCategory` (1_/F/|/D/) where /D/ is the 'diagonalFunctor' and /F/ is the 'Diagram' of interest.
    --
    -- Intuitively, a 'Cocone' is a 'nadir', a base and a set of legs indexed by the indexing objects of /F/ such that the legs commute with every arrow in the base of the 'Cocone'.
    --
    -- A 'Cocone' is simply the dual of a 'Cone'.
    type Cocone c1 m1 o1 c2 m2 o2 = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | Return the nadir of a `Cocone`.
    nadir :: Cocone c1 m1 o1 c2 m2 o2 -> o2
    nadir = indexTarget

    -- | Return the base of a 'Cocone'.
    baseCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                            Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
            Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
    baseCocone = source.selectedArrow
    
    -- | Return the legs of a 'Cocone' as a 'NaturalTransformation'.
    legsCocone :: Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
    legsCocone = selectedArrow

    -- | Transform a `NaturalTransformation` from a 'Diagram' /D/ to a 'constantDiagram' into a `Cocone` on /D/.
    naturalTransformationToCocone :: (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) =>
                                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
    naturalTransformationToCocone nt
        | Set.null (ob (src.source $ nt)) = Nothing
        | target nt /= constDiag = Nothing
        | otherwise = Just $ unsafeCommaObject One nadirCandidate nt
        where
            nadirCandidate = (target nt) ->$ (anElement.ob.src.source $ nt)
            constDiag = constantDiagram (src.source $ nt) (tgt.source $ nt) nadirCandidate
        
    -- | A `CoconeMorphism` is a morphism binding two 'Cocone's. Formally, it is a 'CommaMorphism' in the 'CommaCategory' (1_/F/|/D/) where /D/ is the 'diagonalFunctor' and /F/ is the 'Diagram' of interest.
    type CoconeMorphism c1 m1 o1 c2 m2 o2 = CommaMorphism One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
    
    -- | Return the binding morphism between the two 'Cocone's of a 'CoconeMorphism.
    bindingMorphismCocone :: CoconeMorphism c1 m1 o1 c2 m2 o2 -> m2
    bindingMorphismCocone = indexSecondArrow
    
    -- | A `CoconeCategory` is the category of 'Cocone's of a given 'Diagram', it is a `CommaCategory` (1_/F/|/D/) where /D/ is the 'diagonalFunctor' and /F/ is the 'Diagram' of interest.
    type CoconeCategory c1 m1 o1 c2 m2 o2 = CommaCategory One One One c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

    -- | Construct the category of cocones of a 'Diagram'.
    coconeCategory :: (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) =>
                       Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
    coconeCategory diag@Diagram{src=s,tgt=t,omap=om,mmap=fm} =  CommaCategory {leftDiagram = selectObject (tgt diagonalFunct) diag
                                                                           , rightDiagram = diagonalFunct}
                                                                where
                                                                    diagonalFunct = diagonalFunctor s t
            
    -- | Returns colimits of a diagram (initial cocones).
    colimits :: (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) =>
               Diagram c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
    colimits = initialObjects.coconeCategory