I'd like to define a type of graph where given a set of edges, we can define another graph that has everything from graph 1 but extends the set of edges by adding higher level edges to parallel edges(so like a higher dimensional category, but for graphs) using Coq. I think it needs to be an inductive type, and I'm trying to use the predefined graph constructs from UniMath yet I'm kinda confused, this is the first time I'm using Coq like this.
What I've basically mentally outlined right now
Step 1. Take a graph
Step 2. Take an n
Step 3. if n = 0, graph remains then same, if n = n' inductively add edges to the edge set
But I'd like this to be a dependent type, producing an n-graph type for a given n
I also am not sure if the graph library in Unimath has what I need to implement this, I'm still very new to it.