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.


  • 1
    $\begingroup$ I don't think the mathematical description is particularly clear. Can you provide a rigorous definition (in mathematical English) first? $\endgroup$
    – Trebor
    Commented Jan 23 at 5:17
  • $\begingroup$ I guess you want to adapt this construction: agda.github.io/agda-stdlib/v2.0/…. $\endgroup$
    – James Wood
    Commented Jan 23 at 9:38
  • $\begingroup$ 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... $\endgroup$
    – noCrayCray
    Commented Jan 23 at 10:33


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.