{-# 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 :: forall m1 o1 c1 m2 o2 c2.
(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 o2
apex NaturalTransformation c1 m1 o1 c2 m2 o2
nat
        | 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 c1
indexingCat c2
universeCat o2
apex Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= 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
nat = 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
result
        where 
            indexingCat :: c1
indexingCat = 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
nat
            universeCat :: c2
universeCat = 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
nat
            result :: Cone c1 m1 o1 c2 m2 o2
result = 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
apex One
One NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone o2
apex NaturalTransformation c1 m1 o1 c2 m2 o2
nat = o2
-> One
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> CommaObject o2 One (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject o2
apex One
One NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: forall c1 m1 o1 m2 o2 c2.
(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 Cone c1 m1 o1 c2 m2 o2
c = 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 (Cone c1 m1 o1 c2 m2 o2 -> o2
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone c1 m1 o1 c2 m2 o2
c) One
One NaturalTransformation c1 m1 o1 c2 m2 o2
newNat
        where
            nat :: NaturalTransformation c1 m1 o1 c2 m2 o2
nat = Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c1 m1 o1 c2 m2 o2
c
            prevComp :: Map o1 m2
prevComp = NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components NaturalTransformation c1 m1 o1 c2 m2 o2
nat
            validArrowOnTop :: o1 -> Set m1
validArrowOnTop o1
x = [m1
f | m1
f <- c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arTo (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
indexingCategory NaturalTransformation c1 m1 o1 c2 m2 o2
nat) o1
x, (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
f) o1 -> Set o1 -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.isIn` (Map o1 m2 -> Set o1
forall k v. Map k v -> Set k
keys' Map o1 m2
prevComp)]
            comp :: o1 -> Maybe m2
comp o1
x
                | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe m2 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe m2 -> Bool) -> Maybe m2 -> Bool
forall a b. (a -> b) -> a -> b
$ Map o1 m2
prevComp Map o1 m2 -> o1 -> Maybe m2
forall k v. Eq k => Map k v -> k -> Maybe v
|?| o1
x = Map o1 m2
prevComp Map o1 m2 -> o1 -> Maybe m2
forall k v. Eq k => Map k v -> k -> Maybe v
|?| o1
x
                | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m1 -> Bool
forall a. Set a -> Bool
Set.null (Set m1 -> Bool) -> Set m1 -> Bool
forall a b. (a -> b) -> a -> b
$ o1 -> Set m1
validArrowOnTop o1
x = m2 -> Maybe m2
forall a. a -> Maybe a
Just (m2 -> Maybe m2) -> m2 -> Maybe m2
forall a b. (a -> b) -> a -> b
$ ((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
nat) Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (Set m1 -> m1
forall a. Set a -> a
anElement (Set m1 -> m1) -> Set m1 -> m1
forall a b. (a -> b) -> a -> b
$ o1 -> Set m1
validArrowOnTop o1
x)) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (Map o1 m2
prevComp Map o1 m2 -> o1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
source (Set m1 -> m1
forall a. Set a -> a
anElement (Set m1 -> m1) -> Set m1 -> m1
forall a b. (a -> b) -> a -> b
$ o1 -> Set m1
validArrowOnTop o1
x)))
                | Bool
otherwise = Maybe m2
forall a. Maybe a
Nothing
            newComp :: Map o1 m2
newComp = Set (o1, m2) -> Map o1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet (Set (o1, m2) -> Map o1 m2) -> Set (o1, m2) -> Map o1 m2
forall a b. (a -> b) -> a -> b
$ Set (Maybe (o1, m2)) -> Set (o1, m2)
forall a. Set (Maybe a) -> Set a
Set.catMaybes [(o1, Maybe m2) -> Maybe (o1, m2)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => (o1, m a) -> m (o1, a)
sequence (o1
x,o1 -> Maybe m2
comp o1
x) | o1
x <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
indexingCategory NaturalTransformation c1 m1 o1 c2 m2 o2
nat)]
            newNat :: NaturalTransformation c1 m1 o1 c2 m2 o2
newNat = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
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 (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
nat) (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
nat) Map o1 m2
newComp
    
    
    -- | 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) => 
            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) =>
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)
-> (Cone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone 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
        
    -- | 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 {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).

    --

    -- 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 :: 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
    
    
    -- | 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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses c
c = [[o
y | o
y <- c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
x o
y, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
y o
x] | o
x <- c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
topObjects c
c = [Set o
loopClass | Set o
loopClass <- c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses c
c, Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
f -> (Bool -> Bool
not (m -> o
forall m o. Morphism m o => m -> o
source m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsTopContained c
c = [[o]] -> Set [o]
forall a. [a] -> Set a
set([[o]] -> Set [o]) -> (Set [o] -> [[o]]) -> Set [o] -> Set [o]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set [o] -> [[o]]
forall a. Eq a => Set a -> [a]
setToList (Set [o] -> Set [o]) -> Set [o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ [Set o] -> Set [o]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets ([Set o] -> Set [o]) -> [Set o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ Set (Set o) -> [Set o]
forall a. Eq a => Set a -> [a]
setToList (Set (Set o) -> [Set o]) -> Set (Set o) -> [Set o]
forall a b. (a -> b) -> a -> b
$ c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
topObjects c
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 :: forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps a -> b -> Bool
cond Set a
dom Set b
codom
        | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
dom = [Map a b] -> Set (Map a b)
forall a. [a] -> Set a
set [AssociationList a b -> Map a b
forall k v. AssociationList k v -> Map k v
weakMap []]
        | Set b -> Bool
forall a. Set a -> Bool
Set.null Set b
codom = [Map a b] -> Set (Map a b)
forall a. [a] -> Set a
set []
        | Set b -> Bool
forall a. Set a -> Bool
Set.null Set b
compatibleYs = [Map a b] -> Set (Map a b)
forall a. [a] -> Set a
set []
        | Bool
otherwise = a -> b -> Map a b -> Map a b
forall k a. k -> a -> Map k a -> Map k a
Map.insert a
x b
y (Map a b -> Map a b) -> Set (Map a b) -> Set (Map a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps a -> b -> Bool
cond Set a
xs Set b
ys
            where
                x :: a
x = Set a -> a
forall a. Set a -> a
anElement Set a
dom
                xs :: Set a
xs = a -> Set a -> Set a
forall a. Eq a => a -> Set a -> Set a
Set.delete a
x Set a
dom
                compatibleYs :: Set b
compatibleYs = [b
a | b
a <- Set b
codom, a -> b -> Bool
cond a
x b
a]
                y :: b
y = Set b -> b
forall a. Set a -> a
anElement Set b
compatibleYs
                ys :: Set b
ys = b -> Set b -> Set b
forall a. Eq a => a -> Set a -> Set a
Set.delete b
y Set b
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 :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 Cone c1 m1 o1 c3 m3 o3
c1 Cone c2 m2 o2 c3 m3 o3
c2
        | Cone c1 m1 o1 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone c1 m1 o1 c3 m3 o3
c1 o3 -> o3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cone c2 m2 o2 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone c2 m2 o2 c3 m3 o3
c2 = Set (Map o1 o2)
maps
        | Bool
otherwise = [Map o1 o2] -> Set (Map o1 o2)
forall a. [a] -> Set a
set []
        where
            doms :: Set [o1]
doms = c1 -> Set [o1]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsTopContained (c1 -> Set [o1]) -> c1 -> Set [o1]
forall a b. (a -> b) -> a -> b
$ Cone c1 m1 o1 c3 m3 o3 -> c1
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 -> c1
indexingCategoryCone Cone c1 m1 o1 c3 m3 o3
c1
            maps :: Set (Map o1 o2)
maps = Set (Set (Map o1 o2)) -> Set (Map o1 o2)
forall a. Set (Set a) -> Set a
Set.concat2 [(o1 -> o2 -> Bool) -> Set o1 -> Set o2 -> Set (Map o1 o2)
forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps (\o1
x o2
y -> Cone c1 m1 o1 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c1 m1 o1 c3 m3 o3
c1 NaturalTransformation c1 m1 o1 c3 m3 o3 -> o1 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
x m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cone c2 m2 o2 c3 m3 o3 -> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c2 m2 o2 c3 m3 o3
c2 NaturalTransformation c2 m2 o2 c3 m3 o3 -> o2 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o2
y) ([o1] -> Set o1
forall a. [a] -> Set a
set [o1]
dom) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Cone c2 m2 o2 c3 m3 o3 -> c2
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 -> c1
indexingCategoryCone Cone c2 m2 o2 c3 m3 o3
c2)) | [o1]
dom <- Set [o1]
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,
                                         Category c2 m2 o2, Morphism m2 o2) => 
        Cone c1 m1 o1 c2 m2 o2 -> m2 -> Cone c1 m1 o1 c2 m2 o2
    precomposeConeWithMorphism :: 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) =>
Cone c1 m1 o1 c2 m2 o2 -> m2 -> Cone c1 m1 o1 c2 m2 o2
precomposeConeWithMorphism Cone c1 m1 o1 c2 m2 o2
c m2
m = 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 (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m) One
One (Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
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 (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)
-> (Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cone 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
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone (Cone c1 m1 o1 c2 m2 o2 -> c1) -> Cone c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ Cone c1 m1 o1 c2 m2 o2
c) (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)
-> (Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cone 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
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone (Cone c1 m1 o1 c2 m2 o2 -> c2) -> Cone c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ Cone c1 m1 o1 c2 m2 o2
c) (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m)) (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)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall a b. (a -> b) -> a -> b
$ Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c1 m1 o1 c2 m2 o2
c) ((m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ m2
m) (m2 -> m2) -> Map o1 m2 -> Map o1 m2
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall a b. (a -> b) -> a -> b
$ Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c1 m1 o1 c2 m2 o2
c)))
    
    -- | Postcompose a cone with a functor going from the universe category. 

    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 :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 Cone c1 m1 o1 c2 m2 o2
c Diagram c2 m2 o2 c3 m3 o3
f = o3
-> One
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> CommaObject o3 One (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject (Diagram c2 m2 o2 c3 m3 o3
f Diagram c2 m2 o2 c3 m3 o3 -> o2 -> o3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ (Cone c1 m1 o1 c2 m2 o2 -> o2
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone c1 m1 o1 c2 m2 o2
c)) One
One (Diagram c2 m2 o2 c3 m3 o3
f Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 Morphism m3 o3) =>
Diagram c2 m2 o2 c3 m3 o3
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<-@<= (Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone Cone c1 m1 o1 c2 m2 o2
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 :: forall m1 o1 c1 m2 o2 c2.
(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 o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
nat
        | 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 c1
indexingCat c2
universeCat o2
nadir Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Bool
forall a. Eq a => a -> a -> Bool
/= 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
nat = 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
result
        where 
            indexingCat :: c1
indexingCat = 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
nat
            universeCat :: c2
universeCat = 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
nat
            result :: Cocone c1 m1 o1 c2 m2 o2
result = 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
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
nat = One
-> o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> CommaObject One o2 (NaturalTransformation c1 m1 o1 c2 m2 o2)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One o2
nadir NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: forall c1 m1 o1 m2 o2 c2.
(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 Cocone c1 m1 o1 c2 m2 o2
cc = 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 (Cocone c1 m1 o1 c2 m2 o2 -> o2
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone c1 m1 o1 c2 m2 o2
cc) NaturalTransformation c1 m1 o1 c2 m2 o2
newNat
        where
            nat :: NaturalTransformation c1 m1 o1 c2 m2 o2
nat = Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c1 m1 o1 c2 m2 o2
cc
            prevComp :: Map o1 m2
prevComp = NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components NaturalTransformation c1 m1 o1 c2 m2 o2
nat
            validArrowOnBottom :: o1 -> Set m1
validArrowOnBottom o1
x = [m1
f | m1
f <- c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
indexingCategory NaturalTransformation c1 m1 o1 c2 m2 o2
nat) o1
x, (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
f) o1 -> Set o1 -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.isIn` (Map o1 m2 -> Set o1
forall k v. Map k v -> Set k
keys' Map o1 m2
prevComp)]
            comp :: o1 -> Maybe m2
comp o1
x
                | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe m2 -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe m2 -> Bool) -> Maybe m2 -> Bool
forall a b. (a -> b) -> a -> b
$ Map o1 m2
prevComp Map o1 m2 -> o1 -> Maybe m2
forall k v. Eq k => Map k v -> k -> Maybe v
|?| o1
x = Map o1 m2
prevComp Map o1 m2 -> o1 -> Maybe m2
forall k v. Eq k => Map k v -> k -> Maybe v
|?| o1
x
                | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set m1 -> Bool
forall a. Set a -> Bool
Set.null (Set m1 -> Bool) -> Set m1 -> Bool
forall a b. (a -> b) -> a -> b
$ o1 -> Set m1
validArrowOnBottom o1
x = m2 -> Maybe m2
forall a. a -> Maybe a
Just (m2 -> Maybe m2) -> m2 -> Maybe m2
forall a b. (a -> b) -> a -> b
$ (Map o1 m2
prevComp Map o1 m2 -> o1 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
target (Set m1 -> m1
forall a. Set a -> a
anElement (Set m1 -> m1) -> Set m1 -> m1
forall a b. (a -> b) -> a -> b
$ o1 -> Set m1
validArrowOnBottom o1
x))) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ ((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
nat) Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ (Set m1 -> m1
forall a. Set a -> a
anElement (Set m1 -> m1) -> Set m1 -> m1
forall a b. (a -> b) -> a -> b
$ o1 -> Set m1
validArrowOnBottom o1
x))
                | Bool
otherwise = Maybe m2
forall a. Maybe a
Nothing
            newComp :: Map o1 m2
newComp = Set (o1, m2) -> Map o1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet (Set (o1, m2) -> Map o1 m2) -> Set (o1, m2) -> Map o1 m2
forall a b. (a -> b) -> a -> b
$ Set (Maybe (o1, m2)) -> Set (o1, m2)
forall a. Set (Maybe a) -> Set a
Set.catMaybes [(o1, Maybe m2) -> Maybe (o1, m2)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => (o1, m a) -> m (o1, a)
sequence (o1
x,o1 -> Maybe m2
comp o1
x) | o1
x <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> c1
indexingCategory NaturalTransformation c1 m1 o1 c2 m2 o2
nat)]
            newNat :: NaturalTransformation c1 m1 o1 c2 m2 o2
newNat = Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
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 (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
nat) (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
nat) Map o1 m2
newComp
    
    -- | 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) => 
            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) =>
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)
-> (Cocone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone 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 {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).

    -- 

    -- 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 :: 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
    
    -- | 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 :: 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 -> c2
universeCategoryCone = 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)
-> (Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cone 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
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: 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 -> c2
universeCategoryCocone = 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)
-> (Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cocone 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
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: 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 -> c1
indexingCategoryCone = 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)
-> (Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cone 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
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: 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 -> c1
indexingCategoryCocone = 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)
-> (Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cocone 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
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
bottomObjects c
c = [Set o
loopClass | Set o
loopClass <- c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
loopClasses c
c, Set m -> Bool
forall a. Set a -> Bool
Set.null (Set m -> Bool) -> Set m -> Bool
forall a b. (a -> b) -> a -> b
$ (m -> Bool) -> Set m -> Set m
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\m
f -> (Bool -> Bool
not (m -> o
forall m o. Morphism m o => m -> o
target m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
source m
f o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
loopClass)) (Set m -> Set m) -> Set m -> Set m
forall a b. (a -> b) -> a -> b
$ c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
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 :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsBottomContained c
c = [[o]] -> Set [o]
forall a. [a] -> Set a
set([[o]] -> Set [o]) -> (Set [o] -> [[o]]) -> Set [o] -> Set [o]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Set [o] -> [[o]]
forall a. Eq a => Set a -> [a]
setToList (Set [o] -> Set [o]) -> Set [o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ [Set o] -> Set [o]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets ([Set o] -> Set [o]) -> [Set o] -> Set [o]
forall a b. (a -> b) -> a -> b
$ Set (Set o) -> [Set o]
forall a. Eq a => Set a -> [a]
setToList (Set (Set o) -> [Set o]) -> Set (Set o) -> [Set o]
forall a b. (a -> b) -> a -> b
$ c -> Set (Set o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set (Set o)
bottomObjects c
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 :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 Cocone c1 m1 o1 c3 m3 o3
cc1 Cocone c2 m2 o2 c3 m3 o3
cc2
        | Cocone c1 m1 o1 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone c1 m1 o1 c3 m3 o3
cc1 o3 -> o3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cocone c2 m2 o2 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone c2 m2 o2 c3 m3 o3
cc2 = Set (Map o1 o2)
maps
        | Bool
otherwise = [Map o1 o2] -> Set (Map o1 o2)
forall a. [a] -> Set a
set []
        where
            doms :: Set [o1]
doms = c1 -> Set [o1]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set [o]
possibleDomainsBottomContained (c1 -> Set [o1]) -> c1 -> Set [o1]
forall a b. (a -> b) -> a -> b
$ Cocone c1 m1 o1 c3 m3 o3 -> c1
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 -> c1
indexingCategoryCocone Cocone c1 m1 o1 c3 m3 o3
cc1
            maps :: Set (Map o1 o2)
maps = Set (Set (Map o1 o2)) -> Set (Map o1 o2)
forall a. Set (Set a) -> Set a
Set.concat2 [(o1 -> o2 -> Bool) -> Set o1 -> Set o2 -> Set (Map o1 o2)
forall a b.
(Eq a, Eq b) =>
(a -> b -> Bool) -> Set a -> Set b -> Set (Map a b)
enumerateInjectiveMaps (\o1
x o2
y -> Cocone c1 m1 o1 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c1 m1 o1 c3 m3 o3
cc1 NaturalTransformation c1 m1 o1 c3 m3 o3 -> o1 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o1
x m3 -> m3 -> Bool
forall a. Eq a => a -> a -> Bool
== Cocone c2 m2 o2 c3 m3 o3 -> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c2 m2 o2 c3 m3 o3
cc2 NaturalTransformation c2 m2 o2 c3 m3 o3 -> o2 -> m3
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ o2
y) ([o1] -> Set o1
forall a. [a] -> Set a
set [o1]
dom) (c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Cocone c2 m2 o2 c3 m3 o3 -> c2
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 -> c1
indexingCategoryCocone Cocone c2 m2 o2 c3 m3 o3
cc2)) | [o1]
dom <- Set [o1]
doms]
            
     -- | Precompose a cocone with a functor going to the universe category.

    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 :: forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(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 Cocone c2 m2 o2 c3 m3 o3
cc Diagram c1 m1 o1 c2 m2 o2
f = One
-> o3
-> NaturalTransformation c1 m1 o1 c3 m3 o3
-> CommaObject One o3 (NaturalTransformation c1 m1 o1 c3 m3 o3)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One (Cocone c2 m2 o2 c3 m3 o3 -> o3
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone c2 m2 o2 c3 m3 o3
cc) ((Cocone c2 m2 o2 c3 m3 o3 -> NaturalTransformation c2 m2 o2 c3 m3 o3
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c2 m2 o2 c3 m3 o3
cc) NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
forall c1 m1 o1 c2 m2 o2 m3 o3 c3.
(Category c1 m1 o1, Morphism m1 o1, Eq m1, FiniteCategory c2 m2 o2,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2, Morphism m3 o3, Eq c3, Eq m3,
 Eq o3) =>
NaturalTransformation c2 m2 o2 c3 m3 o3
-> Diagram c1 m1 o1 c2 m2 o2
-> NaturalTransformation c1 m1 o1 c3 m3 o3
<=@<- Diagram c1 m1 o1 c2 m2 o2
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,
                                            Category c2 m2 o2, Morphism m2 o2) =>
        Cocone c1 m1 o1 c2 m2 o2 -> m2 -> Cocone c1 m1 o1 c2 m2 o2
    postcomposeCoconeWithMorphism :: 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) =>
Cocone c1 m1 o1 c2 m2 o2 -> m2 -> Cocone c1 m1 o1 c2 m2 o2
postcomposeCoconeWithMorphism Cocone c1 m1 o1 c2 m2 o2
cc m2
m = 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 (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m) (Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
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 (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)
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall a b. (a -> b) -> a -> b
$ Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c1 m1 o1 c2 m2 o2
cc) (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)
-> (Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cocone 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
target(NaturalTransformation c1 m1 o1 c2 m2 o2
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone (Cocone c1 m1 o1 c2 m2 o2 -> c1) -> Cocone c1 m1 o1 c2 m2 o2 -> c1
forall a b. (a -> b) -> a -> b
$ Cocone c1 m1 o1 c2 m2 o2
cc) (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)
-> (Cocone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2)
-> Cocone 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
target(NaturalTransformation c1 m1 o1 c2 m2 o2
 -> Diagram c1 m1 o1 c2 m2 o2)
-> (Cocone c1 m1 o1 c2 m2 o2
    -> NaturalTransformation c1 m1 o1 c2 m2 o2)
-> Cocone c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone (Cocone c1 m1 o1 c2 m2 o2 -> c2) -> Cocone c1 m1 o1 c2 m2 o2 -> c2
forall a b. (a -> b) -> a -> b
$ Cocone c1 m1 o1 c2 m2 o2
cc) (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m)) ((m2
m m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@) (m2 -> m2) -> Map o1 m2 -> Map o1 m2
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall c1 m1 o1 c2 m2 o2.
NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
components (NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2)
-> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Map o1 m2
forall a b. (a -> b) -> a -> b
$ Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone c1 m1 o1 c2 m2 o2
cc)))