{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : A 'ColimitCategory' is the colimit of a diagram in 'FinCat'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'ColimitCategory' is the colimit of a diagram in 'FinCat'. To compute colimits in a usual category, see Math.CocompleteCategory. To compute colimits in a custom 'FiniteCategory', see 'colimits' in Math.ConeCategory.

Note that computing a 'ColimitCategory' is MUCH slower than computing a 'LimitCategory' as coequalizers of categories are trickier than equalizers of categories. We can only compute colimits of 'CompositionGraph's as coequalizing might create new formal morphisms when gluing two objects. Therefore 'colimit' transforms all given categories into 'CompositionGraph's. If you already have a 'CompositionGraph', consider using 'colimitOfCompositionGraphs' instead of 'colimit'.
-}

module Math.FiniteCategories.ColimitCategory
(
    glueObject,
    glueObjects,
    glueMorphism,
    glueMorphisms,
    colimitOfCompositionGraphs,
    coprojectBaseCompositionGraphs
)
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.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.FiniteCategoryError
    import              Math.CocompleteCategory
    import              Math.Categories.FunctorCategory
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.FiniteCategories.CompositionGraph
    import              Math.FiniteCategories.Parallel
    import              Math.Categories.FinGrph
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | Glue two objects of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    glueObject :: (Eq a, Eq b) => CompositionGraph a b -> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueObject :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObject CompositionGraph a b
cg a
a a
b = Diagram
  (CompositionGraph a b)
  (CGMorphism a b)
  a
  (CompositionGraph a b)
  (CGMorphism a b)
  a
-> Diagram
     (CompositionGraph a b)
     (CGMorphism a b)
     a
     (CompositionGraph a b)
     (CGMorphism a b)
     a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph a b
src=CompositionGraph a b
cg,tgt :: CompositionGraph a b
tgt=CompositionGraph a b
newCG, omap :: Map a a
omap = Map a a
omapD, mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap = Map (CGMorphism a b) (CGMorphism a b)
mmapD}
        where
            glueObj :: a -> a
glueObj a
obj = if a
obj a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then a
a else a
obj
            omapD :: Map a a
omapD = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
glueObj (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set a) -> CompositionGraph a b -> Set a
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            glueArr :: Arrow a e -> Arrow a e
glueArr Arrow a e
arr = Arrow{sourceArrow :: a
sourceArrow = a -> a
glueObj(a -> a) -> (Arrow a e -> a) -> Arrow a e -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a e -> a
forall n e. Arrow n e -> n
sourceArrow (Arrow a e -> a) -> Arrow a e -> a
forall a b. (a -> b) -> a -> b
$ Arrow a e
arr, targetArrow :: a
targetArrow = a -> a
glueObj(a -> a) -> (Arrow a e -> a) -> Arrow a e -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a e -> a
forall n e. Arrow n e -> n
targetArrow (Arrow a e -> a) -> Arrow a e -> a
forall a b. (a -> b) -> a -> b
$ Arrow a e
arr, labelArrow :: e
labelArrow = Arrow a e -> e
forall n e. Arrow n e -> e
labelArrow Arrow a e
arr}
            mmapD :: Map (CGMorphism a b) (CGMorphism a b)
mmapD = (CGMorphism a b -> CGMorphism a b)
-> Set (CGMorphism a b) -> Map (CGMorphism a b) (CGMorphism a b)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction ((CompositionGraph a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionGraph a b -> Arrow a b -> CGMorphism a b
unsafeArrowToCGMorphism CompositionGraph a b
cg)(Arrow a b -> CGMorphism a b)
-> (CGMorphism a b -> Arrow a b)
-> CGMorphism a b
-> CGMorphism a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
glueArr(Arrow a b -> Arrow a b)
-> (CGMorphism a b -> Arrow a b) -> CGMorphism a b -> Arrow a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow) (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId CompositionGraph a b
cg)
            newCG :: CompositionGraph a b
newCG = Graph a b -> CompositionLaw a b -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Map a a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values Map a a
omapD) (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
glueArr (Arrow a b -> Arrow a b) -> Set (Arrow a b) -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph a b -> Set (Arrow a b))
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set (Arrow a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set (Arrow a b))
-> CompositionGraph a b -> Set (Arrow a b)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg))) (CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
cg)
    
    -- | Glue objects of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    glueObjects :: (Eq a, Eq b) => CompositionGraph a b -> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueObjects :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObjects CompositionGraph a b
cg Set a
objects
        | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
objects = [Char] -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => [Char] -> a
error [Char]
"glue 0 object"
        | Bool
otherwise = (a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\a
obj FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObject (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) a
representant a
obj) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg) Set a
objects
        where
            representant :: a
representant = Set a -> a
forall a. Set a -> a
anElement Set a
objects

    -- | Glue two morphisms with same source and target of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    -- The first argument should not be composite if the second is a generator.

    glueMorphism :: (Eq a, Eq b) => CompositionGraph a b -> CGMorphism a b -> CGMorphism a b -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueMorphism :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphism CompositionGraph a b
cg CGMorphism a b
m1 CGMorphism a b
m2
        | CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isComposite_ CGMorphism a b
m1 Bool -> Bool -> Bool
&& CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m2 = [Char] -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => [Char] -> a
error [Char]
"Glue composite to generator."
        | CGMorphism a b
m1 CGMorphism a b -> CGMorphism a b -> Bool
forall a. Eq a => a -> a -> Bool
== CGMorphism a b
m2 = FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg
        | CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m1 Bool -> Bool -> Bool
&& CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m2 = FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph a b
src=CompositionGraph a b
cg,tgt :: CompositionGraph a b
tgt=CompositionGraph a b
newCGGG,omap :: Map a a
omap=Map a a
omapGG,mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap=Map (CGMorphism a b) (CGMorphism a b)
mmapGG}
        | Bool
otherwise = FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph a b
src=CompositionGraph a b
cg,tgt :: CompositionGraph a b
tgt=CompositionGraph a b
newCG,omap :: Map a a
omap=Map a a
omapGG,mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap=Map (CGMorphism a b) (CGMorphism a b)
mmapId}
        where
            isGenerator_ :: CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m = [Arrow a b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall a b. (a -> b) -> a -> b
$ CGMorphism a b
m) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
            isComposite_ :: CGMorphism a b -> Bool
isComposite_ = Bool -> Bool
not(Bool -> Bool)
-> (CGMorphism a b -> Bool) -> CGMorphism a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_
            glueMorph :: CGMorphism a b -> CGMorphism a b
glueMorph CGMorphism a b
m = if CGMorphism a b
m CGMorphism a b -> CGMorphism a b -> Bool
forall a. Eq a => a -> a -> Bool
== CGMorphism a b
m2 then CGMorphism a b
m1 else CGMorphism a b
m
            glueArr :: Arrow a b -> Arrow a b
glueArr Arrow a b
a = if Arrow a b
a Arrow a b -> Arrow a b -> Bool
forall a. Eq a => a -> a -> Bool
== (CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m2) then CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m1 else Arrow a b
a
            omapGG :: Map a a
omapGG = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
forall a. a -> a
id (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set a) -> CompositionGraph a b -> Set a
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            mmapGG :: Map (CGMorphism a b) (CGMorphism a b)
mmapGG = (CGMorphism a b -> CGMorphism a b)
-> Set (CGMorphism a b) -> Map (CGMorphism a b) (CGMorphism a b)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction CGMorphism a b -> CGMorphism a b
glueMorph (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId CompositionGraph a b
cg)
            newLawGG :: Map [Arrow a b] [Arrow a b]
