unionWith package:Agda
Union. The function is used to combine edge labels for edges that
occur in both graphs (labels from the first graph are given as the
first argument to the function).
Time complexity: O(n₁ log (n₂n₁ + 1) + e₁ log e₂), where
n₁/ is the number of nodes in the graph with the smallest number
of nodes and n₂ is the number of nodes in the other graph, and
e₁ is the number of edges in the graph with the smallest number
of edges and e₂ is the number of edges in the other graph.
Less complicated time complexity: O((n + e) log n (where
n and e refer to the resulting graph).
Pointwise union with merge function for values.