module Cat.Instances.Graphs.Exponentials where
Exponential graphsπ
The exponential objects in the category of graphs have a particularly simple description: the nodes are arbitrary functions between the node-sets, and an edge between and is given by a family of edges for each in
Graphs[_,_] : β {o β o' β'} β Graph o β β Graph o' β' β Graph (o β o') (o β β β β') Graphs[ G , H ] .Node = β G β β β H β Graphs[ G , H ] .Edge f g = β {x y} β G .Edge x y β H .Edge (f x) (g y) Graphs[ G , H ] .Node-set = hlevel 2 Graphs[ G , H ] .Edge-set = hlevel 2
Since this is basically an unpacking of the type of graph homomorphisms, it is easy to show that it satisfies the universal property of exponentials: the evaluation and currying maps are as in
Graphs-closed : β {β} β Cartesian-closed (Graphs β β) Graphs-products Graphs-terminal Graphs-closed .has-exp A B .B^A = Graphs[ A , B ] Graphs-closed .has-exp A B .ev = record where node (f , x) = f x edge (e , a) = e a Graphs-closed .has-exp A B .has-is-exp .Ζ m = record where node a b = m .node (a , b) edge a b = m .edge (a , b) Graphs-closed .has-exp A B .has-is-exp .commutes m = trivialα΄³! Graphs-closed .has-exp A B .has-is-exp .unique m' x = ext record where node a b i = x i .node (a , b) edge a i b = x i .edge (a , b)