# how to inductively define paths from paths using unimath

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.

TIA

• I don't think the mathematical description is particularly clear. Can you provide a rigorous definition (in mathematical English) first?
– Trebor
Commented Jan 23 at 5:17
• I guess you want to adapt this construction: agda.github.io/agda-stdlib/v2.0/…. Commented Jan 23 at 9:38
• Sorry, the idea is this: I have the base set of vertices, call this V, V is level 0. Level 1 is morphisms in between these vertices, so if v1,v2 are in V, level 1 has morphisms 'f, g: v1 -> v2'. Then level 2 has morphisms 'a,b : f -> g' and so on n so forth... Commented Jan 23 at 10:33