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


{-| Module  : FiniteCategories
Description : The __'FinGrph'__ category has finite multidigraphs as objects and multidigraph homomorphisms as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'FinGrph'__ category has finite multidigraphs as objects and multidigraph homomorphisms as morphisms.
-}

module Math.Categories.FinGrph
(
    -- * Graph

    Arrow(..),
    Graph,
    -- ** Getters

    nodes,
    edges,
    -- ** Smart constructors

    graph,
    unsafeGraph,
    -- ** Transformation

    mapOnNodes,
    mapOnEdges,
    -- * Graph homomorphism

    GraphHomomorphism,
    -- ** Getters

    nodeMap,
    edgeMap,
    -- ** Smart constructor

    checkGraphHomomorphism,
    graphHomomorphism,
    unsafeGraphHomomorphism,
    -- * FinGrph

    FinGrph(..),
    underlyingGraph,
    underlyingGraphFormat,
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    import              Math.IO.PrettyPrint
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.FiniteCategories.Parallel
    
    import              Data.WeakSet        (Set)
    import qualified    Data.WeakSet    as  Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap        (Map)
    import qualified    Data.WeakMap    as  Map
    import              Data.WeakMap.Safe
    import              Data.Simplifiable
    
    import              GHC.Generics
    
    -- | An 'Arrow' is composed of a source node, a target node and a label.

    data Arrow n e = Arrow{
                            forall n e. Arrow n e -> n
sourceArrow :: n,
                            forall n e. Arrow n e -> n
targetArrow :: n,
                            forall n e. Arrow n e -> e
labelArrow :: e
                          }
                          deriving (Arrow n e -> Arrow n e -> Bool
(Arrow n e -> Arrow n e -> Bool)
-> (Arrow n e -> Arrow n e -> Bool) -> Eq (Arrow n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq n, Eq e) => Arrow n e -> Arrow n e -> Bool
$c== :: forall n e. (Eq n, Eq e) => Arrow n e -> Arrow n e -> Bool
== :: Arrow n e -> Arrow n e -> Bool
$c/= :: forall n e. (Eq n, Eq e) => Arrow n e -> Arrow n e -> Bool
/= :: Arrow n e -> Arrow n e -> Bool
Eq, Int -> Arrow n e -> ShowS
[Arrow n e] -> ShowS
Arrow n e -> String
(Int -> Arrow n e -> ShowS)
-> (Arrow n e -> String)
-> ([Arrow n e] -> ShowS)
-> Show (Arrow n e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. (Show n, Show e) => Int -> Arrow n e -> ShowS
forall n e. (Show n, Show e) => [Arrow n e] -> ShowS
forall n e. (Show n, Show e) => Arrow n e -> String
$cshowsPrec :: forall n e. (Show n, Show e) => Int -> Arrow n e -> ShowS
showsPrec :: Int -> Arrow n e -> ShowS
$cshow :: forall n e. (Show n, Show e) => Arrow n e -> String
show :: Arrow n e -> String
$cshowList :: forall n e. (Show n, Show e) => [Arrow n e] -> ShowS
showList :: [Arrow n e] -> ShowS
Show, (forall x. Arrow n e -> Rep (Arrow n e) x)
-> (forall x. Rep (Arrow n e) x -> Arrow n e)
-> Generic (Arrow n e)
forall x. Rep (Arrow n e) x -> Arrow n e
forall x. Arrow n e -> Rep (Arrow n e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n e x. Rep (Arrow n e) x -> Arrow n e
forall n e x. Arrow n e -> Rep (Arrow n e) x
$cfrom :: forall n e x. Arrow n e -> Rep (Arrow n e) x
from :: forall x. Arrow n e -> Rep (Arrow n e) x
$cto :: forall n e x. Rep (Arrow n e) x -> Arrow n e
to :: forall x. Rep (Arrow n e) x -> Arrow n e
Generic, Arrow n e -> Arrow n e
(Arrow n e -> Arrow n e) -> Simplifiable (Arrow n e)
forall a. (a -> a) -> Simplifiable a
forall n e.
(Simplifiable n, Simplifiable e) =>
Arrow n e -> Arrow n e
$csimplify :: forall n e.
(Simplifiable n, Simplifiable e) =>
Arrow n e -> Arrow n e
simplify :: Arrow n e -> Arrow n e
Simplifiable)
    
    instance (PrettyPrint n, PrettyPrint e) => PrettyPrint (Arrow n e) where
        pprint :: Int -> Arrow n e -> String
pprint Int
v Arrow n e
a = (Int -> n -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (n -> String) -> n -> String
forall a b. (a -> b) -> a -> b
$ Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"-"String -> ShowS
forall a. [a] -> [a] -> [a]
++(Int -> e -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (e -> String) -> e -> String
forall a b. (a -> b) -> a -> b
$ Arrow n e -> e
forall n e. Arrow n e -> e
labelArrow Arrow n e
a)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"->"String -> ShowS
forall a. [a] -> [a] -> [a]
++(Int -> n -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
v (n -> String) -> n -> String
forall a b. (a -> b) -> a -> b
$ Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a)
        
        -- pprintWithIndentations cv ov indent a = indentation (ov - cv) indent ++  (pprint cv $ sourceArrow a)++"-"++(pprint cv $ labelArrow a)++"->"++(pprint cv $ targetArrow a) ++ "\n"

    
    -- | A 'Graph' is a set of nodes and a set of 'Arrow's.

    -- 

    -- 'Graph' is private, use smart constructor 'graph'.

    data Graph n e = Graph {
                        forall n e. Graph n e -> Set n
nodes :: Set n, -- ^ The set of nodes of the graph.

                        forall n e. Graph n e -> Set (Arrow n e)
edges :: Set (Arrow n e) -- ^ The set of arrows of the graph.

                        } deriving (Graph n e -> Graph n e -> Bool
(Graph n e -> Graph n e -> Bool)
-> (Graph n e -> Graph n e -> Bool) -> Eq (Graph n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq n, Eq e) => Graph n e -> Graph n e -> Bool
$c== :: forall n e. (Eq n, Eq e) => Graph n e -> Graph n e -> Bool
== :: Graph n e -> Graph n e -> Bool
$c/= :: forall n e. (Eq n, Eq e) => Graph n e -> Graph n e -> Bool
/= :: Graph n e -> Graph n e -> Bool
Eq, (forall x. Graph n e -> Rep (Graph n e) x)
-> (forall x. Rep (Graph n e) x -> Graph n e)
-> Generic (Graph n e)
forall x. Rep (Graph n e) x -> Graph n e
forall x. Graph n e -> Rep (Graph n e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n e x. Rep (Graph n e) x -> Graph n e
forall n e x. Graph n e -> Rep (Graph n e) x
$cfrom :: forall n e x. Graph n e -> Rep (Graph n e) x
from :: forall x. Graph n e -> Rep (Graph n e) x
$cto :: forall n e x. Rep (Graph n e) x -> Graph n e
to :: forall x. Rep (Graph n e) x -> Graph n e
Generic, Int -> Int -> String -> Graph n e -> String
Int -> Graph n e -> String
(Int -> Graph n e -> String)
-> (Int -> Int -> String -> Graph n e -> String)
-> (Int -> Graph n e -> String)
-> PrettyPrint (Graph n e)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall n e.
(PrettyPrint n, PrettyPrint e, Eq n, Eq e) =>
Int -> Int -> String -> Graph n e -> String
forall n e.
(PrettyPrint n, PrettyPrint e, Eq n, Eq e) =>
Int -> Graph n e -> String
$cpprint :: forall n e.
(PrettyPrint n, PrettyPrint e, Eq n, Eq e) =>
Int -> Graph n e -> String
pprint :: Int -> Graph n e -> String
$cpprintWithIndentations :: forall n e.
(PrettyPrint n, PrettyPrint e, Eq n, Eq e) =>
Int -> Int -> String -> Graph n e -> String
pprintWithIndentations :: Int -> Int -> String -> Graph n e -> String
$cpprintIndent :: forall n e.
(PrettyPrint n, PrettyPrint e, Eq n, Eq e) =>
Int -> Graph n e -> String
pprintIndent :: Int -> Graph n e -> String
PrettyPrint, Graph n e -> Graph n e
(Graph n e -> Graph n e) -> Simplifiable (Graph n e)
forall a. (a -> a) -> Simplifiable a
forall n e.
(Simplifiable n, Simplifiable e, Eq n, Eq e) =>
Graph n e -> Graph n e
$csimplify :: forall n e.
(Simplifiable n, Simplifiable e, Eq n, Eq e) =>
Graph n e -> Graph n e
simplify :: Graph n e -> Graph n e
Simplifiable)
    
    instance (Show n, Show e) => Show (Graph n e) where
        show :: Graph n e -> String
show Graph n e
g = String
"(unsafeGraph "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Set n -> String
forall a. Show a => a -> String
show (Set n -> String) -> Set n -> String
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Set (Arrow n e) -> String
forall a. Show a => a -> String
show (Set (Arrow n e) -> String) -> Set (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    -- | Smart constructor of 'Graph'. The only error possible when creating a 'Graph' is that the source or target of an arrow is not in the set of nodes of the 'Graph'.

    graph :: (Eq n) => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
    graph :: forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph Set n
ns Set (Arrow n e)
es
        | (Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow (Arrow n e -> n) -> Set (Arrow n e) -> Set n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Arrow n e)
es) Set n -> Set n -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` Set n
ns Bool -> Bool -> Bool
&& (Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow (Arrow n e -> n) -> Set (Arrow n e) -> Set n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Arrow n e)
es) Set n -> Set n -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` Set n
ns = Graph n e -> Maybe (Graph n e)
forall a. a -> Maybe a
Just Graph{nodes :: Set n
nodes=Set n
ns, edges :: Set (Arrow n e)
edges=Set (Arrow n e)
es}
        | Bool
otherwise = Maybe (Graph n e)
forall a. Maybe a
Nothing
        
    -- | Unsafe constructor of 'Graph', does not check the 'Graph' structure.

    unsafeGraph :: Set n -> Set (Arrow n e) -> Graph n e
    unsafeGraph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph Set n
n Set (Arrow n e)
e = Graph{nodes :: Set n
nodes=Set n
n, edges :: Set (Arrow n e)
edges=Set (Arrow n e)
e}
    
    -- | Map a function on nodes of a 'Graph'.

    mapOnNodes :: (n1 -> n2) -> Graph n1 e -> Graph n2 e
    mapOnNodes :: forall n1 n2 e. (n1 -> n2) -> Graph n1 e -> Graph n2 e
mapOnNodes n1 -> n2
transformNode Graph n1 e
g = Graph {nodes :: Set n2
nodes = n1 -> n2
transformNode (n1 -> n2) -> Set n1 -> Set n2
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n1 e -> Set n1
forall n e. Graph n e -> Set n
nodes Graph n1 e
g, edges :: Set (Arrow n2 e)
edges = Arrow n1 e -> Arrow n2 e
forall {e}. Arrow n1 e -> Arrow n2 e
transformArrow (Arrow n1 e -> Arrow n2 e) -> Set (Arrow n1 e) -> Set (Arrow n2 e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n1 e -> Set (Arrow n1 e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n1 e
g}
        where
            transformArrow :: Arrow n1 e -> Arrow n2 e
transformArrow Arrow n1 e
arr = Arrow{sourceArrow :: n2
sourceArrow = n1 -> n2
transformNode (n1 -> n2) -> n1 -> n2
forall a b. (a -> b) -> a -> b
$ Arrow n1 e -> n1
forall n e. Arrow n e -> n
sourceArrow Arrow n1 e
arr, targetArrow :: n2
targetArrow = n1 -> n2
transformNode (n1 -> n2) -> n1 -> n2
forall a b. (a -> b) -> a -> b
$ Arrow n1 e -> n1
forall n e. Arrow n e -> n
targetArrow Arrow n1 e
arr, labelArrow :: e
labelArrow = Arrow n1 e -> e
forall n e. Arrow n e -> e
labelArrow Arrow n1 e
arr}
    
    -- | Map a function on edges of a 'Graph'.

    mapOnEdges :: (e1 -> e2) -> Graph n e1 -> Graph n e2
    mapOnEdges :: forall e1 e2 n. (e1 -> e2) -> Graph n e1 -> Graph n e2
mapOnEdges e1 -> e2
transformEdge Graph n e1
g = Graph {nodes :: Set n
nodes = Graph n e1 -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e1
g, edges :: Set (Arrow n e2)
edges = Arrow n e1 -> Arrow n e2
forall {n}. Arrow n e1 -> Arrow n e2
transformArrow (Arrow n e1 -> Arrow n e2) -> Set (Arrow n e1) -> Set (Arrow n e2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n e1 -> Set (Arrow n e1)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e1
g}
        where
            transformArrow :: Arrow n e1 -> Arrow n e2
transformArrow Arrow n e1
arr = Arrow{sourceArrow :: n
sourceArrow = Arrow n e1 -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e1
arr, targetArrow :: n
targetArrow = Arrow n e1 -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e1
arr, labelArrow :: e2
labelArrow = e1 -> e2
transformEdge (e1 -> e2) -> e1 -> e2
forall a b. (a -> b) -> a -> b
$ Arrow n e1 -> e1
forall n e. Arrow n e -> e
labelArrow Arrow n e1
arr}
    
    -- | A 'GraphHomomorphism' is composed of a map between the nodes of the graphs, a map between the edges of the graphs, and the target 'Graph' so that we can recover it from the morphism.

    --

    -- It must follow axioms such that the image of an arrow is not torn appart, that is why the constructor is private. Use the smart constructor 'graphHomomorphism' instead.

    data GraphHomomorphism n e = GraphHomomorphism {
                                    forall n e. GraphHomomorphism n e -> Map n n
nodeMap :: Map n n, -- ^ The mapping of nodes.

                                    forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap :: Map (Arrow n e) (Arrow n e), -- ^ The mapping of edges.

                                    forall n e. GraphHomomorphism n e -> Graph n e
targetGraph :: Graph n e -- ^ The target graph.

                                    } deriving (GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
(GraphHomomorphism n e -> GraphHomomorphism n e -> Bool)
-> (GraphHomomorphism n e -> GraphHomomorphism n e -> Bool)
-> Eq (GraphHomomorphism n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e.
(Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
$c== :: forall n e.
(Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
== :: GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
$c/= :: forall n e.
(Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
/= :: GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
Eq, (forall x. GraphHomomorphism n e -> Rep (GraphHomomorphism n e) x)
-> (forall x.
    Rep (GraphHomomorphism n e) x -> GraphHomomorphism n e)
-> Generic (GraphHomomorphism n e)
forall x. Rep (GraphHomomorphism n e) x -> GraphHomomorphism n e
forall x. GraphHomomorphism n e -> Rep (GraphHomomorphism n e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n e x.
Rep (GraphHomomorphism n e) x -> GraphHomomorphism n e
forall n e x.
GraphHomomorphism n e -> Rep (GraphHomomorphism n e) x
$cfrom :: forall n e x.
GraphHomomorphism n e -> Rep (GraphHomomorphism n e) x
from :: forall x. GraphHomomorphism n e -> Rep (GraphHomomorphism n e) x
$cto :: forall n e x.
Rep (GraphHomomorphism n e) x -> GraphHomomorphism n e
to :: forall x. Rep (GraphHomomorphism n e) x -> GraphHomomorphism n e
Generic, GraphHomomorphism n e -> GraphHomomorphism n e
(GraphHomomorphism n e -> GraphHomomorphism n e)
-> Simplifiable (GraphHomomorphism n e)
forall a. (a -> a) -> Simplifiable a
forall n e.
(Simplifiable n, Simplifiable e, Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e
$csimplify :: forall n e.
(Simplifiable n, Simplifiable e, Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e
simplify :: GraphHomomorphism n e -> GraphHomomorphism n e
Simplifiable)
    
    -- | Check wether the structure of 'GraphHomomorphism' is respected or not.

    checkGraphHomomorphism :: (Eq n, Eq e) => GraphHomomorphism n e -> Bool
    checkGraphHomomorphism :: forall n e. (Eq n, Eq e) => GraphHomomorphism n e -> Bool
checkGraphHomomorphism GraphHomomorphism n e
gh = Bool
imageInTarget Bool -> Bool -> Bool
&& Set Bool -> Bool
Set.and Set Bool
noTear
        where
            noTear :: Set Bool
noTear = [(GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| (Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
arr) n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow ((GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
arr) Bool -> Bool -> Bool
&& (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| (Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
arr) n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow ((GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
arr)| Arrow n e
arr <- (Map (Arrow n e) (Arrow n e) -> Set (Arrow n e)
forall k a. Map k a -> Set k
domain(Map (Arrow n e) (Arrow n e) -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e))
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap) GraphHomomorphism n e
gh]
            imageInTarget :: Bool
imageInTarget = (Map n n -> Set n
forall k a. Eq k => Map k a -> Set a
image(Map n n -> Set n)
-> (GraphHomomorphism n e -> Map n n)
-> GraphHomomorphism n e
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap) GraphHomomorphism n e
gh Set n -> Set n -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes(Graph n e -> Set n)
-> (GraphHomomorphism n e -> Graph n e)
-> GraphHomomorphism n e
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph) GraphHomomorphism n e
gh Bool -> Bool -> Bool
&& (Map (Arrow n e) (Arrow n e) -> Set (Arrow n e)
forall k a. Eq k => Map k a -> Set a
image(Map (Arrow n e) (Arrow n e) -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e))
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap) GraphHomomorphism n e
gh Set (Arrow n e) -> Set (Arrow n e) -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph n e -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Graph n e)
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph) GraphHomomorphism n e
gh
    
    -- | The smart constructor of 'GraphHomomorphism'.

    graphHomomorphism :: (Eq n, Eq e) => Map n n -> Map (Arrow n e) (Arrow n e) -> Graph n e -> Maybe (GraphHomomorphism n e)
    graphHomomorphism :: forall n e.
(Eq n, Eq e) =>
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> Maybe (GraphHomomorphism n e)
graphHomomorphism Map n n
nm Map (Arrow n e) (Arrow n e)
em Graph n e
tg
        | GraphHomomorphism n e -> Bool
forall n e. (Eq n, Eq e) => GraphHomomorphism n e -> Bool
checkGraphHomomorphism GraphHomomorphism n e
gh = GraphHomomorphism n e -> Maybe (GraphHomomorphism n e)
forall a. a -> Maybe a
Just GraphHomomorphism n e
gh
        | Bool
otherwise = Maybe (GraphHomomorphism n e)
forall a. Maybe a
Nothing
        where
            gh :: GraphHomomorphism n e
gh = GraphHomomorphism{nodeMap :: Map n n
nodeMap=Map n n
nm, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap=Map (Arrow n e) (Arrow n e)
em, targetGraph :: Graph n e
targetGraph=Graph n e
tg}
    
    -- | Unsafe constructor of 'GraphHomomorphism' which does not check the structure of the 'GraphHomomorphism'.

    unsafeGraphHomomorphism :: Map n n -> Map (Arrow n e) (Arrow n e) -> Graph n e -> GraphHomomorphism n e
    unsafeGraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
unsafeGraphHomomorphism Map n n
nm Map (Arrow n e) (Arrow n e)
em Graph n e
tg = GraphHomomorphism{nodeMap :: Map n n
nodeMap=Map n n
nm, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap=Map (Arrow n e) (Arrow n e)
em, targetGraph :: Graph n e
targetGraph=Graph n e
tg}
    
    instance (Show n, Show e) => Show (GraphHomomorphism n e) where
        show :: GraphHomomorphism n e -> String
show GraphHomomorphism n e
gh = String
"(unsafeGraphHomomorphism "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Map n n -> String
forall a. Show a => a -> String
show (Map n n -> String) -> Map n n -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Map (Arrow n e) (Arrow n e) -> String
forall a. Show a => a -> String
show (Map (Arrow n e) (Arrow n e) -> String)
-> Map (Arrow n e) (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Graph n e -> String
forall a. Show a => a -> String
show (Graph n e -> String) -> Graph n e -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph GraphHomomorphism n e
gh) String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (GraphHomomorphism n e) where
        pprint :: Int -> GraphHomomorphism n e -> String
pprint Int
v GraphHomomorphism n e
gh = String
"GH("String -> ShowS
forall a. [a] -> [a] -> [a]
++(Int -> Map n n -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Map n n -> String) -> Map n n -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Int -> Map (Arrow n e) (Arrow n e) -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Map (Arrow n e) (Arrow n e) -> String)
-> Map (Arrow n e) (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
        
        -- pprintWithIndentations 0 ov indent gh = indentation ov indent ++ "...\n"

        -- pprintWithIndentations cv ov indent gh = indentation (ov - cv) indent ++  "GH\n" ++ (pprintWithIndentations (cv-1) ov indent (nodeMap gh)) ++ (pprintWithIndentations (cv-1) ov indent (edgeMap gh))

        
    instance (Eq n, Eq e) => Morphism (GraphHomomorphism n e) (Graph n e) where
        source :: GraphHomomorphism n e -> Graph n e
source GraphHomomorphism n e
gh = Graph {nodes :: Set n
nodes = (Map n n -> Set n
forall k a. Map k a -> Set k
domain(Map n n -> Set n)
-> (GraphHomomorphism n e -> Map n n)
-> GraphHomomorphism n e
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap) GraphHomomorphism n e
gh, edges :: Set (Arrow n e)
edges = (Map (Arrow n e) (Arrow n e) -> Set (Arrow n e)
forall k a. Map k a -> Set k
domain(Map (Arrow n e) (Arrow n e) -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e))
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap) GraphHomomorphism n e
gh}
        target :: GraphHomomorphism n e -> Graph n e
target = GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph
        @ :: GraphHomomorphism n e
-> GraphHomomorphism n e -> GraphHomomorphism n e
(@) GraphHomomorphism n e
gh2 GraphHomomorphism n e
gh1 =  GraphHomomorphism {nodeMap :: Map n n
nodeMap = (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh2) Map n n -> Map n n -> Map n n
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh1), edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh2) Map (Arrow n e) (Arrow n e)
-> Map (Arrow n e) (Arrow n e) -> Map (Arrow n e) (Arrow n e)
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh1), targetGraph :: Graph n e
targetGraph = GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh2}
    
    -- | The category of finite graphs.

    data FinGrph n e = FinGrph deriving (FinGrph n e -> FinGrph n e -> Bool
(FinGrph n e -> FinGrph n e -> Bool)
-> (FinGrph n e -> FinGrph n e -> Bool) -> Eq (FinGrph n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. FinGrph n e -> FinGrph n e -> Bool
$c== :: forall n e. FinGrph n e -> FinGrph n e -> Bool
== :: FinGrph n e -> FinGrph n e -> Bool
$c/= :: forall n e. FinGrph n e -> FinGrph n e -> Bool
/= :: FinGrph n e -> FinGrph n e -> Bool
Eq, Int -> FinGrph n e -> ShowS
[FinGrph n e] -> ShowS
FinGrph n e -> String
(Int -> FinGrph n e -> ShowS)
-> (FinGrph n e -> String)
-> ([FinGrph n e] -> ShowS)
-> Show (FinGrph n e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. Int -> FinGrph n e -> ShowS
forall n e. [FinGrph n e] -> ShowS
forall n e. FinGrph n e -> String
$cshowsPrec :: forall n e. Int -> FinGrph n e -> ShowS
showsPrec :: Int -> FinGrph n e -> ShowS
$cshow :: forall n e. FinGrph n e -> String
show :: FinGrph n e -> String
$cshowList :: forall n e. [FinGrph n e] -> ShowS
showList :: [FinGrph n e] -> ShowS
Show, (forall x. FinGrph n e -> Rep (FinGrph n e) x)
-> (forall x. Rep (FinGrph n e) x -> FinGrph n e)
-> Generic (FinGrph n e)
forall x. Rep (FinGrph n e) x -> FinGrph n e
forall x. FinGrph n e -> Rep (FinGrph n e) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n e x. Rep (FinGrph n e) x -> FinGrph n e
forall n e x. FinGrph n e -> Rep (FinGrph n e) x
$cfrom :: forall n e x. FinGrph n e -> Rep (FinGrph n e) x
from :: forall x. FinGrph n e -> Rep (FinGrph n e) x
$cto :: forall n e x. Rep (FinGrph n e) x -> FinGrph n e
to :: forall x. Rep (FinGrph n e) x -> FinGrph n e
Generic, Int -> Int -> String -> FinGrph n e -> String
Int -> FinGrph n e -> String
(Int -> FinGrph n e -> String)
-> (Int -> Int -> String -> FinGrph n e -> String)
-> (Int -> FinGrph n e -> String)
-> PrettyPrint (FinGrph n e)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall n e. Int -> Int -> String -> FinGrph n e -> String
forall n e. Int -> FinGrph n e -> String
$cpprint :: forall n e. Int -> FinGrph n e -> String
pprint :: Int -> FinGrph n e -> String
$cpprintWithIndentations :: forall n e. Int -> Int -> String -> FinGrph n e -> String
pprintWithIndentations :: Int -> Int -> String -> FinGrph n e -> String
$cpprintIndent :: forall n e. Int -> FinGrph n e -> String
pprintIndent :: Int -> FinGrph n e -> String
PrettyPrint, FinGrph n e -> FinGrph n e
(FinGrph n e -> FinGrph n e) -> Simplifiable (FinGrph n e)
forall a. (a -> a) -> Simplifiable a
forall n e. FinGrph n e -> FinGrph n e
$csimplify :: forall n e. FinGrph n e -> FinGrph n e
simplify :: FinGrph n e -> FinGrph n e
Simplifiable)
        
    instance (Eq n, Eq e) => Category (FinGrph n e) (GraphHomomorphism n e) (Graph n e) where
        identity :: Morphism (GraphHomomorphism n e) (Graph n e) =>
FinGrph n e -> Graph n e -> GraphHomomorphism n e
identity FinGrph n e
_ Graph n e
g = GraphHomomorphism {nodeMap :: Map n n
nodeMap = (Set n -> Map n n
forall a. Set a -> Map a a
idFromSet(Set n -> Map n n) -> (Graph n e -> Set n) -> Graph n e -> Map n n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes) Graph n e
g, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = (Set (Arrow n e) -> Map (Arrow n e) (Arrow n e)
forall a. Set a -> Map a a
idFromSet(Set (Arrow n e) -> Map (Arrow n e) (Arrow n e))
-> (Graph n e -> Set (Arrow n e))
-> Graph n e
-> Map (Arrow n e) (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges) Graph n e
g, targetGraph :: Graph n e
targetGraph = Graph n e
g}
        ar :: Morphism (GraphHomomorphism n e) (Graph n e) =>
FinGrph n e
-> Graph n e -> Graph n e -> Set (GraphHomomorphism n e)
ar FinGrph n e
_ Graph n e
s Graph n e
t = [GraphHomomorphism
            {
                nodeMap :: Map n n
nodeMap = Map n n
appO, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = Map (Arrow n e) (Arrow n e)
appF, targetGraph :: Graph n e
targetGraph = Graph n e
t
            } | Map n n
appO <- Set (Map n n)
appObj, Map (Arrow n e) (Arrow n e)
appF <- ((([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e))
-> Set [Map (Arrow n e) (Arrow n e)]
-> Set (Map (Arrow n e) (Arrow n e))
forall a b. (a -> b) -> Set a -> Set b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e))
 -> Set [Map (Arrow n e) (Arrow n e)]
 -> Set (Map (Arrow n e) (Arrow n e)))
-> ([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e))
-> Set [Map (Arrow n e) (Arrow n e)]
-> Set (Map (Arrow n e) (Arrow n e))
forall a b. (a -> b) -> a -> b
$ ([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e)
forall k a. Eq k => [Map k a] -> Map k a
Map.unions))(Set [Map (Arrow n e) (Arrow n e)]
 -> Set (Map (Arrow n e) (Arrow n e)))
-> ([Set (Map (Arrow n e) (Arrow n e))]
    -> Set [Map (Arrow n e) (Arrow n e)])
-> [Set (Map (Arrow n e) (Arrow n e))]
-> Set (Map (Arrow n e) (Arrow n e))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Set (Map (Arrow n e) (Arrow n e))]
-> Set [Map (Arrow n e) (Arrow n e)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets ([Set (Map (Arrow n e) (Arrow n e))]
 -> Set (Map (Arrow n e) (Arrow n e)))
-> [Set (Map (Arrow n e) (Arrow n e))]
-> Set (Map (Arrow n e) (Arrow n e))
forall a b. (a -> b) -> a -> b
$ [n -> n -> Map n n -> Set (Map (Arrow n e) (Arrow n e))
twoObjToEdgeMaps n
x n
y Map n n
appO | n
x <- (Set n -> [n]
forall a. Eq a => Set a -> [a]
setToList (Set n -> [n]) -> Set n -> [n]
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
s), n
y <- (Set n -> [n]
forall a. Eq a => Set a -> [a]
setToList (Set n -> [n]) -> Set n -> [n]
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
s)])]
            where
                appObj :: Set (Map n n)
appObj = Set n -> Set n -> Set (Map n n)
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
s) (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
t)
                twoObjToEdgeMaps :: n -> n -> Map n n -> Set (Map (Arrow n e) (Arrow n e))
twoObjToEdgeMaps n
n1 n
n2 Map n n
nMap = Set (Arrow n e)
-> Set (Arrow n e) -> Set (Map (Arrow n e) (Arrow n e))
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps ((Arrow n e -> Bool) -> Set (Arrow n e) -> Set (Arrow n e)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow n e
a -> Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
n1 Bool -> Bool -> Bool
&& Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
n2) (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
s)) ((Arrow n e -> Bool) -> Set (Arrow n e) -> Set (Arrow n e)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow n e
a -> Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Map n n
nMap Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
n1 Bool -> Bool -> Bool
&& Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Map n n
nMap Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
n2) (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
t))
    
    instance (Eq n, Eq e, Eq oIndex) => HasProducts (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) oIndex where
        product :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit oIndex e))
product Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag = Graph (Limit oIndex n) (Limit oIndex e)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit oIndex e))
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit oIndex e))
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone Graph (Limit oIndex n) (Limit oIndex e)
productGraph NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Limit oIndex n) (Limit oIndex e))
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
  (Graph (Limit oIndex n) (Limit oIndex e))