newLawGG =  Set ([Arrow a b], [Arrow a b]) -> Map [Arrow a b] [Arrow a b]
forall k v. Set (k, v) -> Map k v
weakMapFromSet (Set ([Arrow a b], [Arrow a b]) -> Map [Arrow a b] [Arrow a b])
-> Set ([Arrow a b], [Arrow a b]) -> Map [Arrow a b] [Arrow a b]
forall a b. (a -> b) -> a -> b
$ (\([Arrow a b]
x,[Arrow a b]
y) -> (Arrow a b -> Arrow a b
glueArr (Arrow a b -> Arrow a b) -> [Arrow a b] -> [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
x, Arrow a b -> Arrow a b
glueArr (Arrow a b -> Arrow a b) -> [Arrow a b] -> [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
y)) (([Arrow a b], [Arrow a b]) -> ([Arrow a b], [Arrow a b]))
-> Set ([Arrow a b], [Arrow a b]) -> Set ([Arrow a b], [Arrow a b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map [Arrow a b] [Arrow a b] -> Set ([Arrow a b], [Arrow a b])
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet)(Map [Arrow a b] [Arrow a b] -> Set ([Arrow a b], [Arrow a b]))
-> (CompositionGraph a b -> Map [Arrow a b] [Arrow a b])
-> CompositionGraph a b
-> Set ([Arrow a b], [Arrow a b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Map [Arrow a b] [Arrow a b]
forall a b. CompositionGraph a b -> CompositionLaw a b
law (CompositionGraph a b -> Set ([Arrow a b], [Arrow a b]))
-> CompositionGraph a b -> Set ([Arrow a b], [Arrow a b])
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            newCGGG :: CompositionGraph a b
newCGGG = Graph a b -> Map [Arrow a b] [Arrow a b] -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set a) -> CompositionGraph a b -> Set a
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg) ((Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph a b -> Set (Arrow a b))
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set (Arrow a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set (Arrow a b))
-> CompositionGraph a b -> Set (Arrow a b)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg) Set (Arrow a b) -> Set (Arrow a b) -> Set (Arrow a b)
forall a. Eq a => Set a -> Set a -> Set a
`Set.difference` ([Arrow a b] -> Set (Arrow a b)
forall a. [a] -> Set a
set [CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m2]))) Map [Arrow a b] [Arrow a b]
newLawGG
            newLaw :: Map [Arrow a b] [Arrow a b]
newLaw = [Arrow a b]
-> [Arrow a b]
-> Map [Arrow a b] [Arrow a b]
-> Map [Arrow a b] [Arrow a b]
forall k a. k -> a -> Map k a -> Map k a
Map.insert ((a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall a b. (a -> b) -> a -> b
$ CGMorphism a b
m2) ((a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall a b. (a -> b) -> a -> b
$ CGMorphism a b
m1) (CompositionGraph a b -> Map [Arrow a b] [Arrow a b]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
cg)
            mmapId :: Map (CGMorphism a b) (CGMorphism a b)
mmapId = (CGMorphism a b -> CGMorphism a b)
-> Set (CGMorphism a b) -> Map (CGMorphism a b) (CGMorphism a b)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\CGMorphism a b
morph -> CGMorphism{path :: (a, [Arrow a b])
path=CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path CGMorphism a b
morph, compositionLaw :: Map [Arrow a b] [Arrow a b]
compositionLaw = Map [Arrow a b] [Arrow a b]
newLaw}) (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId CompositionGraph a b
cg)
            newCG :: CompositionGraph a b
newCG = Graph a b -> Map [Arrow a b] [Arrow a b] -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a b
cg) Map [Arrow a b] [Arrow a b]
newLaw
            
    -- | Glue morphisms with same source and target of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    glueMorphisms :: (Eq a, Eq b) => CompositionGraph a b -> Set (CGMorphism a b) -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueMorphisms :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphisms CompositionGraph a b
cg Set (CGMorphism a b)
morphisms
        | Set (CGMorphism a b) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism a b)
morphisms = [Char] -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => [Char] -> a
error [Char]
"glue 0 morphism"
        | Set (CGMorphism a b) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism a b)
generators = (CGMorphism a b
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\CGMorphism a b
morph FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphism (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (Set (CGMorphism a b) -> CGMorphism a b
forall a. Set a -> a
anElement Set (CGMorphism a b)
morphisms) CGMorphism a b
morph) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg) Set (CGMorphism a b)
morphisms
        | Bool
otherwise = (CGMorphism a b
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\CGMorphism a b
morph FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphism (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (Set (CGMorphism a b) -> CGMorphism a b
forall a. Set a -> a
anElement Set (CGMorphism a b)
generators) CGMorphism a b
morph) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg) Set (CGMorphism a b)
morphisms
        where
            generators :: Set (CGMorphism a b)
generators = (CGMorphism a b -> Bool)
-> Set (CGMorphism a b) -> Set (CGMorphism a b)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator CompositionGraph a b
cg) Set (CGMorphism a b)
morphisms


    instance (Eq e, Eq n, Eq oIndex) => 
        HasCoproducts (FinCat (CompositionGraph n e) (CGMorphism n e) n) (FinFunctor (CompositionGraph n e) (CGMorphism n e) n) (CompositionGraph n e) (FinCat (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) (CGMorphism (Colimit oIndex n) (Colimit oIndex e)) (Colimit oIndex n)) (FinFunctor (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) (CGMorphism (Colimit oIndex n) (Colimit oIndex e)) (Colimit oIndex n)) (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) oIndex where
        coproduct :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
coproduct Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG = CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
coproductCG NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
natCoproduct
            where
                indexingCategory :: DiscreteCategory oIndex
indexingCategory = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG
                coproductCG :: CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
coproductCG = Graph (Colimit oIndex n) (Colimit oIndex e)
-> CompositionLaw (Colimit oIndex n) (Colimit oIndex e)
-> CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
-> Graph (Colimit oIndex n) (Colimit oIndex e)
forall c1 m1 o1 c2 m2 o2. Cocone c1 m1 o1 c2 m2 o2 -> o2
nadir Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
coproductGraphCocone) ([CompositionLaw (Colimit oIndex n) (Colimit oIndex e)]
-> CompositionLaw (Colimit oIndex n) (Colimit oIndex e)
forall k a. Eq k => [Map k a] -> Map k a
Map.unions [AssociationList
  (RawPath (Colimit oIndex n) (Colimit oIndex e))
  (RawPath (Colimit oIndex n) (Colimit oIndex e))
-> CompositionLaw (Colimit oIndex n) (Colimit oIndex e)
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList
   (RawPath (Colimit oIndex n) (Colimit oIndex e))
   (RawPath (Colimit oIndex n) (Colimit oIndex e))
 -> CompositionLaw (Colimit oIndex n) (Colimit oIndex e))
-> AssociationList
     (RawPath (Colimit oIndex n) (Colimit oIndex e))
     (RawPath (Colimit oIndex n) (Colimit oIndex e))
-> CompositionLaw (Colimit oIndex n) (Colimit oIndex e)
forall a b. (a -> b) -> a -> b
$ (\([Arrow n e]
rp1,[Arrow n e]
rp2) -> (oIndex -> Arrow n e -> Arrow (Colimit oIndex n) (Colimit oIndex e)
forall {i} {n} {t}.
i -> Arrow n t -> Arrow (Colimit i n) (Colimit i t)
transformArrowIntoArrowCoproduct oIndex
i (Arrow n e -> Arrow (Colimit oIndex n) (Colimit oIndex e))
-> [Arrow n e] -> RawPath (Colimit oIndex n) (Colimit oIndex e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow n e]
rp1, oIndex -> Arrow n e -> Arrow (Colimit oIndex n) (Colimit oIndex e)
forall {i} {n} {t}.
i -> Arrow n t -> Arrow (Colimit i n) (Colimit i t)
transformArrowIntoArrowCoproduct oIndex
i (Arrow n e -> Arrow (Colimit oIndex n) (Colimit oIndex e))
-> [Arrow n e] -> RawPath (Colimit oIndex n) (Colimit oIndex e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow n e]
rp2)) (([Arrow n e], [Arrow n e])
 -> (RawPath (Colimit oIndex n) (Colimit oIndex e),
     RawPath (Colimit oIndex n) (Colimit oIndex e)))
-> [([Arrow n e], [Arrow n e])]
-> AssociationList
     (RawPath (Colimit oIndex n) (Colimit oIndex e))
     (RawPath (Colimit oIndex n) (Colimit oIndex e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map [Arrow n e] [Arrow n e] -> [([Arrow n e], [Arrow n e])]
forall k v. Eq k => Map k v -> AssociationList k v
Map.mapToList (CompositionGraph n e -> Map [Arrow n e] [Arrow n e]
forall a b. CompositionGraph a b -> CompositionLaw a b
law (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> oIndex -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i))) | oIndex
i <- (Set oIndex -> [oIndex]
forall a. Eq a => Set a -> [a]
setToList (DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCategory))])
                transformObjectIntoObjectCoproduct :: i -> t -> Colimit i t
