{-# LANGUAGE MonadComprehensions #-}
{-| 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)'limits' of a 'Diagram'. Note that the functions 'limits' and 'colimits' scan the entire 'ConeCategory' to find the limits and colimits of a 'Diagram'. It is therefore quite slow, if you work with a 'Category' where limits and colimits are easily constructible like in Set or in Cat, you should maybe construct them yourself or use Kan extensions of 'Math.Functors.SetValued' and the function 'colimitOfCompositionGraphs'.
-}

module Math.Categories.ConeCategory
(
    -- * Cone
    Cone(..),
    -- ** Cone construcion
    cone,
    unsafeCone,
    completeCone,
    -- ** Helper functions
    apex,
    baseCone,
    legsCone,
    universeCategoryCone,
    indexingCategoryCone,
    precomposeConeWithMorphism,
    postcomposeConeWithFunctor,
    topInjectionsCone,
    -- * Cone Morphism
    ConeMorphism,
    -- ** Helper function
    bindingMorphismCone,
    -- * Cone Category
    ConeCategory,
    -- ** Helper functions
    coneCategory,
    limits,
    -- * Cocone
    Cocone(..),
    -- ** Cocone construction
    cocone,
    unsafeCocone,
    completeCocone,
    -- ** Helper functions
    nadir,
    baseCocone,
    legsCocone,
    universeCategoryCocone,
    indexingCategoryCocone,
    precomposeCoconeWithFunctor,
    postcomposeCoconeWithMorphism,
    bottomInjectionsCocone,
    -- * 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              Data.Simplifiable
    
    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)
    
    -- | Constructs a 'Cone' from an apex and a 'NaturalTransformation'. Return nothing if the source of the 'NaturalTransformation' is not a constant diagram on the apex.
    cone :: (Morphism m1 o1, FiniteCategory c1 m1 o1,
             Morphism m2 o2, FiniteCategory c2 m2 o2,
             Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) => 
            o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
    cone apex nat
        | constantDiagram indexingCat universeCat apex /= source nat = Nothing
        | otherwise = Just result
        where 
            indexingCat = src.source $ nat
            universeCat = tgt.source $ nat
            result = unsafeCommaObject apex One nat
            
    -- | Constructs a 'Cone' from an apex and a 'NaturalTransformation'. Does NOT check if the source of the 'NaturalTransformation' is a constant diagram on the apex. You may use this function at your own risk, consider using 'cone' if you are not sure.
    --
    -- If you give an incomplete natural transformation to this function, you can use 'completeCone' to complete the natural transformation.
    unsafeCone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
    unsafeCone apex nat = unsafeCommaObject apex One nat
    
    -- | Given a cone with a partial underlying natural transformation, tries to complete it. You can use 'checkNaturalTransformation.legsCone' to check that the cone was correctly completed. 
    completeCone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cone c1 m1 o1 c2 m2 o2 -> Cone c1 m1 o1 c2 m2 o2
    completeCone c = unsafeCommaObject (apex c) One newNat
        where
            nat = legsCone c
            prevComp = components nat
            validArrowOnTop x = [f | f <- arTo (indexingCategory nat) x, (source f) `Set.isIn` (keys' prevComp)]
            comp x
                | not $ null $ prevComp |?| x = prevComp |?| x
                | not $ Set.null $ validArrowOnTop x = Just $ ((target nat) ->£ (anElement $ validArrowOnTop x)) @ (prevComp |!| (source (anElement $ validArrowOnTop x)))
                | otherwise = Nothing
            newComp = weakMapFromSet $ Set.catMaybes [sequence (x,comp x) | x <- ob (indexingCategory nat)]
            newNat = unsafeNaturalTransformation (source nat) (target nat) newComp
    
    
    -- | 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) => 
            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
        
    -- | 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).
    --
    -- Note that the functions 'limits' and 'colimits' scan the entire 'ConeCategory' to find the limits and colimits of a 'Diagram'. It is therefore quite slow, if you work with a 'Category' where limits and colimits are easily constructible like in Set or in Cat, you should maybe construct them yourself or use Kan extensions of 'Math.Functors.SetValued' and the function 'colimitOfCompositionGraphs'.
    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
    
    
    -- | Given a category, return equivalence classes according to the loop relation : two objects A and B are equivalent if and only if there is a morphism from A to B and a morphism from B to A.
    loopClasses :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
        c -> Set (Set o)
    loopClasses c = [[y | y <- ob c, not $ Set.null $ ar c x y, not $ Set.null $ ar c y x] | x <- ob c]
    
    -- | The top objects of a category are all loop classes X such that all arrows going to X have source in X.                               
    topObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
        c -> Set (Set o)
    topObjects c = [loopClass | loopClass <- loopClasses c, Set.null $ Set.filter (\f -> (not (source f `isIn` loopClass)) && (target f `isIn` loopClass)) $ arrows c]
                     
    -- | Possible domains of the injective map to determine if a cone is top contained in another.
    possibleDomainsTopContained :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
        c -> Set [o]
    possibleDomainsTopContained c = set.setToList $ cartesianProductOfSets $ setToList $ topObjects c
    
    -- | Enumerate injective maps which satisfy a condition.
    enumerateInjectiveMaps :: (Eq a, Eq b) => (a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
    enumerateInjectiveMaps cond dom codom
        | Set.null dom = set [weakMap []]
        | Set.null codom = set []
        | Set.null compatibleYs = set []
        | otherwise = Map.insert x y <$> enumerateInjectiveMaps cond xs ys
            where
                x = anElement dom
                xs = Set.delete x dom
                compatibleYs = [a | a <- codom, cond x a]
                y = anElement compatibleYs
                ys = Set.delete y codom
    
    
    -- | A 'Cone' c1 is top contained in another 'Cone' c2 if every top leg of c1 is a leg of c2 in an injective manner.
    topInjectionsCone :: (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) => 
        Cone c1 m1 o1 c3 m3 o3 -> Cone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
    topInjectionsCone c1 c2
        | apex c1 == apex c2 = maps
        | otherwise = set []
        where
            doms = possibleDomainsTopContained $ indexingCategoryCone c1
            maps = Set.concat2 [enumerateInjectiveMaps (\x y -> legsCone c1 =>$ x == legsCone c2 =>$ y) (set dom) (ob (indexingCategoryCone c2)) | dom <- doms]
    
    -- | Precompose a cone with a morphism going to the apex. (Does not check that the morphism has the apex as target.)
    precomposeConeWithMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                        Morphism m2 o2) => 
        Cone c1 m1 o1 c2 m2 o2 -> m2 -> Cone c1 m1 o1 c2 m2 o2
    precomposeConeWithMorphism c m = unsafeCommaObject (source m) One (unsafeNaturalTransformation (source $ legsCone c) (target $ legsCone c) ((@ m) <$> (components $ legsCone c)))
    
    -- | Postcompose a cone with a functor going from the base. 
    postcomposeConeWithFunctor :: (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) => 
        Cone c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c3 m3 o3 -> Cone c1 m1 o1 c3 m3 o3
    postcomposeConeWithFunctor c f = unsafeCommaObject (f ->$ (apex c)) One (f <-@<= (legsCone c))
    
    -- -- --------------------------------
    -- -- 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)
    
    -- | Constructs a 'Cocone' from a nadir and a 'NaturalTransformation'. Return nothing if the target of the 'NaturalTransformation' is not a constant diagram on the nadir.
    cocone :: (Morphism m1 o1, FiniteCategory c1 m1 o1,
             Morphism m2 o2, FiniteCategory c2 m2 o2,
             Eq c1, Eq m1, Eq o1, Eq c2, Eq m2, Eq o2) => 
            o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
    cocone nadir nat
        | constantDiagram indexingCat universeCat nadir /= target nat = Nothing
        | otherwise = Just result
        where 
            indexingCat = src.source $ nat
            universeCat = tgt.source $ nat
            result = unsafeCommaObject One nadir nat
            
    -- | Constructs a 'Cocone' from a nadir and a 'NaturalTransformation'. Does NOT check if the target of the 'NaturalTransformation' is a constant diagram on the nadir. You may use this function at your own risk, consider using 'cocone' if you are not sure.
    --
    -- If you give an incomplete natural transformation to this function, you can use 'completeCocone' to complete the natural transformation.
    unsafeCocone :: o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
    unsafeCocone nadir nat = unsafeCommaObject One nadir nat
    
    -- | Given a cocone with a partial underlying natural transformation, tries to complete it. You can use 'checkNaturalTransformation.legsCocone' to check that the cocone was correctly completed. 
    completeCocone :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Morphism m2 o2) => Cocone c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c2 m2 o2
    completeCocone cc = unsafeCommaObject One (nadir cc) newNat
        where
            nat = legsCocone cc
            prevComp = components nat
            validArrowOnBottom x = [f | f <- arFrom (indexingCategory nat) x, (target f) `Set.isIn` (keys' prevComp)]
            comp x
                | not $ null $ prevComp |?| x = prevComp |?| x
                | not $ Set.null $ validArrowOnBottom x = Just $ (prevComp |!| (target (anElement $ validArrowOnBottom x))) @ ((source nat) ->£ (anElement $ validArrowOnBottom x))
                | otherwise = Nothing
            newComp = weakMapFromSet $ Set.catMaybes [sequence (x,comp x) | x <- ob (indexingCategory nat)]
            newNat = unsafeNaturalTransformation (source nat) (target nat) newComp
    
    -- | 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) => 
            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).
    -- 
    -- Note that the functions 'limits' and 'colimits' scan the entire 'ConeCategory' to find the limits and colimits of a 'Diagram'. It is therefore quite slow, if you work with a 'Category' where limits and colimits are easily constructible like in Set or in Cat, you should maybe construct them yourself or use Kan extensions of 'Math.Functors.SetValued' and the function 'colimitOfCompositionGraphs'.
    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
    
    -- | Return the category in which a 'Cone' lives.
    universeCategoryCone :: (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 -> c2
    universeCategoryCone = tgt.source.legsCone
    
    -- | Return the category in which a 'Cocone' lives.
    universeCategoryCocone :: (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 -> c2
    universeCategoryCocone = tgt.source.legsCocone
    
    -- | Return the indexing category of a 'Cone'.
    indexingCategoryCone :: (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 -> c1
    indexingCategoryCone = src.source.legsCone
    
    -- | Return the indexing category of a 'Cocone'.
    indexingCategoryCocone :: (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 -> c1
    indexingCategoryCocone = src.source.legsCocone
    
    
    -- | The bottom objects of a category are all loop classes X such that all arrows going from X have target in X.                               
    bottomObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
        c -> Set (Set o)
    bottomObjects c = [loopClass | loopClass <- loopClasses c, Set.null $ Set.filter (\f -> (not (target f `isIn` loopClass)) && (source f `isIn` loopClass)) $ arrows c]
                     
    -- | Possible domains of the injective map to determine if a cocone is bottom contained in another.
    possibleDomainsBottomContained :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
        c -> Set [o]
    possibleDomainsBottomContained c = set.setToList $ cartesianProductOfSets $ setToList $ bottomObjects c
    
    -- | A 'Cocone' c1 is bottom contained in another 'Cocone' c2 if every bottom leg of c1 is a leg of c2 in an injective manner.
    bottomInjectionsCocone :: (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) => 
        Cocone c1 m1 o1 c3 m3 o3 -> Cocone c2 m2 o2 c3 m3 o3 -> Set (Map o1 o2)
    bottomInjectionsCocone cc1 cc2
        | nadir cc1 == nadir cc2 = maps
        | otherwise = set []
        where
            doms = possibleDomainsBottomContained $ indexingCategoryCocone cc1
            maps = Set.concat2 [enumerateInjectiveMaps (\x y -> legsCocone cc1 =>$ x == legsCocone cc2 =>$ y) (set dom) (ob (indexingCategoryCocone cc2)) | dom <- doms]
            
     -- | Precompose a cocone with a functor going to the base.
    precomposeCoconeWithFunctor :: (      Category 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) =>
        Cocone c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Cocone c1 m1 o1 c3 m3 o3
    precomposeCoconeWithFunctor cc f = unsafeCommaObject One (nadir cc) ((legsCocone cc) <=@<- f)
    
    -- | Postcompose a cone with a morphism going from the nadir. (Does not check that the morphism has the nadir as source.)
    postcomposeCoconeWithMorphism :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                                         Morphism m2 o2) =>
        Cocone c1 m1 o1 c2 m2 o2 -> m2 -> Cocone c1 m1 o1 c2 m2 o2
    postcomposeCoconeWithMorphism cc m = unsafeCommaObject One (target m) (unsafeNaturalTransformation (source $ legsCocone cc) (target $ legsCocone cc) ((m @) <$> (components $ legsCocone cc)))