nat
            where
                indexingCat :: DiscreteCategory oIndex
indexingCat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag
                productGraph :: Graph (Limit oIndex n) (Limit oIndex e)
productGraph = Graph{nodes :: Set (Limit oIndex n)
nodes = Set (Limit oIndex n)
productNodes, edges :: Set (Arrow (Limit oIndex n) (Limit oIndex e))
edges = Set (Arrow (Limit oIndex n) (Limit oIndex e))
productEdges}
                productNodes :: Set (Limit oIndex n)
productNodes = (Map oIndex n -> Limit oIndex n
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement)(Map oIndex n -> Limit oIndex n)
-> ([(oIndex, n)] -> Map oIndex n)
-> [(oIndex, n)]
-> Limit oIndex n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(oIndex, n)] -> Map oIndex n
forall k v. AssociationList k v -> Map k v
weakMap ([(oIndex, n)] -> Limit oIndex n)
-> Set [(oIndex, n)] -> Set (Limit oIndex n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (oIndex, n)] -> Set [(oIndex, n)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets (Set (Set (oIndex, n)) -> [Set (oIndex, n)]
forall a. Eq a => Set a -> [a]
setToList [(\n
x -> (oIndex
i,n
x)) (n -> (oIndex, n)) -> Set n -> Set (oIndex, n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> oIndex -> Graph 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
indexingCat])
                productEdges :: Set (Arrow (Limit oIndex n) (Limit oIndex e))
productEdges = (\Map oIndex (Arrow n e)
tupleEdges -> Arrow{sourceArrow :: Limit oIndex n
sourceArrow = Map oIndex n -> Limit oIndex n
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow (Arrow n e -> n) -> Map oIndex (Arrow n e) -> Map oIndex n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex (Arrow n e)
tupleEdges), targetArrow :: Limit oIndex n
targetArrow = Map oIndex n -> Limit oIndex n
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow (Arrow n e -> n) -> Map oIndex (Arrow n e) -> Map oIndex n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex (Arrow n e)
tupleEdges), labelArrow :: Limit oIndex e
labelArrow = Map oIndex e -> Limit oIndex e
forall oIndex t. Map oIndex t -> Limit oIndex t
ProductElement (Arrow n e -> e
forall n e. Arrow n e -> e
labelArrow (Arrow n e -> e) -> Map oIndex (Arrow n e) -> Map oIndex e
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map oIndex (Arrow n e)
tupleEdges)}) (Map oIndex (Arrow n e) -> Arrow (Limit oIndex n) (Limit oIndex e))
-> ([(oIndex, Arrow n e)] -> Map oIndex (Arrow n e))
-> [(oIndex, Arrow n e)]
-> Arrow (Limit oIndex n) (Limit oIndex e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(oIndex, Arrow n e)] -> Map oIndex (Arrow n e)
forall k v. AssociationList k v -> Map k v
weakMap ([(oIndex, Arrow n e)] -> Arrow (Limit oIndex n) (Limit oIndex e))
-> Set [(oIndex, Arrow n e)]
-> Set (Arrow (Limit oIndex n) (Limit oIndex e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (oIndex, Arrow n e)] -> Set [(oIndex, Arrow n e)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets (Set (Set (oIndex, Arrow n e)) -> [Set (oIndex, Arrow n e)]
forall a. Eq a => Set a -> [a]
setToList [(\Arrow n e
x -> (oIndex
i,Arrow n e
x)) (Arrow n e -> (oIndex, Arrow n e))
-> Set (Arrow n e) -> Set (oIndex, Arrow n e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> oIndex -> Graph 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
indexingCat])
                newDiag :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Limit oIndex n) (Limit oIndex e))
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
  (Graph (Limit oIndex n) (Limit oIndex e))
newDiag = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Limit oIndex n) (Limit oIndex e))
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
  (Graph (Limit oIndex n) (Limit oIndex e))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit 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