transformObjectIntoObjectCoproduct i
i t
x = i -> t -> Colimit i t
forall i t. i -> t -> Colimit i t
CoproductElement i
i t
x
                transformArrowIntoArrowCoproduct :: i -> Arrow n t -> Arrow (Colimit i n) (Colimit i t)
transformArrowIntoArrowCoproduct i
i Arrow n t
a = Arrow{sourceArrow :: Colimit i n
sourceArrow = i -> n -> Colimit i n
forall i t. i -> t -> Colimit i t
CoproductElement i
i (Arrow n t -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n t
a), targetArrow :: Colimit i n
targetArrow = i -> n -> Colimit i n
forall i t. i -> t -> Colimit i t
CoproductElement i
i (Arrow n t -> n
forall n e. Arrow n e -> n
targetArrow Arrow n t
a), labelArrow :: Colimit i t
labelArrow = i -> t -> Colimit i t
forall i t. i -> t -> Colimit i t
CoproductElement i
i (Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a)}
                coproductGraphCocone :: Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
coproductGraphCocone = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Colimit oIndex n) (Colimit oIndex e))
     (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
     (Graph (Colimit oIndex n) (Colimit oIndex e))
forall c m o cLim mLim oLim oIndex.
HasCoproducts c m o cLim mLim oLim oIndex =>
Diagram
  (DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     cLim
     mLim
     oLim
coproduct (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram (Diagram
   (DiscreteCategory oIndex)
   (DiscreteMorphism oIndex)
   oIndex
   (FinGrph n e)
   (GraphHomomorphism n e)
   (Graph n e)
 -> Diagram
      (DiscreteCategory oIndex)
      (DiscreteMorphism oIndex)
      oIndex
      (FinGrph n e)
      (GraphHomomorphism n e)
      (Graph n e))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
forall a b. (a -> b) -> a -> b
$ Diagram{src :: DiscreteCategory oIndex
src = DiscreteCategory oIndex
indexingCategory, tgt :: FinGrph n e
tgt = FinGrph n e
forall n e. FinGrph n e
FinGrph, omap :: Map oIndex (Graph n e)
omap = Set (oIndex, Graph n e) -> Map oIndex (Graph n e)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i, CompositionGraph n e -> Graph n e
forall a b. CompositionGraph a b -> Graph a b
support (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> oIndex -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i))| oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCategory], mmap :: Map (DiscreteMorphism oIndex) (GraphHomomorphism n e)
mmap = AssociationList (DiscreteMorphism oIndex) (GraphHomomorphism n e)
-> Map (DiscreteMorphism oIndex) (GraphHomomorphism n e)
forall k v. AssociationList k v -> Map k v
weakMap []})
                newDiagOfCG :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
newDiagOfCG = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: DiscreteCategory oIndex
src = DiscreteCategory oIndex
indexingCategory, tgt :: FinCat
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
  (Colimit oIndex n)
tgt = FinCat
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
  (Colimit oIndex n)
forall c m o. FinCat c m o
FinCat, omap :: Map oIndex (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
omap = Set
  (oIndex, CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> Map
     oIndex (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i,CompositionGraph n e
-> CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG CompositionGraph n e
cg) | (oIndex
i,CompositionGraph n e
cg) <- Map oIndex (CompositionGraph n e)
-> Set (oIndex, CompositionGraph n e)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> Map oIndex (CompositionGraph n e)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG)], mmap :: Map
  (DiscreteMorphism oIndex)
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
mmap = AssociationList
  (DiscreteMorphism oIndex)
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
-> Map
     (DiscreteMorphism oIndex)
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
forall k v. AssociationList k v -> Map k v
weakMap []}
                natCoproduct :: NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
natCoproduct = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> Map
     oIndex
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
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 Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
newDiagOfCG (DiscreteCategory oIndex
-> FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
-> CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
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 DiscreteCategory oIndex
indexingCategory FinCat
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
  (Colimit oIndex n)
forall c m o. FinCat c m o
FinCat CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
coproductCG) (Set
  (oIndex,
   FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
-> Map
     oIndex
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(oIndex
i, oIndex
-> FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
forall {i}.
Eq i =>
oIndex
-> Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit i e))
     (CGMorphism (Colimit oIndex n) (Colimit i e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
insertionFunctor oIndex
i)| oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCategory])
                coprojectArrow :: Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow Arrow n t
a = Arrow{sourceArrow :: Colimit i n
sourceArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n t
a, targetArrow :: Colimit i n
targetArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
targetArrow Arrow n t
a, labelArrow :: Colimit i t
labelArrow = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> t -> Colimit i t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                coprojectGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph Graph a t
g = Set (Colimit i a)
-> Set (Arrow (Colimit i a) (Colimit i t))
-> Graph (Colimit i a) (Colimit i t)
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((a -> Colimit i a
forall i t. t -> Colimit i t
Coprojection) (a -> Colimit i a) -> Set a -> Set (Colimit i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set a
forall n e. Graph n e -> Set n
nodes Graph a t
g) ((Arrow a t -> Arrow (Colimit i a) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow) (Arrow a t -> Arrow (Colimit i a) (Colimit i t))
-> Set (Arrow a t) -> Set (Arrow (Colimit i a) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set (Arrow a t)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a t
g)
                coprojectLaw :: Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw Map (f (Arrow n t)) (f (Arrow n t))
cl = Set
  (f (Arrow (Colimit i n) (Colimit i t)),
   f (Arrow (Colimit i n) (Colimit i t)))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp1, Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp2) | (f (Arrow n t)
rp1,f (Arrow n t)
rp2) <- Map (f (Arrow n t)) (f (Arrow n t))
-> Set (f (Arrow n t), f (Arrow n t))
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map (f (Arrow n t)) (f (Arrow n t))
cl]
                coprojectCG :: CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG CompositionGraph a t
cg = Graph (Colimit i a) (Colimit i t)
-> CompositionLaw (Colimit i a) (Colimit i t)
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Graph a t -> Graph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (Graph a t -> Graph (Colimit i a) (Colimit i t))
-> Graph a t -> Graph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Graph a t
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a t
cg) (Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw (Map [Arrow a t] [Arrow a t]
 -> CompositionLaw (Colimit i a) (Colimit i t))
-> Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Map [Arrow a t] [Arrow a t]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a t
cg)
                coprojectCGMorphism :: CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path = (t
a, [Arrow t t]
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw = CompositionLaw t t
cl} = CGMorphism{path :: Path (Colimit i t) (Colimit i t)
path = (t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
a, Arrow t t -> Arrow (Colimit i t) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow t t -> Arrow (Colimit i t) (Colimit i t))
-> [Arrow t t] -> [Arrow (Colimit i t) (Colimit i t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow t t]
rp), compositionLaw :: CompositionLaw (Colimit i t) (Colimit i t)
compositionLaw = CompositionLaw t t -> CompositionLaw (Colimit i t) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw CompositionLaw t t
cl}
                insertionFunctor :: oIndex
-> Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit i e))
     (CGMorphism (Colimit oIndex n) (Colimit i e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
insertionFunctor oIndex
i = Diagram
  (CompositionGraph (Colimit oIndex n) (Colimit i e))
  (CGMorphism (Colimit oIndex n) (Colimit i e))
  (Colimit oIndex n)
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
  (Colimit oIndex n)
-> Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit i e))
     (CGMorphism (Colimit oIndex n) (Colimit i e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph (Colimit oIndex n) (Colimit i e)
src = CompositionGraph n e
-> CompositionGraph (Colimit oIndex n) (Colimit i e)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> oIndex -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i), tgt :: CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
tgt = CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
coproductCG, omap :: Map (Colimit oIndex n) (Colimit oIndex n)
omap = Set (Colimit oIndex n, Colimit oIndex n)
-> Map (Colimit oIndex n) (Colimit oIndex n)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(Colimit oIndex n
o, (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
-> Map (Colimit oIndex n) (Colimit oIndex n)
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
insertionGH) Map (Colimit oIndex n) (Colimit oIndex n)
-> Colimit oIndex n -> Colimit oIndex n
forall k v. Eq k => Map k v -> k -> v
|!| Colimit oIndex n
o) | Colimit oIndex n
o <- CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
-> Set (Colimit oIndex n)
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
newDiagOfCG Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> oIndex -> CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i)], mmap :: Map
  (CGMorphism (Colimit oIndex n) (Colimit i e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
mmap = Set
  (CGMorphism (Colimit oIndex n) (Colimit i e),
   CGMorphism (Colimit oIndex n) (Colimit oIndex e))
-> Map
     (CGMorphism (Colimit oIndex n) (Colimit i e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(CGMorphism n e -> CGMorphism (Colimit oIndex n) (Colimit i e)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism n e
m, (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
-> Arrow (Colimit oIndex n) (Colimit oIndex e)
-> CGMorphism (Colimit oIndex n) (Colimit oIndex e)
forall a b. CompositionGraph a b -> Arrow a b -> CGMorphism a b
unsafeArrowToCGMorphism CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
coproductCG (oIndex -> Arrow n e -> Arrow (Colimit oIndex n) (Colimit oIndex e)
forall {i} {n} {t}.
i -> Arrow n t -> Arrow (Colimit i n) (Colimit i t)
transformArrowIntoArrowCoproduct oIndex
i (CGMorphism n e -> Arrow n e
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism n e
m)))) | CGMorphism n e
m <- (CompositionGraph n e -> Set (CGMorphism n e)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diagOfCG Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> oIndex -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i))]}
                    where
                        insertionGH :: GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
insertionGH = (Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Colimit oIndex n) (Colimit oIndex e))
     (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
     (Graph (Colimit oIndex n) (Colimit oIndex e))
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
coproductGraphCocone) NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
-> oIndex
-> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ oIndex
i
        

    instance (Eq n, Eq e) => HasCoequalizers (FinCat (CompositionGraph n e) (CGMorphism n e) n) (FinFunctor (CompositionGraph n e) (CGMorphism n e) n) (CompositionGraph n e) where
        coequalize :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
coequalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag = CompositionGraph n e
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone CompositionGraph n e
coeq NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
nat
            where
                selectingObjects :: Set n
selectingObjects = CompositionGraph n e -> Set n
forall c m o. FiniteCategory c m o => c -> Set o
ob (CompositionGraph n e -> Set n) -> CompositionGraph n e -> Set n
forall a b. (a -> b) -> a -> b
$ Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelOb -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA
                idFunct :: FinFunctor (CompositionGraph n e) (CGMorphism n e) n
idFunct = Diagram{src :: CompositionGraph n e
src = (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelOb -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB), tgt :: CompositionGraph n e
tgt = (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelOb -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB), omap :: Map n n
omap = (n -> n) -> Set n -> Map n n
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction n -> n
forall a. a -> a
id (CompositionGraph n e -> Set n
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelOb -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB)), mmap :: Map (CGMorphism n e) (CGMorphism n e)
mmap = (CGMorphism n e -> CGMorphism n e)
-> Set (CGMorphism n e) -> Map (CGMorphism n e) (CGMorphism n e)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction CGMorphism n e -> CGMorphism n e
forall a. a -> a
id (CompositionGraph n e -> Set (CGMorphism n e)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelOb -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB))}
                glueObjectsFunctor :: FinFunctor (CompositionGraph n e) (CGMorphism n e) n
glueObjectsFunctor = (n
 -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
 -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> Set n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\n
obj FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct -> (CompositionGraph n e
-> Set n -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObjects (FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> CompositionGraph n e
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct) ([n] -> Set n
forall a. [a] -> Set a
set [(FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelAr
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ ParallelAr
ParallelF)) FinFunctor (CompositionGraph n e) (CGMorphism n e) n -> n -> n
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ n
obj,(FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelAr
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ ParallelAr
ParallelG)) FinFunctor (CompositionGraph n e) (CGMorphism n e) n -> n -> n
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ n
obj])) FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct) FinFunctor (CompositionGraph n e) (CGMorphism n e) n
idFunct Set n
selectingObjects
                selectingArrows :: Set (CGMorphism n e)
selectingArrows = CompositionGraph n e -> Set (CGMorphism n e)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId (CompositionGraph n e -> Set (CGMorphism n e))
-> CompositionGraph n e -> Set (CGMorphism n e)
forall a b. (a -> b) -> a -> b
$ Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelOb -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA
                glueArrowsFunctor :: FinFunctor (CompositionGraph n e) (CGMorphism n e) n
glueArrowsFunctor = (CGMorphism n e
 -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
 -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> Set (CGMorphism n e)
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\CGMorphism n e
morph FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct -> (CompositionGraph n e
-> Set (CGMorphism n e)
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphisms (FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> CompositionGraph n e
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct) ([CGMorphism n e] -> Set (CGMorphism n e)
forall a. [a] -> Set a
set [(FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelAr
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ ParallelAr
ParallelF)) FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> CGMorphism n e -> CGMorphism n e
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
->£ CGMorphism n e
morph,(FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelAr
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ ParallelAr
ParallelG)) FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> CGMorphism n e -> CGMorphism n e
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
->£ CGMorphism n e
morph])) FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph n e) (CGMorphism n e) n
funct) FinFunctor (CompositionGraph n e) (CGMorphism n e) n
glueObjectsFunctor Set (CGMorphism n e)
selectingArrows
                coeq :: CompositionGraph n e
coeq = FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> CompositionGraph n e
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph n e) (CGMorphism n e) n
glueArrowsFunctor
                nat :: NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
