Definition make_cgraph (G : precgraph) (h : isaset (node G)) (k : isaset (arc G)) : cgraph := tpair _ G (make_dirprod h k).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.