indexingCat, tgt :: FinGrph (Limit oIndex n) (Limit oIndex e)
tgt = FinGrph (Limit oIndex n) (Limit oIndex e)
forall n e. FinGrph n e
FinGrph, omap :: Map oIndex (Graph (Limit oIndex n) (Limit oIndex e))
omap = Graph n e -> Graph (Limit oIndex n) (Limit oIndex e)
forall {a} {t} {oIndex} {oIndex}.
Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph (Graph n e -> Graph (Limit oIndex n) (Limit oIndex e))
-> Map oIndex (Graph n e)
-> Map oIndex (Graph (Limit oIndex n) (Limit oIndex e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map oIndex (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag, mmap :: Map
  (DiscreteMorphism oIndex)
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
mmap = AssociationList
  (DiscreteMorphism oIndex)
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
-> Map
     (DiscreteMorphism oIndex)
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
forall k v. AssociationList k v -> Map k v
weakMap []}
                nat :: NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Limit oIndex n) (Limit oIndex e))
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
  (Graph (Limit oIndex n) (Limit oIndex e))
nat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Limit oIndex n) (Limit oIndex e))
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
  (Graph (Limit oIndex n) (Limit oIndex e))
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit oIndex e))
-> Map oIndex (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit 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 (DiscreteCategory oIndex
-> FinGrph (Limit oIndex n) (Limit oIndex e)
-> Graph (Limit oIndex n) (Limit oIndex e)
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit 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 (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag) FinGrph (Limit oIndex n) (Limit oIndex e)
forall n e. FinGrph n e
FinGrph Graph (Limit oIndex n) (Limit oIndex e)
productGraph) Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph (Limit oIndex n) (Limit oIndex e))
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
  (Graph (Limit oIndex n) (Limit oIndex e))
