Definition cgraph : UU := ∑ G : precgraph, isaset (node G) × isaset (arc G).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.