{-| 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 :: forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2) -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
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 :: forall c1 m1 o1 m2 o2 c2.
(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 = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target(NaturalTransformation c1 m1 o1 c2 m2 o2
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
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 :: forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone = CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
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 :: forall c1 m1 o1 c2 m2 o2.
(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 NaturalTransformation c1 m1 o1 c2 m2 o2
nt
        | Set o1 -> Bool
forall a. Set a -> Bool
Set.null (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src(Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)) = Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        | NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= Diagram c1 m1 o1 c2 m2 o2
constDiag = Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        | Bool
otherwise = Cone c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just (Cone c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2))
-> Cone c1 m1 o1 c2 m2 o2 -> Maybe (Cone c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ o2
-> One
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject o2
apexCandidate One
One NaturalTransformation c1 m1 o1 c2 m2 o2
nt
        where
            apexCandidate :: o2
apexCandidate = (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source NaturalTransformation c1 m1 o1 c2 m2 o2
nt) Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (Set o1 -> o1
forall a. Set a -> a
anElement(Set o1 -> o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src(Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
            constDiag :: Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(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 (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src(Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt(Diagram c1 m1 o1 c2 m2 o2 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) o2
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 :: forall c1 m1 o1 c2 m2 o2. ConeMorphism c1 m1 o1 c2 m2 o2 -> m2
bindingMorphismCone = CommaMorphism
  o2 One m2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> m2
forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m1
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 :: forall c1 m1 o1 c2 m2 o2.
(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 c1 m1 o1 c2 m2 o2
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
fm} =  CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiagram :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
leftDiagram = Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct
                                                                           , rightDiagram :: Diagram
  One
  One
  One
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
rightDiagram = FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct) Diagram c1 m1 o1 c2 m2 o2
diag}
                                                                where
                                                                    diagonalFunct :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct = c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunctor c1
s c2
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 :: forall c1 m1 o1 c2 m2 o2.
(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 = ConeCategory c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
terminalObjects(ConeCategory c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2))
-> (Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> Set (Cone c1 m1 o1 c2 m2 o2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> ConeCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(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
    
                                
    -- -- --------------------------------

    -- -- 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 :: forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2) -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
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 :: forall c1 m1 o1 m2 o2 c2.
(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 = NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source(NaturalTransformation c1 m1 o1 c2 m2 o2
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
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 :: forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone = CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
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 :: forall c1 m1 o1 c2 m2 o2.
(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 NaturalTransformation c1 m1 o1 c2 m2 o2
nt
        | Set o1 -> Bool
forall a. Set a -> Bool
Set.null (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src(Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)) = Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        | NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= Diagram c1 m1 o1 c2 m2 o2
constDiag = Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. Maybe a
Nothing
        | Bool
otherwise = Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a. a -> Maybe a
Just (Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2))
-> Cocone c1 m1 o1 c2 m2 o2 -> Maybe (Cocone c1 m1 o1 c2 m2 o2)
forall a b. (a -> b) -> a -> b
$ One
-> o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One o2
nadirCandidate NaturalTransformation c1 m1 o1 c2 m2 o2
nt
        where
            nadirCandidate :: o2
nadirCandidate = (NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
target NaturalTransformation c1 m1 o1 c2 m2 o2
nt) Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (Set o1 -> o1
forall a. Set a -> a
anElement(Set o1 -> o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Set o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob(c1 -> Set o1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Set o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src(Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt)
            constDiag :: Diagram c1 m1 o1 c2 m2 o2
constDiag = c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(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 (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src(Diagram c1 m1 o1 c2 m2 o2 -> c1)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt(Diagram c1 m1 o1 c2 m2 o2 -> c2)
-> (NaturalTransformation c1 m1 o1 c2 m2 o2
    -> Diagram c1 m1 o1 c2 m2 o2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> c2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall m o. Morphism m o => m -> o
source (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ NaturalTransformation c1 m1 o1 c2 m2 o2
nt) o2
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 :: forall c1 m1 o1 c2 m2 o2. CoconeMorphism c1 m1 o1 c2 m2 o2 -> m2
bindingMorphismCocone = CommaMorphism
  One o2 One m2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
-> m2
forall o1 o2 m1 m2 m3. CommaMorphism o1 o2 m1 m2 m3 -> m2
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 :: forall c1 m1 o1 c2 m2 o2.
(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 c1 m1 o1 c2 m2 o2
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c1
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c2
t,omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map o1 o2
om,mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map m1 m2
fm} =  CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiagram :: Diagram
  One
  One
  One
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
leftDiagram = FunctorCategory c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     One
     One
     One
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
-> FunctorCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct) Diagram c1 m1 o1 c2 m2 o2
diag
                                                                           , rightDiagram :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
rightDiagram = Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct}
                                                                where
                                                                    diagonalFunct :: Diagram
  c2
  m2
  o2
  (FunctorCategory c1 m1 o1 c2 m2 o2)
  (NaturalTransformation c1 m1 o1 c2 m2 o2)
  (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunct = c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, FiniteCategory c2 m2 o2,
 Morphism m2 o2) =>
c1
-> c2
-> Diagram
     c2
     m2
     o2
     (FunctorCategory c1 m1 o1 c2 m2 o2)
     (NaturalTransformation c1 m1 o1 c2 m2 o2)
     (Diagram c1 m1 o1 c2 m2 o2)
diagonalFunctor c1
s c2
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 :: forall c1 m1 o1 c2 m2 o2.
(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 = CoconeCategory c1 m1 o1 c2 m2 o2 -> Set (Cocone c1 m1 o1 c2 m2 o2)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
initialObjects(CoconeCategory c1 m1 o1 c2 m2 o2
 -> Set (Cocone c1 m1 o1 c2 m2 o2))
-> (Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> Set (Cocone c1 m1 o1 c2 m2 o2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> CoconeCategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
(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