newDiag (Set (oIndex, GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
-> Map oIndex (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i, oIndex -> GraphHomomorphism (Limit oIndex n) (Limit oIndex e)
leg oIndex
i) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCat])
                projectArrow :: Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
a = Arrow{sourceArrow :: Limit oIndex n
sourceArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex 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 :: Limit oIndex n
targetArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex 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 :: Limit oIndex t
labelArrow = t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection (t -> Limit oIndex t) -> t -> Limit oIndex t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                projectGraph :: Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph Graph a t
g = Graph{nodes :: Set (Limit oIndex a)
nodes = a -> Limit oIndex a
forall oIndex t. t -> Limit oIndex t
Projection (a -> Limit oIndex a) -> Set a -> Set (Limit oIndex 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, edges :: Set (Arrow (Limit oIndex a) (Limit oIndex t))
edges = Arrow a t -> Arrow (Limit oIndex a) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow (Arrow a t -> Arrow (Limit oIndex a) (Limit oIndex t))
-> Set (Arrow a t) -> Set (Arrow (Limit oIndex a) (Limit oIndex 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}
                leg :: oIndex -> GraphHomomorphism (Limit oIndex n) (Limit oIndex e)
leg oIndex
i = GraphHomomorphism{targetGraph :: Graph (Limit oIndex n) (Limit oIndex e)
targetGraph = Graph n e -> Graph (Limit oIndex n) (Limit oIndex e)
forall {a} {t} {oIndex} {oIndex}.
Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> oIndex -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i), nodeMap :: Map (Limit oIndex n) (Limit oIndex n)
nodeMap = Set (Limit oIndex n, Limit oIndex n)
-> Map (Limit oIndex n) (Limit oIndex n)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Limit oIndex n
n, n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex n
forall a b. (a -> b) -> a -> b
$ Map oIndex n
tuple Map oIndex n -> oIndex -> n
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
i) | n :: Limit oIndex n
n@(ProductElement Map oIndex n
tuple)  <- Graph (Limit oIndex n) (Limit oIndex e) -> Set (Limit oIndex n)
forall n e. Graph n e -> Set n
nodes Graph (Limit oIndex n) (Limit oIndex e)
productGraph], edgeMap :: Map
  (Arrow (Limit oIndex n) (Limit oIndex e))
  (Arrow (Limit oIndex n) (Limit oIndex e))
edgeMap = Set
  (Arrow (Limit oIndex n) (Limit oIndex e),
   Arrow (Limit oIndex n) (Limit oIndex e))
-> Map
     (Arrow (Limit oIndex n) (Limit oIndex e))
     (Arrow (Limit oIndex n) (Limit oIndex e))
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(Arrow (Limit oIndex n) (Limit oIndex e)
e, Arrow{sourceArrow :: Limit oIndex n
sourceArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex n
forall a b. (a -> b) -> a -> b
$ (Limit oIndex n -> Map oIndex n
forall {oIndex} {t}. Limit oIndex t -> Map oIndex t
extractProd(Limit oIndex n -> Map oIndex n)
-> (Arrow (Limit oIndex n) (Limit oIndex e) -> Limit oIndex n)
-> Arrow (Limit oIndex n) (Limit oIndex e)
-> Map oIndex n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow (Limit oIndex n) (Limit oIndex e) -> Limit oIndex n
forall n e. Arrow n e -> n
sourceArrow (Arrow (Limit oIndex n) (Limit oIndex e) -> Map oIndex n)
-> Arrow (Limit oIndex n) (Limit oIndex e) -> Map oIndex n
forall a b. (a -> b) -> a -> b
$ Arrow (Limit oIndex n) (Limit oIndex e)
e) Map oIndex n -> oIndex -> n
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
i , targetArrow :: Limit oIndex n
targetArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex n
forall a b. (a -> b) -> a -> b
$  (Limit oIndex n -> Map oIndex n
forall {oIndex} {t}. Limit oIndex t -> Map oIndex t
extractProd(Limit oIndex n -> Map oIndex n)
-> (Arrow (Limit oIndex n) (Limit oIndex e) -> Limit oIndex n)
-> Arrow (Limit oIndex n) (Limit oIndex e)
-> Map oIndex n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow (Limit oIndex n) (Limit oIndex e) -> Limit oIndex n
forall n e. Arrow n e -> n
targetArrow (Arrow (Limit oIndex n) (Limit oIndex e) -> Map oIndex n)
-> Arrow (Limit oIndex n) (Limit oIndex e) -> Map oIndex n
forall a b. (a -> b) -> a -> b
$ Arrow (Limit oIndex n) (Limit oIndex e)
e) Map oIndex n -> oIndex -> n
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
i, labelArrow :: Limit oIndex e
labelArrow = e -> Limit oIndex e
forall oIndex t. t -> Limit oIndex t
Projection (e -> Limit oIndex e) -> e -> Limit oIndex e
forall a b. (a -> b) -> a -> b
$ (Limit oIndex e -> Map oIndex e
forall {oIndex} {t}. Limit oIndex t -> Map oIndex t
extractProd(Limit oIndex e -> Map oIndex e)
-> (Arrow (Limit oIndex n) (Limit oIndex e) -> Limit oIndex e)
-> Arrow (Limit oIndex n) (Limit oIndex e)
-> Map oIndex e
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow (Limit oIndex n) (Limit oIndex e) -> Limit oIndex e
forall n e. Arrow n e -> e
labelArrow (Arrow (Limit oIndex n) (Limit oIndex e) -> Map oIndex e)
-> Arrow (Limit oIndex n) (Limit oIndex e) -> Map oIndex e
forall a b. (a -> b) -> a -> b
$ Arrow (Limit oIndex n) (Limit oIndex e)
e) Map oIndex e -> oIndex -> e
forall k v. Eq k => Map k v -> k -> v
|!| oIndex
i}) | Arrow (Limit oIndex n) (Limit oIndex e)
e <- Graph (Limit oIndex n) (Limit oIndex e)
-> Set (Arrow (Limit oIndex n) (Limit oIndex e))
forall n e. Graph n e -> Set (Arrow n e)
edges Graph (Limit oIndex n) (Limit oIndex e)
productGraph]}
                extractProd :: Limit oIndex t -> Map oIndex t
