Definition cgraph_mor_id (G : precgraph) : cgraph_mor G G := make_cgraph_mor (idfun (node G)) (idfun (arc G)) (is_cgraph_mor_id G).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.