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)