extractProd (ProductElement Map oIndex t
x) = Map oIndex t
x
    
    instance (Eq n, Eq e) => HasEqualizers (FinGrph n e) (GraphHomomorphism n e) (Graph n e) where
        equalize :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Cone
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
equalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag = Graph n e
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Cone
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone Graph n e
equalizedGraph NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
nat
            where
                equalizedGraph :: Graph n e
equalizedGraph = Graph{nodes :: Set n
nodes = (n -> Bool) -> Set n -> Set n
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\n
n -> (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelF)) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelG)) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
n)  (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelOb -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA)), edges :: Set (Arrow n e)
edges = (Arrow n e -> Bool) -> Set (Arrow n e) -> Set (Arrow n e)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow n e
e -> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelF)) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
e Arrow n e -> Arrow n e -> Bool
forall a. Eq a => a -> a -> Bool
== (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelG)) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
e)  (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelOb -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA))}
                mappingNode :: p -> Map n n
mappingNode p
i = (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 (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
equalizedGraph)
                mappingEdge :: p -> Map (Arrow n e) (Arrow n e)
mappingEdge p
i = (Arrow n e -> Arrow n e)
-> Set (Arrow n e) -> Map (Arrow n e) (Arrow n e)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Arrow n e -> Arrow n e
forall a. a -> a
id (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
equalizedGraph)
                constDiag :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
constDiag = Parallel
-> FinGrph n e
-> Graph n e
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph 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 FinGrph n e
forall n e. FinGrph n e
FinGrph Graph n e
equalizedGraph
                nat :: NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
nat = (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Map ParallelOb (GraphHomomorphism n e)
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
constDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag (AssociationList ParallelOb (GraphHomomorphism n e)
-> Map ParallelOb (GraphHomomorphism n e)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA,GraphHomomorphism n e
legA), (ParallelOb
ParallelB, (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelF) GraphHomomorphism n e
-> GraphHomomorphism n e -> GraphHomomorphism n e
forall m o. Morphism m o => m -> m -> m
@ GraphHomomorphism n e
legA) ]))
                legA :: GraphHomomorphism n e