nat = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
-> Map
     ParallelOb (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
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 Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag (Parallel
-> FinCat (CompositionGraph n e) (CGMorphism n e) n
-> CompositionGraph n e
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
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 Parallel
Parallel FinCat (CompositionGraph n e) (CGMorphism n e) n
forall c m o. FinCat c m o
FinCat CompositionGraph n e
coeq) (AssociationList
  ParallelOb (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
-> Map
     ParallelOb (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelB, FinFunctor (CompositionGraph n e) (CGMorphism n e) n
glueArrowsFunctor), (ParallelOb
ParallelA, FinFunctor (CompositionGraph n e) (CGMorphism n e) n
glueArrowsFunctor FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> ParallelAr
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ ParallelAr
ParallelF))])
        
    -- | Note that computing a 'ColimitCategory' is MUCH slower than computing a 'LimitCategory' as coequalizers of categories are trickier than equalizers of categories. We can only compute colimits of 'CompositionGraph's as coequalizing might create new formal morphisms when gluing two objects. Therefore 'colimit' transforms all given categories into 'CompositionGraph's. If you already have a 'CompositionGraph', consider using 'colimitOfCompositionGraphs' instead of 'colimit'.

    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o,
              FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq oIndex, Eq mIndex) => 
        CocompleteCategory (FinCat c m o) (FinFunctor c m o) c (FinCat (CompositionGraph (Colimit oIndex o) (Colimit oIndex m)) (CGMorphism (Colimit oIndex o) (Colimit oIndex m)) (Colimit oIndex o)) (FinFunctor (CompositionGraph (Colimit oIndex o) (Colimit oIndex m)) (CGMorphism (Colimit oIndex o) (Colimit oIndex m)) (Colimit oIndex o)) (CompositionGraph (Colimit oIndex o) (Colimit oIndex m)) cIndex mIndex oIndex where
        colimit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
     (FinFunctor
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
colimit Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag = (Diagram
   (CompositionGraph o m)
   (CGMorphism o m)
   o
   (CompositionGraph o m)
   (CGMorphism o m)
   o
 -> FinFunctor
      (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
      (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
      (Colimit oIndex o))
-> Diagram
     cIndex
     mIndex
     oIndex
     (FinCat (CompositionGraph o m) (CGMorphism o m) o)
     (Diagram
        (CompositionGraph o m)
        (CGMorphism o m)
        o
        (CompositionGraph o m)
        (CGMorphism o m)
        o)
     (CompositionGraph o m)
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
     (FinFunctor
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
forall c m o cLim mLim oLim oIndex cIndex mIndex.
(Category c m o, Morphism m o, Category cLim mLim oLim,
 Morphism mLim oLim, HasCoproducts c m o cLim mLim oLim oIndex,
 HasCoequalizers cLim mLim oLim,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq oIndex, Eq mIndex, Eq cIndex) =>
(m -> mLim)
-> Diagram cIndex mIndex oIndex c m o
-> Cocone cIndex mIndex oIndex cLim mLim oLim
colimitFromCoproductsAndCoequalizers Diagram
  (CompositionGraph o m)
  (CGMorphism o m)
  o
  (CompositionGraph o m)
  (CGMorphism o m)
  o
-> FinFunctor
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
     (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
     (Colimit oIndex o)
forall {a} {t} {a} {t} {t} {t} {t} {t} {o1} {o2} {i} {i} {i} {i}
       {i} {i} {i} {i} {i} {i}.
(Eq a, Eq t, Eq a, Eq t, Eq t, Eq t, Eq t, Eq t) =>
Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Diagram
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o2)
coprojectDiag Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph o m) (CGMorphism o m) o)
  (Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
  (CompositionGraph o m)
forall {c} {m} {o}.
Diagram
  cIndex
  mIndex
  oIndex
  (FinCat c m o)
  (Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
  (CompositionGraph o m)
newDiag
            where
                newDiag :: Diagram
  cIndex
  mIndex
  oIndex
  (FinCat c m o)
  (Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
  (CompositionGraph o m)
newDiag = Diagram{src :: cIndex
src = Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag, tgt :: FinCat c m o
tgt = FinCat c m o
forall c m o. FinCat c m o
FinCat, omap :: Map oIndex (CompositionGraph o m)
omap = Map oIndex (CompositionGraph o m)
newOmap, mmap :: Map
  mIndex
  (Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
mmap = Map
  mIndex
  (Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
newMmap}
                newOmap :: Map oIndex (CompositionGraph o m)
newOmap = Set (oIndex, CompositionGraph o m)
-> Map oIndex (CompositionGraph o m)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
k, Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
-> CompositionGraph o m
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
 -> CompositionGraph o m)
-> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
-> CompositionGraph o m
forall a b. (a -> b) -> a -> b
$ c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
finiteCategoryToCompositionGraph2 (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
k)) | oIndex
k <- cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                newMmap :: Map
  mIndex
  (Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
newMmap =  Set
  (mIndex,
   Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o)
-> Map
     mIndex
     (Diagram
        (CompositionGraph o m)
        (CGMorphism o m)
        o
        (CompositionGraph o m)
        (CGMorphism o m)
        o)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(mIndex
a, FinFunctor c m o
-> Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     (CompositionGraph o1 m1)
     (CGMorphism o1 m1)
     o1
     (CompositionGraph o2 m2)
     (CGMorphism o2 m2)
     o2
diagramToDiagramOfCompositionGraphs2 (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
->£ mIndex
a)) | mIndex
a <-  cIndex -> Set mIndex
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag)]
                coprojectArrow :: Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow Arrow n t
a = Arrow{sourceArrow :: Colimit i n
sourceArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n t
a, targetArrow :: Colimit i n
targetArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
targetArrow Arrow n t
a, labelArrow :: Colimit i t
labelArrow = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> t -> Colimit i t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                coprojectGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph Graph a t
g = Set (Colimit i a)
-> Set (Arrow (Colimit i a) (Colimit i t))
-> Graph (Colimit i a) (Colimit i t)
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((a -> Colimit i a
forall i t. t -> Colimit i t
Coprojection) (a -> Colimit i a) -> Set a -> Set (Colimit i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set a
forall n e. Graph n e -> Set n
nodes Graph a t
g) ((Arrow a t -> Arrow (Colimit i a) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow) (Arrow a t -> Arrow (Colimit i a) (Colimit i t))
-> Set (Arrow a t) -> Set (Arrow (Colimit i a) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set (Arrow a t)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a t
g)
                coprojectLaw :: Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw Map (f (Arrow n t)) (f (Arrow n t))
cl = Set
  (f (Arrow (Colimit i n) (Colimit i t)),
   f (Arrow (Colimit i n) (Colimit i t)))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp1, Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp2) | (f (Arrow n t)
rp1,f (Arrow n t)
rp2) <- Map (f (Arrow n t)) (f (Arrow n t))
-> Set (f (Arrow n t), f (Arrow n t))
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map (f (Arrow n t)) (f (Arrow n t))
cl]
                coprojectCG :: CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG CompositionGraph a t
cg = Graph (Colimit i a) (Colimit i t)
-> CompositionLaw (Colimit i a) (Colimit i t)
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Graph a t -> Graph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (Graph a t -> Graph (Colimit i a) (Colimit i t))
-> Graph a t -> Graph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Graph a t
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a t
cg) (Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw (Map [Arrow a t] [Arrow a t]
 -> CompositionLaw (Colimit i a) (Colimit i t))
-> Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Map [Arrow a t] [Arrow a t]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a t
cg)
                coprojectCGMorphism :: CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path = (t
a, [Arrow t t]
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw = CompositionLaw t t
cl} = CGMorphism{path :: Path (Colimit i t) (Colimit i t)
path = (t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
a, Arrow t t -> Arrow (Colimit i t) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow t t -> Arrow (Colimit i t) (Colimit i t))
-> [Arrow t t] -> [Arrow (Colimit i t) (Colimit i t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow t t]
rp), compositionLaw :: CompositionLaw (Colimit i t) (Colimit i t)
compositionLaw = CompositionLaw t t -> CompositionLaw (Colimit i t) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw CompositionLaw t t
cl}
                coprojectDiag :: Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Diagram
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o2)
coprojectDiag Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d = Diagram{src :: CompositionGraph (Colimit i a) (Colimit i t)
src = CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph a t
 -> CompositionGraph (Colimit i a) (Colimit i t))
-> CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> CompositionGraph a t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, tgt :: CompositionGraph (Colimit i a) (Colimit i t)
tgt = CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph a t
 -> CompositionGraph (Colimit i a) (Colimit i t))
-> CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> CompositionGraph a t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, omap :: Map (Colimit i o1) (Colimit i o2)
omap = (\(o1
x,o2
y) -> (o1 -> Colimit i o1
forall i t. t -> Colimit i t
Coprojection o1
x, o2 -> Colimit i o2
forall i t. t -> Colimit i t
Coprojection o2
y)) ((o1, o2) -> (Colimit i o1, Colimit i o2))
-> Map o1 o2 -> Map (Colimit i o1) (Colimit i o2)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, mmap :: Map
  (CGMorphism (Colimit i t) (Colimit i t))
  (CGMorphism (Colimit i t) (Colimit i t))
mmap = (\(CGMorphism t t
x,CGMorphism t t
y) -> (CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism t t
x, CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism t t
y)) ((CGMorphism t t, CGMorphism t t)
 -> (CGMorphism (Colimit i t) (Colimit i t),
     CGMorphism (Colimit i t) (Colimit i t)))
-> Map (CGMorphism t t) (CGMorphism t t)
-> Map
     (CGMorphism (Colimit i t) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Map (CGMorphism t t) (CGMorphism t t)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d}

        coprojectBase :: Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> Diagram
     (FinCat c m o)
     (FinFunctor c m o)
     c
     (FinCat
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
     (FinFunctor
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
coprojectBase Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag = Diagram{src :: FinCat c m o
src = FinCat c m o
forall c m o. FinCat c m o
FinCat, tgt :: FinCat
  (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
  (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
  (Colimit oIndex o)
tgt = FinCat
  (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
  (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
  (Colimit oIndex o)
forall c m o. FinCat c m o
FinCat, omap :: Map c (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
omap = Set (c, CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
-> Map c (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i,CompositionGraph o m
-> CompositionGraph (Colimit oIndex o) (Colimit oIndex m)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph o m
 -> CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
-> CompositionGraph o m
-> CompositionGraph (Colimit oIndex o) (Colimit oIndex m)
forall a b. (a -> b) -> a -> b
$ Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
-> CompositionGraph o m
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
 -> CompositionGraph o m)
-> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
-> CompositionGraph o m
forall a b. (a -> b) -> a -> b
$ c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
finiteCategoryToCompositionGraph2 (c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o)
-> c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
forall a b. (a -> b) -> a -> b
$  Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> oIndex -> c
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i) | oIndex
i <- cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (cIndex -> Set oIndex) -> cIndex -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag], mmap :: Map
  (FinFunctor c m o)
  (FinFunctor
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
     (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
     (Colimit oIndex o))
mmap = Set
  (FinFunctor c m o,
   FinFunctor
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
     (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
     (Colimit oIndex o))
-> Map
     (FinFunctor c m o)
     (FinFunctor
        (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
        (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
        (Colimit oIndex o))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
->£ mIndex
f,Diagram
  (CompositionGraph o m)
  (CGMorphism o m)
  o
  (CompositionGraph o m)
  (CGMorphism o m)
  o
-> FinFunctor
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
     (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
     (Colimit oIndex o)
forall {a} {t} {a} {t} {t} {t} {t} {t} {o1} {o2} {i} {i} {i} {i}
       {i} {i} {i} {i} {i} {i}.
(Eq a, Eq t, Eq a, Eq t, Eq t, Eq t, Eq t, Eq t) =>
Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Diagram
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o2)
coprojectDiag  (Diagram
   (CompositionGraph o m)
   (CGMorphism o m)
   o
   (CompositionGraph o m)
   (CGMorphism o m)
   o
 -> FinFunctor
      (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
      (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
      (Colimit oIndex o))
-> Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o
-> FinFunctor
     (CompositionGraph (Colimit oIndex o) (Colimit oIndex m))
     (CGMorphism (Colimit oIndex o) (Colimit oIndex m))
     (Colimit oIndex o)
forall a b. (a -> b) -> a -> b
$ FinFunctor c m o
-> Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2
-> Diagram
     (CompositionGraph o1 m1)
     (CGMorphism o1 m1)
     o1
     (CompositionGraph o2 m2)
     (CGMorphism o2 m2)
     o2
diagramToDiagramOfCompositionGraphs2 (FinFunctor c m o
 -> Diagram
      (CompositionGraph o m)
      (CGMorphism o m)
      o
      (CompositionGraph o m)
      (CGMorphism o m)
      o)
-> FinFunctor c m o
-> Diagram
     (CompositionGraph o m)
     (CGMorphism o m)
     o
     (CompositionGraph o m)
     (CGMorphism o m)
     o
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> mIndex -> FinFunctor c m o
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
->£ mIndex
f) | mIndex
f <- cIndex -> Set mIndex
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (cIndex -> Set mIndex) -> cIndex -> Set mIndex
forall a b. (a -> b) -> a -> b
$ Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c
diag] }
            where
                coprojectArrow :: Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow Arrow n t
a = Arrow{sourceArrow :: Colimit i n
sourceArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n t
a, targetArrow :: Colimit i n
targetArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
targetArrow Arrow n t
a, labelArrow :: Colimit i t
labelArrow = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> t -> Colimit i t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                coprojectGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph Graph a t
g = Set (Colimit i a)
-> Set (Arrow (Colimit i a) (Colimit i t))
-> Graph (Colimit i a) (Colimit i t)
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((a -> Colimit i a
forall i t. t -> Colimit i t
Coprojection) (a -> Colimit i a) -> Set a -> Set (Colimit i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set a
forall n e. Graph n e -> Set n
nodes Graph a t
g) ((Arrow a t -> Arrow (Colimit i a) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow) (Arrow a t -> Arrow (Colimit i a) (Colimit i t))
-> Set (Arrow a t) -> Set (Arrow (Colimit i a) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set (Arrow a t)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a t
g)
                coprojectLaw :: Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw Map (f (Arrow n t)) (f (Arrow n t))
cl = Set
  (f (Arrow (Colimit i n) (Colimit i t)),
   f (Arrow (Colimit i n) (Colimit i t)))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp1, Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp2) | (f (Arrow n t)
rp1,f (Arrow n t)
rp2) <- Map (f (Arrow n t)) (f (Arrow n t))
-> Set (f (Arrow n t), f (Arrow n t))
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map (f (Arrow n t)) (f (Arrow n t))
cl]
                coprojectCG :: CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG CompositionGraph a t
cg = Graph (Colimit i a) (Colimit i t)
-> CompositionLaw (Colimit i a) (Colimit i t)
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Graph a t -> Graph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (Graph a t -> Graph (Colimit i a) (Colimit i t))
-> Graph a t -> Graph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Graph a t
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a t
cg) (Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw (Map [Arrow a t] [Arrow a t]
 -> CompositionLaw (Colimit i a) (Colimit i t))
-> Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Map [Arrow a t] [Arrow a t]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a t
cg)
                coprojectCGMorphism :: CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path = (t
a, [Arrow t t]
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw = CompositionLaw t t
cl} = CGMorphism{path :: Path (Colimit i t) (Colimit i t)
path = (t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
a, Arrow t t -> Arrow (Colimit i t) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow t t -> Arrow (Colimit i t) (Colimit i t))
-> [Arrow t t] -> [Arrow (Colimit i t) (Colimit i t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow t t]
rp), compositionLaw :: CompositionLaw (Colimit i t) (Colimit i t)
compositionLaw = CompositionLaw t t -> CompositionLaw (Colimit i t) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw CompositionLaw t t
cl}
                coprojectDiag :: Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Diagram
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o2)
coprojectDiag Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d = Diagram{src :: CompositionGraph (Colimit i a) (Colimit i t)
src = CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph a t
 -> CompositionGraph (Colimit i a) (Colimit i t))
-> CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> CompositionGraph a t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, tgt :: CompositionGraph (Colimit i a) (Colimit i t)
tgt = CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph a t
 -> CompositionGraph (Colimit i a) (Colimit i t))
-> CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> CompositionGraph a t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, omap :: Map (Colimit i o1) (Colimit i o2)
omap = (\(o1
x,o2
y) -> (o1 -> Colimit i o1
forall i t. t -> Colimit i t
Coprojection o1
x, o2 -> Colimit i o2
forall i t. t -> Colimit i t
Coprojection o2
y)) ((o1, o2) -> (Colimit i o1, Colimit i o2))
-> Map o1 o2 -> Map (Colimit i o1) (Colimit i o2)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, mmap :: Map
  (CGMorphism (Colimit i t) (Colimit i t))
  (CGMorphism (Colimit i t) (Colimit i t))
mmap = (\(CGMorphism t t
x,CGMorphism t t
y) -> (CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism t t
x, CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism t t
y)) ((CGMorphism t t, CGMorphism t t)
 -> (CGMorphism (Colimit i t) (Colimit i t),
     CGMorphism (Colimit i t) (Colimit i t)))
-> Map (CGMorphism t t) (CGMorphism t t)
-> Map
     (CGMorphism (Colimit i t) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Map (CGMorphism t t) (CGMorphism t t)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d}
                
    -- | Computes the colimit of a 'Diagram' of 'CompositionGraph's, use this if you already have a 'Diagram' of 'CompositionGraph's. 

    colimitOfCompositionGraphs :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex, Eq n, Eq e) => 
        Diagram cIndex mIndex oIndex (FinCat (CompositionGraph n e) (CGMorphism n e) n) (FinFunctor (CompositionGraph n e) (CGMorphism n e) n) (CompositionGraph n e) -> Cocone cIndex mIndex oIndex (FinCat (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) (CGMorphism (Colimit oIndex n) (Colimit oIndex e)) (Colimit oIndex n)) (FinFunctor (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) (CGMorphism (Colimit oIndex n) (Colimit oIndex e)) (Colimit oIndex n)) (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
    colimitOfCompositionGraphs :: forall cIndex mIndex oIndex n e.
(FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex, Eq n, Eq e) =>
Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
colimitOfCompositionGraphs = (FinFunctor (CompositionGraph n e) (CGMorphism n e) n
 -> FinFunctor
      (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
      (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
      (Colimit oIndex n))
-> Diagram
     cIndex
     mIndex
     oIndex
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
forall c m o cLim mLim oLim oIndex cIndex mIndex.
(Category c m o, Morphism m o, Category cLim mLim oLim,
 Morphism mLim oLim, HasCoproducts c m o cLim mLim oLim oIndex,
 HasCoequalizers cLim mLim oLim,
 FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq oIndex, Eq mIndex, Eq cIndex) =>
(m -> mLim)
-> Diagram cIndex mIndex oIndex c m o
-> Cocone cIndex mIndex oIndex cLim mLim oLim
colimitFromCoproductsAndCoequalizers FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> FinFunctor
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
forall {i} {o1} {i} {t} {i} {o2} {i} {t}.
(Eq i, Eq o1, Eq i, Eq t, Eq i, Eq o2, Eq i, Eq t) =>
Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
-> Diagram
     (CompositionGraph (Colimit i o1) (Colimit i t))
     (CGMorphism (Colimit i o1) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i o2) (Colimit i t))
     (CGMorphism (Colimit i o2) (Colimit i t))
     (Colimit i o2)
coprojectDiag
            where
                coprojectArrow :: Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow Arrow n t
a = Arrow{sourceArrow :: Colimit i n
sourceArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n t
a, targetArrow :: Colimit i n
targetArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
targetArrow Arrow n t
a, labelArrow :: Colimit i t
labelArrow = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> t -> Colimit i t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                coprojectGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph Graph a t
g = Set (Colimit i a)
-> Set (Arrow (Colimit i a) (Colimit i t))
-> Graph (Colimit i a) (Colimit i t)
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((a -> Colimit i a
forall i t. t -> Colimit i t
Coprojection) (a -> Colimit i a) -> Set a -> Set (Colimit i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set a
forall n e. Graph n e -> Set n
nodes Graph a t
g) ((Arrow a t -> Arrow (Colimit i a) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow) (Arrow a t -> Arrow (Colimit i a) (Colimit i t))
-> Set (Arrow a t) -> Set (Arrow (Colimit i a) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set (Arrow a t)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a t
g)
                coprojectLaw :: Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw Map (f (Arrow n t)) (f (Arrow n t))
cl = Set
  (f (Arrow (Colimit i n) (Colimit i t)),
   f (Arrow (Colimit i n) (Colimit i t)))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp1, Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp2) | (f (Arrow n t)
rp1,f (Arrow n t)
rp2) <- Map (f (Arrow n t)) (f (Arrow n t))
-> Set (f (Arrow n t), f (Arrow n t))
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map (f (Arrow n t)) (f (Arrow n t))
cl]
                coprojectCG :: CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG CompositionGraph a t
cg = Graph (Colimit i a) (Colimit i t)
-> CompositionLaw (Colimit i a) (Colimit i t)
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Graph a t -> Graph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (Graph a t -> Graph (Colimit i a) (Colimit i t))
-> Graph a t -> Graph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Graph a t
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a t
cg) (Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw (Map [Arrow a t] [Arrow a t]
 -> CompositionLaw (Colimit i a) (Colimit i t))
-> Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Map [Arrow a t] [Arrow a t]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a t
cg)
                coprojectCGMorphism :: CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path = (t
a, [Arrow t t]
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw = CompositionLaw t t
cl} = CGMorphism{path :: Path (Colimit i t) (Colimit i t)
path = (t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
a, Arrow t t -> Arrow (Colimit i t) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow t t -> Arrow (Colimit i t) (Colimit i t))
-> [Arrow t t] -> [Arrow (Colimit i t) (Colimit i t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow t t]
rp), compositionLaw :: CompositionLaw (Colimit i t) (Colimit i t)
compositionLaw = CompositionLaw t t -> CompositionLaw (Colimit i t) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw CompositionLaw t t
cl}
                coprojectDiag :: Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
-> Diagram
     (CompositionGraph (Colimit i o1) (Colimit i t))
     (CGMorphism (Colimit i o1) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i o2) (Colimit i t))
     (CGMorphism (Colimit i o2) (Colimit i t))
     (Colimit i o2)
coprojectDiag Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
d = Diagram
  (CompositionGraph (Colimit i o1) (Colimit i t))
  (CGMorphism (Colimit i o1) (Colimit i t))
  (Colimit i o1)
  (CompositionGraph (Colimit i o2) (Colimit i t))
  (CGMorphism (Colimit i o2) (Colimit i t))
  (Colimit i o2)
-> Diagram
     (CompositionGraph (Colimit i o1) (Colimit i t))
     (CGMorphism (Colimit i o1) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i o2) (Colimit i t))
     (CGMorphism (Colimit i o2) (Colimit i t))
     (Colimit i o2)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph (Colimit i o1) (Colimit i t)
src = CompositionGraph o1 t
-> CompositionGraph (Colimit i o1) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph o1 t
 -> CompositionGraph (Colimit i o1) (Colimit i t))
-> CompositionGraph o1 t
-> CompositionGraph (Colimit i o1) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
-> CompositionGraph o1 t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
d, tgt :: CompositionGraph (Colimit i o2) (Colimit i t)
tgt = CompositionGraph o2 t
-> CompositionGraph (Colimit i o2) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph o2 t
 -> CompositionGraph (Colimit i o2) (Colimit i t))
-> CompositionGraph o2 t
-> CompositionGraph (Colimit i o2) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
-> CompositionGraph o2 t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
d, omap :: Map (Colimit i o1) (Colimit i o2)
omap = (\(o1
x,o2
y) -> (o1 -> Colimit i o1
forall i t. t -> Colimit i t
Coprojection o1
x, o2 -> Colimit i o2
forall i t. t -> Colimit i t
Coprojection o2
y)) ((o1, o2) -> (Colimit i o1, Colimit i o2))
-> Map o1 o2 -> Map (Colimit i o1) (Colimit i o2)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
-> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
d, mmap :: Map
  (CGMorphism (Colimit i o1) (Colimit i t))
  (CGMorphism (Colimit i o2) (Colimit i t))
mmap = (\(CGMorphism o1 t
x,CGMorphism o2 t
y) -> (CGMorphism o1 t -> CGMorphism (Colimit i o1) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism o1 t
x, CGMorphism o2 t -> CGMorphism (Colimit i o2) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism o2 t
y)) ((CGMorphism o1 t, CGMorphism o2 t)
 -> (CGMorphism (Colimit i o1) (Colimit i t),
     CGMorphism (Colimit i o2) (Colimit i t)))
-> Map (CGMorphism o1 t) (CGMorphism o2 t)
-> Map
     (CGMorphism (Colimit i o1) (Colimit i t))
     (CGMorphism (Colimit i o2) (Colimit i t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
-> Map (CGMorphism o1 t) (CGMorphism o2 t)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (CompositionGraph o1 t)
  (CGMorphism o1 t)
  o1
  (CompositionGraph o2 t)
  (CGMorphism o2 t)
  o2
d}
                
    -- | Uncoproject a base of 'CompositionGraph's.

    coprojectBaseCompositionGraphs :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex, Eq e, Eq n) => Diagram cIndex mIndex oIndex (FinCat (CompositionGraph n e) (CGMorphism n e) n) (FinFunctor (CompositionGraph n e) (CGMorphism n e) n) (CompositionGraph n e) -> Diagram (FinCat (CompositionGraph n e) (CGMorphism n e) n) (FinFunctor (CompositionGraph n e) (CGMorphism n e) n) (CompositionGraph n e) (FinCat (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) (CGMorphism (Colimit oIndex n) (Colimit oIndex e)) (Colimit oIndex n)) (FinFunctor (CompositionGraph (Colimit oIndex n) (Colimit oIndex e)) (CGMorphism (Colimit oIndex n) (Colimit oIndex e)) (Colimit oIndex n)) (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
    coprojectBaseCompositionGraphs :: forall cIndex mIndex oIndex e n.
(FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq mIndex, Eq oIndex, Eq e, Eq n) =>
Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> Diagram
     (FinCat (CompositionGraph n e) (CGMorphism n e) n)
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (CompositionGraph n e)
     (FinCat
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (FinFunctor
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
coprojectBaseCompositionGraphs Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag = Diagram{src :: FinCat (CompositionGraph n e) (CGMorphism n e) n
src = FinCat (CompositionGraph n e) (CGMorphism n e) n
forall c m o. FinCat c m o
FinCat, tgt :: FinCat
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
  (Colimit oIndex n)
tgt = FinCat
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
  (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
  (Colimit oIndex n)
forall c m o. FinCat c m o
FinCat, omap :: Map
  (CompositionGraph n e)
  (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
omap = Set
  (CompositionGraph n e,
   CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> Map
     (CompositionGraph n e)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> oIndex -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i,CompositionGraph n e
-> CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph n e
 -> CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
-> CompositionGraph n e
-> CompositionGraph (Colimit oIndex n) (Colimit oIndex e)
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> oIndex -> CompositionGraph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i) | oIndex
i <- cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (cIndex -> Set oIndex) -> cIndex -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag], mmap :: Map
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
mmap = Set
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n,
   Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n))
-> Map
     (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
     (Diagram
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n)
        (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
        (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
        (Colimit oIndex n))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> mIndex -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ mIndex
f,FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
forall {a} {t} {a} {t} {t} {t} {t} {t} {o1} {o2} {i} {i} {i} {i}
       {i} {i} {i} {i} {i} {i}.
(Eq a, Eq t, Eq a, Eq t, Eq t, Eq t, Eq t, Eq t) =>
Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Diagram
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o2)
coprojectDiag (FinFunctor (CompositionGraph n e) (CGMorphism n e) n
 -> Diagram
      (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
      (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
      (Colimit oIndex n)
      (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
      (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
      (Colimit oIndex n))
-> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
-> Diagram
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
     (CompositionGraph (Colimit oIndex n) (Colimit oIndex e))
     (CGMorphism (Colimit oIndex n) (Colimit oIndex e))
     (Colimit oIndex n)
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> mIndex -> FinFunctor (CompositionGraph n e) (CGMorphism n e) n
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
->£ mIndex
f) | mIndex
f <- cIndex -> Set mIndex
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (cIndex -> Set mIndex) -> cIndex -> Set mIndex
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  cIndex
  mIndex
  oIndex
  (FinCat (CompositionGraph n e) (CGMorphism n e) n)
  (FinFunctor (CompositionGraph n e) (CGMorphism n e) n)
  (CompositionGraph n e)
diag] }
        where
            coprojectArrow :: Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow Arrow n t
a = Arrow{sourceArrow :: Colimit i n
sourceArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n t
a, targetArrow :: Colimit i n
targetArrow = n -> Colimit i n
forall i t. t -> Colimit i t
Coprojection (n -> Colimit i n) -> n -> Colimit i n
forall a b. (a -> b) -> a -> b
$ Arrow n t -> n
forall n e. Arrow n e -> n
targetArrow Arrow n t
a, labelArrow :: Colimit i t
labelArrow = t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection (t -> Colimit i t) -> t -> Colimit i t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
            coprojectGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph Graph a t
g = Set (Colimit i a)
-> Set (Arrow (Colimit i a) (Colimit i t))
-> Graph (Colimit i a) (Colimit i t)
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((a -> Colimit i a
forall i t. t -> Colimit i t
Coprojection) (a -> Colimit i a) -> Set a -> Set (Colimit i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set a
forall n e. Graph n e -> Set n
nodes Graph a t
g) ((Arrow a t -> Arrow (Colimit i a) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow) (Arrow a t -> Arrow (Colimit i a) (Colimit i t))
-> Set (Arrow a t) -> Set (Arrow (Colimit i a) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph a t -> Set (Arrow a t)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a t
g)
            coprojectLaw :: Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw Map (f (Arrow n t)) (f (Arrow n t))
cl = Set
  (f (Arrow (Colimit i n) (Colimit i t)),
   f (Arrow (Colimit i n) (Colimit i t)))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp1, Arrow n t -> Arrow (Colimit i n) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow n t -> Arrow (Colimit i n) (Colimit i t))
-> f (Arrow n t) -> f (Arrow (Colimit i n) (Colimit i t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Arrow n t)
rp2) | (f (Arrow n t)
rp1,f (Arrow n t)
rp2) <- Map (f (Arrow n t)) (f (Arrow n t))
-> Set (f (Arrow n t), f (Arrow n t))
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map (f (Arrow n t)) (f (Arrow n t))
cl]
            coprojectCG :: CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG CompositionGraph a t
cg = Graph (Colimit i a) (Colimit i t)
-> CompositionLaw (Colimit i a) (Colimit i t)
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Graph a t -> Graph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (Graph a t -> Graph (Colimit i a) (Colimit i t))
-> Graph a t -> Graph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Graph a t
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a t
cg) (Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw (Map [Arrow a t] [Arrow a t]
 -> CompositionLaw (Colimit i a) (Colimit i t))
-> Map [Arrow a t] [Arrow a t]
-> CompositionLaw (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a t -> Map [Arrow a t] [Arrow a t]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a t
cg)
            coprojectCGMorphism :: CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path = (t
a, [Arrow t t]
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw = CompositionLaw t t
cl} = CGMorphism{path :: Path (Colimit i t) (Colimit i t)
path = (t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
a, Arrow t t -> Arrow (Colimit i t) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow (Arrow t t -> Arrow (Colimit i t) (Colimit i t))
-> [Arrow t t] -> [Arrow (Colimit i t) (Colimit i t)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow t t]
rp), compositionLaw :: CompositionLaw (Colimit i t) (Colimit i t)
compositionLaw = CompositionLaw t t -> CompositionLaw (Colimit i t) (Colimit i t)
forall {f :: * -> *} {n} {t} {f :: * -> *} {n} {t} {i} {i} {i} {i}.
(Eq (f (Arrow n t)), Functor f, Functor f) =>
Map (f (Arrow n t)) (f (Arrow n t))
-> Map
     (f (Arrow (Colimit i n) (Colimit i t)))
     (f (Arrow (Colimit i n) (Colimit i t)))
coprojectLaw CompositionLaw t t
cl}
            coprojectDiag :: Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Diagram
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o1)
     (CompositionGraph (Colimit i a) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
     (Colimit i o2)
coprojectDiag Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d = Diagram{src :: CompositionGraph (Colimit i a) (Colimit i t)
src = CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph a t
 -> CompositionGraph (Colimit i a) (Colimit i t))
-> CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> CompositionGraph a t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, tgt :: CompositionGraph (Colimit i a) (Colimit i t)
tgt = CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall {a} {t} {i} {i}.
(Eq a, Eq t) =>
CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
coprojectCG (CompositionGraph a t
 -> CompositionGraph (Colimit i a) (Colimit i t))
-> CompositionGraph a t
-> CompositionGraph (Colimit i a) (Colimit i t)
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> CompositionGraph a t
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, omap :: Map (Colimit i o1) (Colimit i o2)
omap = (\(o1
x,o2
y) -> (o1 -> Colimit i o1
forall i t. t -> Colimit i t
Coprojection o1
x, o2 -> Colimit i o2
forall i t. t -> Colimit i t
Coprojection o2
y)) ((o1, o2) -> (Colimit i o1, Colimit i o2))
-> Map o1 o2 -> Map (Colimit i o1) (Colimit i o2)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Map o1 o2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d, mmap :: Map
  (CGMorphism (Colimit i t) (Colimit i t))
  (CGMorphism (Colimit i t) (Colimit i t))
mmap = (\(CGMorphism t t
x,CGMorphism t t
y) -> (CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism t t
x, CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
CGMorphism t t -> CGMorphism (Colimit i t) (Colimit i t)
coprojectCGMorphism CGMorphism t t
y)) ((CGMorphism t t, CGMorphism t t)
 -> (CGMorphism (Colimit i t) (Colimit i t),
     CGMorphism (Colimit i t) (Colimit i t)))
-> Map (CGMorphism t t) (CGMorphism t t)
-> Map
     (CGMorphism (Colimit i t) (Colimit i t))
     (CGMorphism (Colimit i t) (Colimit i t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
-> Map (CGMorphism t t) (CGMorphism t t)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (CompositionGraph a t)
  (CGMorphism t t)
  o1
  (CompositionGraph a t)
  (CGMorphism t t)
  o2
d}