legA = GraphHomomorphism {nodeMap :: Map n n
nodeMap=ParallelOb -> Map n n
forall {p}. p -> Map n n
mappingNode ParallelOb
ParallelA, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = ParallelOb -> Map (Arrow n e) (Arrow n e)
forall {p}. p -> Map (Arrow n e) (Arrow n e)
mappingEdge ParallelOb
ParallelA, targetGraph :: Graph n e
targetGraph = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelOb -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA}
                
    instance (Eq n, Eq e, Eq mIndex, Eq oIndex) => CompleteCategory (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Limit oIndex n) (Limit oIndex e)) (GraphHomomorphism (Limit oIndex n) (Limit oIndex e)) (Graph (Limit oIndex n) (Limit oIndex e)) cIndex mIndex oIndex where
        limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Cone
     cIndex
     mIndex
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit oIndex e))
limit = (GraphHomomorphism n e
 -> GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
-> Diagram
     cIndex
     mIndex
     oIndex
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Cone
     cIndex
     mIndex
     oIndex
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit 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, Eq cLim, Eq mLim, Eq oLim,
 HasProducts c m o cLim mLim oLim oIndex,
 HasEqualizers 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
-> Cone cIndex mIndex oIndex cLim mLim oLim
limitFromProductsAndEqualizers GraphHomomorphism n e
-> GraphHomomorphism (Limit oIndex n) (Limit oIndex e)
forall {k1} {t} {oIndex} {oIndex}.
GraphHomomorphism k1 t
-> GraphHomomorphism (Limit oIndex k1) (Limit oIndex t)
projectGraphHomomorphism
            where
                projectArrow :: Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
a = Arrow{sourceArrow :: Limit oIndex n
sourceArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex 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 :: Limit oIndex n
targetArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex 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 :: Limit oIndex t
labelArrow = t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection (t -> Limit oIndex t) -> t -> Limit oIndex t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                projectGraph :: Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph Graph a t
g = Graph{nodes :: Set (Limit oIndex a)
nodes = a -> Limit oIndex a
forall oIndex t. t -> Limit oIndex t
Projection (a -> Limit oIndex a) -> Set a -> Set (Limit oIndex 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, edges :: Set (Arrow (Limit oIndex a) (Limit oIndex t))
edges = Arrow a t -> Arrow (Limit oIndex a) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow (Arrow a t -> Arrow (Limit oIndex a) (Limit oIndex t))
-> Set (Arrow a t) -> Set (Arrow (Limit oIndex a) (Limit oIndex 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}
                projectGraphHomomorphism :: GraphHomomorphism k1 t
-> GraphHomomorphism (Limit oIndex k1) (Limit oIndex t)
projectGraphHomomorphism GraphHomomorphism k1 t
gh = GraphHomomorphism{nodeMap :: Map (Limit oIndex k1) (Limit oIndex k1)
nodeMap = (k1, k1) -> (Limit oIndex k1, Limit oIndex k1)
forall {t} {t} {oIndex} {oIndex}.
(t, t) -> (Limit oIndex t, Limit oIndex t)
doubleProject ((k1, k1) -> (Limit oIndex k1, Limit oIndex k1))
-> Map k1 k1 -> Map (Limit oIndex k1) (Limit oIndex k1)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism k1 t -> Map k1 k1
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism k1 t
gh, edgeMap :: Map
  (Arrow (Limit oIndex k1) (Limit oIndex t))
  (Arrow (Limit oIndex k1) (Limit oIndex t))
edgeMap = (Arrow k1 t, Arrow k1 t)
-> (Arrow (Limit oIndex k1) (Limit oIndex t),
    Arrow (Limit oIndex k1) (Limit oIndex t))
forall {n} {t} {n} {t} {oIndex} {oIndex} {oIndex} {oIndex}.
(Arrow n t, Arrow n t)
-> (Arrow (Limit oIndex n) (Limit oIndex t),
    Arrow (Limit oIndex n) (Limit oIndex t))
doubleProjectArrow ((Arrow k1 t, Arrow k1 t)
 -> (Arrow (Limit oIndex k1) (Limit oIndex t),
     Arrow (Limit oIndex k1) (Limit oIndex t)))
-> Map (Arrow k1 t) (Arrow k1 t)
-> Map
     (Arrow (Limit oIndex k1) (Limit oIndex t))
     (Arrow (Limit oIndex k1) (Limit oIndex t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism k1 t -> Map (Arrow k1 t) (Arrow k1 t)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism k1 t
gh, targetGraph :: Graph (Limit oIndex k1) (Limit oIndex t)
targetGraph = Graph k1 t -> Graph (Limit oIndex k1) (Limit oIndex t)
forall {a} {t} {oIndex} {oIndex}.
Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph (Graph k1 t -> Graph (Limit oIndex k1) (Limit oIndex t))
-> Graph k1 t -> Graph (Limit oIndex k1) (Limit oIndex t)
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism k1 t -> Graph k1 t
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph GraphHomomorphism k1 t
gh}
                doubleProject :: (t, t) -> (Limit oIndex t, Limit oIndex t)
doubleProject (t
x,t
y) = (t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
x, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
y)
                doubleProjectArrow :: (Arrow n t, Arrow n t)
-> (Arrow (Limit oIndex n) (Limit oIndex t),
    Arrow (Limit oIndex n) (Limit oIndex t))
doubleProjectArrow (Arrow n t
x,Arrow n t
y) = (Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
x, Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
y)
                
        projectBase :: Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Diagram
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
     (FinGrph (Limit oIndex n) (Limit oIndex e))
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
     (Graph (Limit oIndex n) (Limit oIndex e))
projectBase Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
diag = Diagram{src :: FinGrph n e
src = FinGrph n e
forall n e. FinGrph n e
FinGrph, tgt :: FinGrph (Limit oIndex n) (Limit oIndex e)
tgt = FinGrph (Limit oIndex n) (Limit oIndex e)
forall n e. FinGrph n e
FinGrph, omap :: Map (Graph n e) (Graph (Limit oIndex n) (Limit oIndex e))
omap = (Graph n e -> Graph (Limit oIndex n) (Limit oIndex e))
-> Set (Graph n e)
-> Map (Graph n e) (Graph (Limit oIndex n) (Limit oIndex e))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Graph n e -> Graph (Limit oIndex n) (Limit oIndex e)
forall {a} {t} {oIndex} {oIndex}.
Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph (Map oIndex (Graph n e) -> Set (Graph n e)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map oIndex (Graph n e)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
diag)), mmap :: Map
  (GraphHomomorphism n e)
  (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
mmap = (GraphHomomorphism n e
 -> GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
-> Set (GraphHomomorphism n e)
-> Map
     (GraphHomomorphism n e)
     (GraphHomomorphism (Limit oIndex n) (Limit oIndex e))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction GraphHomomorphism n e
-> GraphHomomorphism (Limit oIndex n) (Limit oIndex e)
forall {k1} {t} {oIndex} {oIndex}.
GraphHomomorphism k1 t
-> GraphHomomorphism (Limit oIndex k1) (Limit oIndex t)
projectGraphHomomorphism (Map mIndex (GraphHomomorphism n e) -> Set (GraphHomomorphism n e)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map mIndex (GraphHomomorphism n e)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
diag))}
            where
                projectArrow :: Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
a = Arrow{sourceArrow :: Limit oIndex n
sourceArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex 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 :: Limit oIndex n
targetArrow = n -> Limit oIndex n
forall oIndex t. t -> Limit oIndex t
Projection (n -> Limit oIndex n) -> n -> Limit oIndex 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 :: Limit oIndex t
labelArrow = t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection (t -> Limit oIndex t) -> t -> Limit oIndex t
forall a b. (a -> b) -> a -> b
$ Arrow n t -> t
forall n e. Arrow n e -> e
labelArrow Arrow n t
a}
                projectGraph :: Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph Graph a t
g = Graph{nodes :: Set (Limit oIndex a)
nodes = a -> Limit oIndex a
forall oIndex t. t -> Limit oIndex t
Projection (a -> Limit oIndex a) -> Set a -> Set (Limit oIndex 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, edges :: Set (Arrow (Limit oIndex a) (Limit oIndex t))
edges = Arrow a t -> Arrow (Limit oIndex a) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow (Arrow a t -> Arrow (Limit oIndex a) (Limit oIndex t))
-> Set (Arrow a t) -> Set (Arrow (Limit oIndex a) (Limit oIndex 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}
                projectGraphHomomorphism :: GraphHomomorphism k1 t
-> GraphHomomorphism (Limit oIndex k1) (Limit oIndex t)
projectGraphHomomorphism GraphHomomorphism k1 t
gh = GraphHomomorphism{nodeMap :: Map (Limit oIndex k1) (Limit oIndex k1)
nodeMap = (k1, k1) -> (Limit oIndex k1, Limit oIndex k1)
forall {t} {t} {oIndex} {oIndex}.
(t, t) -> (Limit oIndex t, Limit oIndex t)
doubleProject ((k1, k1) -> (Limit oIndex k1, Limit oIndex k1))
-> Map k1 k1 -> Map (Limit oIndex k1) (Limit oIndex k1)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism k1 t -> Map k1 k1
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism k1 t
gh, edgeMap :: Map
  (Arrow (Limit oIndex k1) (Limit oIndex t))
  (Arrow (Limit oIndex k1) (Limit oIndex t))
edgeMap = (Arrow k1 t, Arrow k1 t)
-> (Arrow (Limit oIndex k1) (Limit oIndex t),
    Arrow (Limit oIndex k1) (Limit oIndex t))
forall {n} {t} {n} {t} {oIndex} {oIndex} {oIndex} {oIndex}.
(Arrow n t, Arrow n t)
-> (Arrow (Limit oIndex n) (Limit oIndex t),
    Arrow (Limit oIndex n) (Limit oIndex t))
doubleProjectArrow ((Arrow k1 t, Arrow k1 t)
 -> (Arrow (Limit oIndex k1) (Limit oIndex t),
     Arrow (Limit oIndex k1) (Limit oIndex t)))
-> Map (Arrow k1 t) (Arrow k1 t)
-> Map
     (Arrow (Limit oIndex k1) (Limit oIndex t))
     (Arrow (Limit oIndex k1) (Limit oIndex t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism k1 t -> Map (Arrow k1 t) (Arrow k1 t)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism k1 t
gh, targetGraph :: Graph (Limit oIndex k1) (Limit oIndex t)
targetGraph = Graph k1 t -> Graph (Limit oIndex k1) (Limit oIndex t)
forall {a} {t} {oIndex} {oIndex}.
Graph a t -> Graph (Limit oIndex a) (Limit oIndex t)
projectGraph (Graph k1 t -> Graph (Limit oIndex k1) (Limit oIndex t))
-> Graph k1 t -> Graph (Limit oIndex k1) (Limit oIndex t)
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism k1 t -> Graph k1 t
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph GraphHomomorphism k1 t
gh}
                doubleProject :: (t, t) -> (Limit oIndex t, Limit oIndex t)
doubleProject (t
x,t
y) = (t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
x, t -> Limit oIndex t
forall oIndex t. t -> Limit oIndex t
Projection t
y)
                doubleProjectArrow :: (Arrow n t, Arrow n t)
-> (Arrow (Limit oIndex n) (Limit oIndex t),
    Arrow (Limit oIndex n) (Limit oIndex t))
doubleProjectArrow (Arrow n t
x,Arrow n t
y) = (Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
x, Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
forall {n} {t} {oIndex} {oIndex}.
Arrow n t -> Arrow (Limit oIndex n) (Limit oIndex t)
projectArrow Arrow n t
y)
                
    instance (Eq n, Eq e, Eq oIndex) => HasCoproducts (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Colimit oIndex n) (Colimit oIndex e)) (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)) (Graph (Colimit oIndex n) (Colimit oIndex e)) oIndex where
        coproduct :: 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))
coproduct Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag = 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))
result
            where
                indexingCat :: DiscreteCategory oIndex
indexingCat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag
                coprod :: Graph (Colimit oIndex n) (Colimit oIndex e)
coprod = Graph{nodes :: Set (Colimit oIndex n)
nodes = [Set (Colimit oIndex n)] -> Set (Colimit oIndex n)
forall (f :: * -> *) a. Foldable f => f (Set a) -> Set a
Set.unions (Set (Set (Colimit oIndex n)) -> [Set (Colimit oIndex n)]
forall a. Eq a => Set a -> [a]
setToList [oIndex -> n -> Colimit oIndex n
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i (n -> Colimit oIndex n) -> Set n -> Set (Colimit oIndex n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> oIndex -> Graph 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
indexingCat]), edges :: Set (Arrow (Colimit oIndex n) (Colimit oIndex e))
edges = [Set (Arrow (Colimit oIndex n) (Colimit oIndex e))]
-> Set (Arrow (Colimit oIndex n) (Colimit oIndex e))
forall (f :: * -> *) a. Foldable f => f (Set a) -> Set a
Set.unions (Set (Set (Arrow (Colimit oIndex n) (Colimit oIndex e)))
-> [Set (Arrow (Colimit oIndex n) (Colimit oIndex e))]
forall a. Eq a => Set a -> [a]
setToList [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)
coproductArrow oIndex
i (Arrow n e -> Arrow (Colimit oIndex n) (Colimit oIndex e))
-> Set (Arrow n e)
-> Set (Arrow (Colimit oIndex n) (Colimit oIndex e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> oIndex -> Graph 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
indexingCat])}
                coproductArrow :: i -> Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coproductArrow 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)}
                constDiag :: Diagram
  (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))
constDiag = DiscreteCategory oIndex
-> FinGrph (Colimit oIndex n) (Colimit oIndex e)
-> Graph (Colimit oIndex n) (Colimit oIndex e)
-> Diagram
     (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.
(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
indexingCat FinGrph (Colimit oIndex n) (Colimit oIndex e)
forall n e. FinGrph n e
FinGrph Graph (Colimit oIndex n) (Colimit oIndex e)
coprod
                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}
                transformGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
transformGraph Graph a t
g = Graph{nodes :: Set (Colimit i a)
nodes = 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, edges :: Set (Arrow (Colimit i a) (Colimit i t))
edges = 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}
                transformGH :: GraphHomomorphism t t
-> GraphHomomorphism (Colimit i t) (Colimit i t)
transformGH GraphHomomorphism{nodeMap :: forall n e. GraphHomomorphism n e -> Map n n
nodeMap = Map t t
nm, edgeMap :: forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap = Map (Arrow t t) (Arrow t t)
em, targetGraph :: forall n e. GraphHomomorphism n e -> Graph n e
targetGraph = Graph t t
tg} = GraphHomomorphism{nodeMap :: Map (Colimit i t) (Colimit i t)
nodeMap = Set (Colimit i t, Colimit i t) -> Map (Colimit i t) (Colimit i t)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
k, t -> Colimit i t
forall i t. t -> Colimit i t
Coprojection t
v) | (t
k,t
v) <- Map t t -> Set (t, t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map t t
nm], edgeMap :: Map
  (Arrow (Colimit i t) (Colimit i t))
  (Arrow (Colimit i t) (Colimit i t))
edgeMap = Set
  (Arrow (Colimit i t) (Colimit i t),
   Arrow (Colimit i t) (Colimit i t))
-> Map
     (Arrow (Colimit i t) (Colimit i t))
     (Arrow (Colimit i t) (Colimit i t))
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(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
k, 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
v) | (Arrow t t
k,Arrow t t
v) <- Map (Arrow t t) (Arrow t t) -> Set (Arrow t t, Arrow t t)
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet Map (Arrow t t) (Arrow t t)
em], targetGraph :: Graph (Colimit i t) (Colimit i t)
targetGraph = Graph t t -> Graph (Colimit i t) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
transformGraph Graph t t
tg}
                newDiag :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism (Colimit i n) (Colimit i e))
  (Graph (Colimit i n) (Colimit i e))
newDiag = Diagram{src :: DiscreteCategory oIndex
src = DiscreteCategory oIndex
indexingCat, tgt :: FinGrph n e
tgt = FinGrph n e
forall n e. FinGrph n e
FinGrph, omap :: Map oIndex (Graph (Colimit i n) (Colimit i e))
omap = Graph n e -> Graph (Colimit i n) (Colimit i e)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
transformGraph (Graph n e -> Graph (Colimit i n) (Colimit i e))
-> Map oIndex (Graph n e)
-> Map oIndex (Graph (Colimit i n) (Colimit i e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map oIndex (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag), mmap :: Map
  (DiscreteMorphism oIndex)
  (GraphHomomorphism (Colimit i n) (Colimit i e))
mmap = GraphHomomorphism n e
-> GraphHomomorphism (Colimit i n) (Colimit i e)
forall {t} {t} {i} {i}.
(Eq t, Eq t) =>
GraphHomomorphism t t
-> GraphHomomorphism (Colimit i t) (Colimit i t)
transformGH (GraphHomomorphism n e
 -> GraphHomomorphism (Colimit i n) (Colimit i e))
-> Map (DiscreteMorphism oIndex) (GraphHomomorphism n e)
-> Map
     (DiscreteMorphism oIndex)
     (GraphHomomorphism (Colimit i n) (Colimit i e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map (DiscreteMorphism oIndex) (GraphHomomorphism n e)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
discreteDiag)}
                mapping :: oIndex -> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
mapping oIndex
i = GraphHomomorphism{nodeMap :: Map (Colimit oIndex n) (Colimit oIndex n)
nodeMap = (Colimit oIndex n -> Colimit oIndex n)
-> Set (Colimit oIndex n)
-> Map (Colimit oIndex n) (Colimit oIndex n)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\(Coprojection n
x) -> oIndex -> n -> Colimit oIndex n
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i n
x) (Graph (Colimit oIndex n) (Colimit Any e) -> Set (Colimit oIndex n)
forall n e. Graph n e -> Set n
nodes (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph Any Any)
  (GraphHomomorphism (Colimit Any n) (Colimit Any e))
  (Graph (Colimit oIndex n) (Colimit Any e))
forall {n} {e} {i} {i} {i} {i}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism (Colimit i n) (Colimit i e))
  (Graph (Colimit i n) (Colimit i e))
newDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph Any Any)
  (GraphHomomorphism (Colimit Any n) (Colimit Any e))
  (Graph (Colimit oIndex n) (Colimit Any e))
-> oIndex -> Graph (Colimit oIndex n) (Colimit Any e)
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i)), edgeMap :: Map
  (Arrow (Colimit oIndex n) (Colimit oIndex e))
  (Arrow (Colimit oIndex n) (Colimit oIndex e))
edgeMap = (Arrow (Colimit oIndex n) (Colimit oIndex e)
 -> Arrow (Colimit oIndex n) (Colimit oIndex e))
-> Set (Arrow (Colimit oIndex n) (Colimit oIndex e))
-> Map
     (Arrow (Colimit oIndex n) (Colimit oIndex e))
     (Arrow (Colimit oIndex n) (Colimit oIndex e))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\Arrow{sourceArrow :: forall n e. Arrow n e -> n
sourceArrow = Coprojection n
s, targetArrow :: forall n e. Arrow n e -> n
targetArrow = Coprojection n
t, labelArrow :: forall n e. Arrow n e -> e
labelArrow = Coprojection e
l} -> Arrow{sourceArrow :: Colimit oIndex n
sourceArrow = oIndex -> n -> Colimit oIndex n
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i n
s, targetArrow :: Colimit oIndex n
targetArrow = oIndex -> n -> Colimit oIndex n
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i n
t, labelArrow :: Colimit oIndex e
labelArrow = oIndex -> e -> Colimit oIndex e
forall i t. i -> t -> Colimit i t
CoproductElement oIndex
i e
l}) (Graph (Colimit oIndex n) (Colimit oIndex e)
-> Set (Arrow (Colimit oIndex n) (Colimit oIndex e))
forall n e. Graph n e -> Set (Arrow n e)
edges (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph Any Any)
  (GraphHomomorphism (Colimit Any n) (Colimit Any e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
forall {n} {e} {i} {i} {i} {i}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism (Colimit i n) (Colimit i e))
  (Graph (Colimit i n) (Colimit i e))
newDiag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph Any Any)
  (GraphHomomorphism (Colimit Any n) (Colimit Any e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
-> oIndex -> Graph (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)), targetGraph :: Graph (Colimit oIndex n) (Colimit oIndex e)
targetGraph = Graph (Colimit oIndex n) (Colimit oIndex e)
coprod}
                result :: 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))
result = 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))
-> 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 o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone Graph (Colimit oIndex n) (Colimit oIndex e)
coprod (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))
 -> 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))
-> 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 a b. (a -> b) -> a -> b
$ Diagram
  (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))
-> Diagram
     (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))
-> Map
     oIndex (GraphHomomorphism (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.
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
  (FinGrph (Colimit oIndex n) (Colimit oIndex e))
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
  (Graph (Colimit oIndex n) (Colimit oIndex e))
forall {n} {e} {i} {i} {i} {i}.
Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (FinGrph n e)
  (GraphHomomorphism (Colimit i n) (Colimit i e))
  (Graph (Colimit i n) (Colimit i e))
newDiag Diagram
  (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))
constDiag ((oIndex -> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
-> Set oIndex
-> Map
     oIndex (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction oIndex -> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
mapping (DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob DiscreteCategory oIndex
indexingCat))
                
    -- | BEWARE, for the coequalizer to be correct, ALL arrow labels should be different (two arrows with different source and target might have the same source and target after the coequalization process).

    instance (Eq e, Eq n) => HasCoequalizers (FinGrph n e) (GraphHomomorphism n e) (Graph n e) where
        coequalize :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
coequalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag = Cocone
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
result
            where
                glueEdge :: Arrow n e -> GraphHomomorphism n e -> GraphHomomorphism n e
glueEdge Arrow n e
edge GraphHomomorphism n e
gh
                    | Arrow n e
imageEdgeByF Arrow n e -> Arrow n e -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow n e
imageEdgeByG = GraphHomomorphism n e
gh
                    | Bool
otherwise = GraphHomomorphism{nodeMap :: Map n n
nodeMap = GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = (Arrow n e -> Arrow n e)
-> Arrow n e
-> Map (Arrow n e) (Arrow n e)
-> Map (Arrow n e) (Arrow n e)
forall k a. Eq k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (Arrow n e -> Arrow n e -> Arrow n e
forall a b. a -> b -> a
const (Arrow n e -> Arrow n e -> Arrow n e)
-> Arrow n e -> Arrow n e -> Arrow n e
forall a b. (a -> b) -> a -> b
$ Arrow n e
imageEdgeByG) Arrow n e
imageEdgeByF (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh), targetGraph :: Graph n e
targetGraph = Graph n e
newGraph}
                    where
                        imageEdgeByF :: Arrow n e
imageEdgeByF = (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelF)) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
edge
                        imageEdgeByG :: Arrow n e
imageEdgeByG = (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelG)) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
edge
                        newGraph :: Graph n e
newGraph = Graph{nodes :: Set n
nodes = Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes (GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh), edges :: Set (Arrow n e)
edges = Arrow n e -> Set (Arrow n e) -> Set (Arrow n e)
forall a. Eq a => a -> Set a -> Set a
Set.delete Arrow n e
imageEdgeByF (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges (GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh))}
                glueNode :: n -> GraphHomomorphism n e -> GraphHomomorphism n e
glueNode n
node GraphHomomorphism n e
gh
                    | n
imageNodeByF n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
imageNodeByG = GraphHomomorphism n e
gh
                    | Bool
otherwise = GraphHomomorphism{nodeMap :: Map n n
nodeMap = (n -> n) -> n -> Map n n -> Map n n
forall k a. Eq k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (n -> n -> n
forall a b. a -> b -> a
const (n -> n -> n) -> n -> n -> n
forall a b. (a -> b) -> a -> b
$ n
imageNodeByG) n
imageNodeByF (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh), edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = Arrow n e -> Arrow n e
forall {e}. Arrow n e -> Arrow n e
updateArrow (Arrow n e -> Arrow n e)
-> Map (Arrow n e) (Arrow n e) -> Map (Arrow n e) (Arrow n e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh, targetGraph :: Graph n e
targetGraph = Graph n e
newGraph}
                    where
                        imageNodeByF :: n
imageNodeByF = (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelF)) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
node
                        imageNodeByG :: n
imageNodeByG = (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelG)) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
node
                        updateNode :: n -> n
updateNode n
n = if n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
imageNodeByF then n
imageNodeByG else n
n
                        updateArrow :: Arrow n e -> Arrow n e
updateArrow Arrow n e
a = Arrow{sourceArrow :: n
sourceArrow = n -> n
updateNode (Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a), targetArrow :: n
targetArrow = n -> n
updateNode (Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a), labelArrow :: e
labelArrow = Arrow n e -> e
forall n e. Arrow n e -> e
labelArrow Arrow n e
a}
                        newGraph :: Graph n e
newGraph = Graph{nodes :: Set n
nodes = n -> Set n -> Set n
forall a. Eq a => a -> Set a -> Set a
Set.delete n
imageNodeByF (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes (GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh)), edges :: Set (Arrow n e)
edges = Arrow n e -> Arrow n e
forall {e}. Arrow n e -> Arrow n e
updateArrow (Arrow n e -> Arrow n e) -> Set (Arrow n e) -> Set (Arrow n e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges (GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh)}
                gh1 :: GraphHomomorphism n e
gh1 = (Arrow n e -> GraphHomomorphism n e -> GraphHomomorphism n e)
-> GraphHomomorphism n e
-> Set (Arrow n e)
-> GraphHomomorphism n e
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr Arrow n e -> GraphHomomorphism n e -> GraphHomomorphism n e
glueEdge (FinGrph n e -> Graph n e -> GraphHomomorphism n e
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinGrph n e
forall n e. FinGrph n e
FinGrph (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelOb -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB)) (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelOb -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA))
                gh2 :: GraphHomomorphism n e
gh2 = (n -> GraphHomomorphism n e -> GraphHomomorphism n e)
-> GraphHomomorphism n e -> Set n -> GraphHomomorphism n e
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr n -> GraphHomomorphism n e -> GraphHomomorphism n e
forall {e}.
Eq e =>
n -> GraphHomomorphism n e -> GraphHomomorphism n e
glueNode GraphHomomorphism n e
gh1 (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelOb -> Graph n e
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA))
                constDiag :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
constDiag = Parallel
-> FinGrph n e
-> Graph n e
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph 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 FinGrph n e
forall n e. FinGrph n e
FinGrph (GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh2)
                result :: Cocone
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
result = Graph n e
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph 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 (GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh2) (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Map ParallelOb (GraphHomomorphism n e)
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph 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
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
constDiag (AssociationList ParallelOb (GraphHomomorphism n e)
-> Map ParallelOb (GraphHomomorphism n e)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA,GraphHomomorphism n e
gh2 GraphHomomorphism n e
-> GraphHomomorphism n e -> GraphHomomorphism n e
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> ParallelAr -> GraphHomomorphism 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
->£ ParallelAr
ParallelF)), (ParallelOb
ParallelB, GraphHomomorphism n e
gh2) ]))
        
    instance (Eq e, Eq n, Eq mIndex, Eq oIndex) => CocompleteCategory (FinGrph n e) (GraphHomomorphism n e) (Graph n e) (FinGrph (Colimit oIndex n) (Colimit oIndex e)) (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)) (Graph (Colimit oIndex n) (Colimit oIndex e)) cIndex mIndex oIndex where
        colimit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Cocone
     cIndex
     mIndex
     oIndex
     (FinGrph (Colimit oIndex n) (Colimit oIndex e))
     (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
     (Graph (Colimit oIndex n) (Colimit oIndex e))
colimit = (GraphHomomorphism n e
 -> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
-> Diagram
     cIndex
     mIndex
     oIndex
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
-> Cocone
     cIndex
     mIndex
     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 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 GraphHomomorphism n e
-> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
forall {v1} {t} {i} {i}.
GraphHomomorphism v1 t
-> GraphHomomorphism (Colimit i v1) (Colimit i t)
transformGHToColimGH
            where
                transformGHToColimGH :: GraphHomomorphism v1 t
-> GraphHomomorphism (Colimit i v1) (Colimit i t)
transformGHToColimGH GraphHomomorphism v1 t
gh = GraphHomomorphism{nodeMap :: Map (Colimit i v1) (Colimit i v1)
nodeMap = (v1 -> Colimit i v1) -> (v1, v1) -> (Colimit i v1, Colimit i v1)
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
both v1 -> Colimit i v1
forall i t. t -> Colimit i t
Coprojection ((v1, v1) -> (Colimit i v1, Colimit i v1))
-> Map v1 v1 -> Map (Colimit i v1) (Colimit i v1)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism v1 t -> Map v1 v1
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism v1 t
gh, edgeMap :: Map
  (Arrow (Colimit i v1) (Colimit i t))
  (Arrow (Colimit i v1) (Colimit i t))
edgeMap = (Arrow v1 t -> Arrow (Colimit i v1) (Colimit i t))
-> (Arrow v1 t, Arrow v1 t)
-> (Arrow (Colimit i v1) (Colimit i t),
    Arrow (Colimit i v1) (Colimit i t))
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
both Arrow v1 t -> Arrow (Colimit i v1) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow ((Arrow v1 t, Arrow v1 t)
 -> (Arrow (Colimit i v1) (Colimit i t),
     Arrow (Colimit i v1) (Colimit i t)))
-> Map (Arrow v1 t) (Arrow v1 t)
-> Map
     (Arrow (Colimit i v1) (Colimit i t))
     (Arrow (Colimit i v1) (Colimit i t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism v1 t -> Map (Arrow v1 t) (Arrow v1 t)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism v1 t
gh, targetGraph :: Graph (Colimit i v1) (Colimit i t)
targetGraph = Graph v1 t -> Graph (Colimit i v1) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectTargetGraph (GraphHomomorphism v1 t -> Graph v1 t
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph GraphHomomorphism v1 t
gh)}
                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}
                both :: (t -> b) -> (t, t) -> (b, b)
both t -> b
f (t
x,t
y) = (t -> b
f t
x,t -> b
f t
y)
                coprojectTargetGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectTargetGraph Graph a t
g = Graph{nodes :: Set (Colimit i a)
nodes = 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, edges :: Set (Arrow (Colimit i a) (Colimit i t))
edges = 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}
        
        coprojectBase :: Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Diagram
     (FinGrph n e)
     (GraphHomomorphism n e)
     (Graph n e)
     (FinGrph (Colimit oIndex n) (Colimit oIndex e))
     (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
     (Graph (Colimit oIndex n) (Colimit oIndex e))
coprojectBase Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
diag = Diagram{src :: FinGrph n e
src = FinGrph n e
forall n e. FinGrph n e
FinGrph, tgt :: FinGrph (Colimit oIndex n) (Colimit oIndex e)
tgt = FinGrph (Colimit oIndex n) (Colimit oIndex e)
forall n e. FinGrph n e
FinGrph, omap :: Map (Graph n e) (Graph (Colimit oIndex n) (Colimit oIndex e))
omap = (Graph n e -> Graph (Colimit oIndex n) (Colimit oIndex e))
-> Set (Graph n e)
-> Map (Graph n e) (Graph (Colimit oIndex n) (Colimit oIndex e))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction Graph n e -> Graph (Colimit oIndex n) (Colimit oIndex e)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (Map oIndex (Graph n e) -> Set (Graph n e)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map oIndex (Graph n e)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
diag)), mmap :: Map
  (GraphHomomorphism n e)
  (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
mmap = (GraphHomomorphism n e
 -> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
-> Set (GraphHomomorphism n e)
-> Map
     (GraphHomomorphism n e)
     (GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction GraphHomomorphism n e
-> GraphHomomorphism (Colimit oIndex n) (Colimit oIndex e)
forall {v1} {t} {i} {i}.
GraphHomomorphism v1 t
-> GraphHomomorphism (Colimit i v1) (Colimit i t)
transformGHToColimGH (Map mIndex (GraphHomomorphism n e) -> Set (GraphHomomorphism n e)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
-> Map mIndex (GraphHomomorphism n e)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  cIndex
  mIndex
  oIndex
  (FinGrph n e)
  (GraphHomomorphism n e)
  (Graph n e)
diag))}
            where
                transformGHToColimGH :: GraphHomomorphism v1 t
-> GraphHomomorphism (Colimit i v1) (Colimit i t)
transformGHToColimGH GraphHomomorphism v1 t
gh = GraphHomomorphism{nodeMap :: Map (Colimit i v1) (Colimit i v1)
nodeMap = (v1 -> Colimit i v1) -> (v1, v1) -> (Colimit i v1, Colimit i v1)
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
both v1 -> Colimit i v1
forall i t. t -> Colimit i t
Coprojection ((v1, v1) -> (Colimit i v1, Colimit i v1))
-> Map v1 v1 -> Map (Colimit i v1) (Colimit i v1)
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism v1 t -> Map v1 v1
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism v1 t
gh, edgeMap :: Map
  (Arrow (Colimit i v1) (Colimit i t))
  (Arrow (Colimit i v1) (Colimit i t))
edgeMap = (Arrow v1 t -> Arrow (Colimit i v1) (Colimit i t))
-> (Arrow v1 t, Arrow v1 t)
-> (Arrow (Colimit i v1) (Colimit i t),
    Arrow (Colimit i v1) (Colimit i t))
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
both Arrow v1 t -> Arrow (Colimit i v1) (Colimit i t)
forall {n} {t} {i} {i}.
Arrow n t -> Arrow (Colimit i n) (Colimit i t)
coprojectArrow ((Arrow v1 t, Arrow v1 t)
 -> (Arrow (Colimit i v1) (Colimit i t),
     Arrow (Colimit i v1) (Colimit i t)))
-> Map (Arrow v1 t) (Arrow v1 t)
-> Map
     (Arrow (Colimit i v1) (Colimit i t))
     (Arrow (Colimit i v1) (Colimit i t))
forall k1 v1 k2 v2.
((k1, v1) -> (k2, v2)) -> Map k1 v1 -> Map k2 v2
<|$|> GraphHomomorphism v1 t -> Map (Arrow v1 t) (Arrow v1 t)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism v1 t
gh, targetGraph :: Graph (Colimit i v1) (Colimit i t)
targetGraph = Graph v1 t -> Graph (Colimit i v1) (Colimit i t)
forall {a} {t} {i} {i}.
Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph (GraphHomomorphism v1 t -> Graph v1 t
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph GraphHomomorphism v1 t
gh)}
                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}
                both :: (t -> b) -> (t, t) -> (b, b)
both t -> b
f (t
x,t
y) = (t -> b
f t
x,t -> b
f t
y)
                coprojectGraph :: Graph a t -> Graph (Colimit i a) (Colimit i t)
coprojectGraph Graph a t
g = Graph{nodes :: Set (Colimit i a)
nodes = 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, edges :: Set (Arrow (Colimit i a) (Colimit i t))
edges = 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}
        
        
        
        
        
        
        
        
        
        
    -- | Return the underlying graph of a 'FiniteCategory'.

    underlyingGraph :: (FiniteCategory c m o, Morphism m o) => c -> Graph o m
    underlyingGraph :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Graph o m
underlyingGraph c
c = Graph{
                                nodes :: Set o
nodes = c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c,
                                edges :: Set (Arrow o m)
edges = (\m
m -> Arrow{sourceArrow :: o
sourceArrow=m -> o
forall m o. Morphism m o => m -> o
source m
m, targetArrow :: o
targetArrow=m -> o
forall m o. Morphism m o => m -> o
target m
m, labelArrow :: m
labelArrow=m
m}) (m -> Arrow o m) -> Set m -> Set (Arrow o m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c
                            }
                            
    -- | Return the underlying graph of a 'FiniteCategory' and apply formatting functions on objects and arrows.

    underlyingGraphFormat :: (FiniteCategory c m o, Morphism m o) => (o -> a) -> (m -> b) -> c -> Graph a b
    underlyingGraphFormat :: forall c m o a b.
(FiniteCategory c m o, Morphism m o) =>
(o -> a) -> (m -> b) -> c -> Graph a b
underlyingGraphFormat o -> a
formatObj m -> b
formatAr c
c = Graph{
                                                        nodes :: Set a
nodes = o -> a
formatObj (o -> a) -> Set o -> Set a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c,
                                                        edges :: Set (Arrow a b)
edges = (\m
m -> Arrow{sourceArrow :: a
sourceArrow=o -> a
formatObj(o -> a) -> (m -> o) -> m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.m -> o
forall m o. Morphism m o => m -> o
source (m -> a) -> m -> a
forall a b. (a -> b) -> a -> b
$ m
m, targetArrow :: a
targetArrow=o -> a
formatObj(o -> a) -> (m -> o) -> m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.m -> o
forall m o. Morphism m o => m -> o
target (m -> a) -> m -> a
forall a b. (a -> b) -> a -> b
$ m
m, labelArrow :: b
labelArrow=m -> b
formatAr m
m}) (m -> Arrow a b) -> Set m -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c
                                                    }